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.

### Reference

[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.

lengthof the proof, measured by the total number of symbols used in it? $\endgroup$