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)$?
Best Answer
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, 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.