Larry_D'Anna 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: Larry_D'Anna 20 August 2008 01:05:20AM 0 points [-]

simon:

I was thinking that Lรถb's Theorem was a theorem in PA

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.

in which case the step going from

PA + ?(?C -> C) |- ?(?L -> C)

to

PA + ?(?C -> C) |- ?(?(?L -> C))

seems legitimate given

PA |- (?X -> ?(?X))

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.

In any case, if we do not use the deduction theorem to derive the implication in Lรถb's Theorem, what do we use?

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".