Combining First-Order Classical and Intuitionistic Logic

TL;DR

This paper develops a proof-theoretic framework for a first-order logic system combining classical and intuitionistic logic, introducing a sequent calculus with cut-elimination and completeness results.

Contribution

It introduces a new sequent calculus G(FOC+J) for first-order combined classical and intuitionistic logic, with cut-elimination and strong completeness proofs.

Findings

Cut-elimination ensures the subformula property.

G(FOC+J) is conservative over first-order intuitionistic and classical logic.

Strong completeness is established via a canonical model argument.

Abstract

This paper studies a first-order expansion of a combination C+J of intuitionistic and classical propositional logic, which was studied by Humberstone (1979) and del Cerro and Herzig (1996), from a proof-theoretic viewpoint. While C+J has both classical and intuitionistic implications, our first-order expansion adds classical and intuitionistic universal quantifiers and one existential quantifier to C+J. This paper provides a multi-succedent sequent calculus G(FOC+J) for our combination of the first-order intuitionistic and classical logic. Our sequent calculus G(FOC+J) restricts contexts of the right rules for intuitionistic implication and intuitionistic universal quantifier to particular forms of formulas. The cut-elimination theorem is established to ensure the subformula property. As a corollary, G(FOC+J) is conservative over both first-order intuitionistic and classical logic. Strong completeness of G(FOC+J) is proved via a canonical model argument.