simon2 comments on The Cartoon Guide to Löb's Theorem - Less Wrong

12 Post author: Eliezer_Yudkowsky 17 August 2008 08:35PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (90)

Sort By: Old

You are viewing a single comment's thread.

Comment author: simon2 19 August 2008 10:49:21PM 0 points [-]

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?