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)$?

lengthof the proof, measured by the total number of symbols used in it? $\endgroup$ – Joel David Hamkins Jan 27 '15 at 14:37