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.]
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” for “parametric polymorphism trick, v 0.2″.) [ETA: added “K>0” condition.]