# Kuroda's Translation for the $\lambda\Pi$-Calculus Modulo Theory and Dedukti

Thomas Traversié

Université Paris-Saclay, CentraleSupélec, MICS
Gif-sur-Yvette, France

Université Paris-Saclay, Inria, CNRS, ENS-Paris-Saclay, LMF
Gif-sur-Yvette, France

thomas.traversie@centralesupelec.fr

Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translation to higher-order logic. In this paper, we adapt it for theories encoded in higher-order logic in the $\lambda\Pi$-calculus modulo theory, a logical framework that extends $\lambda$-calculus with dependent types and user-defined rewrite rules. We develop a tool that implements Kuroda's translation for proofs written in DEDUKTI, a proof language based on the $\lambda\Pi$-calculus modulo theory.

## 1 Introduction

The $\lambda\Pi$-calculus modulo theory [6] is an extension of simply typed $\lambda$-calculus with dependent types and user-defined rewrite rules. It is a logical framework, meaning that one can express many theories in it— through the definitions of typed constants and rewrite rules. For instance, it is possible to encode Predicative Logic, Simple Type Theory and the Calculus of Constructions in the $\lambda\Pi$-calculus modulo theory [2]. In particular, theories from other proof systems can be expressed inside this logical framework [20]. The $\lambda\Pi$-calculus modulo theory has been implemented in the concrete language DEDUKTI [1, 15]. Besides automatic proof checking, DEDUKTI can be used as a common language to exchange proofs between different systems. However, if one wants to translate proofs from the classical proof assistant HOL LIGHT to the intuitionistic proof assistant COQ via DEDUKTI, one must transform classical proofs into intuitionistic proofs inside DEDUKTI.

Classical logic corresponds to intuitionistic logic extended with the principle of excluded middle $A \lor \neg A$, or equivalently the double-negation elimination $\neg\neg A \Rightarrow A$. Classical logic can be embedded into intuitionistic logic, using double-negations translations. Glivenko [12] proved that any propositional formula $A$ is provable in classical logic if and only if its double negation $\neg\neg A$ is provable in intuitionistic logic. Kolmogorov [17], Gödel [13], Gentzen [10] and Kuroda [18] developed double-negation translations $A \mapsto A^*$, which transforms any first-order formula $A$ such that:

(i) if $A$ is provable in classical logic then its translation $A^*$ is provable in intuitionistic logic,

(ii) $A$ and $A^*$ are classically equivalent.

More recently, Brown and Rizkallah [4] showed that Kolmogorov's and Gödel-Gentzen's translations cannot be extended to higher-order logic. They proved that, in higher-order logic, Kuroda's translation satisfies Property (i), but that it fails in the presence of functional extensionality. In fact [21], Property (i) holds in the presence of functional extensionality under some specific condition, and Property (ii) holds when assuming functional extensionality and propositional extensionality.
**Contribution.** In this paper, we express Kuroda's translation for theories of the λΠ-calculus modulo theory that are encoded in higher-order logic. It is both an encoding-into a logical framework that features proofs as terms—and an extension—to a logical framework that features dependent types and user-defined rewrite rules—of Kuroda's translation. We implement such translation inside CONSTRUKTI, a tool that translates DEDUKTI files. CONSTRUKTI is tested on a benchmark of a hundred formal proofs. This tool and this benchmark are available at https://github.com/Deducteam/Construkti.

**Outline of the paper.** In Section 2, we present the λΠ-calculus modulo theory and we detail an encoding of higher-order logic in it. In Section 3, we define Kuroda's translation for theories of λΠ-calculus modulo theory that are encoded in higher-order logic, and we prove the embedding of classical logic into intuitionistic logic. In Section 4, we implement CONSTRUKTI and test it on DEDUKTI proofs.

# 2 Higher-Order Logic in the λΠ-Calculus Modulo Theory

In this section, we present the λΠ-calculus modulo theory, and we detail an encoding of higher-order logic in this logical framework. We characterize the theories considered in the rest of this paper—theories encoded in higher-order logic.

## 2.1 The λΠ-Calculus Modulo Theory

The Edinburgh Logical Framework [14], also called λΠ-calculus, is an extension of simply typed λ-calculus with dependent types. The λΠ-calculus modulo theory [6] corresponds to the Edinburgh Logical Framework extended with user-defined rewrite rules [7]. Its syntax is given by:

<table><tr><td>Sorts</td><td>s ::= TYPE | KIND</td></tr><tr><td>Terms</td><td>t, u, A, B ::= c | x | s | Πx : A. B | λx : A. t | t u</td></tr><tr><td>Contexts</td><td>Γ ::= &lt;&gt; | Γ, x : A</td></tr><tr><td>Signatures</td><td>Σ ::= &lt;&gt; | Σ, c : A</td></tr><tr><td>Rewrite systems</td><td>&R ::= &lt;&gt; | &R, ℓ ↦→ r</td></tr></table>

where c is a constant and x is a variable (ranging over disjoint sets). TYPE and KIND are two sorts: terms of type TYPE are called types, and terms of type KIND are called kinds. Πx : A. B is a dependent product (simply written A → B if x does not occur in B), λx : A. t is an abstraction, and t u is an application. Contexts, signatures and rewrite systems are finite sequences, and are written $\langle \rangle$ when empty. Signatures Σ are composed of typed constants c : A, where A is a closed term (that is a term with no free variables). Rewrite systems $\mathcal{R}$ are composed of rewrite rules $\ell \leftrightarrow r$, where the head symbol of $\ell$ is a constant. The λΠ-calculus modulo theory is a logical framework, in which Σ and $\mathcal{R}$ are fixed by the users depending on the logic they are working in. The relation $\leftrightarrow_{\beta\mathcal{R}}$ is generated by β-reduction and by the rewrite rules of $\mathcal{R}$. The conversion $\equiv_{\beta\mathcal{R}}$ is the reflexive, symmetric, and transitive closure of $\leftrightarrow_{\beta\mathcal{R}}$.

The typing rules for the λΠ-calculus modulo theory are given in Figure 1. We write $\vdash \Gamma$ when the context $\Gamma$ is well formed, and $\Gamma \vdash t : A$ when the term $t$ is of type $A$ in the context $\Gamma$. For convenience, $\langle \rangle \vdash t : A$ is simply written $\vdash t : A$. The standard weakening rule is admissible.

We write $\Lambda(\Sigma)$ for the set of terms whose constants belong to $\Sigma$. We say that $(\Sigma, \mathcal{R})$ is a theory when: (i) for each rule $\ell \leftrightarrow r \in \mathcal{R}$, both $\ell$ and $r$ belongs to $\Lambda(\Sigma)$, (ii) $\leftrightarrow_{\beta\mathcal{R}}$ is confluent on $\Lambda(\Sigma)$, and (iii) each
<figure><img src="image_1.png" /><figcaption>Figure 1: Typing rules of the λΠ-calculus modulo theory.</figcaption></figure>

rule $\ell \mapsto r \in \mathcal{R}$ preserves types (for all context $\Gamma$, substitution $\theta$, and term $A \in \Lambda(\Sigma)$), if $\Gamma \vdash \ell\theta : A$ then $\Gamma \vdash r\theta : A$).

In the λΠ-calculus modulo theory, if $\Gamma \vdash t : A$ then $\Gamma$ is well-formed and $A$ is well-typed. To prove this, we use the two following properties.

**Lemma 1.** If $\Gamma \vdash t : A$, then either $A = \text{KIND}$ or $\Gamma \vdash A : s$ for $s = \text{TYPE}$ or $s = \text{KIND}$. If $\Gamma \vdash \Pi x : A. B : s$, then $\Gamma \vdash A : \text{TYPE}$.

## 2.2 An Encoding of Higher-Order Logic

It is possible to express higher-order logic in the λΠ-calculus modulo theory [2]. For this, we have to introduce the notions of proposition and proof. We declare the constant *Set*, which represents the universe of sorts, along with the injection *El* that maps sorts to the type of its elements. The constant *Prop* defines the universe of propositions, and the injection *Prf* maps propositions into the type of its proofs. In this encoding, we say that *P* of type *Prop* is a proposition, that *Prf P* is a formula and that a term of type *Prf P* is a proof of *P*.

