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 Author

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

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

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

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

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

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

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

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

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