An Alternative Natural Deduction for the Intuitionistic Propositional Logic

Mirjana Ilić

Bulletin of the Section of Logic (2016)

  • Volume: 45, Issue: 1
  • ISSN: 0138-0680

Abstract

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

How to cite

top

Mirjana Ilić. "An Alternative Natural Deduction for the Intuitionistic Propositional Logic." Bulletin of the Section of Logic 45.1 (2016): null. <http://eudml.org/doc/295532>.

@article{MirjanaIlić2016,
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.},
author = {Mirjana Ilić},
journal = {Bulletin of the Section of Logic},
keywords = {natural deduction; intuitionistic logic},
language = {eng},
number = {1},
pages = {null},
title = {An Alternative Natural Deduction for the Intuitionistic Propositional Logic},
url = {http://eudml.org/doc/295532},
volume = {45},
year = {2016},
}

TY - JOUR
AU - Mirjana Ilić
TI - An Alternative Natural Deduction for the Intuitionistic Propositional Logic
JO - Bulletin of the Section of Logic
PY - 2016
VL - 45
IS - 1
SP - null
AB - 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.
LA - eng
KW - natural deduction; intuitionistic logic
UR - http://eudml.org/doc/295532
ER -

References

top
  1. [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. [2] N. Francez, Relevant harmony, Journal of Logic and Computation, Volume 26, Number 1 (2016), pp. 235–245. 
  3. [3] G. Gentzen, Investigations into logical deduction, The Collected Papers of Gerhard Gentzen, Szabo, M. E. (ed.) North–Holland, pp. 68–131, (1969). 
  4. [4] S. Negri, A normalizing system of natural deduction for intuitionistic linear logic, Archive for Mathematical Logic 41 (2002), pp. 789–810. 
  5. [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. [6] J. von Plato, Natural deduction with general elimination rules, Archive for Mathematical Logic 40 (2001), pp. 541–567. 
  7. [7] G. Restall, Proof theory & philosophy, manuscript, available at http://consequently.org/writing/ptp 
  8. [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. [9] A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, (1996). 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.