Set : TYPE
El : Set → TYPE
≈ : Set → Set → Set
o : Set
Prop : TYPE
Prf : Prop → TYPE
El (x ≈ y) ↦ El x → El y
El o ↦ Prop

The arrow $\approx$ (written infix) is used to represent function types between terms of type *Set*. Propositions are considered as objects, using the sort *o* and the rewrite rule *El o* $\leftrightarrow$ *Prop*.

Now that we have introduced the notions of proposition and proof, we can define the logical connectives and quantifiers of predicate logic.

$\Rightarrow : \mathbf{Prop} \to \mathbf{Prop} \to \mathbf{Prop}$
$\top : \mathbf{Prop}$
$\forall : \Pi x : \mathbf{Set}. (El x \to \mathbf{Prop}) \to \mathbf{Prop}$
$\land : \mathbf{Prop} \to \mathbf{Prop} \to \mathbf{Prop}$
$\bot : \mathbf{Prop}$
$\exists : \Pi x : \mathbf{Set}. (El x \to \mathbf{Prop}) \to \mathbf{Prop}$
$\lor : \mathbf{Prop} \to \mathbf{Prop} \to \mathbf{Prop}$
$\neg : \mathbf{Prop} \to \mathbf{Prop}$
$\Leftrightarrow : \mathbf{Prop} \to \mathbf{Prop} \to \mathbf{Prop}$

Remark that $\forall$ and $\exists$ are polymorphic quantifiers that can be applied to the sort of proposition *o*. Hence the higher-order feature directly derives from the rewrite rule *El o* $\leftrightarrow$ *Prop*.
In natural deduction, each connective and quantifier comes with an introduction and an elimination inference rule. The encoding of the notions of proposition and proof is well-suited for representing inference rules: logical consequences are represented by arrow types, and parameters are represented by dependent types. For instance, the inference rule for the elimination of disjunction

$$ \frac{\Gamma \vdash P \lor Q \qquad \Gamma, P \vdash R \qquad \Gamma, Q \vdash R}{\Gamma \vdash R} $$

is simply expressed by the constant or<sub>e</sub> of type

$$ \Pi p, q : \text{Prop.} \Prf (p \lor q) \rightarrow \Pi r : \text{Prop.} \Prf (p \rightarrow \Prf r) \rightarrow (\Prf q \rightarrow \Prf r) \rightarrow \Prf r $$

that can be used for any context Γ. The constants representing the natural deduction rules for the logical connectives are:

$$ \text{imp}_i : \Pi p, q : \text{Prop.} \Prf (p \rightarrow \Prf q) \rightarrow \Prf (p \Rightarrow q) $$

$$ \text{imp}_e : \Pi p, q : \text{Prop.} \Prf (p \Rightarrow q) \rightarrow \Prf p \rightarrow \Prf q $$

$$ \text{and}_i : \Pi p : \text{Prop.} \Prf p \rightarrow \Pi q : \text{Prop.} \Prf q \rightarrow \Prf (p \land q) $$

$$ \text{and}_{e\ell} : \Pi p, q : \text{Prop.} \Prf (p \land q) \rightarrow \Prf p $$

$$ \text{and}_{er} : \Pi p, q : \text{Prop.} \Prf (p \land q) \rightarrow \Prf q $$

$$ \text{or}_{i\ell} : \Pi p : \text{Prop.} \Prf p \rightarrow \Pi q : \text{Prop.} \Prf (p \lor q) $$

$$ \text{or}_{ir} : \Pi p, q : \text{Prop.} \Prf q \rightarrow \Prf (p \lor q) $$

$$ \text{or}_e : \Pi p, q : \text{Prop.} \Prf (p \lor q) \rightarrow \Pi r : \text{Prop.} \Prf (p \rightarrow \Prf r) \rightarrow (\Prf q \rightarrow \Prf r) \rightarrow \Prf r $$

$$ \text{neg}_i : \Pi p : \text{Prop.} \Prf (p \rightarrow \Prf \perp) \rightarrow \Prf (\neg p) $$

$$ \text{neg}_e : \Pi p : \text{Prop.} \Prf (\neg p) \rightarrow \Prf p \rightarrow \Prf \perp $$

For convenience, the semantic of the logical biconditional is encoded through the rewrite rule $p \Leftrightarrow q \leftrightarrow (p \Rightarrow q) \land (q \Rightarrow p)$. The introduction of tautology and the elimination of contradiction are encoded by:

$$ \text{top}_i : \Prf \top $$

$$ \text{bot}_e : \Prf \bot \rightarrow \Pi p : \text{Prop.} \Prf p $$

The natural deduction rules for the quantifiers are represented by the following constants:

$$ \text{all}_i : \Pi a : \text{Set.} \Pi p : \text{El } a \rightarrow \text{Prop.} \ (\Pi x : \text{El } a. \ \text{Prf} (p x)) \rightarrow \text{Prf} (\forall a p) $$

$$ \text{all}_e : \Pi a : \text{Set.} \Pi p : \text{El } a \rightarrow \text{Prop.} \Prf (\forall a p) \rightarrow \Pi x : \text{El } a. \ \text{Prf} (p x) $$

$$ \text{ex}_i : \Pi a : \text{Set.} \Pi p : \text{El } a \rightarrow \text{Prop.} \Pi x : \text{El } a. \ \text{Prf} (p x) \rightarrow \Prf (\exists a p) $$

$$ \text{ex}_e : \Pi a : \text{Set.} \Pi p : \text{El } a \rightarrow \text{Prop.} \Prf (\exists a p) \rightarrow \Pi r : \text{Prop.} \ (\Pi x : \text{El } a. \ \text{Prf} (p x) \rightarrow \Prf r) \rightarrow \Prf r $$

All those constants and rewrite rules define the encoding of intuitionistic higher-order logic in the λΠ-calculus modulo theory. We write $\Sigma_{HOL}^i$ for its constants and $\mathcal{R}_{HOL}$ for its rewrite rules. The principle of excluded middle is represented by:

$$ \text{pem} : \Pi p : \text{Prop.} \Prf (p \lor \neg p) $$

Classical higher-order logic is encoded in the λΠ-calculus modulo theory by the constants $\Sigma_{HOL}^c$ (that is $\Sigma_{HOL}^i$ along with pem) and by the rewrite rules $\mathcal{R}_{HOL}$.
Remark that we have decided to encode the natural deduction rules via *typed constants*, while they are often expressed via *rewrite rules* in the $\lambda\Pi$-calculus modulo theory [2]. For instance, both the introduction and the elimination of implication can be derived from the rewrite rule $\mathit{Prf}(p \Rightarrow q) \leftrightarrow \mathit{Prf} p \rightarrow \mathit{Prf} q$. So as to perform the translation from classical logic to intuitionistic logic, the natural deduction steps must be *explicit* deduction steps, and cannot be *implicit* computation steps. That is why we encode the natural deduction rules with a deep embedding—via typed constants—instead of a shallow embedding—via rewrite rules.

## 2.3 Theories Encoded in Higher-Order Logic

When working with the encoding of higher-order logic in the $\lambda\Pi$-calculus modulo theory, it is possible to mix sorts, propositions and proofs—which is not expected in higher-order logic. For example, propositions can be inserted in sorts when we have a term of type $\mathit{Prop} \to \mathit{Set}$, and proofs can be inserted in propositions when we have a term of type $\Pi p : \mathit{Prop}$. $\mathit{Prf} p \to \mathit{Prop}$. To avoid such behavior, we introduce five grammars:

$$ \kappa_1 ::= \mathit{Set} \mid \kappa_1 \to \kappa_1 $$

$$ \kappa_2 ::= \mathit{Prop} \mid \mathit{El} a \mid \Pi x : \kappa_i. \kappa_2 \text{ with } i \in \{1, 2\} $$

