caa a22 4500 388039353 CHVBK 20180307125016.0 cr unu---uuuuu 161130e199806 xx s 000 0 eng 10.2307/2586859 doi S0022481200015176 pii (NATIONALLICENCE)cambridge-10.2307/2586859 Takeuti Gaisi Department of Mathematics, University of Illinois, Urbana, Illinois 61801, USA, E-mail: takeuti@saul.cis.upenn.edu Frege proof system and TNC° [Elektronische Daten] [Gaisi Takeuti] A Frege proof system F is any standard system of prepositional calculus, e.g., a Hilbert style system based on finitely many axiom schemes and inference rules. An Extended Frege system EF is obtained from F as follows. An EF-sequence is a sequence of formulas ψ1, ..., ψκ such that eachψ i is either an axiom of F, inferred from previous ψ u and ψ v (= ψ u → ψ i ) by modus ponens or of the form q ↔ φ, where q is an atom occurring neither in φ nor in any of ψ1, ,ψ i−1. Such q ↔ φ, is called an extension axiom and q a new extension atom. An EF-proof is any EF-sequence whose last formula does not contain any extension atom. In [12], S. A. Cook and R. Reckhow proved that the pigeonhole principle PHP has a simple polynomial size EF-proof and conjectured that PHP does not admit polynomial size F-proof. In [5], S. R. Buss refuted this conjecture by furnishing polynomial size F-proof for PHP. Since then the important separation problem of polynomial size F and polynomial size EF has not shown any progress. In [11], S. A. Cook introduced the system PV, a free variable equational logic whose provable functional equalities are ‘polynomial time verifiable' and showed that the metamathematics of F and EF can be developed in PV and the soundness of EF proved in PV. In [3], S. R. Buss introduced the first order system and showed that is essentially a conservative extension of PV. There he also introduced a second order system (BD). Copyright © Association for Symbolic Logic 1998 The Journal of Symbolic Logic Cambridge University Press 63/2(1998-06), 709-738 0022-4812 63:2<709 1998 63 JSL https://doi.org/10.2307/2586859 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.2307/2586859 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Takeuti Gaisi Department of Mathematics, University of Illinois, Urbana, Illinois 61801, USA, E-mail: takeuti@saul.cis.upenn.edu NATIONALLICENCE 773 0- The Journal of Symbolic Logic Cambridge University Press 63/2(1998-06), 709-738 0022-4812 63:2<709 1998 63 JSL CC0 http://creativecommons.org/publicdomain/zero/1.0 nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-cambridge