= 27d567bc2d48d9f40e9ccc20ea370b15)
A puzzle: How can one rigorously construct Self-PA as recursively axiomatized first order theory in the language of PA?
In response to
The Cartoon Guide to Löb's Theorem
simon: Let me explain some of the terminology here, because that may be where the confusion lies.
A scentence is a finite string symbols that satisfies a certain set of syntactic constraints.
A theory is a (possibly infinite) set of sentences. PA is a theory.
A proof from a theory T is a finite set of sentences, each of which is either an element of T, or follows from the ones before according to a fixed set of rules.
The notation PA + X, where X is a sentences is just the union of PA and {X}.
The notation PA |- Y means that a proof from PA that ends in Y exists.
Now I have left out some technical details, like what exactly are the syntactic constraints on sentences, and what is the fixed set of rules for proofs, but we have enough to say what the deduction theorem means. It says
PA + X |- Y => PA |- "X -> Y"
or in english: if there is a proof from the theory PA + X to the scentence Y, then there is a proof from PA alone that X->Y.
So, you see, the deduction theorem is really just a technical lemma. It meerly shows that (in one particular way) our technical definition of a first order proof behaves the way it ought to.
Now on to Lob's theorem, which says that if PA |- "â—ťC -> C" then PA |- "C". Now in general if you want to prove PA |- A implies that PA |- B, one way to do it is to write a first order proof inside of PA that starts with A and ends with B. But that is not what is going on here. Instead we start with a proof of "â—ťC->C" and do something totally different than a first order proof inside of PA in order to come up with a proof that PA |- C.
In response to
The Cartoon Guide to Löb's Theorem
Psy-Kosh: There are two points of view of where the flaw is.
My point view is that the flaw is here:
"Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C. Applying the Deduction Theorem to Löb's Theorem gives us, for all C: ((◻C)->C)->C"
Because, in fact Lob's Theorem is: (PA |- "◻C -> C") => (PA |- "C") and the Deduction theorem says (PA + X |- Y) => (PA |- "X->Y"). We don't have PA + X proving anything for any X. The deduction theorem just doesn't apply. The flaw is that the informal prose just does not accurately reflect the actual math.
Eliezer's point of view (correct me if I'm wrong) is that in the cartoon, we have 10 steps all of the form "PA proves ...." They each follow logically from the ones that came before. So they look like a proof inside of PA. And if they were a proof inside of PA then the deduction theorem would apply, and his contradiction would go through. So the flaw is that while all of the steps are justified, one of them is only justified from outside of PA. And that one is step 8.
Both of these views are correct.
Brian Jaress:
I think if you used Lob's Theorem correctly, you'd have something like:
if PA |- []C -> C then PA |- C [Lob]
PA |- ([]C -> C) -> C [Deduction]
This is incorrect because the if-then is outside of PA. The deduction theorem does not apply.
In response to
The Cartoon Guide to Löb's Theorem
"I just tested and anecdotally confirmed a hypothesis made with very little data: I suspected that neither Douglas Knight nor Larry D'Anna, the two who pinpointed 8 as the critical step, would be among the objectors to my metaethics. (Either of them can torpedo this nascent theory by stating otherwise.)"
I like your metaethics just fine.
In response to
The Cartoon Guide to Löb's Theorem
Psy-Kosh: No that isn't the problem. If there is a proof that 1=2, then 1=2. If there isn't, then 1=2. Either way 1=2. The problem is the mixing of meta-levels / inappropriate use of the deduction theorem / tacit assumption that ◻a -> ◻b is the same as "a -> b".
Sebastian Hagen: no ◻X is PA |- "X". My best guess as to what Eliezer meant by "interpret the smiley face as saying.." is that he meant to interpret the cartoonproof as a proof from the assumption "(◻C -> C)" to the conclusion "C", rather than a proof from "◻(◻C -> C)" to "◻C".
In response to
The Cartoon Guide to Löb's Theorem
Eliezer: "Larry, interpret the smiley face as saying:
PA + (◻C -> C) |-"
OK ignoring the fact that this is exactly what it doesn't say, I suppose we could notice that every step is surrounded at the top by a happy-face-says, so, if we may be inclined to think we can take those off and get a proof inside PA, starting with "◻C -> C" as a hypothesis. Lets see what happens.
1. ◻L <-> ◻(◻L -> C) 2. ◻C -> C
ok these are our hypothesis.
3. ◻(◻L->C) -> (◻◻L -> ◻C)
Modus Ponens works in PA, fine
4. ◻L -> (◻◻L -> ◻C)
ordinary MP
5. ◻L -> ◻◻L
if PA can prove it, then PA can prove it can prove it
6. ◻L -> ◻C
ordinary MP
7. ◻L -> C
ordinary MP
8. ◻(◻L -> C)
ARGH WHAT ARE YOU DOING. THERE IS NO RULE OF FIRST ORDER LOGIC THAT ALLOWS YOU TO DO THIS. TO SAY "if i can prove X then i can prove i can prove X" STEPS OUTSIDE OF FIRST ORDER LOGIC YOU LOSE.
9. ◻L
ordinary MP
10 C
ordinary MP
In response to
The Cartoon Guide to Löb's Theorem
Eliezer: "Why doesn't the given proof of Lob's Theorem, the steps 1-10, show that PA + "◻C -> C" |- C?"
That's just not what it says. The hypothesis in step 2 isn't "◻C -> C" it's "◻(◻C -> C)". I suppose if the Hypothesis were "◻C -> C" we could try to find where it breaks. Step 7 is the only step that depends on 2 so it has to be there. Translating the amusing cartoons, we have
2. ◻(◻C -> C) 6. ◻(◻L -> ◻C) 7. ◻(◻L -> C)
Lets say that instead we have
2'. ◻C -> C
Well what are we supposed to do with it? We're stuck. Just because ◻C -> C doesn't mean that PA can prove it.
In response to
The Cartoon Guide to Löb's Theorem
Robert: "You can only say (((◻C)->C)->(◻C))"
No that's not right. The theorem says that if PA proves "◻C -> C" then PA proves C. so that's ◻(◻C -> C) -> ◻C.
The flaw is that the deduction theorem does not cross meta levels. Eliezer says "Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C." and goes on to claim that (◻C->C)->C. But he's intentionally failed to use quotes and mixed up the meta levels here. Lob's Theorem does not give us a proof in first order logic from ((◻C)->C) to C. It gives us a proof that if there is a proof of ((◻C)->C) then there is a proof of C. Which is an entirely diffirent thing altogether.
In response to
The Cartoon Guide to Löb's Theorem
Eliezer: "Any supposed analysis that does not tell you to mention a particular step, is inexact at best, and more probably mistaken."
I'm pretty sure my answer was completely correct. Care to point out the inexactness/mistakes?
= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
= f037147d6e6c911a85753b9abdedda8d){kind=logo}
simon:
It is a theorem about PA, although everything the statement and the proof of it can be expressed in PA if you like, in which case it is a theorem inside of PA about PA. There's no contradiction there, as long as you have everything quoted properly.
That's a valid deduction, but I don't think it's a step that anyone has written down in this thread before. It's not clear to me where you are going with it.
We use 10 steps, 9 of which are proofs inside of PA, and one of which is the fact that if PA |- X then PA |- "PA |- X".