$$ \kappa_3 ::= \mathit{Prf} p \mid \kappa_3 \to \kappa_3 \mid \Pi x : \kappa_i. \kappa_3 \text{ with } i \in \{1, 2\} $$

$$ \kappa_4 ::= \mathit{TYPE} \mid \Pi x : \kappa_i. \kappa_4 \text{ with } i \in \{1, 2\} $$

$$ \kappa_5 ::= \mathit{KIND} $$

The grammar $\kappa_3$ generates formulas and inference rules. The grammar $\kappa_4$ generates a subclass of kinds, and $\kappa_5$ only generates KIND. We characterize the judgments of the $\lambda\Pi$-calculus modulo theory to ensure that types and kinds are generated by one of those grammars.

**Definition 1 (κ-property).** The judgment $\Gamma \vdash t : A$ satisfies the $\kappa$-property when $A \in \kappa_i$ for some $i \in [1, 5]$. The judgment $\vdash \Gamma$ satisfies the $\kappa$-property when for each $(x : A) \in \Gamma$ we have $A \in \kappa_i$ for some $i \in [1, 5]$. A derivation satisfies the $\kappa$-property when each of its judgments satisfies the $\kappa$-property.

Theories encoded in higher-order logic are theories that feature the base higher-order encoding and in which the user-defined constants satisfy the $\kappa$-property.

**Definition 2 (Theory encoded in higher-order logic).** Let $\mathcal{T} = (\Sigma, \mathcal{R})$ be a theory in the $\lambda\Pi$-calculus modulo theory. $\mathcal{T}$ is encoded in higher-order logic when:

1. $\Sigma = \Sigma_{HOL}^k \cup \Sigma_{\mathcal{T}}$ with $k \in \{i, c\}$ and $\Sigma_{HOL} \cap \Sigma_{\mathcal{T}} = \emptyset$,

2. $\mathcal{R} = \mathcal{R}_{HOL} \cup \mathcal{R}_{\mathcal{T}}$ with $\mathcal{R}_{HOL} \cap \mathcal{R}_{\mathcal{T}} = \emptyset$,

3. for every $c : A \in \Sigma_{\mathcal{T}}$, the judgment $\vdash c : A$ satisfies the $\kappa$-property,

4. for every $\ell \to r \in \mathcal{R}_{\mathcal{T}}$, $\ell$ is neither $\mathit{Prf}$ nor $\forall$.

The fourth condition will ensure that the translation of a rewrite rule is a well-defined rewrite rule. Theories encoded in higher-order logic extend higher-order logic with user-defined rewrite rules and inference rules. The introduction of rewrite rules is part and parcel of deduction modulo theory [8], while the introduction of inference rules has been developed in superdeduction modulo theory [3, 16].

When considering a theory encoded in higher-order logic, all the user-defined constants satisfy the $\kappa$-property. In that respect, the only way to mix sorts, propositions and proofs is through $\lambda$-abstractions. For instance, $(\lambda P : \mathit{Prop}. o)$ is a term taking as input a proposition and returning a sort. The type
El `((λP : Prop. o) ⊥)` mixes propositions and sorts, but it is `β-convertible to El o`, in which no proposition occurs. Using this principle, we can transform every derivation of a theory encoded in higher-order logic into a derivation that satisfies the `κ-property`, by applying `β-reduction` on fragments of the derivation. When a derivation satisfies the `κ-property`, the rewrite rules `ℓ ↦ r` with `ℓ` and `r` of type `A ∈ κ₃` cannot be used. In the rest of this paper and without loss of generality, we only consider derivations that satisfy the `κ-property` and rewrite rules `ℓ ↦ r` with `ℓ` and `r` of type `A ∈ κᵢ` for `i ≠ 3`.

**Example 1 (Equational theory).** Consider the theory $\mathcal{T} = (\Sigma_{HOL} \cup \Sigma_{eq}, \mathcal{R}_{HOL} \cup \mathcal{R}_{eq})$, with a polymorphic equality symbol `=` : $Πa : Set. El a → El a → Prop$, and a rewrite rule for the Leibniz principle $Prf (= a x y) ↦ ΠP : El a → Prop. Prf (P x) → Prf (P y)$. This theory is encoded in higher-order logic. We can prove that the equality is reflexive, symmetric and transitive. For instance, the proof of reflexivity is given by $λa : Set. all_i a (λx : El a. = a x x) (λx : El a. λP : El a → Prop. λP_x : Prf (P x). P_x)$ which is of type $Πa : Set. Prf (∀a (λx : El a. = a x x))$.

# 3 Kuroda's Translation in the λΠ-Calculus Modulo Theory

In this section, we adapt Kuroda's double-negation translation to the λΠ-calculus modulo theory, when working in theories encoded in higher-order logic. Kuroda's translation [18] inserts a double negation in front of formulas and one after every universal quantifier. More formally, we have $A^{Ku} := ¬¬A_{Ku}$ where $A_{Ku}$ is defined by induction:

$$ 
\begin{align*}
(A \Rightarrow B)_{Ku} &:= A_{Ku} \Rightarrow B_{Ku} & (\neg A)_{Ku} &:= \neg A_{Ku} & P_{Ku} &:= P \text{ if } P \text{ atomic} \\
(A \land B)_{Ku} &:= A_{Ku} \land B_{Ku} & \top_{Ku} &:= \top & (\forall x A)_{Ku} &:= \forall x \neg\neg A_{Ku} \\
(A \lor B)_{Ku} &:= A_{Ku} \lor B_{Ku} & \bot_{Ku} &:= \bot & (\exists x A)_{Ku} &:= \exists x A_{Ku}
\end{align*}
$$

This translation embeds classical logic into intuitionistic logic, as for any first-order formula A we have $Γ ⊢ A$ in classical logic if and only if $Γ^{Ku} ⊢ A^{Ku}$ in intuitionistic logic.

## 3.1 Translation of Terms and Theories

When working inside a theory encoded in higher-order logic in the λΠ-calculus modulo theory, every formula has head symbol `Prf`. Inserting a double negation in front of every formula is therefore equivalent to inserting it after every `Prf` symbol. In that respect, we define a single translation $t \mapsto t^{Ku}$ by induction on the terms of the λΠ-calculus modulo theory. The translation of `Prf` is $λp. Prf (¬¬p)$, and the translation of the universal quantifier $∀$ is $λa. λp. ∀a (λz. ¬¬(p z))$. The translation of $λ$-abstraction $λx : A. t$ is naturally given by $λx : A^{Ku}. t^{Ku}$, the one of dependent type $Πx : A. B$ is given by $Πx : A^{Ku}. B^{Ku}$ and the one of application $t u$ is defined by $t^{Ku} u^{Ku}$.

As we are in the λΠ-calculus modulo theory with the *proofs-as-terms* paradigm, we have to translate proofs as well. Kuroda's translation relies on the fact that the translation of each natural deduction rule is admissible in intuitionistic logic. For instance, the introduction of implication allows to derive $Γ ⊢ P ⇒ Q$ from $Γ, P ⊢ Q$. In intuitionistic logic, $Γ^{Ku} ⊢ (P ⇒ Q)^{Ku}$ is derivable from $Γ^{Ku}, P^{Ku} ⊢ Q^{Ku}$. In the λΠ-calculus modulo theory, the constant $imp_i$ is of type $Πp, q : Prop. (Prf p → Prf q) → Prf (p ⇒ q)$, and we can build a term $imp_i^j$ of type $Πp, q : Prop. (Prf ¬¬p → Prf ¬¬q) → Prf ¬¬(p ⇒ q)$, that only depends on the constants representing intuitionistic natural deduction rules. Each constant $c$ of type A representing a natural deduction rule is translated by the term $c^i$ of type $A^{Ku}$, where $c^i$ is an intuitionistic proof term of $A^{Ku}$.
**Definition 3** (Translation of terms). Kuroda's translation is inductively defined on the terms of the $\lambda\Pi$-calculus modulo theory by:

