Logic Journal of IGPL Advance Access originally published online on October 12, 2007
Logic Journal of IGPL 2007 15(5-6):767-774; doi:10.1093/jigpal/jzm048
A Note on Gentzen's LJ and NJ Systems Isomorphism
Dept. Filosofia, Universidade Federal de Goiás, Campus II Samambaia, Goiânia,GO, C.P. 131, CEP 74001-970, Brazil. E-mail: sanz{at}fchf.ufg.br
In this paper we are going to examine intuitionistic sequent calculus and its negation rules. We state new negation rules defining, in this way, a new sequent system. It will be used to clarify Gentzen's NJ and LJ systems isomorphism. These new negation rules are a direct reading of new natural deduction negation rules obtained by a slight modification of NJ rules. We also show that the new system is equivalent to LJ and that the Hauptsatz holds for it.
Key Words: negation rules intuitionist sequent calculus negation absurd.
Received for publication 15 September 2006.
References
- Curry HB. The Foundations of Mathematical Logic. (1963) McGraw-Hill.
- Gentzen G. Investigation into logical deduction. In: The Collected Papers of Gerhard Gentzen—Szabo ME, ed. (1969) North-Holland. 68–131.
- Martin-Löf P. On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic (1996) 1(1):11–60. http://www.hf.uio.no/ifikk/filosofi/njpl/vol1no1/meaning/meaning.html.
- Negri S, Von Plato J. Structural Proof Theory. (2001) Cambridge University Press.
- Prawitz D. Natural Deduction. (1965) Almqvist and Wiksells.
- Raggio A. The 50th anniversary of gentzen's thesis. In: Comtemporary Mathematics (1988) 69:93–97.
- Sanz W. Relating intuitionist negation and triviality. Logic Journal of the IGPL (2004) 11;12(6):581–599.[CrossRef]
- Troelstra AS, Schwichtenberg H. Basic Proof Theory. (1996) Cambridge University Press.
| ||||||||||||||||||||||||||||||||||||||||||||||||