Kripke semantics and proof systems for combining intuitionistic logic and classical logic (Q690929)

The basic question discussed here is whether the critical intuitionistic connectives of implication and universal quantification can retain their strength when combined with classical connectives. In order to combine intuitionistic and classical logic the authors introduce a first-order predicate logic called polarized intuitionistic logic (PIL) based on a distinction between two dual polarities defined model-theoretically by means of the Kripke-type semantics for this logic. The proof-theoretical treatment of PIL includes two proof systems: the first one extending Gentzen's sequent calculus for intuitionistic logic, and the second one based on a semantic tableau extending Dragalin's multiple-conclusion sequent calculus for intuitionistic logic. The corresponding soundness and completeness results are obtained having as consequence the admissibility of the cut rule. Various double-negation translations, dual-intuitionistic logic, linear logic, PIL etc. are discussed in the final part of the paper.