×

A new S4 classical modal logic in natural deduction. (English) Zbl 1109.03015

It is first shown that the normalization procedure for S4 modal logic presented by D. Prawitz [Natural deduction. A proof-theoretical study. Stockholm: Almqvist and Wiksell (1965; Zbl 0173.00205)] does not work. A new natural deduction system for S4 classical logic is then introduced. This system is equivalent to that of Prawitz and it is shown that every derivation in it can be transformed into a normal derivation.

MSC:

03B45 Modal logic (including the logic of norms)
03F05 Cut-elimination and normal-form theorems

Citations:

Zbl 0173.00205
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Normalization theorems for full first order classical natural deduction 56 (1991) · Zbl 0735.03028
[2] Natural deduction (1965)
[3] Theoria 7 (1985)
[4] DOI: 10.1093/logcom/3.5.533 · Zbl 0793.03013 · doi:10.1093/logcom/3.5.533
[5] DOI: 10.1023/A:1005291931660 · Zbl 0963.03033 · doi:10.1023/A:1005291931660
[6] Traduções via Teoria da Prova: Aplicações à Lógica Linear (2002)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.