simon2 comments on The Cartoon Guide to Löb's Theorem - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (90)
Hmm. I was thinking that Lรถb's Theorem was a theorem in PA, in which case the step going from
PA + ?(?C -> C) |- ?(?L -> C)
to
PA + ?(?C -> C) |- ?(?(?L -> C))
seems legitimate given
PA |- (?X -> ?(?X))
which we ought to be able to use since PA is part of the theory before the |- symbol.
If we don't have PA on the left, can we use all the "ingredients" without adding additional assumptions?
In any case, if we do not use the deduction theorem to derive the implication in Lรถb's Theorem, what do we use?