Statement provable for all parameters, but unprovable when quantified

Solution 1:

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.

Solution 2:

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.