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'?
  • 1
    $\begingroup$ 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). $\endgroup$
    – TomKern
    Aug 2 at 3:03

It’s easy to express concepts like proof length in any sufficiently complex logical language through Godelization. Once you can express a proof as a number or string, you can define a function as it’s length, so it’s not necessary to add a new symbol for it beyond syntactic sugar.

Complexity is a pretty common concepts in logic and computer science. There are numerous theorems related to it https://en.m.wikipedia.org/wiki/Proof_complexity

Generally speaking, bounding by a fixed constant isn’t that useful since there are infinitely many true things, so you won’t be able to prove everything true within a fixed length. A more useful concept is whether every true statement admits a polynomially bounded proof. The existence of such a proof system is an open problem.

Showing whether any given theorem has a lower bound on proof size is also a generally difficult problem, though we have some proofs in specific cases.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.