# Mixture of Godel's sentence, Berry's paradox and Rosser's sentence

Let $S$ be a "rich enough" theory such as Peano arithmetic or ZFC ; assume that we have a complete formalization of the theory of $S$ so that we may talk about Godel numbers and the length of a proof.

Godel's sentence is constructed so that it says "I am not provable from S". Now let $n$ be a fixed integer, and consider a sentence $\phi_n$ formed likewise that says "I am not provable in at most $n$ steps from S". Then $\phi_n$ is a true statement, and if $\phi_n$ has a proof from $S$ this proof has length at least $n$. What is not clear is whether $\phi_n$ is provable from $S$. Does the answer to that question depend on the formalization we initially choose ?

-

Every true statement of the form "Such-and-such $\phi$ is not provable by a proof that contains at most $n$ symbols" is in fact provable -- the proof can consist of simply listing all strings of $n$ symbols or less and noting that neither of them is a valid proof of $\phi$.
I am fairly sure that the same holds for "at most $n$ steps" instead of "at most $n$ symbols", in any reasonable deductive system (even though the most straightforward way to represent a single "step" can often be arbitrarily long). But I can't think of a simple generic argument for this right away.
I suppose that $\phi_n$ is always provable, unless I am making some basic mistake. Given a string of length at most $n$, you can determine if it happens to be a proof for $\phi_n$. Now, just brute-seach all possible strings of length at most $n$ to see that none of them is a proof of $\phi_n$ (none can be, since $\phi_n$ is true), and you have proved $\phi_n$.