Combining First-Order Classical and Intuitionistic Logic

This paper studies a proof-theoretic aspect of a first-order expansion of a combined logic $\mathbf{C+J}$ of intuitionistic and classical propositional logic, which was studied by Humberstone [8] and del Cerro and Herzig [3]. While $\mathbf{C+J}$ has both classical and intuitionistic implications, our first-order expansion adds classical and intuitionistic universal quantifiers and one existential quantifier to $\mathbf{C+J}$. In particular, this paper proposes a cut-free sequent calculus called $\mathsf{G}(\mathbf{FOC}+\mathbf{J})$, which is an expansion of the calculus $\mathsf{G}(\mathbf{C}+\mathbf{J})$ in [25] for the combination of intuitionistic and classical propositional logic.

There are various semantic methods to combine intuitionistic and classical logic, such as ones in [2, 4, 5], but this paper follows the semantic treatment in [3, 8], whose main idea is adding intuitionistic and classical implications into one logic called $\mathbf{C+J}$. Each implication (expressed as $\mathbin{\to}_{\_}{\mathtt{i}},\mathbin{\to}_{\_}{\mathtt{c}}$, respectively) is interpreted in a Kripke model as follows:

where $M$ is an intuitionistic Kripke model, $w$ is a possible world in $M$, and $R$ is a preorder equipped in $M$.

It is well-known that an intuitionistically valid formula $A\mathbin{\to}_{\_}{\mathtt{i}}(B\mathbin{\to}_{\_}{\mathtt{i}}A)$ corresponds to the property called heredity with respect to $A$ in intuitionistic Kripke semantics, which is defined as: $w\models A$ and $wRv$ jointly imply $v\models A$ for all Kripke models $M$ and all states $w$ and $v$ in $M$¹¹1The correspondence between heredity and the formula $A\mathbin{\to}_{\_}{\mathtt{i}}(B\mathbin{\to}_{\_}{\mathtt{i}}A)$ is mentioned in [9, 10, 24]. However, the existence of classical implication breaks this heredity in the Kripke semantics of $\mathbf{C+J}$, i.e., there is a Kripke model where $\neg_{\_}{\mathtt{c}}p\mathbin{\to}_{\_}{\mathtt{i}}(\top\mathbin{\to}_{\_}{\mathtt{i}}\neg_{\_}{\mathtt{c}}p)$ is not valid. Because of this semantic phenomenon, del Cerro and Herzig [3] added to their Hilbert system for $\mathbf{C+J}$ the following syntactically restricted axiom:

where a persistent formula can be understood essentially as a formula of the form atomic $p$ or $A\mathbin{\to}_{\_}{\mathtt{i}}B$ ($A$ and $B$ possibly contain the classical implication)²²2The reason why we use the expression “essentially” is the definition provided in [3] is slightly different..

By employing the idea of the axiom (PER), a cut-free sequent calculus $\mathsf{G}(\mathbf{C}+\mathbf{J})$ of $\mathbf{C+J}$ was proposed in [25] where the right rule for the intuitionistic implication is restricted as follows:

while the ordinary right rule for the intuitionistic implication is of the following form:

When expanding $\mathbf{C+J}$ to a first-order syntax, we add intuitionistic and classical universal quantifiers (expressed as $\forall_{\_}{\mathtt{i}},\forall_{\_}{\mathtt{c}}$, respectively) and one existential quantifier (expressed as $\exists$). Each universal quantifier is interpreted in a Kripke model as follows:

where $M$ is a Kripke model for first-order intuitionistic logic and $\underline{d}$ is a syntactic name of an element $d$ in a domain. As a Kripke model for propositional intuitionistic logic, $w$ and $v$ are possible worlds in $M$ and $R$ is a preorder equipped in $M$.

This paper is structured as follows. Section 2 provides our syntax, Kripke semantics for it, and the sequent calculus $\mathsf{G}(\mathbf{FOC}+\mathbf{J})$. The soundness is shown in the section. Section 3 demonstrates the cut elimination theorem. Section 4 establishes the strong completeness for Kripke semantics via a canonical model argument. Section 5 concludes the paper and gives further direction of research.

