An Alternative Natural Deduction for the Intuitionistic Propositional Logic

Mirjana Ilić

doi:10.18778/0138-0680.45.1.03

Authors

Mirjana Ilić University of Belgrade, Faculty of Economics

DOI:

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

Keywords:

natural deduction, intuitionistic logic

Abstract

A natural deduction system NI, for the full propositional intuitionistic logic, is proposed. The operational rules of NI are obtained by the translation from Gentzen’s calculus LJ and the normalization is proved, via translations from sequent calculus derivations to natural deduction derivations and back.

References

[1] K. Došen, A Historical Introduction to Substructural Logics, Substructural Logics, (eds. P. Schroeder-Heister and K. Došen), pp. 1–30, Oxford Science Publication, (1993).
Google Scholar

[2] N. Francez, Relevant harmony, Journal of Logic and Computation, Volume 26, Number 1 (2016), pp. 235–245.
Google Scholar

[3] G. Gentzen, Investigations into logical deduction, The Collected Papers of Gerhard Gentzen, Szabo, M. E. (ed.) North–Holland, pp. 68–131, (1969).
Google Scholar

[4] S. Negri, A normalizing system of natural deduction for intuitionistic linear logic, Archive for Mathematical Logic 41 (2002), pp. 789–810.
Google Scholar

[5] S. Negri, J. von Plato, Sequent calculus in natural deduction style, The Journal of Symbolic Logic, Volume 66, Number 4 (20011), pp. 1803–1816.
Google Scholar

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

[7] G. Restall, Proof theory & philosophy, manuscript, available at http://consequently.org/writing/ptp
Google Scholar

[8] M. H. Sørensen, P. Urzyczyn, Lectures on the Curry–Howard Isomorphism, Studies in Logic and the Foundations of Mathematics, Volume 149 (2006), Elsevier.
Google Scholar

[9] A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, (1996).
Google Scholar