A Frege proof systemFis any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege systemEFis obtained fromFas follows. AnEF-sequence is a sequence of formulas ψ1, …, ψκsuch that eachψiis either an axiom ofF, inferred from previous ψuand ψv by modus ponens or of the formq↔ φ, whereqis an atom occurring neither in φ nor in any of ψ1,…,ψi−1. Suchq↔ φ, is called an extension axiom andqa new extension (...) atom. AnEF-proof is anyEF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principlePHPhas a simple polynomial sizeEF-proof and conjectured thatPHPdoes not admit polynomial sizeF-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial sizeF-proof forPHP. Since then the important separation problem of polynomial sizeFand polynomial sizeEFhas not shown any progress.In [11], S. A. Cook introduced the systemPV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable’ and showed that the metamathematics ofFandEFcan be developed inPVand the soundness ofEFproved inPV. In [3], S. R. Buss introduced the first order systemand showed thatis essentially a conservative extension ofPV. There he also introduced a second order system. (shrink)