From Gentzen to Jaskowski and Back: Algorithmic Translation of Derivations Between the Two Main Systems of Natural Deduction

Jan von Plato

doi:10.18778/0138-0680.46.1.2.06

Authors

Jan von Plato University of Helsinki, Department of Philosophy, Helsinki, Finland

DOI:

https://doi.org/10.18778/0138-0680.46.1.2.06

Keywords:

proof systems, linear natural deduction, Gentzen, Jaśkowski

Abstract

The way from linearly written derivations in natural deduction, introduced by Jaskowski and often used in textbooks, is a straightforward root-first translation. The other direction, instead, is tricky, because of the partially ordered assumption formulas in a tree that can get closed by the end of a derivation. An algorithm is defined that operates alternatively from the leaves and root of a derivation and solves the problem.

References

[1] H. Curry, (1965) Remarks on inferential deduction, [in:] A. Tyminiecka (ed.), Contributions to Logic and Methodology in Honor of J. M. Bochenski, North-Holland (1965), pp. 45–72.
Google Scholar

[2] G. Gentzen, Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1934-35), pp. 176–210 and 405-431.
Google Scholar

[3] S. Jaśkowski, On the rules of supposition in formal logic (1934), as reprinted [in:] S. McCall (ed.), Polish Logic 1920–1939, pp. 232–258, Oxford U. P. 1967.
Google Scholar

[4] J. von Plato, Natural deduction with general elimination rules, Archive for Mathematical Logic, vol. 40 (2001), pp. 541–567.
Google Scholar

[5] J. von Plato, Elements of Logical Reasoning, Cambridge, 2013.
Google Scholar

[6] D. Prawitz, ABC i Symbolisk Logik, Mimeographed compendium. Later expanded and printed editions with Bokförlaget Thales, 1973.
Google Scholar