Comment by btilly
1 month ago
I think we are saying the same thing.
If PA proves that it proves a statement, PA cannot conclude from that fact that it proves that statement.
If PA proves that it proves a statement, and then fails to prove it, PA is unsound.
There exist collections of statements such that PA proves that it proves each statement, and PA does prove each statement, but PA does not prove the collection of statements.
Our understanding of the last is helped by understanding that "PA proves that PA proves S" is logically not the same statement as, "PA proves S". Even though they always have the same truth value.
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.
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.)
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?
1 reply →
> There exist collections of statements such that PA proves that it proves each statement, and PA does prove each statement, but PA does not prove the collection of statements.
I think this is true (although I would like a significantly more succinct proof than one using Goodstein sequences as I mention here https://news.ycombinator.com/item?id=44277809), but regardless this is substantially weaker than your assertion that there are statements PA can prove that it can prove, but cannot itself prove.
In particular I can prove that for all propositions P, PA proves P if and only if P proves "Provable(P)" (i.e. "P is provable in PA").
Given PA proves P, take the finite proof of P in PA and do the usual Godel encoding to get a single number. That is a witness to the implicit existential statement behind "Provable(P)".
In the other direction, given P proves "Provable(P)", take the natural number witness of the implicit existential statement. Because the standard natural numbers satisfy PA (this is basically equivalent to the assumption that PA is consistent), we know that this natural number is in fact a standard, finite natural number. Hence we can transform this natural number back to a proof of P in PA.
This equivalence is precisely the reason why the provability relation (more accurately for our purposes stated as "provability in PA") "Provable" is valuable. If the equivalence didn't hold it would be very weird to call this relation "Provable".
In particular, this means PA proves P if and only if P proves "Provable(Provable(P))" (and so on for as many nestings of Provable as you'd like).
> If PA proves that it proves a statement, PA cannot conclude from that fact that it proves that statement.
I kind of think I know what you mean by this, but definitely your conclusion is way too strong. In particular, it is true in a certain intuitive sense that PA cannot "use" the fact of "Provable(P)" to actually prove P. It is in a sense a coincidence that every P for which PA can prove P, PA can also prove "Provable(P)", since that equivalence is carried "outside" of PA. But that's not really anything to do with PA itself, but that's just rather the nature of any encoded representation.
Even what tromp is saying is quite strange to me (in apparently implying that it's normal for PA to have an omega-consistency issue). It would be very strange to assert PA is omega-inconsistent. It is tantamount to saying PA is inconsistent, since stating that PA is omega-inconsistent is saying that the standard natural numbers are not a valid model of PA.
> Even what tromp is saying is quite strange to me
Indeed I mis-spoke. While for all n, PA can prove P(n), it cannot prove "for all n: P(n)". I don't know if there is a name for this, but it's not an omega-inconsistency. It would only be omega-inconsistent to have PA contradict "for all n: P(n)", i.e. to prove "there exists an n: not P(n)".