endoself comments on An angle of attack on Open Problem #1 - Less Wrong

30 Post author: Benja 18 August 2012 12:08PM

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

Article Navigation

Comments (84)

Comments (84)

You are viewing a single comment's thread. Show more comments above.

Comment author: Eliezer_Yudkowsky 19 August 2012 01:18:54AM 1 point [-]

Now let's extend the language of PA by a constant symbol K, and define PAK := Peano Arithmetic (actually, the natural extension of PA to this new language) + for all formulas 'C' of the base language: "if PA(K) proves 'C', then C".

Either I didn't understand how PA(K) is constructed at all, or this instantly dies by Lob's Theorem. If any language L proves 'If L proves C, then C', then L proves C. So if PA(K) has "If PA(K) proves 2=1, then 2=1" then PA(K) proves 2=1.

Comment author: endoself 19 August 2012 02:10:52AM *  3 points [-]

PAK != PA(K)

PAK is the language that Benja is defining there, while PA(K) is just the Kth-level PA in the PA hierarchy.

Comment author: Benja 19 August 2012 09:01:16AM *  2 points [-]

That's exactly right, and Will_Sawin is right about it being confusing -- perhaps I should have used a more creative name for PA_K.

Powered by Reddit Powered by Reddit