Statement provable for all parameters, but unprovable when quantified

Question

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?

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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.