Logic and Logical Philosophy 27 (1):67-84 (2018)

We consider four natural deduction systems: Fitch-style systems, Gentzen-style systems (in the form of dags), general deduction Frege systems and nested deduction Frege systems, as well as dag-like Gentzen-style sequent calculi. All these calculi soundly and completely formalize classical propositional logic. We show that general deduction Frege systems and Gentzen-style natural calculi provide at most quadratic speedup over nested deduction Frege systems and Fitch-style natural calculi and at most cubic speedup over Gentzen-style sequent calculi.
Keywords speedup, natural deduction  Gentzen-style calculi  simulation  proof system
Categories (categorize this paper)
DOI 10.12775/LLP.2017.009
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 51,508
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Cut as Consequence.Curtis Franks - 2010 - History and Philosophy of Logic 31 (4):349-379.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
A Survey of Nonstandard Sequent Calculi.Andrzej Indrzejczak - 2014 - Studia Logica 102 (6):1295-1322.
A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
On Quine's Approach to Natural Deduction'.Carlo Cellucci - 1995 - In Paolo Leonardi & Marco Santambrogio (eds.), On Quine: New Essays. Cambridge University Press. pp. 314--335.
Marginalia on Sequent Calculi.A. S. Troelstra - 1999 - Studia Logica 62 (2):291-303.
Translating a Suppes-Lemmon Style Natural Deduction Into a Sequent Calculus.Pavlović Edi - 2015 - European Journal of Analytic Philosophy 11 (2):79--88.
From Axiomatic Logic to Natural Deduction.Jan von Plato - 2014 - Studia Logica 102 (6):1167-1184.
Sequent Calculus in Natural Deduction Style.Sara Negri & Jan von Plato - 2001 - Journal of Symbolic Logic 66 (4):1803-1816.


Added to PP index

Total views
19 ( #508,970 of 2,331,007 )

Recent downloads (6 months)
4 ( #194,675 of 2,331,007 )

How can I increase my downloads?


My notes