An attempt related to our approach the most was the one in [12]. In [12], a sequent calculus for a first-order combination of intuitionistic and classical logic, denoted by $\mathbf{FO^{\supset}}$, was given. This calculus is provided by adding intuitionistic implication to first-order classical logic, so it has only one universal quantifier (a classical one). Therefore, this study is also regarded as a different first-order expansion of $\mathbf{C+J}$ from ours. From our perspective, however, the intuitionistic universal quantifier is missing in [12]. In order to deal with the failure of the heredity mentioned in Section 1.1, the calculus employs the notion of structured single succedent sequent of the form: $\Gamma_{\_}{1};\cdots;\Gamma_{\_}{n}\Rightarrow A$, where $\Gamma_{\_}{i}$ is a finite set of formulas. For example, $B_{\_}{1},B_{\_}{2};C_{\_}{1},C_{\_}{2},C_{\_}{3};D\Rightarrow A$ is a structured sequent and its semantic interpretation (see [12, Definition 16]) is: for any $w_{\_}{1},w_{\_}{2},w_{\_}{3}$ such that $w_{\_}{1}\leqslant w_{\_}{2}\leqslant w_{\_}{3}$, if $w_{\_}{1}\models B_{\_}{i}$ for all $i$, $w_{\_}{2}\models C_{\_}{j}$ for all $j$ and $w_{\_}{3}\models D$, then $w_{\_}{3}\models A$. Thanks to this notion, no restriction on contexts is needed for sequents in $\mathbf{FO^{\supset}}$. It is noted that some rule for $\mathbf{FO^{\supset}}$ does not satisfy the subformula property. Lucio [12] proved that $\mathbf{FO^{\supset}}$ is sound and complete for the intended Kripke semantics.

Other than $\mathbf{C+J}$, there are many attempts to combine intuitionistic and classical logic. In [2], a logic called $\mathbf{CIPL}$, whose syntax consists of propositional variables and intuitionistic and classical implications, was proposed, and a Hilbert system and a Kripke semantics were given. The Kripke semantics has an interpretation of classical implication different from that of $\mathbf{C+J}$. In [4, 5], the logic called $\mathbf{IPC}^{\sim}$ was given by adding a negation called “empirical negation” to intuitionistic logic. This negation may be regarded as classical negation, but the semantic interpretation of empirical negation was different from classical one. That is, the empirical negation is evaluated at a base state of a Kripke model where a base state can see all states. Also, a semantic consequence relation in [4, 5] is defined in terms of base states of Kripke models. It should be noted that all formulas satisfy heredity in $\mathbf{IPC}^{\sim}$. In [4, 5], a Hilbert system was given for $\mathbf{IPC}^{\sim}$. We, however, emphasize that all of [2, 4, 5] stay at the propositional level. Our study of a first-order expansion of $\mathbf{C+J}$ may be useful to expand these systems to the first-order level.

This section introduces the syntax for $\mathsf{G}(\mathbf{FOC}+\mathbf{J})$. Our syntax $\mathcal{L}$ consists of the following:

• •

  A countably infinite set of variables $\mathsf{Var}$ := $\{x_{\_}{1},x_{\_}{2},\ldots\}$,

• •

  A countably infinite set of constant symbols $\{c_{\_}{1},c_{\_}{2},\ldots\}$,

• •

  A countably infinite set of predicate symbols $\{P_{\_}{1},P_{\_}{2},\ldots\}$,

• •

  Logical connectives: $\bot,\land,\lor,\mathbin{\to}_{\_}{\mathtt{i}},\mathbin{\to}_{\_}{\mathtt{c}}$,

• •

  Quantifiers: $\forall_{\_}{\mathtt{i}},\forall_{\_}{\mathtt{c}},\exists$.

Terms consist of variables and constant symbols and are denoted by $t_{\_}{1},t_{\_}{2},\ldots$. A constant symbol is called a closed term, since it has no occurrence of free variables. The set of all formulas $\mathsf{Form}_{\_}{\mathcal{L}}$ (often written as $\mathsf{Form}$) for the syntax $\mathcal{L}$, is defined inductively as follows:

where $P$ denotes a predicate symbol. We denote by $\mathsf{Form}_{\_}{\mathbf{C}}$ and $\mathsf{Form}_{\_}{\mathbf{J}}$ the set of all classical formulas and the set of all intuitionistic formulas in $\mathcal{L}$, respectively. The set of free variables in a formula $A$ is denoted by $\mathsf{FV}(A)$. We define a closed formula as a formula which has no occurrence of a free variable. We employ the notion of clash avoiding substitution $[t/x]$ when we do substitution in a formula, as [17]. By employing this notion, we can avoid the case where $t$ becomes a bound variable in the formula as an effect of substitution of $t$ for $x$. We also consider a syntax $L$ different from $\mathcal{L}$, which contains all the logical connectives and the set of predicate and constant symbols of $\mathcal{L}$. That is, $L$ and $\mathcal{L}$ are different only in a set of variables. We denote the set of variables in a syntax $L$ by $\mathsf{Var}(L)$, and the set of all formulas in a syntax $L$ is denoted by $\mathsf{Form}_{\_}{L}$. We call a formula $A$ an $L$-formula if $A\in\mathsf{Form}_{\_}{L}$.

