A Simulation of Natural Deduction and Gentzen Sequent Calculus

• Authors: Kozhemiachenko Daniil
• Languages of publication: EN

Abstracts

EN

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

EN

speedup; natural deduction; Gentzen-style calculi; simulation; proof system

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2018
• Volume: 27
• Issue: 1
• Pages: 67–84

Dates

published

2018-03-15

Contributors

author

Kozhemiachenko Daniil

• Department of Philosophy, Moscow State University, Lomonosovsky prospekt, 27-4, GSP-1, Moscow 119991, Russian Federation

References

• Bonet, M.L., and S.R. Buss, “The deduction rule and linear and nearlinear proof simulations”, The Journal of Symbolic Logic 58, 2 (1993): 688–709. DOI: 10.2307/2275228
• Buss, S.R. (ed.), Handbook of Proof Theory, volume 137 of Studies in Logic and Foundations of Mathematic, Elsevier Science, Amsterdam, 1st edition, 1998.
• Cook, S.A., and P. Nguyen, Logical Foundations of Proof Complexity, Cambridge University Press, Cambridge, 2010.
• Cook, S.A., and R.A. Reckhow, “The relative efficiency of propositional proof systems”, The Journal of Symbolic Logic 44, 1 (1979): 36–50. DOI: 10.2307/2273702
• D’Agostino, M., Investigations into the Complexity of Some Propositional Calculi, Oxford University Computing Laboratory, Oxford, 1990.
• Finger, M., “Dag sequent proofs with a substitution rule”, pages 671–686 in We Will Show Them: Essays in Honor of Dov Gabbay’s 60th Birthday, London, Kings College Publications, 2005.
• Fitch, F.B., Symbolic Logic: An Introduction, The Ronald Press Company, N.Y., 1952.
• Gentzen, G., “Untersuchungen über das logische Schließen I”, Mathematische Zeitschrift 39 (1935): 176–210. DOI: 10.1007/BF01201353
• Jaśkowski, S., “On the rules of supposition in formal logic”, Studia Logica 1 (1934).
• Krajìček, J., “On the number of steps in proofs”, Annals of Pure and Applied Logics 41 (1989): 153–178.
• Papadimitriou, C.H., Computational Complexity, Addison-Wesley Publishing Company, Inc., NY, 1995.
• Pelletier, F.J., “A brief history of natural deduction”, History and Philosophy of Logic 20 (1999): 1–31. DOI: 10.1080/014453499298165
• Reckhow, R.A., “On the lengths of proofs in the propositional calculus”, PhD thesis, University of Toronto, 1976.
• Smullyan, R.M., First-Order Logic, Dover Publications, Inc., N.Y., 1995.
• Tseitin, G.S., On the Complexity of Derivation in Propositional Calculus, pages 466–483, Springer-Verlag, NY, 1983.
• Urquhart, A., “The complexity of gentzen systems for propositional logic”, Theoretical Computer Science 66, 1 (1989): 87–97. DOI: 10.1016/0304-3975(89)90147-3
• Urquhart, A., “The relative complexity of resolution and cut-free Gentzen systems”, Annals of Mathematics and Artificial Intelligence 6, 1–3 (1992): 157–168. DOI: 10.1007/BF01531026
• Urquhart, A., “The complexity of propositional proofs”, The Bulletin of Symbolic Logic 1, 4 (1995): 425–467.

Identifiers

DOI

10.12775/LLP.2017.009