# 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 Commented Sep 7, 2016 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 Commented Sep 8, 2016 at 1:28

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 ? Commented Sep 7, 2016 at 12:10
• @Peter Yes, because it requires only a finite computation. See my edit to the answer. Commented Sep 7, 2016 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. Commented Sep 7, 2016 at 20:56

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. Commented Sep 7, 2016 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 :-) Commented Sep 7, 2016 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 Commented Sep 13, 2016 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 Commented Sep 13, 2016 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) Commented Feb 2, 2017 at 19:17

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. Commented Sep 7, 2016 at 12:21
• By "finite" I meant standard, I'll edit that. But yes, in this response I'm assuming that PA is consistent. Commented Sep 7, 2016 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. Commented Sep 7, 2016 at 16:25
• Thanks for your answer. I guess now I am starting to understand the question! Commented Sep 8, 2016 at 6:23
• Sometimes I get random downvotes on this answer even if it was well perceived :). Commented Feb 24, 2017 at 14:14