Let us move to the semantics for our syntax $\mathcal{L}$. We give a valuation and a satisfaction relation only to closed formulas, and deal with possibly non-closed formulas in the definition of semantic consequence relation (Definition 5). First, we define a Kripke frame $F$ and then proceed to defining valuation $V$.

Let $\mathcal{L}(A)$ be an expanded syntax of $\mathcal{L}$ by the constant symbols $\{\underline{a}|a\in A\}$ to all the elements of $A$.

We proceed to the matter of heredity in a Kripke model. Heredity is known as an important feature of pure intuitionistic logic, i.e., Fact 1 holds.

This section provides a sequent calculus $\mathsf{G}(\mathbf{FOC}+\mathbf{J})$, which is a first-order expansion of propositional $\mathsf{G}(\mathbf{C}+\mathbf{J})$ in [25]. The calculus employs the ordinary notion of multi-succedent sequent. A sequent is a pair of finite multisets of formulas denoted by $\Gamma\Rightarrow\Delta$, which is read as “if all formulas in $\Gamma$ hold then some formulas in $\Delta$ hold.”

The sequent calculus $\mathsf{G}(\mathbf{FOC}+\mathbf{J})$ consists of the axioms and the rules in Table 1. The notion of derivability is defined as an existence of a finite tree, which is called a derivation, generated by inference rules of Table 1 from initial sequents $(Id)$ and $(\bot)$ of Table 1.

Our basic strategy of constructing $\mathsf{G}(\mathbf{FOC}+\mathbf{J})$ is to add classical implication and universal quantifier to the multi-succedent sequent calculus $\mathbf{mLJ}$, proposed by Maehara [13], where the right rules for intuitionistic implication and universal quantifier are of the following form:

where $\Gamma$ is a finite multiset of intuitionistic formulas. However, if the ordinary left and right rules for classical implication were added to $\mathbf{mLJ}$, the soundness of the resulting calculus would fail, because formulas $\neg_{\_}{\mathtt{c}}P(t)\mathbin{\to}_{\_}{\mathtt{c}}(\top\mathbin{\to}_{\_}{\mathtt{i}}\neg_{\_}{\mathtt{c}}P(t))$ and $\forall_{\_}{\mathtt{i}}y(\neg_{\_}{\mathtt{c}}\forall_{\_}{\mathtt{c}}xP(x)\mathbin{\to}_{\_}{\mathtt{i}}\neg_{\_}{\mathtt{c}}P(y))\mathbin{\to}_{\_}{\mathtt{i}}(\neg_{\_}{\mathtt{c}}\forall_{\_}{\mathtt{c}}xP(x)\mathbin{\to}_{\_}{\mathtt{i}}\forall_{\_}{\mathtt{i}}y\neg_{\_}{\mathtt{c}}P(y))$ would be derivable, which are found invalid by Propositions 3 and 5. This is the reason why the original right rules for intuitionistic implication and universal quantifier of $\mathbf{mLJ}$ described above are restricted to the right rules given in Table 1. Although the restriction should be imposed on a context $\Gamma$ of theses rules, no extra restriction is needed. Thus, the following applications of $(\Rightarrow\mathbin{\to}_{\_}{\mathtt{i}})$ and $(\Rightarrow\forall_{\_}{\mathtt{i}})$ are always legitimate:

Based on the abbreviation defined in Section 2.1, the following rules for the negations are obtained.

For example, the sequent $\top\mathbin{\to}_{\_}{\mathtt{i}}\forall_{\_}{\mathtt{c}}xP(x)\Rightarrow\forall_{\_}{\mathtt{c}}x(\top\mathbin{\to}_{\_}{\mathtt{i}}P(x))$ is derivable in $\mathsf{G}(\mathbf{FOC}+\mathbf{J})$ as follows:

As is noted in Section 1.1 for the propositional $\mathsf{G}(\mathbf{C}+\mathbf{J})$, although the context of the right rule for intuitionistic implication is restricted, all sequents derivable in propositional intuitionistic logic are also derivable. Similarly, all sequents derivable in first-order $\mathbf{mLJ}$ are also derivable in $\mathsf{G}(\mathbf{FOC}+\mathbf{J})$. The following proposition ensures this.

We proceed to the soundness theorem. We use $\Gamma\models\Delta$ to mean: for some formula $C\in\Delta$, $\Gamma\models C$ holds.

Formulas occurring at a context of the right rules for the intuitionistic implication and universal quantifier must be persistent. In what follows, we use $\Theta$ to denote a multiset of persistent formulas. This is just for making the notation simpler. By this notation, the right rules for the intuitionistic implication and the intuitionistic universal quantifier are described as follows: