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.
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:
This is incorrect because the if-then is outside of PA. The deduction theorem does not apply.