Okay, I still don’t see why we had to pinpoint the flaw in your proof by pointing to a step in someone else’s valid proof.
Larry D’Anna identified the step you were looking for, but he did it by trying to transform the proof of Lob’s Theorem into a different proof that said what you were pretending it said.
I think, properly speaking, the flaw is pinpointed by saying that you were misusing the theorems, not that the mean old theorem had a step that wouldn’t convert into what you wanted it to be.
I’ve been looking more at the textual proof you linked (the cartoon was helpful, but it spread the proof out over more space) which is a little different and has an all-ascii notation that I’m going to borrow from.
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]
PA |- (not []C) → C [Definition of implication]
(PA |- ((not []C) → C) and (PA |- not []C) [New assumption]
PA |- ((not []C) → C) and (not []C) [If you can derive two things, you can derive the conjunction]
PA |- C [Definition of implication]
And conclude that all provably unprovable statements are also provable, not that all unprovable statements are true.
(Disclaimer: I am definitely not a mathematician, and I skipped over your meta-ethics because I only like philosophy in small doses.)
Okay, I still don’t see why we had to pinpoint the flaw in your proof by pointing to a step in someone else’s valid proof.
Larry D’Anna identified the step you were looking for, but he did it by trying to transform the proof of Lob’s Theorem into a different proof that said what you were pretending it said.
I think, properly speaking, the flaw is pinpointed by saying that you were misusing the theorems, not that the mean old theorem had a step that wouldn’t convert into what you wanted it to be.
I’ve been looking more at the textual proof you linked (the cartoon was helpful, but it spread the proof out over more space) which is a little different and has an all-ascii notation that I’m going to borrow from.
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]
PA |- (not []C) → C [Definition of implication]
(PA |- ((not []C) → C) and (PA |- not []C) [New assumption]
PA |- ((not []C) → C) and (not []C) [If you can derive two things, you can derive the conjunction]
PA |- C [Definition of implication]
And conclude that all provably unprovable statements are also provable, not that all unprovable statements are true.
(Disclaimer: I am definitely not a mathematician, and I skipped over your meta-ethics because I only like philosophy in small doses.)