My next question is whether you agree with the proof. In other words, do you agree with the assumptions inherent in the meta-system MS that are needed to prove the incompleteness theorems?
Some logicians will claim that PA itself can do it, but there is philosophical reason to say that this claim is not meaningful, because it essentially boils down to showing that PA |− ( Con(PA) ⇒ ¬Prov(Con(PA)) ), where Con(PA) and Prov(Con(PA)) are two arithmetical sentences. The problem is that these sentences cannot be justified to make sense without some notion of natural numbers. To quote from my post:
9
The things you actually write on the paper or some other medium are not definable as any kind of mathematical objects. Mathematical structures can at most be used to model (or approximate) the real world structures. For example we might say that we can have strings of symbols of arbitrary length,...
> The catch is that the sentence "Prov(P)" is completely meaningless unless we have some notion of interpretation of a sentence over T, which we have completely avoided so far so that everything is purely syntactic.
At that point in my post, I had only justified syntactic manipulation, which is basically all that PA can do natively (without encoding that requires us to imbue the coding with external meaning).
This is vague, because even 'native' support for something in a formal system is ultimately still syntactic. Just because "1+1" is a valid expression in a system does not mean that it really means 1+1, but at least it's philosophically more satisfying because it 'means what it says' (or at least 'says what it means'). =)
I should have said earlier that PA can prove the internal incompleteness theorem for any formal system S that interprets PA, and this proof is uniformly computable from a proof verifier V for S. Namely, there is a single program that one can write down explicitly, that given input V will output a proof of ( Con(S) ⇒ ¬Prov(Con(S)) ) over PA.
So in my opinion the most natural system that can play the role of MS is not PA but ACA. ACA can natively construct the set of theorems of S, where arithmetical sentences are still encoded as natural numbers, but now we no longer need to encode the notion of consistency as an arithmetical sentence; ACA can natively form and prove the sentence:
> For any program V that is a verifier for a formal system S (given as a set of theorems) that interprets PA via translation i, if S does not prove the i("0=1") then S does not prove both i(P) and i("¬"+P) for some arithmetical sentence P.
Ok so I shouldn't have said "most natural"; the most natural would be a system with native string manipulation. But traditionally well-known foundational systems in reverse mathematics have always been over the language of arithmetic so...
If you like, we can use the language of strings plus axioms of TC plus all finite turing jump oracles plus the full induction schema. That would be equivalent to ACA with a computable translation.
@user170039 This does not seem to make sense. I contend that AC (axiom of choice) is not a universally accepted proposition of established mathematical practice. One aspect of the incompleteness theorems is that it shows that there can be no such notion of universal acceptance even in principle. Would you accept PA+Con(ZFC)? Or would you accept PA+¬Con(ZFC)? How about PA+Con(ZF+Reinhardt) where Reinhardt stands for existence of a Reinhardt cardinal?
@user170039 However, if you just mean that PM aimed to formalize only the body of mathematics at that particular time, then your previous comment about "accepted propositions" does make sense, but I disagree with this notion, because nobody creates a formal system to merely be able to prove existing facts.
Rather, formal systems are always created with the intent to prove not only existing accepted theorems but also all other theorems that would conceivably be accepted, and yet without proving what would conceivably be rejected (like "0=1").
@user170039 I won't comment much on his answer, except that as I said earlier it is very likely he doesn't understand the incompleteness theorems, so there's nothing to say.
@user170039 I feel I should say that this and the previous comment are simply wrong. Godel's sentence is not self-referential. Only MS can 'observe' that it appears to refer to itself. But it itself is not and cannot be self-referential because it is simply not permitted to construct any such thing in the system itself.
I guess the only way to fully understand the nature of the apparent self-reference is to go back to the basics of proof+model theory. Recall that MS assumes the existence of a model N for PA. MS can construct an arithmetical sentence Q and prove that PA proves ( Q ⇔ ¬Prov(Q) ). MS can prove that ( PA proves Q ) iff ( N |= Prov(Q) ). Since MS proves ( N |= PA ), MS can hence prove that ( PA proves Q ) iff ( N |= ¬Q ). There is no self-reference.
