The deduction rule and linear and near-linear proof simulations

Journal of Symbolic Logic 58 (2):688-709 (1993)

Abstract
We introduce new proof systems for propositional logic, simple deduction Frege systems, general deduction Frege systems, and nested deduction Frege systems, which augment Frege systems with variants of the deduction rule. We give upper bounds on the lengths of proofs in Frege proof systems compared to lengths in these new systems. As applications we give near-linear simulations of the propositional Gentzen sequent calculus and the natural deduction calculus by Frege proofs. The length of a proof is the number of lines in the proof. A general deduction Frege proof system provides at most quadratic speedup over Frege proof systems. A nested deduction Frege proof system provides at most a nearly linear speedup over Frege system where by "nearly linear" is meant the ratio of proof lengths is O) where α is the inverse Ackermann function. A nested deduction Frege system can linearly simulate the propositional sequent calculus, the tree-like general deduction Frege calculus, and the natural deduction calculus. Hence a Frege proof system can simulate all those proof systems with proof lengths bounded by O). Also we show that a Frege proof of n lines can be transformed into a tree-like Frege proof of O lines and of height O. As a corollary of this fact we can prove that natural deduction and sequent calculus tree-like systems simulate Frege systems with proof lengths bounded by O.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.2307/2275228
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 46,330
Through your library

References found in this work BETA

Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
The Collected Papers of Gerhard Gentzen.G. Kreisel - 1971 - Journal of Philosophy 68 (8):238-265.
Introduction to Metamathematics.H. Rasiowa - 1954 - Journal of Symbolic Logic 19 (3):215-216.

Add more references

Citations of this work BETA

Some Remarks on Lengths of Propositional Proofs.Samuel R. Buss - 1995 - Archive for Mathematical Logic 34 (6):377-394.
Lower Complexity Bounds in Justification Logic.Samuel R. Buss & Roman Kuznets - 2012 - Annals of Pure and Applied Logic 163 (7):888-905.

Add more citations

Similar books and articles

Analytics

Added to PP index
2009-01-28

Total views
45 ( #197,896 of 2,285,998 )

Recent downloads (6 months)
11 ( #79,901 of 2,285,998 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature