Authors: Olaf Beyersdorff
Publish Date: 2008/09/27
Volume: 47, Issue: 1, Pages: 162-178
Abstract
This paper focuses on the deduction theorem for propositional logic We define and investigate different deduction properties and show that the presence of these deduction properties for strong proof systems is powerful enough to characterize the existence of optimal and even polynomially bounded proof systems We also exhibit a similar but apparently weaker condition that implies the existence of complete disjoint mathsfNP pairs In particular this yields a sufficient condition for the completeness of the canonical pair of Frege systems and provides a general framework for the search for complete mathsfNP pairs
Keywords: