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?

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.
