Frege proof system and TNC°

E-ISSN： 1943-5886|63|2|709-738

ISSN： 0022-4812

Source： The Journal of Symbolic Logic, Vol.63, Iss.2, 1998-06, pp. : 709-738

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

Abstract

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 ψ₁, …, ψ_κ 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 ψ₁,…,ψ_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.