Full-text resources of CEJSH and other databases are now available in the new Library of Science.
Visit https://bibliotekanauki.pl


2018 | 27 | 1 | 67–84

Article title

A Simulation of Natural Deduction and Gentzen Sequent Calculus


Title variants

Languages of publication



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.








Physical description




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


  • 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.

Document Type

Publication order reference


YADDA identifier

JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.