An Alternative Natural Deduction for the Intuitionistic Propositional Logic

• Autorzy: Mirjana Ilić
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

natural deduction; intuitionistic logic

• Wydawca: Wydawnictwo Uniwersytetu Łódzkiego
• Czasopismo: Bulletin of the Section of Logic
• Rocznik: 2016
• Tom: 45
• Numer: 1

Daty

wydano

2016-03-30

Twórcy

autor

Mirjana Ilić

• University of Belgrade, Faculty of Economics

Bibliografia

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

Identyfikatory

DOI

10.18778/0138-0680.45.1.03