Comparison of Proof Sizes in Frege Systems and Substitution Frege Systems

摘要

It is known that the minimal number of the steps in a proof of a tautology in a Frege system can be exponentially larger than in a substitution Frege system, but it is an open problem whether Frege systems can polynomially simulate substitution Frege systems by sizes. Many people conjecture that the answer is no. We prove that the answer is yes. As a bridge between substitution Frege systems and Frege systems we consider the Frege systems, augmented with restricted substitution (single renaming) rule. We prove that Frege systems with single renaming rule polynomially simulate by size Frege systems with substitution rule without any restrictions, and Frege systems without substitution rule polynomially simulate Frege systems with single renaming rule both by steps and by size.