Comment by ComplexSystems

Comment by 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)".

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