Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic

Chuck Liang 1 Dale Miller 2, 3
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : We combine intuitionistic logic and classical logic into a new, first-order logic called Polarized Intuitionistic Logic. This logic is based on a distinction between two dual polarities which we call red and green to distinguish them from other forms of polarization. The meaning of these polarities is defined model-theoretically by a Kripke-style semantics for the logic. Two proof systems are also formulated. The first system extends Gentzen's intuitionistic sequent calculus LJ. In addition, this system also bears essential similarities to Girard's LC proof system for classical logic. The second proof system is based on a semantic tableau and extends Dragalin's multiple-conclusion version of intuitionistic sequent calculus. We show that soundness and completeness hold for these notions of semantics and proofs, from which it follows that cut is admissible in the proof systems and that the propositional fragment of the logic is decidable.
Type de document :
Article dans une revue
Annals of Pure and Applied Logic, Elsevier Masson, 2013, 164 (2), pp.86-111. 〈10.1016/j.apal.2012.09.005〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00787601
Contributeur : Dale Miller <>
Soumis le : mardi 12 février 2013 - 14:35:12
Dernière modification le : jeudi 10 mai 2018 - 02:06:58
Document(s) archivé(s) le : lundi 13 mai 2013 - 04:11:23

Fichier

pil-final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Chuck Liang, Dale Miller. Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic. Annals of Pure and Applied Logic, Elsevier Masson, 2013, 164 (2), pp.86-111. 〈10.1016/j.apal.2012.09.005〉. 〈hal-00787601〉

Partager

Métriques

Consultations de la notice

3224

Téléchargements de fichiers

511