This approach to studying the minimal intuitionistic modal logic is based on a generalization of Gentzen's original sequent calculus introduced and developed by the author in a previous paper [see Ann. Pure Appl. Logic 58 (1992), no. 3, 229--246; MR1191942 (93k:03056)]. The complete proof-theoretic treatment of the calculus is presented, including the cut elimination theorem with some of its consequences. The author considers the corresponding 2-natural deduction system, followed by the normalization theorem, and analyzes its relationship with the 2-sequent calculus. Such an approach to the proof-theoretic analysis of logical systems seems to be very natural, fruitful and applicable to a wide class of logics.

2-sequent calculus: intuitionism and natural deduction

MASINI, Andrea
1993

Abstract

This approach to studying the minimal intuitionistic modal logic is based on a generalization of Gentzen's original sequent calculus introduced and developed by the author in a previous paper [see Ann. Pure Appl. Logic 58 (1992), no. 3, 229--246; MR1191942 (93k:03056)]. The complete proof-theoretic treatment of the calculus is presented, including the cut elimination theorem with some of its consequences. The author considers the corresponding 2-natural deduction system, followed by the normalization theorem, and analyzes its relationship with the 2-sequent calculus. Such an approach to the proof-theoretic analysis of logical systems seems to be very natural, fruitful and applicable to a wide class of logics.
proof theory; sequent calculus; natural deduction; modal logics
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/430358
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact