Eliezer Yudkowsky comments on An angle of attack on Open Problem #1

Eliezer Yudkowsky 19 Aug 2012 21:33 UTC
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)
```
- Benya 19 Aug 2012 22:02 UTC
  0 points
  Parent
  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.]
- wuncidunci 19 Aug 2012 21:48 UTC
  0 points
  Parent
  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.