Eliezer_Yudkowsky 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: Benja 19 August 2012 10:02:20PM * 0 points [-]

Ha! I'm not sure what the exact relation to PAK is, but PAT is almost exactly what I'm using in my new proof:

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

("PPT" for "parametric polymorphism trick, v 0.2".) [ETA: added "K>0" condition.]

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)