Label-free natural deduction systems for intuitionistic and classical modal logics

In this paper we study natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T, B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple labelfree natural deduction sy...

Full description

Saved in:
Bibliographic Details
Published in:Journal of applied non-classical logics 2010, Vol.20 (4), p.373-421
Main Authors: Galmiche, Didier, Salhi, Yakoub
Format: Article
Language:English
Subjects:
Computer programming
Computer Science
intuitionistic modal logics
Logic
Logic in Computer Science
natural deduction
normalization
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper we study natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T, B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple labelfree natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the subformula property in the intuitionistic case.
ISSN:1166-3081
1958-5780
1958-5780
1166-3081
DOI:10.3166/jancl.20.373-421