# Statement provable for all parameters, but unprovable when quantified

I've been reading a book on Gödel's incompleteness theorems and it makes the following claim regarding provability of statements in Peano arithmetic (paraphrased):

There exists a formula $A(x)$ such that the statements $A(0), A(1), A(2), \dots$ are all provable, but $\forall x\, A(x)$ is not provable.

It goes on to say that while Gödel's first incompleteness theorem guarantees its existence, it is not easy to find such a property for a theory as strong as PA.

Is there a specific example of such a formula or has none been found yet?

• Potentially relevant: 1, 2 – 6005 Sep 7 '16 at 11:05
• I am not sure if this would be a valid example, if other comments disagree I will remove it: e.g. Mills' constant formula for $A$.It is not known if $A_{\infty}$ is rational or not but it is possible to calculate the value of Mills' constant for any "discrete" value of $n$ and demonstrate that it is not rational but we can not say that is true for every $A_n$ because the case in the limit to infinity $A_{\infty}$ is not provable.A question regarding this: math.stackexchange.com/q/1839268/189215 – iadvd Sep 8 '16 at 1:28

Possibly the easiest example is to let $A(x)$ say that $x$ is not the Gödel number of a proof of $0=1$ from the axioms of PA.

Because there is no such proof, $A(0)$ is true, $A(1)$ is true, etc., and because of their syntactic form each of these is provable in PA.

However, $(\forall x)A(x)$ is the statement $\text{Con}(\text{PA})$ which the second incompleteness theorem shows is not provable in PA.

There are other examples, as well. Some are related to the Paris-Harrington theorem and other independence results; others are related more directly to the incompleteness theorems.

• We have several independent consistency proofs for PA. The simplest is in ZFC, but Gödel and Gentzen provided additional consistency proofs in systems much weaker than ZFC. – Carl Mummert Sep 7 '16 at 11:11
• In any case if PA isn't consistent then of course there's no formula $A(x)$ such that $\forall x\, A(x)$ isn't provable in PA. Never mind about $A(0)$ etc. So it doesn't create any great mystery to add "if PA is consistent" to the front of the statement in the question, it's just blinking obvious that if PA is inconsistent then there's no such $A$. So if you don't want to worry about what the weakest system is that proves the consistency of PA, and whether or not you think that system is consistent, just add "if PA is consistent" and get on with your life :-) – Steve Jessop Sep 7 '16 at 18:49
• The trouble is that $A(0)$, $A(1)$, $A(2)$, ... have different proofs which get longer and longer. To prove $(\forall n)A(n)$ we need a single proof that applies for all $n$. To put it another way: it is OK in a proof to divide into finitely many cases, but PA doesn't have a proof rule that allows us to split $(\forall n)A(n)$ into infinitely many cases $A(0)$, $A(1)$, etc. That rule has been well studied - it is called the $\omega$-rule - and it is true that PA plus the $\omega$ rule proves that PA is consistent. But the $\omega$-rule is infinitary - proofs that use it can be infinite. @Mark – Carl Mummert Sep 13 '16 at 12:56
• First-order PA has quantifiers for number variables. So if you can state a formula $\phi(x)$ you can also state the formula $(\forall x)\phi(x)$. Of course, there are nonstandard models of PA, so the "meaning" the quantifier is that $\phi(x)$ is supposed to hold for all $x$ in the model, in order for $(\forall x)\phi(x)$ to hold in the model. @Mark Hurd – Carl Mummert Sep 13 '16 at 14:02
• @MarkHurd The problem with your proof isn't a second-order vs. first-order issue, it's that you're implicitly assuming that PA proves "If I prove $p$, then $p$ is true." In fact, the theory PA+"PA is inconsistent" is consistent (assuming PA itself is)! The issue is that even if PA proves "PA proves 0=1," it can't directly turn that into a proof of "0=1," so it can't use it in a proof by contradiction directly. All PA can do is prove for each specific $n$ that $n$ isn't a code for a proof of $0=1$. (cont'd) – Noah Schweber Feb 2 '17 at 19:17

Great question! Yes, there are specific examples. One of the most famous is Goodstein's theorem. If $A(n)$ is the statement that Goodstein's sequence starting at $n$ terminates, then it is known (via stronger theories than PA, namely use of a clever ordinal argument) that $\forall n \; A(n)$ is true.

Moreover, for a specific $n$, given that $A(n)$ is true, it must be provable: just write out the finite sequence, and that gives a proof that it terminates. (Once you get to $n = 4$ or larger, it will be a very very long proof -- one that we humans cannot actually have the space or memory to write down.)

However, $\forall n \; A(n)$ is known to be unprovable in PA.

• Can it be proven in PA for all $n$ that $A(n)$ is true ? – Peter Sep 7 '16 at 12:10
• @Peter Yes, because it requires only a finite computation. See my edit to the answer. – 6005 Sep 7 '16 at 12:13
• @Peter gotta be careful with order of quantifiers, which is not natural in casual English. It is true that for all $n$, it can be proven in PA than $A(n)$ is true. It is not true that it can be proven in PA that for all $n$, $A(n)$ is true. – Richard Rast Sep 7 '16 at 20:56

Let $\phi(x)$ be the formula expressing "x is not a code for a proof of '0 = 1' from the axioms of $\textsf{PA}$".

Since $\textsf{PA}$ does not prove that there is no proof of '0 = 1' (that is, $\textsf{PA}$ does not prove that $\textsf{PA}$ is consistent), then it is not the case that $\textsf{PA}$ proves that there is no code for such a proof. But since if there were such a proof, its code could not be standard (otherwise, it'd be a code for an actual proof, which would imply that $\textsf{PA}$ actually proves that it is inconsistent), then we know $\phi(0), \phi(1)$, etc all hold.

• "if there were such a proof, its code could not be finite (otherwise, it'd be a code for an actual proof, which would imply that PAPA actually proves that it is inconsistent)" Firstly, isn't the code for any proof defined to finite? Secondly, to clarify, there's nothing strictly contradictory about PA proving that PA is inconsistent, however, we know via stronger theories that PA is consistent, thus we know (under the axioms of these stronger theories) that $\phi(0), \phi(1)$ etc. hold. To me, the dependency on the consistency of PA is key. – 6005 Sep 7 '16 at 12:21
• By "finite" I meant standard, I'll edit that. But yes, in this response I'm assuming that PA is consistent. – Athar Abdul-Quader Sep 7 '16 at 12:27

If you simulate a Turing Machine using a Universal Turing Machine and you run the simulation for exactly N steps you will see either that the machine Halts in N steps or that the machine does not Halts in N steps.

However in general you cannot proove that a Turing Machine Halts by mere simulation, because if it does not halt your simulation would run forever. I think that's the same but in different words.

You know the answer to the question:

• Does the machine halt in N steps? (Decideable)

You don't know the answer to the question:

• Does the machine halts in any number of steps? (Undecideable)

You could use as formula a machine that require the turing machine to reach a determined state. You know if the state can be reached in a limited amount of steps, but not if you let it run forever with unlimited amount of memory.

• This is a good answer, however I think this particular question is calling for a specific example of a statement $A(n)$, thus you would need to provide a specific Turing machine whose halting behavior $A(n)$ is unprovable in PA. Alternately, you could include the description of a turing machine in the parameter $n$, as well as the number of steps. But that complicates things a bit for the description you gave. – 6005 Sep 7 '16 at 16:25
• Thanks for your answer. I guess now I am starting to understand the question! – lesnik Sep 8 '16 at 6:23
• Sometimes I get random downvotes on this answer even if it was well perceived :). – CoffeDeveloper Feb 24 '17 at 14:14