The Deduction Theorem for Strong Propositional Proof Systems
Olaf Beyersdorff
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 NP-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
NP-pairs.
PDF: delhi_final.pdf