Comment by dwohnitmok

> 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.