Let $Con(\mathtt{ZFC}, n)$ denote the statement "$\mathtt{ZFC}$ cannot prove the contradiction within $n$ steps (or better within $n$ symbols) within a given proof system (say a natural deduction to avoid trivialities)". Suppose that ($\mathtt{ZFC}$ is consistent and) $\mathtt{ZFC} \models Con(\mathtt{ZFC}, n)$, then since the sentence could be represented as a first order statement using codings for proofs, by Godel's completeness theorem, it can be proved as well. Or more directly (without the assumption of the consistency of $\mathtt{ZFC}$) one could produce an algorithm that would enumerate all the possible statements provable within $n$ steps from $\mathtt{ZFC}$ and then it would check if such a statement is a contradiction or not and output the corresponding proof in $\mathtt{ZFC}$ of $Con(\mathtt{ZFC}, n)$. But any such proof for all statements derivable in $n$ steps would be very large, at least of size $O(n)$.

Therefore, is there a large natural number $n > 2^{100}$ and a proof in no more than $n$ steps (symbols) in $\mathtt{ZFC}$ of the sentence $Con(\mathtt{ZFC}, 2^n)$?

  • 8
    $\begingroup$ Could you clarify what you mean by a "step"? Since ZFC has infinitely many axioms, and one might commonly say that an axiom can be proved in one step, this would mean that there are infinitely many proofs with fewer than $n$ steps, contrary to what you seem to suggest in your post. Perhaps you mean to talk about the length of the proof, measured by the total number of symbols used in it? $\endgroup$ Jan 27, 2015 at 14:37
  • $\begingroup$ @JoelDavidHamkins I did not realize that ZFC has an axiom schema. Then closer to my interpretation I would enumerate all the axioms in order and the number of steps to state an axiom would correspond to its index in the enumeration... But your suggestion of the total number of symbols in a proof (as it is in the answer) sounds better. $\endgroup$ Jan 27, 2015 at 17:00

1 Answer 1


It’s not very clear to me what you mean by “steps”. One might interpret it as the number of lines in a Hilbert/natural deduction proof, but then there are infinitely many proofs with a fixed number of steps, so this is inconsistent with the argument outlined in the question.

So, let me use a measure that has the property that there are only finitely many proofs of length $n$, namely the total number of symbols in the proof when written down as a string. The choice of proof system does not matter that much, but natural deduction will do.

Then, for any consistent theory $T$, and $n\in\mathbb N$, $\mathrm{Con}(T,n)$ is a true bounded sentence, and as such it is provable already in Robinson arithmetic. However, the length of its shortest proof is a nontrivial problem. By a result of Pudlák [1], for any mildly reasonable theory $T$, the shortest proof of $\mathrm{Con}(T,n)$ in $T$ has length between $n^\epsilon$ and $n^c$ for some constants $0<\epsilon<1<c$. Both of these are nonobvious: the trivial upper bound obtained by enumerating all proofs of length $n$ has exponential size, whereas the trivial lower bound given by the length of the formula itself is logarithmic (assuming $n$ is written in an efficient way).

One might think that $\mathrm{Con}(S,n)$ could require significantly longer proofs in $T$ for a theory $S$ that is much stronger than $T$, for example $S=T+\mathrm{Con}(T)$. This turns out to be a difficult question: specifically, the statement that for every reasonable theory $T$, there exists a reasonable theory $S$ such that $T$ does not have polynomial-size proofs of $\mathrm{Con}(S,n)$, is equivalent to the nonexistence of optimal propositional proof systems, which is closely related to various problems in computational complexity.


[1] Pavel Pudlák: On the length of proofs of finitistic consistency statements in first order theories, in: Logic Colloquium ’84 (J. B. Paris, A. J. Wilkie, G. M. Wilmers, eds.), Studies in Logic and the Foundations of Mathematics vol. 120, North-Holland, 1986, pp. 165–196, doi 10.1016/S0049-237X(08)70462-2.

  • 2
    $\begingroup$ Fascinating! (I saw this as a non-logician, although I teach a freshman "writing" seminar on logic.) $\endgroup$ Jan 27, 2015 at 15:25
  • $\begingroup$ Put more formally, there exists constants ϵ and c s.t. for all n ... I had the quantifiers the other way around on first reading, which was true but uninteresting. $\endgroup$
    – prosfilaes
    Nov 4, 2022 at 15:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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