# Are there any proof-size-aware logics?

I'm aware of provability logics which have a notation $$\square P$$ for "$$P$$ is provable", but I'm not aware of one which is more 'fine grained' and has a notion of proof term size (e.g. with predicates $$\mathsf{proof}(x, P)$$ for "$$x$$ is a proof of $$P$$" and $$\mathsf{size}(x, n)$$ for "$$x$$ is a term of size $$n$$").

Such a system could express the statement "there is no proof term for $$\bot$$ of size less than $$3\widehat{}\widehat{}\widehat{}3$$". Perhaps it has a proof of that statement, and the proof term is (much) smaller than $$3\widehat{}\widehat{}\widehat{}3$$. This leads me to some follow-up questions:

• Would this result be useful? I assume most mathematicians want their logical systems to be completely consistent, but I could settle for "consistent within the bounds of proof terms I can ever observe".
• Is there some obvious diagonalization/Gödelian argument which prevents this sort of result?
• Is this somehow related to paraconsistent arithmetic, in the sense that we don't care about contradictions which are sufficiently 'far away'?
• You may be interested in some work in ultrafinitism, such as Vladimir Yu. Sazonov's "On Feasible Numbers". Here the premise is to show that a system of arithmetic, plus the axiom that "$2^{1000}$ doesn't exist" has a shortest proof of contradiction of a particularly large size (specifically too large to actually write down in the known physical universe). Aug 2 at 3:03