Proof Analysis in Intermediate Logics

Roy Dyckhoff, Sara Negri

Research output: Contribution to journalArticlepeer-review

55 Citations (Scopus)

Abstract

Using labelled formulae, a cut-free sequent calculus for intuitionistic propositional logic is presented, together with an easy cut-admissibility proof; both extend to cover, in a uniform fashion, all intermediate logics characterised by frames satisfying conditions expressible by one or more geometric implications. Each of these logics is embedded by the Gödel–McKinsey–Tarski translation into an extension of S4. Faithfulness of the embedding is proved in a simple and general way by constructive proof-theoretic methods, without appeal to semantics other than in the explanation of the rules.
Original languageEnglish
Pages (from-to)71–92
Number of pages22
JournalArchive for Mathematical Logic
Volume51
Issue number1-2
DOIs
Publication statusPublished - 2012

Fingerprint

Dive into the research topics of 'Proof Analysis in Intermediate Logics'. Together they form a unique fingerprint.

Cite this