Comment by btilly

Comment by btilly 3 days ago

> If PA proves "PA proves X" then PA can prove X.

Not true.

From PA we can construct a function that can search all possible proofs that can be constructed in PA. In fact I outlined one way to do this at the end of my answer.

With this function, we can construct a function will-return that analyzes whether a given function, with a given input, will return. This is kind of like an attempted solution to the Halting Problem. We know that it doesn't always work. But we also know that it works a lot of the time.

From will-return we can create a function opposite-return that tries to return if a given function with a given input would not, and doesn't return if that function would. This construction is identical to the one in the standard proof of the Halting Problem.

Now we consider (opposite-return opposite-return opposite-return). (Actually you need a step to expand the argument into this recursive form. I've left that out, but that is identical to the one in the standard proof of the Halting problem.)

PA can prove the following:

- PA proves that if PA can prove that opposite-return returns, then it doesn't. - PA proves that if PA can prove that opposite-return doesn't return, then it does. - PA proves that if it can prove everything that it proves that it can prove, then PA must have a proof of one of the two previous statements. - Therefore PA proves that if it can prove everything that it proves that it can prove, then PA is inconsistent.

This is a form of Gödel's second incompleteness theorem.

And, therefore, there must be a distinction to be made between "PA proves" and "PA proves that it proves".

ComplexSystems 2 days ago

I am not sure I follow and it is possible I may not be on the same wavelength, but here is another thought.

For any sentence S, if first-order PA (or any first-order theory) proves S, then that means that S holds true in every model of that theory, via the completeness (not incompleteness) theorem.

The statement "PA proves x" is equivalent to saying "there exists a natural number N which is a Gödel number encoding a proof of x." The letter "x", here, is a natural number that is assumed to encode some sentence we want to prove, that is, x = #S for some sentence S.

The above is a predicate with one existential quantifier: Provable(x) = there exists N such that IsProof(N, x) holds true, where IsProof says that N is the Gödel number of a valid proof ending in x.

If PA proves "Provable(x)", that means that the predicate "Provable(x)" holds in every model of PA. This means every model of PA would have some natural number N that satisfies IsProof(N, x). Of course, this number can vary from model to model.

However: the standard model, which has only standard natural numbers, is also another model of PA. So if PA proves "Provable(x)," and Provable(x) thus holds in every model, it must also hold in the standard model of PA. This means that there must be a regular, standard, finite natural number N_st that encodes a proof of x.

Since the standard model is an initial segment of every other model of PA, then every other model includes the standard model and all the standard natural numbers. Thus, if PA proves Provable(x), then the standard number N_st must exist in all models.

So we cannot have a situation where PA proves Provable(x) but all proofs of x must be nonstandard and infinite in length. This would mean no such proof exists in the standard model of PA - but then, via completeness, PA would not be able to prove "Provable(x)".

Reply View 3 replies

btilly 2 days ago

For every n, the function will return a function, that PA proves has a proof in PA.
Suppose that we're in a nonstandard model. For all standard n, there really will be a proof. For nonstandard n, there may or may not actually be a proof.
And so PA cannot prove from the fact that it proved the existence of a proof, that PA actually proves it.

Reply View | 2 replies
- ComplexSystems 2 days ago
  
  That is very different though. You are now saying that for all n, PA proves that it has a proof the Goodstein sequence terminates for that n. But that is very different from the earlier claim:
  "And, therefore, there must be a distinction to be made between "PA proves" and "PA proves that it proves"."
  It seems that for each standard n, PA proves that the Goodstein sequence terminates for that n. If also proves that it proves that the Goodstein sequence terminates for all n, and so on. But this is very different from saying "PA proves that it proves the sentence 'for all n, the corresponding Goodstein sequence terminates,'" which is what I thought you were saying.
  
  Reply View | 1 reply
  
  btilly 2 days ago
  
  No, it is not different from the earlier claim. If you think that it is, then you were misreading me.
  My earlier claim is that for each n, "PA proves that it proves that G(n) terminates". But in logic there is an important distinction to be made between "PA proves" and "PA proves that it proves". From the second, you cannot conclude the first. You must actually present the proof, and then verify it.
  And the reason is this. It is true that, for all standard n, "PA proves that it proves" implies that "PA proves". But for nonstandard n it does not. Since PA cannot itself distinguish standard n from nonstandard n, PA cannot follow that implication to a proof.
  (All of this is based on long conversations with my logic professor back in grad school. To the extent that I get it right, https://faculty-directory.dartmouth.edu/marcia-j-groszek deserves the credit. To the extent that I get it wrong, I deserve the blame.)
  
  Reply View | 0 replies

tromp 3 days ago

> > If PA proves "PA proves X" then PA can prove X.

If we assume PA to be sound, then indeed everything it proves is true.

> Not true.

Now you're saying PA is unsound.

But your article wasn't about PA proves "PA proves X", it was about "forall n : PA proves G(n)".

For PA not to prove "forall n: G(n)", there is no soundness issue, only a ω-consistency issue.

Reply View 7 replies

btilly 3 days 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.

Reply View | 6 replies
- ComplexSystems 2 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.
  
  Reply View | 3 replies
  
  btilly 2 days ago
  
  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.)
  
  Reply View | 2 replies
- dwohnitmok 2 days ago
  
  > 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.
  
  Reply View | 1 reply
  
  tromp 2 days ago
  
  > 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)".
  
  Reply View | 0 replies

dwohnitmok 3 days ago

> PA proves that if it can prove everything that it proves that it can prove, then PA must have a proof of one of the two previous statements.

I don't believe this is true. I don't know what result you're using here, but I think you're mixing up "provable" and "true".

In particular your line of reasoning violates Lob's Theorem, which is a corollary of the second incompleteness theorem.

Reply View 0 replies