1 Introduction
The principle of excluded middle
$A \mathbin {\vee } \neg A$
, or equivalently the double-negation elimination
$\neg \neg A \mathbin {\Rightarrow } A$
, are classical logic postulates which are not derivable in intuitionistic logic. It follows that provability in classical logic does not generally imply provability in intuitionistic logic. It is however possible to embed classical logic into intuitionistic logic. Glivenko [Reference Glivenko12] proved that, for any provable formula
$A$
in classical propositional logic, there exists an intuitionistic proof of its double negation
$\neg \neg A$
. Kolmogorov [Reference Kolmogorov15], Gödel [Reference Gödel13], Gentzen [Reference Gentzen11], and Kuroda [Reference Kuroda16] developed translations
$A \mapsto A^{\star }$
that insert double negations inside formulas. For any first-order context
$\Gamma $
and formula
$A$
, such translations satisfy two properties:
-
(i) if $\Gamma \vdash _c A$
then
$\Gamma ^{\star } \vdash _i A^{\star }$
(soundness), -
(ii) $\vdash _c A^{\star } \Leftrightarrow A$
(characterization).
Both properties [Reference Gaspar10, Reference Troelstra and van Dalen21, Reference van den Berg23] are essential to fully characterize translations that embed classical logic into intuitionistic logic. The soundness property ensures that judgments are translated from classical logic to intuitionistic logic. The characterization property ensures that the meaning of formulas is preserved by the translation—this is captured by checking that
$A$
and
$A^{\star }$
are equivalent in classical logic. The characterization property is sometimes replaced [Reference Ferreira, Oliva, Berger, Diener, Schuster and Seisenberger7, Reference Troelstra and van Dalen21] by:
-
(iii) if $\Gamma ^{\star } \vdash _i A^{\star }$
then
$\Gamma \vdash _c A$
(reverse translation).
The reverse translation property ensures that if a translated judgment is provable in intuitionistic logic, then the original judgment is provable in classical logic. It follows from the characterization property.
Brown and Rizkallah [Reference Brown and Rizkallah3] recently investigated double-negation translations for higher-order logic. They showed that Kolmogorov’s translation and the Gödel–Gentzen translation cannot be directly extended to higher-order logic, as they do not preserve
$\beta $
-conversion. They proved that Kuroda’s translation can be extended to higher-order logic so that it satisfies the soundness property, but they did not examine the characterization and reverse translation properties. Moreover, they looked into different forms of extensionality, and showed that the soundness property fails in the presence of functional extensionality.
In this article, we investigate further the extension of Kuroda’s translation to higher-order logic. Our contribution is twofold.
First, we prove that the soundness property holds in the presence of functional extensionality, assuming a weak form of functional extensionality. We discuss alternative conditions, including the double-negation shift.
Second, we show that the characterization property and the reverse translation property—which are straightforward in first-order logic—do not necessarily hold in higher-order logic. We identify a necessary and sufficient condition for the characterization property. We prove that both properties hold under functional extensionality and propositional extensionality.
The basics of higher-order logic are recalled in Section 2. We extend Kuroda’s translation to higher-order logic in Section 3. We investigate the soundness property in Section 4, the characterization property in Section 5, and the reverse translation property in Section 6.
2 Higher-order logic
In higher-order logic, functions, predicates, and propositions are all terms of Church’s simple type theory [Reference Church4]. Types are defined inductively:
$\iota $
is the type of individuals,
$o$
is the type of propositions, and if
$\tau $
and
$\sigma $
are types then
$\tau \rightarrow \sigma $
is a type. For every type
$\tau $
, let
$\mathcal {V}_{\tau }$
be the set of variables of type
$\tau $
and
$\mathcal {C}_{\tau }$
be a set of constants of type
$\tau $
. The set of variables
$\mathcal {V} \mathrel {\mathop :}= \bigcup _{\tau } \mathcal {V}_{\tau }$
and the set of constants
$\mathcal {C} \mathrel {\mathop :}= \bigcup _{\tau } \mathcal {C}_{\tau }$
are assumed to be disjoint. For any set of constants
$\mathcal {C}$
, the sets
$\Lambda ^{\mathcal {C}}_{\tau }$
of terms of type
$\tau $
are defined by induction:
-
• For every $x \in \mathcal {V}_{\tau }$
,
$x \in \Lambda ^{\mathcal {C}}_{\tau }$
. -
• For every $c \in \mathcal {C}_{\tau }$
,
$c \in \Lambda ^{\mathcal {C}}_{\tau }$
. -
• For every $x \in \mathcal {V}_{\tau }$
and
$t \in \Lambda ^{\mathcal {C}}_{\sigma }$
, then
$(\lambda x. t) \in \Lambda ^{\mathcal {C}}_{\tau \rightarrow \sigma }$
. -
• For every $t \in \Lambda ^{\mathcal {C}}_{\tau \rightarrow \sigma }$
and
$u \in \Lambda ^{\mathcal {C}}_{\tau }$
, then
$(t u) \in \Lambda ^{\mathcal {C}}_{\sigma }$
.
$\lambda x. t$
is a
$\lambda $
-abstraction and
$t u$
is an application. Computation is introduced in this
$\lambda $
-calculus, thanks to the
$\beta $
-reduction rule
$(\lambda x. t) u \hookrightarrow t[x \leftarrow u]$
, where
$t[x \leftarrow u]$
corresponds to the term
$t$
in which
$x$
has been substituted by
$u$
. We denote
$\equiv _{\beta }$
the congruence generated by
$\beta $
-reduction.
Formulas are terms of type
$o$
. There are particular constants defining the logical connectives and quantifiers: tautology
$\top $
and contradiction
$\bot $
of type
$o$
, negation
$\neg $
of type
$o \rightarrow o$
, implication
$\mathbin {\Rightarrow }$
, conjunction
$\mathbin {\wedge }$
and disjunction
$\mathbin {\vee }$
of type
$o \rightarrow o \rightarrow o$
, and quantifiers
${\forall }_{\tau }$
and
${\exists }_{\tau }$
of type
$(\tau \rightarrow o) \rightarrow o$
. For convenience, terms of the form
${\forall }_{\tau } (\lambda x. A)$
and
${\exists }_{\tau } (\lambda x. A)$
are simply abbreviated as
${\forall } x. A$
and
${\exists } x. A$
. The logical biconditional
$\Leftrightarrow $
is defined by
$A \Leftrightarrow B \mathrel {\mathop :}= (A \mathbin {\Rightarrow } B) \mathbin {\wedge } (B \mathbin {\Rightarrow } A)$
. For every type
$\tau $
, we define an equality symbol
$=_{\tau }$
of type
$\tau \rightarrow \tau \rightarrow o$
. The equality symbols are infix, and we write
$t = u$
when there is no ambiguity on the type
$\tau $
.
A context
$\Gamma $
is a finite sequence of formulas. We write
${\textit {FV}}(t_1, \ldots , t_n)$
for the set of free variables that occur in the terms
$t_1, \ldots , t_n$
. The natural deduction rules for classical logic are given in Figure 1. The principle of excluded middle is equivalent to the double-negation elimination
$\neg \neg A \mathbin {\Rightarrow } A$
. The double-negation equivalence
${\neg \neg A \Leftrightarrow A}$
holds in classical logic. The natural deduction rules for intuitionistic logic are those of classical logic, except the principle of excluded middle PEM. The standard weakening inference rule is admissible in classical logic and in intuitionistic logic. The natural deduction rules for equality are given in Figure 2.
We write
$\Gamma \vdash _i A$
when
$\Gamma \vdash A$
is derivable in intuitionistic logic, and
$\Gamma \vdash _c A$
when it is derivable in classical logic. For any
$k \in \{ c, i \}$
, we write
$\Gamma \vdash _k^* A$
with
$* \in \{ \mathfrak {e}, \mathfrak {e}\mathfrak {p}, \mathfrak {e}\mathfrak {f}, \mathfrak {e}\mathfrak {f}\mathfrak {p} \}$
when
$\Gamma \vdash _k A$
is derivable with possibly additional inference rules: with Eq-I and Eq-E if
$\mathfrak {e}$
is in
$*$
, with PropExt if
$\mathfrak {p}$
is in
$*$
, and with FunExt if
$\mathfrak {f}$
is in
$*$
.
Natural deduction rules for higher-order logic.
Natural deduction rules for equality.
Let us recall some well-known results about intuitionistic logic.
Proposition 2.1. Let
$A$
and
$B$
be formulas, and
$P$
be a predicate.
-
1. $\vdash _i \neg \neg \bot \mathbin {\Rightarrow } \bot $
-
2. $\vdash _i \neg \neg \top \mathbin {\Rightarrow } \top $
-
3. $\vdash _i \neg \neg (A \mathbin {\vee } \neg A)$
-
4. $\vdash _i A \mathbin {\Rightarrow } \neg \neg A$
-
5. $\vdash _i \neg \neg \neg A \Leftrightarrow \neg A$
-
6. $\vdash _i \neg \neg (A \mathbin {\Rightarrow } B) \Leftrightarrow (\neg \neg A \mathbin {\Rightarrow } \neg \neg B)$
-
7. $\vdash _i \neg \neg (A \mathbin {\wedge } B) \Leftrightarrow (\neg \neg A \mathbin {\wedge } \neg \neg B)$
-
8. $\vdash _i \neg (A \mathbin {\vee } B) \Leftrightarrow (\neg A \mathbin {\wedge } \neg B)$
-
9. $\vdash _i \neg \neg {\forall } P \mathbin {\Rightarrow } {\forall } x. \neg \neg (P x)$
-
10. $\vdash _i \neg {\exists } P \Leftrightarrow {\forall } x. \neg (P x)$
Proof. These results are well-known, see, for example, [Reference Troelstra and van Dalen21, Chapter 2].
3 Kuroda’s translation for higher-order logic
Kuroda’s translation for first-order logic [Reference Kuroda16] inserts a double negation in front of formulas and a double negation after every universal quantifier. More formally, we first define
$A_{Ku}$
by induction on
$A$
:
and then we set
$A^{Ku} \mathrel {\mathop :}= \neg \neg A_{Ku}$
. We extend Kuroda’s translation to the terms of higher-order logic.
Definition 3.1 (Kuroda’s translation for higher-order logic)
Let
$A$
be a formula in higher-order logic. Its Kuroda’s translation is
$A^{Ku} \mathrel {\mathop :}= \neg \neg A_{Ku}$
, where
$A_{Ku}$
is inductively defined by:
While in first-order logic we have
$(A[z \leftarrow w])^{Ku} = A^{Ku}[z \leftarrow w]$
, this result cannot hold anymore in higher-order logic, since
$w$
is modified when it contains universal quantifiers
${\forall }$
. Instead, we have
$(A[z \leftarrow w])^{Ku} = A^{Ku}[z \leftarrow w_{Ku}]$
.
Proposition 3.2. For any term
$t$
, we have
$(t[z \leftarrow w])_{Ku} = t_{Ku}[z \leftarrow w_{Ku}]$
.
Proof. By induction on the term
$t$
.
Corollary 3.3. For any higher-order formula
$A$
, we have
$(A[z \leftarrow w])^{Ku} = A^{Ku}[z \leftarrow w_{Ku}]$
.
Higher-order logic is defined using simple type theory, so
$\beta $
-conversions may be used in the derivations. As Kuroda’s proof relies on the fact that we can translate each step of the derivation, each time we have
$A \equiv _{\beta } B$
in the classical derivation, we want to use
$A^{Ku} \equiv _{\beta } B^{Ku}$
in the intuitionistic derivation.
Proposition 3.4. For any terms
$t$
and
$u$
, if
$t \equiv _{\beta } u$
then
$t_{Ku} \equiv _{\beta } u_{Ku}$
.
Proof. We have
$((\lambda x. t) u)_{Ku} = (\lambda x. t_{Ku}) u_{Ku} \hookrightarrow t_{Ku}[x \leftarrow u_{Ku}]$
, so that
$((\lambda x. t) u)_{Ku} \equiv _{\beta } (t[x \leftarrow u])_{Ku}$
using Proposition 3.2. Closure by context, reflexivity, symmetry, and transitivity are immediate.
Corollary 3.5. For any higher-order formulas
$A$
and
$B$
, if
$A \equiv _{\beta } B$
then
${A_{Ku} \equiv _{\beta } B_{Ku}}$
and
$A^{Ku} \equiv _{\beta } B^{Ku}$
.
4 Soundness property
In this section, we prove the soundness property, with and without the extensionality principles. In particular, we identify different conditions that are sufficient to derive the soundness property in the presence of functional extensionality.
It is noteworthy that we state and prove the soundness property with
$\Gamma _{Ku}$
instead of
$\Gamma ^{Ku}$
, thus introducing fewer double negations in the context. All the results can be simply adapted to have the version with
$\Gamma ^{Ku}$
.
4.1 Without extensionality
To prove that
$\Gamma \vdash _c A$
implies
$\Gamma _{Ku} \vdash _i A^{Ku}$
, we do not follow the proof of Brown and Rizkallah [Reference Brown and Rizkallah3], which proceeds in two steps—transforming
$A$
into a formula
$A'$
that does not contain any universal quantifier and then applying to
$A'$
an extension of Glivenko’s theorem to higher-order logic without universal quantifiers. We proceed to a more direct proof that follows the intuition of the first-order case.
Theorem 4.1. Let
$A$
be a formula and
$\Gamma $
be a context in higher-order logic. If
$\Gamma \vdash _c A$
then
$\Gamma _{Ku} \vdash _i A^{Ku}$
.
Proof. By induction on the derivation:
-
• All-I : By induction, we have $\Gamma _{Ku} \vdash _i\neg \neg (P_{Ku} x)$
. Using All-I, we derive
$\Gamma _{Ku} \vdash _i{\forall } x. \neg \neg (P_{Ku} x)$
. We conclude using Proposition 2.1(4). -
• All-E : By induction, we have $\Gamma _{Ku} \vdash _i\neg \neg {\forall } x. \neg \neg (P_{Ku} x)$
. It follows from Proposition 2.1(9) that
$\Gamma _{Ku} \vdash _i{\forall } x. \neg \neg \neg \neg (P_{Ku} x)$
. Using All-E, we obtain
$\Gamma _{Ku} \vdash _i\neg \neg \neg \neg (P_{Ku} t_{Ku})$
. We conclude using Proposition 2.1(5). -
• Ex-I : By induction, we have $\Gamma _{Ku} \vdash _i\neg \neg (P_{Ku} t_{Ku})$
. We write
$\Delta $
for the context
$\Gamma _{Ku}, {\forall } x. \neg (P_{Ku} x)$
. -
• Ex-E : We get $\Gamma _{Ku} \vdash _i\neg \neg {\exists } P_{Ku}$
and
$\Gamma _{Ku}, P_{Ku} x \vdash _i\neg \neg A_{Ku}$
by induction. We want to prove
$\Gamma _{Ku} \vdash _i\neg \neg A_{Ku}$
. We use Not-I and then Not-E with
$\neg {\forall } x. \neg (P_{Ku} x)$
. The proof of the first subgoal, where the context
$\Delta $
denotes
$\Gamma _{Ku}, \neg A_{Ku}$
, is:The second subgoal $\Gamma _{Ku}, \neg A_{Ku} \vdash _i\neg {\forall } x. \neg (P_{Ku} x)$
derives from the first induction hypothesis, using Proposition 2.1(10) and weakening. -
• Or-IL : By induction, we have $\Gamma _{Ku} \vdash _i\neg \neg A_{Ku}$
. We want to prove that
$\Gamma _{Ku} \vdash _i\neg \neg (A_{Ku} \mathbin {\vee } B_{Ku})$
. We apply Not-I and then Not-E with
$\neg A_{Ku}$
. The first subgoal
$\Gamma _{Ku}, \neg (A_{Ku} \mathbin {\vee } B_{Ku}) \vdash _i\neg \neg A_{Ku}$
is proved by weakening the induction hypothesis. The second subgoal is: We proceed similarly for Or-IR .
-
• Or-E : We have $\Gamma _{Ku} \vdash _i\neg \neg (A_{Ku} \mathbin {\vee } B_{Ku})$
, and
$\Gamma _{Ku}, A_{Ku} \vdash _i\neg \neg C_{Ku}$
, and
$\Gamma _{Ku}, B_{Ku} \vdash _i\neg \neg C_{Ku}$
by induction. We want to prove
$\Gamma _{Ku} \vdash _i\neg \neg C_{Ku}$
. We use Not-I and Not-E with
$\neg A_{Ku} \mathbin {\wedge } \neg B_{Ku}$
.For the first subgoal, we have to prove $\Gamma _{Ku}, \neg C_{Ku} \vdash _i\neg (\neg A_{Ku} \mathbin {\wedge } \neg B_{Ku})$
. Using Proposition 2.1(8), we have to show
$\Gamma _{Ku}, \neg C_{Ku} \vdash _i\neg \neg (A_{Ku} \mathbin {\vee } B_{Ku})$
. We prove it by weakening the first induction hypothesis.For the second subgoal, we have to prove $\Gamma _{Ku}, \neg C_{Ku} \vdash _i\neg A_{Ku} \mathbin {\wedge } \neg B_{Ku}$
. We prove both
$\Gamma _{Ku}, \neg C_{Ku} \vdash _i\neg A_{Ku}$
and
$\Gamma _{Ku}, \neg C_{Ku} \vdash _i\neg B_{Ku}$
. Let us show
$\Gamma _{Ku}, \neg C_{Ku} \vdash _i\neg A_{Ku}$
. We use Not-I and Not-E with
$\neg C_{Ku}$
. We derive
$\Gamma _{Ku}, \neg C_{Ku}, A_{Ku} \vdash _i\neg \neg C_{Ku}$
by weakening the third induction hypothesis and
$\Gamma _{Ku}, \neg C_{Ku}, A_{Ku} \vdash _i\neg C_{Ku}$
by Ax. We show
$\Gamma _{Ku}, \neg C_{Ku} \vdash _i\neg B_{Ku}$
similarly. -
• Conv derives from the induction hypothesis and Corollary 3.5.
-
• The remaining items are direct applications of Proposition 2.1.
4.2 With extensionality
We now investigate the soundness property in the setting of extensionality. We want to prove that
$\Gamma \vdash _c^* A$
implies
$\Gamma _{Ku} \vdash _i^* A^{Ku}$
whatever
$* \in \{ \mathfrak {e}, \mathfrak {e}\mathfrak {p}, \mathfrak {e}\mathfrak {f}, \mathfrak {e}\mathfrak {f}\mathfrak {p} \}$
. Brown and Rizkallah showed that it fails in the presence of functional extensionality. To get around this problem, it is sufficient to assume
${\forall } f {\forall } g. ({\forall } x. \neg \neg (f x = g x)) \mathbin {\Rightarrow } \neg \neg (f= g)$
, written
$\Delta ^{\mathfrak {f}}$
.
Theorem 4.2. Let
$A$
be a formula and
$\Gamma $
be a context in higher-order logic.
-
1. For $* \in \{ \mathfrak {e}, \mathfrak {e}\mathfrak {p} \}$
, if
$\Gamma \vdash _c^* A$
then
$\Gamma _{Ku} \vdash _i^* A^{Ku}$
. -
2. For $* \in \{ \mathfrak {e}\mathfrak {f}, \mathfrak {e}\mathfrak {f}\mathfrak {p} \}$
, if
$\Gamma \vdash _c^* A$
then
$\Delta ^{\mathfrak {f}}, \Gamma _{Ku} \vdash _i^* A^{Ku}$
.
Proof. For the first item, we complete the proof of Theorem 4.1:
-
• Eq-I derives from Eq-I and Proposition 2.1(4).
-
• Eq-E : We have $\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} \neg \neg (P_{Ku} u_{Ku})$
and
$\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} \neg \neg (u_{Ku} = v_{Ku})$
by induction. We directly have
$\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} P_{Ku} u_{Ku} \mathbin {\Rightarrow } (u_{Ku} = v_{Ku}) \mathbin {\Rightarrow } P_{Ku} v_{Ku}$
by Eq-E. We get
$\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} \neg \neg (P_{Ku} u_{Ku}) \mathbin {\Rightarrow } \neg \neg (u_{Ku} = v_{Ku}) \mathbin {\Rightarrow } \neg \neg (P_{Ku} v_{Ku})$
using Proposition 2.1(4) and Proposition 2.1(6). Therefore, we conclude
$\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} \neg \neg (P_{Ku} v_{Ku})$
. -
• PropExt : By induction, we have $\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} \neg \neg (A_{Ku} \Leftrightarrow B_{Ku})$
. Using PropExt, we directly have
$\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} (A_{Ku} \Leftrightarrow B_{Ku}) \mathbin {\Rightarrow } (A_{Ku} = B_{Ku})$
. We get
$\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} \neg \neg (A_{Ku} \Leftrightarrow B_{Ku}) \mathbin {\Rightarrow } \neg \neg (A_{Ku} = B_{Ku})$
by Proposition 2.1(4) and Proposition 2.1(6). We conclude
$\Gamma _{Ku} \vdash _i^{\mathfrak {e}\mathfrak {p}} \neg \neg (A_{Ku} = B_{Ku})$
.
For the second item, we adapt the three cases of the first item and we prove the additional
FunExt
case. We use the assumption
$\Delta ^{\mathfrak {f}}$
on the induction hypothesis
$\Delta ^{\mathfrak {f}}, \Gamma _{Ku} \vdash _i \neg \neg (f_{Ku} x = g_{Ku} x)$
to get
$\Delta ^{\mathfrak {f}}, \Gamma _{Ku} \vdash _i \neg \neg (f_{Ku} = g_{Ku})$
.
The formula
$\Delta ^{\mathfrak {f}}$
corresponds to a weak form of functional extensionality, where double negations have been inserted in front of equality predicates. In classical logic, it is equivalent to functional extensionality. We link
$\Delta ^{\mathfrak {f}}$
to the well-known double-negation shift
$({\forall } x. \neg \neg A) \mathbin {\Rightarrow } (\neg \neg {\forall } x. A)$
, written
. Such a principle implies
$\Delta ^{\mathfrak {f}}$
in intuitionistic logic with functional extensionality.
Proposition 4.3.
.
Proof. We have
using FunExt. We successively apply Propositions 2.1(4), 2.1(9), and 2.1(6) to derive
. Using
, we conclude
.
The double-negation shift is derivable in classical logic but not in intuitionistic logic. It is deeply connected to Glivenko’s theorem, which is generalized by Kuroda’s translation. More precisely, such a principle is required to extend Glivenko’s theorem to first-order logic [Reference Gabbay8, Reference Umezawa22] and to substructural first-order logic [Reference Farahani and Ono6]. Moreover, the modal counterpart of the double-negation shift
$\square \neg \neg A \mathbin {\Rightarrow } \neg \neg \square A$
plays an important role when studying Glivenko’s theorem for modal logic [Reference Litak, Polzer, Rabenstein and Miller17]. Here, we have emphasized a new connection between the double-negation shift and Kuroda’s translation.
To prove the soundness property in the presence of functional extensionality, it is therefore sufficient to assume the weak form of functional extensionality or the double-negation shift.
We could also assume the double-negation elimination on equality predicates
${\forall } x {\forall } y. \neg \neg (x = y) \mathbin {\Rightarrow } x = y$
, written
. Indeed, it implies
$\Delta ^{\mathfrak {f}}$
in intuitionistic logic with functional extensionality. However, such a principle must be handled with care: when combined with the comprehension axiom of set theory or with propositional extensionality, it entails the double-negation elimination. For instance, let us prove
for any proposition
$P$
. We easily derive
$\vdash _i^{\mathfrak {e}\mathfrak {p}} \neg \neg P \mathbin {\Rightarrow } \neg \neg (P = \top )$
and
$\vdash _i^{\mathfrak {e}} (P = \top ) \mathbin {\Rightarrow } P$
. The double-negation elimination then follows from
applied to
$P$
and
$\top $
.
Another approach to get around the problem of the soundness property in the presence of functional extensionality is to apply a translation that eliminates extensionality [Reference Brown, Rizkallah, Blanchette and Urban2, Reference Gandy9, Reference Takeuti20]. To do so, the Takeuti–Gandy translation [Reference Gandy9, Reference Takeuti20] resorts to relativization and quantifies over extensional elements. This translation was later refined [Reference Brown, Rizkallah, Blanchette and Urban2] and coupled with a double-negation translation. The main advantage of our approach is that the translated statement remains close to the original statement, as no predicates have been inserted to account for the elimination of functional extensionality. In exchange, however, we assume an additional axiom.
5 Characterization property
We have shown that, if the formula
$A$
is provable from
$\Gamma $
, then there exists an intuitionistic proof of
$A^{Ku}$
from
$\Gamma _{Ku}$
. We now want to prove the characterization property:
$A$
and
$A^{Ku}$
are classically equivalent. Such a result is routine in first-order logic, but does not generally hold in higher-order logic.
5.1 Counter-example
Before developing a counter-example of the characterization property, let us illustrate the intensional nature of higher-order logic. Consider a constant
$P$
of type
$o \rightarrow o$
. Even though the propositions
$\top $
and
$\top \mathbin {\wedge } \top $
are equivalent, we cannot prove that
$P \top $
and
$P (\top \mathbin {\wedge } \top )$
are equivalent without further assumptions. This can be shown using the intensional models of higher-order logic developed by Takahashi [Reference Takahashi19] and Prawitz [Reference Prawitz18], based on the V-complex construction [Reference Andrews1]. In such models, the semantic value of a proposition is not its truth value, but a pair consisting of its truth value and a syntactic value. The propositions
$\top $
and
$\top \mathbin {\wedge } \top $
have the same truth value but different syntactic values, and therefore they have different semantic values. The truth value of
$P (\top \mathbin {\wedge } \top )$
(respectively
$P \top $
) depends on the whole semantic value of
$\top \mathbin {\wedge } \top $
(respectively
$\top $
). It follows that
$P \top $
and
$P (\top \mathbin {\wedge } \top )$
can be assigned different truth values. Thus, in the absence of extensionality, we cannot prove that
$P \top $
and
$P (\top \mathbin {\wedge } \top )$
are equivalent, even though
$\top $
and
$\top \mathbin {\wedge } \top $
are.
Consider a constant
$P$
of type
$o \rightarrow o$
and a proposition
$B$
that contains at least one occurrence of the quantifier
${\forall }$
. We take
$A \mathrel {\mathop :}= P B$
. We would like to show
${\vdash _c A^{Ku} \Leftrightarrow A}$
, that is
$\vdash _c \neg \neg (P B_{Ku}) \Leftrightarrow P B$
. As we are in classical logic, it is equivalent to derive
$\vdash _c P B_{Ku} \Leftrightarrow P B$
. Using the intensional models of higher-order logic, this does not hold, even when
$B_{Ku}$
and
$B$
are equivalent. More intuitively, the problem is that the translation inserts double negations inside the argument
$B$
of the predicate
$P$
, but we cannot replace
$B_{Ku}$
by
$B$
in the absence of extensionality. This constitutes a counter-example of the characterization property in higher-order logic.
5.2 Necessary and sufficient condition
When trying to adapt the proof of the characterization property from first-order logic to higher-order logic, we identify a necessary and sufficient condition, called Kuroda equivalence.
Definition 5.1 (Kuroda equivalence)
For any constant or variable
$t$
of type
$\tau _1 \rightarrow \ldots \rightarrow \tau _n \rightarrow o$
and any terms
$u_1, \ldots , u_n$
of type
$\tau _1, \ldots , \tau _n$
, we have
$\vdash _c (t u_1 \ldots u_n)_{Ku} \Leftrightarrow t u_1 \ldots u_n$
.
Theorem 5.2. The characterization property holds if and only if the Kuroda equivalence holds.
Proof. For the direct implication, we apply the characterization property to the formula
$t u_1 \ldots u_n$
to get
$\vdash _c (t u_1 \ldots u_n)^{Ku} \Leftrightarrow t u_1 \ldots u_n$
, so we derive
$\vdash _c (t u_1 \ldots u_n)_{Ku} \Leftrightarrow t u_1 \ldots u_n$
.
For the reverse implication, we only have to show
$\vdash _c A_{Ku} \Leftrightarrow A$
as we are in classical logic. Let
$A_{\beta }$
be the
$\beta $
-normal form of
$A$
. We know that
$A_{\beta } \equiv _{\beta } A$
, so we derive
$(A_{\beta })_{Ku} \equiv _{\beta } A_{Ku}$
by Corollary 3.5. We do a proof by cases on
$A_{\beta }$
. If
$A_{\beta }$
is a variable or a constant,
$(A_{\beta })_{Ku}$
corresponds to
$A_{\beta }$
, therefore we directly have
$\vdash _c (A_{\beta })_{Ku} \Leftrightarrow A_{\beta }$
and we conclude
$\vdash _c A_{Ku} \Leftrightarrow A$
. Otherwise,
$A_{\beta }$
is an application
$t u_1 \ldots u_n$
, where
$t$
is a variable or a constant of type
$\tau _1 \rightarrow \ldots \rightarrow \tau _n \rightarrow o$
and
$u_1, \ldots , u_n$
are terms of type
$\tau _1, \ldots , \tau _n$
. By the Kuroda equivalence, we have
$\vdash _c (A_{\beta })_{Ku} \Leftrightarrow A_{\beta }$
, hence we conclude
$\vdash _c A_{Ku} \Leftrightarrow A$
.
The counter-example 5.1 precisely shows that the Kuroda equivalence does not necessarily hold. To have the characterization property, we could impose the Kuroda equivalence as a principle. However, such a condition is difficult to enforce, as it not only applies to the logical connectives and quantifiers, but also to any variable or constant representing a predicate.
5.3 Extensionality conditions
We now investigate the characterization property in the setting of extensionality. When assuming functional extensionality and propositional extensionality, the formulas
$A$
and
$A^{Ku}$
are equal, and therefore classically equivalent.
Lemma 5.3. For any term
$t$
, we have
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} t_{Ku} = t$
.
Proof. We proceed by induction on the term
$t$
:
-
• Variables and constants: Using Eq-I, we directly derive $\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} x_{Ku} = x$
and
${\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} c_{Ku} = c}$
for
$c \neq {\forall }$
. We prove
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} {\forall }_{Ku} = {\forall }$
with as we have $\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} q y \Leftrightarrow \neg \neg (q y)$
in classical logic. -
• Applications: We have $\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} t_{Ku} u_{Ku} = t_{Ku} u_{Ku}$
using Eq-I. Successively using Eq-E with the induction hypotheses
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} t_{Ku} = t$
and
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} u_{Ku} = u$
, we obtain
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} t_{Ku} u_{Ku} = t u$
. -
• Abstractions: By induction hypothesis, we have $t_{Ku} = t$
. Using FunExt and Conv, we derive
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} (\lambda x. t)_{Ku} = \lambda x. t$
.
Theorem 5.4. For any higher-order formula
$A$
, we have
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A^{Ku} \Leftrightarrow A$
.
Proof. By Lemma 5.3,
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A_{Ku} = A$
. Using Eq-E on the tautology
$A \Leftrightarrow A$
, we get
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A_{Ku} \Leftrightarrow A$
. We conclude
$\vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A^{Ku} \Leftrightarrow A$
as we are in classical logic.
It is noteworthy that Lemma 5.3 implies the Kuroda equivalence, thereby providing an alternative proof of Theorem 5.4.
6 Reverse translation property
We have seen that the characterization property does not generally hold in higher-order logic. In this section, we show that the reverse translation property—a weaker property—does not hold either.
As in Section 4, we state the reverse translation property with
$\Gamma _{Ku}$
instead of
$\Gamma ^{Ku}$
. Again, all the results can be simply adapted to have the version with
$\Gamma ^{Ku}$
.
6.1 Counter-example
To prove that the reverse translation property does not hold in higher-order logic, we exhibit some
$\Gamma $
and
$A$
such that
$\Gamma _{Ku} \vdash _i A^{Ku}$
holds and
$\Gamma \vdash _c A$
does not. Consider a constant R of type
$o \rightarrow o \rightarrow o$
and two constants
$P$
and
$P'$
of type
$\tau \rightarrow o$
. We take
and we therefore have
In intuitionistic logic, we derive
$\Gamma _{Ku} \vdash _i A^{Ku}$
using All-E with
$q \mathrel {\mathop :}= {\forall }$
.
In classical logic, however, we cannot derive
$\Gamma \vdash _c A$
. Indeed, we cannot apply All-E with
${\forall }$
anymore: the extra double negations inside the arguments of
$R$
cannot be removed without further assumptions. We cannot apply All-E with
$\lambda y. {\forall } (\lambda x. P x)$
either, as we would obtain
$R ({\forall } (\lambda x. P x)) ({\forall } (\lambda x. P x))$
instead of
$R ({\forall } (\lambda x. P x)) ({\forall } (\lambda x. P' x))$
. As in the case of the characterization property, it is the absence of extensionality that allows us to build a counter-example.
6.2 Sufficient conditions
Since the characterization property implies the reverse translation property, the sufficient conditions investigated in Section 5 apply. The reverse translation property holds under the Kuroda equivalence.
Theorem 6.1. If the Kuroda equivalence holds, then the reverse translation property holds.
Proof. Suppose
$\Gamma _{Ku} \vdash _i A^{Ku}$
. We directly have
$\Gamma _{Ku} \vdash _c A^{Ku}$
, and we get
$\Gamma ^{Ku} \vdash _c A^{Ku}$
using the double-negation elimination. We use the characterization property that holds under Kuroda equivalence by Theorem 5.2.
The reverse translation property also holds under functional extensionality and propositional extensionality.
Theorem 6.2. Let
$A$
be a formula and
$\Gamma $
be a context in higher-order logic.
-
1. If $\Gamma _{Ku} \vdash _i A^{Ku}$
then
$\Gamma \vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A$
. -
2. For $* \in \{ \mathfrak {e}, \mathfrak {e}\mathfrak {p} \}$
, if
$\Gamma _{Ku} \vdash _i^* A^{Ku}$
then
$\Gamma \vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A$
. -
3. For $* \in \{ \mathfrak {e}\mathfrak {f}, \mathfrak {e}\mathfrak {f}\mathfrak {p} \}$
, if
$\Delta ^{\mathfrak {f}}, \Gamma _{Ku} \vdash _i^* A^{Ku}$
then
$\Gamma \vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A$
.
Proof. For the first and second item, we directly have
$\Gamma _{Ku} \vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A^{Ku}$
. We get
$\Gamma ^{Ku} \vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A^{Ku}$
using the double-negation elimination, and then we derive
$\Gamma \vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A$
using Theorem 5.4. For the third item, we similarly get
$\Delta ^{\mathfrak {f}}, \Gamma \vdash _c^{\mathfrak {e}\mathfrak {f}\mathfrak {p}} A$
, and we conclude using the fact that
$\Delta ^{\mathfrak {f}}$
is derivable from functional extensionality in classical logic.
7 Conclusion
Brown and Rizkallah [Reference Brown and Rizkallah3] extended Kuroda’s translation to higher-order logic, showing that the soundness property holds, except in the presence of functional extensionality. We have discussed several conditions under which the soundness property holds in the presence of functional extensionality, including the double-negation shift.
Brown and Rizkallah neither examined the characterization property nor the reverse translation property. We have shown that both properties do not hold in higher-order logic, although they are straightforward in first-order logic. We have identified conditions under which such properties hold. In particular, it is sufficient to assume functional extensionality and propositional extensionality.
We have seen that the role of both functional extensionality and propositional extensionality is predominant when extending Kuroda’s translation to higher-order logic. One has to be careful when using both principles in an intuitionistic context: the Diaconescu–Goodman–Myhill theorem [Reference Diaconescu5, Reference Goodman and Myhill14] states that, together with the axiom of choice, they entail the principle of excluded middle.
Acknowledgments
The author would like to thank Marc Aiguier, Gilles Dowek, Olivier Hermant, and the anonymous reviewer for their helpful remarks about this work, and Dominik Kirst for pointing out that the double-negation elimination on equality predicates may entail the double-negation elimination.
Open access