$$
\begin{align*}
x^{\mathrm{Ku}} &:= x \\
c^{\mathrm{Ku}} &:= \left\{
\begin{array}{ll}
\lambda p. \mathrm{Prf} (\neg\neg p) & \text{if } c = \mathrm{Prf} \\
\lambda x. \lambda p. \forall x (\lambda z. \neg\neg(p z)) & \text{if } c = \forall \\
c^i & \text{if } c \text{ is a constant representing a natural deduction rule} \\
c & \text{otherwise}
\end{array}
\right. \\
s^{\mathrm{Ku}} &:= s \\
(\lambda x : A. t)^{\mathrm{Ku}} &:= \lambda x : A^{\mathrm{Ku}}. t^{\mathrm{Ku}} \\
(\Pi x : A. B)^{\mathrm{Ku}} &:= \Pi x : A^{\mathrm{Ku}}. B^{\mathrm{Ku}} \\
(t u)^{\mathrm{Ku}} &:= t^{\mathrm{Ku}} u^{\mathrm{Ku}}
\end{align*}
$$

**Proposition 1.** For every constant $c : A \in \Sigma_{HOL}$ representing a natural deduction rule, we have $\vdash c^i : A^{\mathrm{Ku}}$ in the theory $(\Sigma_{HOL}^i, \mathcal{R}_{HOL})$.

*Proof.* We have formalized the proof terms $c^i$ in DEDUKTI<fnref n="1" />. For instance, $\mathrm{top}_i$ is given in Section 4. □

As we are not mixing sorts, propositions and proofs, we know that the symbol $\forall$, the symbol $\mathrm{Prf}$ and the constants representing the natural deduction rules only occur in the grammar $\kappa_3$. Therefore, any type $A \in \kappa_i$ is modified by Kuroda's translation for $i = 3$, whereas $A^{\mathrm{Ku}} = A$ for $i \neq 3$.

We have defined the translation for terms, and we now want to define it for theories. Intuitively, we would like to translate a rewrite rule $\ell \leftrightarrow r$ by $\ell^{\mathrm{Ku}} \leftrightarrow r^{\mathrm{Ku}}$. However, if the head constant of $\ell$ is $\mathrm{Prf}$ or $\forall$, then the head symbol of $\ell^{\mathrm{Ku}}$ is $\mathrm{Prf}^{\mathrm{Ku}}$ or $\forall^{\mathrm{Ku}}$, that is a $\lambda$-abstraction and not a constant. Hence $\ell^{\mathrm{Ku}} \leftrightarrow r^{\mathrm{Ku}}$ may not be a valid rewrite rule in the $\lambda\Pi$-calculus modulo theory. We write $\lfloor \ell^{\mathrm{Ku}} \rfloor$ for the term obtained by $\beta$-reducing the head symbol of $\ell^{\mathrm{Ku}}$ if it is $\mathrm{Prf}^{\mathrm{Ku}}$ or $\forall^{\mathrm{Ku}}$.

**Definition 4.** The translation $t \mapsto t^{\mathrm{Ku}}$ is extended to contexts, signatures and rewrite systems by:

$$
\begin{align*}
\langle\rangle^{\mathrm{Ku}} &::= \langle\rangle \\
(\Gamma, x : A)^{\mathrm{Ku}} &:= \Gamma^{\mathrm{Ku}}, x : A^{\mathrm{Ku}} \\
(\Sigma, c : A)^{\mathrm{Ku}} &:= \Sigma^{\mathrm{Ku}}, c : A^{\mathrm{Ku}} \\
(\mathcal{R}, \ell \leftrightarrow r)^{\mathrm{Ku}} &:= \mathcal{R}^{\mathrm{Ku}}, \lfloor \ell^{\mathrm{Ku}} \rfloor \leftrightarrow r^{\mathrm{Ku}}
\end{align*}
$$

When translating a theory encoded in higher-order logic, we replace $\Sigma_{HOL}^c$ by $\Sigma_{HOL}^i$, and we translate the user-defined signature $\Sigma_{\mathcal{T}}$ and rewrite system $\mathcal{R}_{\mathcal{T}}$.

**Definition 5** (Translation of theories). Let $\mathcal{T} = (\Sigma_{HOL}^c \cup \Sigma_{\mathcal{T}}, \mathcal{R}_{HOL} \cup \mathcal{R}_{\mathcal{T}})$ be a theory encoded in higher-order logic. The translation of $\mathcal{T}$ is $\mathcal{T}^{\mathrm{Ku}} = (\Sigma_{HOL}^i \cup \Sigma_{\mathcal{T}}^{\mathrm{Ku}}, \mathcal{R}_{HOL} \cup \mathcal{R}_{\mathcal{T}}^{\mathrm{Ku}})$.

Remark that $\mathcal{T}^{\mathrm{Ku}}$ is a theory. Specifically, rewrite rules $\lfloor \ell^{\mathrm{Ku}} \rfloor \leftrightarrow r^{\mathrm{Ku}} \in \mathcal{R}_{\mathcal{T}}^{\mathrm{Ku}}$ are always well-defined, since $\ell$ is neither $\mathrm{Prf}$ nor $\forall$, and by definition of $\lfloor \ell^{\mathrm{Ku}} \rfloor$.

## 3.2 Embedding Classical Logic into Intuitionistic Logic

We aim at proving that the extension of Kuroda's translation in the $\lambda\Pi$-calculus modulo theory indeed embeds classical logic into intuitionistic logic. In other words, we want to show that $\Gamma \vdash t : A$ in $\mathcal{T}$ entails $\Gamma^{\mathrm{Ku}} \vdash t^{\mathrm{Ku}} : A^{\mathrm{Ku}}$ in $\mathcal{T}^{\mathrm{Ku}}$. To do so, we translate the derivations step by step. In particular, when the CONV rule is used with $A \equiv_{\beta, \mathcal{R}} B$ in $\mathcal{T}$, we want to have $A^{\mathrm{Ku}} \equiv_{\beta, \mathcal{R}} B^{\mathrm{Ku}}$ in $\mathcal{T}^{\mathrm{Ku}}$.

<footnote n="1">¹See https://github.com/Deducteam/Construkti/blob/master/kuroda.dk.</footnote>
**Lemma 2 (Translation of substitutions).** $(t[z \leftarrow w])^{Ku} = t^{Ku}[z \leftarrow w^{Ku}]$

*Proof.* By induction on the term $t$. We have $(c[z \leftarrow w])^{Ku} = c^{Ku} = c^{Ku}[z \leftarrow w^{Ku}]$ since $c^{Ku}$ is a closed term. Similarly, $(s[z \leftarrow w])^{Ku} = s^{Ku} = s^{Ku}[z \leftarrow w^{Ku}]$. If $x \neq z$, then $(x[z \leftarrow w])^{Ku} = x^{Ku} = x^{Ku}[z \leftarrow w^{Ku}]$. If $x = z$, then $(x[z \leftarrow w])^{Ku} = w^{Ku} = x[z \leftarrow w^{Ku}] = x^{Ku}[z \leftarrow w^{Ku}]$. The cases for $\lambda$-abstractions, dependent types, and applications follow from the induction hypotheses. $\square$

**Lemma 3 (Translation of conversions).** If $A \equiv_{\beta\mathcal{R}} B$ in $\mathcal{T}$, then $A^{Ku} \equiv_{\beta\mathcal{R}} B^{Ku}$ in $\mathcal{T}^{Ku}$.

*Proof.* By induction on the construction of $A \equiv_{\beta\mathcal{R}} B$.

* If $\ell \hookrightarrow r$ in $\mathcal{T}$, then we show $(\ell\theta)^{Ku} \equiv_{\beta\mathcal{R}} (r\theta)^{Ku}$ in $\mathcal{T}^{Ku}$ for any substitution $\theta$. For $\ell \hookrightarrow r \in \mathcal{R}_{HOL}$, we have $\ell^{Ku} = \ell$ and $r^{Ku} = r$, and we use Lemma 2. For $\ell \hookrightarrow r \in \mathcal{R}_{\mathcal{T}}$, we have $\lfloor \ell^{Ku} \rfloor \hookrightarrow r^{Ku} \in \mathcal{R}_{\mathcal{T}}^{Ku}$, which entails that $(\ell\theta)^{Ku} = \ell^{Ku}\theta^{Ku} \equiv_{\beta\mathcal{R}} \lfloor \ell^{Ku} \rfloor\theta^{Ku} \equiv_{\beta\mathcal{R}} r^{Ku}\theta^{Ku} = (r\theta)^{Ku}$ by Lemma 2.

* If $(\lambda x : A. t) u \hookrightarrow t[x \leftarrow u]$ in $\mathcal{T}$, then we have $((\lambda x : A. t) u)^{Ku} = (\lambda x : A^{Ku} . t^{Ku}) u^{Ku}$, which $\beta$-reduces to $t^{Ku}[x \leftarrow u^{Ku}]$, that is $(t[x \leftarrow u])^{Ku}$ using Lemma 2.

* Closure by context, reflexivity, symmetry, and transitivity are immediate. $\square$

**Theorem 1 (Translation of judgments).** Let $\mathcal{T}$ be a theory encoded in higher-order logic.

* If $\Gamma \vdash \Gamma$ in $\mathcal{T}$ then $\Gamma^{Ku}$ in $\mathcal{T}^{Ku}$.

* If $\Gamma \vdash t : A$ in $\mathcal{T}$ then $\Gamma^{Ku} \vdash t^{Ku} : A^{Ku}$ in $\mathcal{T}^{Ku}$.

*Proof.* We proceed by induction on the derivation. We present the most interesting cases, the others follow the definition and the induction hypotheses.

* **CONST**: By induction we have $\Gamma^{Ku}$ and $\Gamma^{Ku} \vdash A^{Ku} : s^{Ku}$ in $\mathcal{T}^{Ku}$.

If $c : A \in \Sigma_{\mathcal{T}}$, then $c : A^{Ku} \in \Sigma_{\mathcal{T}}^{Ku}$ and we derive $\Gamma^{Ku} \vdash c : A^{Ku}$ using CONST.

Suppose that $c = \text{Prf}$. We simply derive $\Gamma^{Ku} \vdash \lambda p. \text{Prf}(\neg\neg p) : \text{Prop} \rightarrow \text{TYPE}$, that is $\Gamma^{Ku} \vdash \text{Prf}^{Ku} : (\text{Prop} \rightarrow \text{TYPE})^{Ku}$, in $\mathcal{T}^{Ku}$.

Suppose that $c = \forall$. We simply derive $\Gamma^{Ku} \vdash \lambda x. \lambda p. \forall x (\lambda z. \neg\neg(pz)) : \Pi x : \text{Set.} (El x \rightarrow \text{Prop}) \rightarrow \text{Prop}$, that is $\Gamma^{Ku} \vdash \forall^{Ku} : (\Pi x : \text{Set.} (El x \rightarrow \text{Prop}) \rightarrow \text{Prop})^{Ku}$, in $\mathcal{T}^{Ku}$.

Suppose that $c$ is a constant representing a natural deduction rule. Using Proposition 1, we have $\Gamma^{Ku} \vdash c^i : A^{Ku}$ in $\mathcal{T}^{Ku}$, that is $\Gamma^{Ku} \vdash c^{Ku} : A^{Ku}$. In particular, we replace the classical axiom pem : $\Pi p : \text{Prop.} \text{Prf}(p \lor \neg p)$ by the intuitionistic term pem$^i$ : $\Pi p : \text{Prop.} \text{Prf}(\neg\neg(p \lor \neg p))$.

Otherwise, $c : A \in \Sigma_{HOL}$ but is not $\text{Prf}$, not $\forall$, and not a constant representing a natural deduction rule. Then $A$ does not contain $\text{Prf}$ and $\forall$, so $A^{Ku} = A$. We derive $\Gamma^{Ku} \vdash c : A^{Ku}$ using CONST.

* **CONV**: By induction we have $\Gamma^{Ku} \vdash t^{Ku} : A^{Ku}$ in $\mathcal{T}^{Ku}$ and $\Gamma^{Ku} \vdash B^{Ku} : s^{Ku}$ in $\mathcal{T}^{Ku}$. From Lemma 3, we know that $A^{Ku} \equiv_{\beta\mathcal{R}} B^{Ku}$, and we conclude that $\Gamma^{Ku} \vdash t^{Ku} : B^{Ku}$ in $\mathcal{T}^{Ku}$ using CONV. $\square$

**Example 2 (Translated equational theory).** The translation of the theory $\mathcal{T} = (\Sigma_{HOL} \cup \Sigma_{eq}, \mathcal{R}_{HOL} \cup \mathcal{R}_{eq})$ of Example 1 is obtained by taking the equality symbol $=$ : $\Pi a : \text{Set.} \ El a \rightarrow El a \rightarrow \text{Prop.}$ (which remains unchanged), and by transforming the rewrite rule $\text{Prf}(= a x y) \leftrightarrow \Pi P : \text{El a} \rightarrow \text{Prop.} \ \text{Prf}(P x) \rightarrow \text{Prf}(P y)$ into $\text{Prf}(\neg\neg(= a x y)) \leftrightarrow \Pi P : \text{El a} \rightarrow \text{Prop.} \ \text{Prf}(\neg\neg(P x)) \rightarrow \text{Prf}(\neg\neg(P y))$. The proof of reflexivity is now given by $\lambda a : \text{Set.} \ \text{all}_i^j a (\lambda x : \text{El a.} = a x x) (\lambda x : \text{El a.} \ \lambda P : \text{El a} \rightarrow \text{Prop.} \ \text{P}_x : \text{Prf}(\neg\neg(P x)))$. $P_x$ which is of type $\Pi a : \text{Set.} \ \text{Prf}(\neg\neg(\forall a (\lambda x : \text{El a.} \ \neg\neg(= a x x))))$.
### 3.3 Back to the Original Theory

We have shown that, in the $\lambda\Pi$-calculus modulo theory, $\Gamma \vdash t : A$ in $\mathcal{T}$ implies $\Gamma^{Ku} \vdash t^{Ku} : A^{Ku}$ in $\mathcal{T}^{Ku}$. We now want to prove the reverse implication: if there exists an intuitionistic proof of $A^{Ku}$ in $\mathcal{T}^{Ku}$, then there exists a classical proof of $A$ in $\mathcal{T}$. To do so, we reason in two steps: first we show that it is possible to build a proof of $A$ from a proof of $A^{Ku}$ in classical logic, and then we show that any result in $\mathcal{T}^{Ku}$ can also be derived in $\mathcal{T}$.

The first step consists in proving that, for any $A \in \kappa_3$, it is possible to derive $A^{Ku}$ from $A$. For this, we show that any proposition $P$ and its translation $P^{Ku}$ are classically equivalent. Such a result is not necessarily true in higher-order logic. We assume some property, called the Kuroda equivalence.

**Definition 6 (Kuroda equivalence).** Let $\Gamma$ be a context, $t$ be a constant or a variable such that $\Gamma \vdash t : T_1 \rightarrow \dots \rightarrow T_n \rightarrow \text{Prop}$, and $u_1, \dots, u_n$ be terms such that $\Gamma \vdash u_i : T_i$. There exists some $p$ such that $\Gamma \vdash p : \text{Prf}((t u_1 \dots u_n)^{Ku} \Leftrightarrow t u_1 \dots u_n)$.

The Kuroda equivalence property is derivable from functional extensionality and propositional extensionality in classical logic [21]. Remark that it is satisfied for the usual logical connectives and quantifiers. For instance, we have $A_{Ku} \wedge B_{Ku} \Leftrightarrow A \wedge B$ and $\forall x \neg\neg A_{Ku} \Leftrightarrow \forall x A$ in classical logic. In the rest of this paper, we work assuming the Kuroda equivalence.

**Lemma 4.** Any proposition $P$ is $\beta$-convertible to a variable $x$, a constant $c$, or an application $t \, u_1 \dots \, u_n$ where $t$ is a constant or a variable of type $T_1 \to \dots \to T_n \to \text{Prop}$ and $u_1, \dots, u_n$ are terms of type $T_1, \dots, T_n$.

The constant $c$ may be $\top$ or $\bot$, and the head symbol of the application may be any connective, quantifier or predicate.

**Proposition 2.** Let $\Gamma \vdash P : \text{Prop}$. In the theory $(\Sigma_{\text{HOL}}^c \cup \Sigma, \mathcal{R}_{\text{HOL}} \cup \mathcal{R})$, there exists some proof term $m_P$ such that $\Gamma \vdash m_P : \text{Prf}(P^{Ku} \Leftrightarrow P)$.

*Proof.* We distinguish cases thanks to Lemma 4.

* Suppose that $P$ is $\beta$-convertible to a variable $x$. We have $x^{Ku} = x$ so we build some $m_x$ such that $\Gamma \vdash m_x : \text{Prf}(x^{Ku} \Leftrightarrow x)$. Since $P$ is $\beta$-convertible to $x$, $P^{Ku}$ is $\beta$-convertible to $x^{Ku}$ (see Lemma 3) and we conclude that $\Gamma \vdash m_x : \text{Prf}(P^{Ku} \Leftrightarrow P)$.

* If $P$ is $\beta$-convertible to a constant $c$, then we are in the case where $c^{Ku} = c$ and we proceed similarly.

* Suppose that $P$ is $\beta$-convertible to an application $t \, u_1 \dots \, u_n$ where $t$ is a constant or a variable. $P^{Ku}$ is $\beta$-convertible to $(t \, u_1 \dots \, u_n)^{Ku}$ and we conclude using the Kuroda equivalence. $\square$

**Lemma 5.** Let $A \in \kappa_3$ and $\ell$ be a strict subterm of $A$. In the theory $(\Sigma_{\text{HOL}}^c \cup \Sigma, \mathcal{R}_{\text{HOL}} \cup \mathcal{R})$, for any context $\Gamma$, there exists some $t$ such that $\Gamma \vdash t : A[\ell]$ if and only if there exists some $t'$ such that $\Gamma \vdash t' : A[\ell^{Ku}]$.

*Proof.* We proceed by induction on the term $A$ using the fact that $A$ is generated by $\kappa_3$.

* Suppose that $A = \text{Prf } P$. If $\forall$ does not occur in $\ell$, then $\ell^{Ku} = \ell$ and $P[\ell^{Ku}] = P[\ell]$, so we directly conclude. Otherwise, we use Proposition 2 on the right proposition.

* Suppose that $A = \Pi x : B. C$ with $B \in \kappa_1$ or $B \in \kappa_2$. If $\ell$ occurs in $B$, then by definition $B[\ell^{Ku}] = B[\ell]$, so $\ell^{Ku} = \ell$ and we directly conclude. Suppose that $\ell$ only occurs in $C$ and that there exists some $t$ such that $\Gamma \vdash t : \Pi x : B. C[\ell]$. By induction on $C$ with $\Gamma, x : B \vdash t : C[\ell]$ (obtained by weakening), we get some $t'_C$ such that $\Gamma, x : B \vdash t'_C : C[\ell^{Ku}]$. Therefore, we have $\Gamma \vdash \lambda x : B. t'_C : \Pi x : B. C[\ell^{Ku}]$. We proceed similarly for the reverse implication.
* Suppose that $A = B \to C$ with $B, C \in \kappa_3$. Suppose that we have $\Gamma \vdash t : B[\ell] \to C[\ell]$. By induction on $B$ with $\Gamma, x : B[\ell^{Ku}] \vdash x : B[\ell^{Ku}]$, we get some $t_B$ such that $\Gamma, x : B[\ell^{Ku}] \vdash t_B : B[\ell]$. By induction on $C$ with $\Gamma, x : B[\ell^{Ku}] \vdash t : B[\ell]$, we get some $t'_C$ such that $\Gamma, x : B[\ell^{Ku}] \vdash t'_C : C[\ell^{Ku}]$. We conclude that $\Gamma \vdash \lambda x : B[\ell^{Ku}]$. $t'_C : B[\ell^{Ku}] \to C[\ell^{Ku}]$. We proceed similarly for the reverse implication. $\square$

**Lemma 6.** Let $A \in \kappa_3$. In the theory $(\Sigma_{HOL}^c \cup \Sigma, \mathcal{R}_{HOL} \cup \mathcal{R})$, for any context $\Gamma$, there exists some $t$ such that $\Gamma \vdash t : A$ if and only if there exists some $t'$ such that $\Gamma \vdash t' : A^{Ku}$.

*Proof.* We proceed by induction on the term $A$ using the fact that $A$ is generated by $\kappa_3$. We use Lemma 5 and the double-negation elimination. $\square$

We have shown that it is possible to build a proof of $A$ in $\mathcal{T}^{Ku}$ using a proof of $A^{Ku}$ and the principle of excluded middle. The next step is to derive a proof of $A$ in the original theory $\mathcal{T}$. In particular, it requires to replace each use of $[\ell^{Ku}] \to r^{Ku} \in \mathcal{R}_{\mathcal{T}}^{Ku}$ by a use of $\ell \to r \in \mathcal{R}_{\mathcal{T}}$.

**Lemma 7.** Let $A \in \kappa_3$ such that $\Gamma \vdash t : A[\ell^{Ku}]$. Using $\ell \to r$, there exists some $t'$ such that $\Gamma \vdash t' : A[r^{Ku}]$.

*Proof.* Using Lemma 5, there exists some $t'$ such that $\Gamma \vdash t' : A[\ell]$. Using $\ell \to r$, we have $\Gamma \vdash t' : A[r]$. We use Lemma 5 to obtain some $t''$ such that $\Gamma \vdash t'' : A[r^{Ku}]$. $\square$

**Lemma 8.** Let $(\Sigma_{HOL}^c \cup \Sigma, \mathcal{R}_{HOL} \cup \mathcal{R}^{Ku})$ and $(\Sigma_{HOL}^c \cup \Sigma, \mathcal{R}_{HOL} \cup \mathcal{R})$ be two theories, abbreviated $\mathcal{R}^{Ku}$ and $\mathcal{R}$.

* If $\Gamma \vdash \Gamma$ in $\mathcal{R}^{Ku}$ then $\Gamma \vdash \in \mathcal{R}$.

* If $\Gamma \vdash t : A$ in $\mathcal{R}^{Ku}$ and $A \in \kappa_i$ with $i \in \{1, 2, 4, 5\}$, then $\Gamma \vdash t : A$ in $\mathcal{R}$.

* If $\Gamma \vdash t : A$ in $\mathcal{R}^{Ku}$ and $A \in \kappa_3$, then there exists some $t'$ such that $\Gamma \vdash t' : A$ in $\mathcal{R}$.

*Proof.* We proceed by induction on the typing derivation. We only present the relevant cases.

* **ABS**: Suppose that $\Gamma \vdash A : \text{TYPE}$ and $\Gamma, x : A \vdash B : s$ and $\Gamma, x : A \vdash t : B$ in $\mathcal{R}^{Ku}$. By induction we have $\Gamma \vdash A : \text{TYPE}$ and $\Gamma, x : A \vdash B : s$ in $\mathcal{R}$.

If $B \in \kappa_i$ with $i \in \{1, 2\}$, then by induction we have $\Gamma, x : A \vdash t : B$ in $\mathcal{R}$, and we derive $\Gamma \vdash \lambda x : A. t : \Pi x : A. B$ in $\mathcal{R}$.

If $B \in \kappa_3$, then by induction we have $\Gamma, x : A \vdash t' : B$ in $\mathcal{R}$. We derive $\Gamma \vdash \lambda x : A. t' : \Pi x : A. B$ in $\mathcal{R}$.

* **APP**: Suppose that $\Gamma \vdash t : \Pi x : A. B$ and $\Gamma \vdash u : A$ in $\mathcal{R}^{Ku}$.

If $\Pi x : A. B \in \kappa_i$ with $i \in \{1, 2, 4\}$, then by induction we have $\Gamma \vdash t : \Pi x : A. B$ and $\Gamma \vdash u : A$ in $\mathcal{R}$. We derive $\Gamma \vdash t u : B[x \leftarrow u]$ in $\mathcal{R}$.

If $\Pi x : A. B \in \kappa_3$, then by induction we have $\Gamma \vdash t' : \Pi x : A. B$ in $\mathcal{R}$. If $A \in \kappa_i$ with $i \in \{1, 2\}$, then by induction we have $\Gamma \vdash u : A$ in $\mathcal{R}$, and we derive $\Gamma \vdash t' u : B[x \leftarrow u]$ in $\mathcal{R}$. If $A \in \kappa_3$ (x does not occur in B), then by induction we have $\Gamma \vdash u' : A$ in $\mathcal{R}$, and we conclude that $\Gamma \vdash_c t' u' : B$.

* **CONV**: If $A \equiv_{\beta\mathcal{R}} B$ is obtained using $\beta$-conversion or the rewrite rules of $\mathcal{R}_{HOL}$, then we conclude using the induction hypothesis and the CONV rule. Otherwise, and without loss of generality, we consider that we only use one rewrite rule of $\mathcal{R}^{Ku}$ per CONV rule.

Suppose that $A \equiv_{\beta\mathcal{R}} B$ is obtained using the rewrite rule $\ell^{Ku} \to r^{Ku} \in \mathcal{R}^{Ku}$. In that case, we have $A = C[\ell^{Ku}]$ and $B = C[r^{Ku}]$ (the case $A = C[r^{Ku}]$ and $B = C[\ell^{Ku}]$ is treated similarly). By assumption, we have $\Gamma \vdash t : C[\ell^{Ku}]$ and $\Gamma \vdash C[r^{Ku}] : s$ in $\mathcal{R}^{Ku}$.
If $A, B \in \kappa_i$ with $i \in \{1, 2, 4, 5\}$, then $\ell^{Ku} = \ell$ and $r^{Ku} = r$. By induction we have $\Gamma \vdash t : C[\ell^{Ku}]$ and $\Gamma \vdash C[r^{Ku}] : s$ in $\mathcal{R}$. We apply CONV with $C[\ell] \equiv_{\beta\mathcal{R}} C[r]$.

If $A, B \in \kappa_3$, then by induction we have $\Gamma \vdash t' : C[\ell^{Ku}]$ and $\Gamma \vdash C[r^{Ku}] : s$ in $\mathcal{R}$. We conclude using Lemma 7.

□

We now have all the tools to show that, for any intuitionistic proof of $A^{Ku}$ in the translated theory $\mathcal{T}^{Ku}$, there exists a classical proof of $A$ in the original theory $\mathcal{T}$.

**Theorem 2.** Let $\mathcal{T}$ be a theory encoded in higher-order logic and $A \in \kappa_3$. If $\Gamma^{Ku} \vdash t : A^{Ku}$ in $\mathcal{T}^{Ku}$, then under the Kuroda equivalence there exists some term $t'$ such that $\Gamma \vdash t' : A$ in $\mathcal{T}$.

*Proof.* We directly have $\Gamma^{Ku} \vdash t : A^{Ku}$ in $(\Sigma_{HOL}^c \cup \Sigma_{\mathcal{T}}^{Ku}, \mathcal{R}_{HOL} \cup \mathcal{R}_{\mathcal{T}}^{Ku})$.

* By Lemma 6, there exists some $t'$ such that $\Gamma^{Ku} \vdash t' : A$ in $(\Sigma_{HOL}^c \cup \Sigma_{\mathcal{T}}^{Ku}, \mathcal{R}_{HOL} \cup \mathcal{R}_{\mathcal{T}}^{Ku})$ and under the Kuroda equivalence.

* Using Lemma 8, there exists some $t''$ such that $\Gamma^{Ku} \vdash t'' : A$ in $(\Sigma_{HOL}^c \cup \Sigma_{\mathcal{T}}^{Ku}, \mathcal{R}_{HOL} \cup \mathcal{R}_{\mathcal{T}})$.

* We replace the signature $\Sigma_{\mathcal{T}}^{Ku}$ by $\Sigma_{\mathcal{T}}$. For each constant $c : C \in \Sigma_{\mathcal{T}}$ with $C \in \kappa_3$, we replace $c$ by $t_c$ (provided by Lemma 6) in $t''$. We obtain $\Gamma^{Ku} \vdash t''[c \leftarrow t_c] : A$ in $(\Sigma_{HOL}^c \cup \Sigma_{\mathcal{T}} \cup \mathcal{R}_{HOL} \cup \mathcal{R}_{\mathcal{T}})$, that is in $\mathcal{T}$. These substitutions work since $c$ cannot occur in a dependent type.

* We replace the context $\Gamma^{Ku}$ by $\Gamma$. For each variable $x : B \in \Gamma$ with $B \in \kappa_3$, we replace $x$ by $t_x$ (provided by Lemma 6) in $t''[c \leftarrow t_c]$. We obtain $\Gamma \vdash t''[c \leftarrow t_c][x \leftarrow t_x] : A$ in $\mathcal{T}$, which achieves the proof.

□

The extension of Kuroda's translation to the $\lambda\Pi$-calculus modulo theory is a generalization of Brown and Rizkallah's translation for simple type theory [4]. Indeed, if $\mathcal{R}_{\mathcal{T}} = \langle\rangle$, then we obtain the result in higher-order logic, at the only difference that proofs are represented by terms.

# 4 Construkti, an Implementation for Dedukti Proofs

**Dedukti.** The $\lambda\Pi$-calculus modulo theory has been implemented in the DEDUKTI proof language. Abstractions $\lambda x : A. t$ are represented by $x : A => t$, and dependent types $\Pi x : A. B$ are represented by $x : A -> B$. Constants $c : A$ are specified by $c : A$, prefixed with the keyword def if the constant can be defined using rewrite rules. Rewrite rules $\ell \to r$, where $x$ and $y$ are the free variables of $\ell$ and $r$, are represented by $[x, y] 1 --> r$. For instance, using the encoding of the notions of proposition and proof, we can encode the addition on natural numbers via rewrite rules.

nat : Set.
0 : El nat.
S : El nat -> El nat.
def add : El nat -> El nat -> El nat.
[x] add x 0 --> x.
[x, y] add x (S y) --> S (add x y).

Theorems are represented by **thm n : T := p**, where **n** is its name, **T** its statement and **p** its proof term. For checking that **p** is indeed a proof of **T**, we can use one of the type checkers of DEDUKTI, for instance **DKCHECK** [19] or **LAMBDAPI** [15].
**Construkti.** We have implemented `CONSTRUKTI`<fnref n="2" />, a tool that performs Kuroda's translation on DEDUKTI proofs. `CONSTRUKTI` takes as input a DEDUKTI file containing the specification of a user-defined theory encoded in higher-order logic, as well as proofs in this theory. It returns a DEDUKTI file containing the specification of the translated theory, as well as the translated proofs.

In this implementation, we insert one double negation after every `Prf` and `∀` symbols, and we replace the constants `c` representing natural deduction rules by the terms `c^i`. For instance, the constant `top_i` of type `Prf ⊤`, representing the introduction of tautology, is replaced in the formal proofs by the term `top_i^i` of type `Prf (¬¬⊤)`. The proof term `top_i^i` relies on the proof of `Πp : Prop. Prf (p ⇒ ¬¬p)`.

top_i : Prf top.

thm prop_double Neg : p : Prop -> Prf (imp p (not (not p)))
:= p => imp_i p (not (not p))
(pP => neg_i (not p) (pNP => neg_e p pNP pP)).

thm top_i_i : Prf (not (not top))
:= imp_e top (not (not top)) (prop_double Neg top) top_i.

So as to obtain readable theorems, we directly β-reduce every application of `Prf^Ku` and `∀^Ku`.

**Benchmark.** We have tested `CONSTRUKTI` on a benchmark of 101 DEDUKTI proofs, available in the file `hol-lib.dk`. These proofs encompass results related to connectives and quantifiers, classical formulas, De Morgan's laws, polymorphic equality, and basic arithmetic. The proofs are expressed in propositional, first-order and higher-order logics. This library of proofs includes user-defined rewrite rules—a feature of the λΠ-calculus modulo theory—and inference rules—thanks to the encoding of the notions of proposition and proof. We compare in Table 1 the different characteristics of the library: the number of proofs, the number of classical proofs, the number of results expressed in higher-order logic, and the number of results that are expressed via admissible inference rules.

<table><caption>Table 1: Comparison of the different libraries.</caption><thead><tr><th rowspan="2">Content of the library</th><th colspan="4">Number of ...</th></tr><tr><th>proofs</th><th>classical proofs</th><th>higher-order results</th><th>admissible inference rules</th></tr></thead><tbody><tr><td>Basic logic</td><td>38</td><td>0</td><td>15</td><td>26</td></tr><tr><td>Classical results</td><td>12</td><td>12</td><td>9</td><td>3</td></tr><tr><td>De Morgan</td><td>8</td><td>6</td><td>4</td><td>8</td></tr><tr><td>Equality</td><td>10</td><td>0</td><td>6</td><td>4</td></tr><tr><td>Arithmetic</td><td>33</td><td>0</td><td>0</td><td>16</td></tr><tr><td>All</td><td>101</td><td>18</td><td>34</td><td>57</td></tr></tbody></table>

After running `CONSTRUKTI`, all the translated proofs of the translated theorems typecheck, and are expressed in intuitionistic logic.

<footnote n="2">²Available at https://github.com/Deducteam/Construkti.</footnote>
# 5 Conclusion

In this paper, we have extended Kuroda’s translation to the theories encoded in higher-logic in the $\lambda\Pi$-calculus modulo theory, that is $\lambda$-calculus extended with dependent types and user-defined rewrite rules. In this logical framework, proofs are terms following the Curry-Howard correspondence, and have to be effectively translated. Due to the encoding of the notions of proposition and proof in the $\lambda\Pi$-calculus modulo theory, we can assume, prove, and translate inference rules. We have implemented CONSTRUKTI, a tool that transforms DEDUKTI proofs following Kuroda’s translation. Both DEDUKTI and CONSTRUKTI pave the way for interoperability between classical proof systems—such as HOL LIGHT or MIZAR—and intuitionistic proof systems—such as COQ, LEAN or AGDA.

**Future work.** There exist large libraries of proofs in higher-order logic, for instance the HOL LIGHT standard library. Blanqui [9] recently translated it to COQ via DEDUKTI, taking the excluded middle as an axiom. Future work would be to obtain an intuitionistic version of the HOL LIGHT standard library, by applying Kuroda’s translation and CONSTRUKTI.

**Related work.** Double-negation translations aim at embedding classical logic into intuitionistic logic. As such, double-negation translations *always* transform classical proofs into intuitionistic ones, but they modify the formulas during the process. Proof constructivization aims at transforming classical proofs into intuitionistic ones *without* translating the formulas, but such a process does not necessarily succeed. Cauderlier [5] developed heuristics to constructivize proofs in DEDUKTI, via rewrite systems that try to remove instances of the principle of excluded middle or of the double-negation elimination. Gilbert [11] designed a constructivization algorithm for first-order logic, that was tested in DEDUKTI and works in practice for large fragments of first-order logic.

# Acknowledgments

The author would like to thank Marc Aiguier, Gilles Dowek and Olivier Hermant for helpful discussions and valuable remarks about this work.

# References

[1] Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant & Ronan Saillard (2016): *Dedukti: a Logical Framework based on the $\lambda\Pi$-Calculus Modulo Theory*. Manuscript.

[2] Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet & François Thiré (2023): *A modular construction of type theories*. *Logical Methods in Computer Science* Volume 19, Issue 1, doi:10.46298/lmcs-19(1:12)2023. Available at https://lmcs.episciences.org/10959.

[3] Paul Brauner, Clement Houtmann & Claude Kirchner (2007): *Principles of Superdeduction*. In: *LICS 2007-22nd Annual IEEE Symposium on Logic in Computer Science*, Wroclaw, Poland, pp. 41–50, doi:10.1109/LICS.2007.37. Available at https://ieeexplore.ieee.org/abstract/document/4276550. ISSN: 1043-6871.

[4] Chad E. Brown & Christine Rizkallah (2014): *Glivenko and Kuroda for simple type theory*. *The Journal of Symbolic Logic* 79(2), pp. 485–495, doi:10.1017/jsl.2013.10. Available at http://www.jstor.org/stable/43303744.
[5] Raphaël Cauderlier (2016): *A Rewrite System for Proof Constructivization*. In: LFMTP 2016 - International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Porto, Portugal, pp. 1–7, doi:10.1145/2966268.2966270. Available at https://inria.hal.science/hal-01420634.

[6] Denis Cousineau & Gilles Dowek (2007): *Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo*. In: Simona Ronchi Della Rocca, editor: *Typed Lambda Calculi and Applications*, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 102–117, doi:10.1007/978-3-540-73228-0_9.

[7] Nachum Dershowitz & Jean-Pierre Jouannaud (1991): *Rewrite Systems*. In: *Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics*, doi:10.1016/B978-0-444-88074-1.50011-1.

[8] Gilles Dowek, Thérèse Hardin & Claude Kirchner (2003): *Theorem Proving Modulo*. Journal of Automated Reasoning 31, pp. 33–72, doi:10.1023/A:1027357912519.

[9] Frédéric Blanqui (2024): *Translating HOL-Light proofs to Coq*. In: *LPAR 2024 - 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning*, Balaclava, Mauritius, pp. 1–18, doi:10.29007/6k4x. Available at https://easychair.org/publications/paper/mtFT.

[10] Gerhard Gentzen (1936): *Die Widerspruchsfreiheit der Reinen Zahlentheorie*. Mathematische Annalen 112, pp. 493–565, doi:10.1007/BF01565428.

[11] Frédéric Gilbert (2017): *Automated Constructivization of Proofs*. In: *FOSSACS 2017 - 20th International Conference on Foundations of Software Science and Computation Structures*, Uppsala, Sweden, pp. 480–495, doi:10.1007/978-3-662-54458-7_28.

[12] Valery Glivenko (1928): *Sur quelques points de la logique de M. Brouwer*. *Bulletins de la classe des sciences* 15, p. 183–188.

[13] Kurt Gödel (1933): *Zur intuitionistischen Arithmetik und Zahlentheorie*. *Ergebnisse eines Mathematischen Kolloquiums* 4, p. 34–38.

[14] Robert Harper, Furio Honsell & Gordon Plotkin (1993): *A Framework for Defining Logics*. *Journal of the ACM* 40(1), p. 143–184, doi:10.1145/138027.138060.

[15] Gabriel Hondet & Frédéric Blanqui (2020): *The New Rewriting Engine of Dedukti*. In: *FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction*, 167, Paris, France, p. 16, doi:10.4230/LIPIcs.FSCD.2020.35. Available at https://inria.hal.science/hal-02981561.

[16] Clément Houtmann (2010): *Représentation et interaction des preuves en superdéduction modulo*. Ph.D. thesis, Université Henri Poincaré - Nancy I. Available at https://theses.hal.science/tel-00553219.

[17] Andrey Nikolaevich Kolmogorov (1925): *O principe tertium non datur*. *Matematicheski Sbornik* 32, p. 646–667.

[18] Sigekatu Kuroda (1951): *Intuitionistische Untersuchungen der formalistischen Logik*. Nagoya Mathematical Journal 2, p. 35–47, doi:10.1017/S0027763000010023.

[19] Ronan Saillard (2015): *Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice*. Ph.D. thesis, Ecole Nationale Supérieure des Mines de Paris. Available at https://pastel.hal.science/tel-01299180.

[20] François Thiré (2020): *Interoperability between proof systems using the logical framework Dedukti*. Ph.D. thesis, Université Paris-Saclay. Available at https://hal.science/tel-03224039.

[21] Thomas Traversié (2024): *Kuroda's translation for higher-order logic*. Available at https://hal.science/hal-04561757. Manuscript.