Comment by ComplexSystems 3 days ago
If PA proves that a number exists with some mathematical property - including being a Gödel number of a proof of something - then some number with that property must exist in every model, including the standard model. So there would have to be a standard number encoding a proof, and the proof that it encodes would have to be correct, assuming your Gödel numbering is.
We are talking past each other. I am responding to this:
"If PA proves that it proves a statement, PA cannot conclude from that fact that it proves that statement."
When you say "PA proves that it proves a statement," this usually means that it proves the existence of a Gödel number of the proof of the statement. If PA proves such a Gödel number exists, then via completeness one must exist in the standard model, and this number will be a standard natural number encoding a valid finite length proof.
If the above somehow doesn't apply to the argument you are making: how?
We definitely are talking past each other.
The existence of a Gödel number in a model of PA, does not imply the existence of a proof corresponding to that Gödel number. PA can only prove the existence of the Gödel number.
Now consider a function, definable from PA, named prove-gn. It is defined such that (prove-gn n) is the Gödel number for a proof from PA that G(n) terminates. This function is somewhat complicated, but it absolutely can be constructed. And from PA we can prove that the function works as advertised.
Suppose that we are in a nonstandard model of PA. For every standard natural n, (prove-gn n) will be a standard natural, and will correspond to an actual proof. So far, so good.
But any nonstandard natural n, and this model has many, will result in (prove-gn n) being a nonstandard natural. That Gödel number does not correspond to a valid proof. And therefore, in this model, PA will prove that it proves a statement, that it does not actually prove.
Therefore, from PA, we may prove that PA proves a statement, even though it does not prove that statement. In fact the statement may even be false. And absolutely none of this causes any contradiction or consistency problem, so long as the statement in question is a statement about a nonstandard natural number, and not a standard one.
Because there is no way from PA to determine if we are in the standard model, or a nonstandard model, from PA we cannot conclude that "PA proves that it proves" implies "PA proves". They really are different concepts. And we will cause ourselves no end of confusion if we confuse them.
The Gödel number for all of the standard statements in that collection will indeed exist.
But if it is an infinite collection, then a nonstandard model of PA will have statements in that collection that are not in the standard model, and they generally don't encode for correct proofs. (For one thing, those proofs tend to be infinitely long.)