MS: Let ⬜P denote the sentence over FM that translates the NL sentence "There is a string E and proof C such that E is a valid encoding of the execution of FM on (C,P) that ends with acceptance.", for any sentence P over FM.
NL: Okay that's not very satisfactory; MS is not supposed to be able to talk about NL. But for the sake of sanity I hope you know what I mean so that I don't have to be completely formal. =D
NL: That's why mathematicians almost never write completely formal proofs.
@LeakyNun I was just going to point that out. Our FM is supposed to be foundational, and presumably it uses classical logic for sentences involving just finite strings.
@LeakyNun Yes, which is why there is a little catch. Earlier I said "any reasonable foundational system". Later I said "FM can reason about finite strings". To be completely rigorous about this we can do as in my post about the incompleteness theorems via a translation function, but I'm going for the intuitive way now.
@Mathmore Once we prove (D1) to (D3) we will almost immediately get the constructive incompleteness theorem for FM.
@Mathmore It does. I don't want to explain the translation function now, as it's a distraction. Just imagine FM as some crazy formal system (represented by a proof verifier program) but that can perform (via some translation) the classical reasoning about finite strings.
(D1) intuitively says that whenever FM proves P then FM itself can see this fact.
How so? Well, if FM really proves P then FM accepts (C,P) for some string C. So we have a finite computation and FM itself can verify each step of that computation.
If this makes sense then that's all there is to it.
That's it. There is a classical proof whose length is proportional to the length of the execution, and FM can perform each step of that classical proof.
Godel without tears is an excellent book, not only because I first clearly understood the incompleteness theorems after reading it, but also because it includes some philosophical explanations of the import of the theorems.
That's why I listed it among my recommended reference texts.
(D2) uses similar reasoning, except that we must produce a proof within FM itself. That's okay. We reason in MS (more like NL) that such a proof exists!
(D2) intuitively says that FM knows that if P is provable and (P⇒Q) is provable then Q is provable too.
Well since FM can perform classical reasoning for sentences about strings, it suffices (think Fitch-style) to show that within FM, under the context where we have ⬜P and ⬜(P⇒Q), we can deduce ⬜Q.
For (D2), we actually need the translation of classical sentences about strings into FM to be nice enough so that we can 'join' together proofs of P and (P⇒Q) to get a proof of Q.
Classical reasoning about strings here refers to classical first-order logic in the language of strings under concatenation.
Truth tables are not enough to capture first-order logic (with quantifiers), so we use inference rules instead. Each inference rule is chosen to be sound, meaning that if you start with true statements and use the rule you will deduce only true statements. We say that these rules are truth-preser...
This gives just the logical rules, not any axioms. There are only 4 axioms needed for strings, which you can see here:
You ask:
How can Peano ever be proved consistent?
Firstly, Peano is a person, and I'm certain that nobody can prove that he is consistent.
I assume you're asking for an absolute proof of consistency of (first-order) PA. That was more or less Hilbert's goal, namely to give a finitist proof...
It's funny that @LeakyNun is about to enter undergrad program having known all this stuff and I... who completed graduation (Masters) and still don't know these things.
@LeakyNun @Mathmore: Actually it would have been gentler to introduce the non-constructive proof to you first, but since we're already halfway through we might as well finish it.
For (D3) the idea is simply to carry out the reasoning for (D1) inside FM itself. Namely, our earlier reasoning in MS gives (D1), and translating that reasoning into FM gives (D3).
Is @Mathmore going to be back later? We need just one more ingredient called the modal fixed-point lemma, and then we can perform Curry's paradox to get the incompleteness theorems.
@LeakyNun: If you want to start first, you can try the following proof-puzzle.
Given premises "⬜P⇒P" and "Q⇔⬜(Q⇒P)", prove "P" (within FM) using only propositional logic and (D1) to (D3).
@LeakyNun I don't understand what problem you have with this. Your proof holds for any P, and we are merely applying the result to a single simple P, namely "0=1".
It's been so long since I touched any analysis. Comes down to just finding a delta that's equal to an expression in terms of epsilon. Useful reminder. After that the existential and universal quantifiers fall into place really quickly.
For any assertion p:
Let q = ( If this assertion is true, then p is true. ).
If q is true:
If q is true then p is true. [Def of q]
p is true.
If q is true then p is true.
q is true. [Def of q]
p is true.
@Mathmore: No it's not the liar paradox and does not involve negation. What is the error in the above 'paradox'?
@shredalert @LeakyNun: You are not allowed to answer this question.
If q is true then the statement : "If this assertion is true then p is true" is a true statement. That means either "This assertion is true" and "p is true" are both true. or "This assertion is true" is false and "p is true" is true, or "This assertion is true" is false and "p is true" is also false.
@user21820
@shredalert yeah. he/she is so much dedicated to educate.
@Mathmore Modus ponens is considered valid. The 'paradox' applies to classical logic. What you can do is to check one line at a time and identify the deductive rule that permits it.
For any assertion p:
Let q = ( If this assertion is true, then p is true. ).
If q is true:
If q is true then p is true. [Def of q]
p is true.
If q is true then p is true.
q is true. [Def of q]
p is true.
And the proof of what is called Lob's theorem (external):
But that apparently minor change is all that is needed to make it possible to be deduced. That change makes the proof of Curry's paradox fail to go through, except unless we also have the first premise "box p implies p".
In sum, Lob's theorem (which we have just proven) states that if FM proves ( ⬜p⇒p ) then FM also proves p.
MS: Given any sentence P over FM we have the following: (D1) If FM proves P then FM proves ⬜P. (D2) FM proves ( ⬜P∧⬜(P⇒Q)⇒⬜Q ). (Note that the precedence order from highest to lowest is ⬜,∧,⇒.) (D3) FM proves ( ⬜P⇒⬜⬜P ).
Note that (D1) can only be used on something that is proven at the outermost level (not under any assumption).
MS: Let ⬜P denote the sentence "There is a string E and proof C such that E is a valid encoding of the execution of FM on (C,P) that ends with acceptance.", for any sentence P over FM.
But the first version is how we want to think about "⬜P".
@LeakyNun This is okay if FM is a classical formal system. As I said earlier, we have to do things slightly differently if we wish to catch all formal systems.
I have seen people using the term incompleteness theorem in philosophy, biology, physics, and what not and some mathematicians destroying their claims to be 'bullshit'
@Mathmore: What @LeakyNun just said above applies to classical formal systems, but I do not want to restrict to those otherwise one could easily claim that there might be non-classical formal systems that avoid the problem.
@Mathmore No I didn't assume that. Remember I said all we require is that FM can perform classical reasoning for strings. It is free to do funny reasoning for other things, or not even reasoning.
Also, remember that I defined "⬜P" precisely to be some sentence about strings.
"0=1" is just a false arithmetical sentence. In the string version take it to denote a false sentence about strings such as "the string with a single zero symbol is equal to the empty string".
Now define Con(FM) to be literally the sentence "¬⬜(0=1)".
So if FM is arithmetically-consistent then FM does not prove "Con(FM)" by Lob's theorem, because we can show that FM proves "Q⇔(⬜Q⇒false)" for some suitable Q.
