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

Sort By: Best

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

Comment author: Eliezer_Yudkowsky 19 August 2012 09:33:26PM 1 point [-]

Try two:

Does the following language do the same thing as PAK?

PAT = PA + symbol K + schema over Formulas of one variable:
- For all P:
-- if P proves-in-PAT 'Formula(K+1)', then Formula(K)

Comment author: wuncidunci 19 August 2012 09:48:19PM -1 points [-]

PAK proves all which your PAT does, but probably not the other way around.

I think this bit is all that's strictly necessary in the proof though.

Comments (84)