# Monad Translations for Higher-Order Logic

Thomas Traversié

► To cite this version:

Thomas Traversié. Monad Translations for Higher-Order Logic. FSCD 2025 - 10th International Conference on Formal Structures for Computation and Deduction, Maribel Fernández, Jul 2025, Birming- ham, United Kingdom. 10.4230/LIPIcs.FSCD.2025.34 . hal-05151149

HAL Id: hal-05151149

https://hal.science/hal-05151149v1

Submitted on 8 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Memo Translations for Higher-Order Logic

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

## Abstract

Classical logic can be embedded into intuitionistic logic by inserting double negations in formulas. Several translations generalize this idea by using monad operators instead of double negations. They eliminate particular axioms, for instance the principle of excluded middle or the principle of explosion, and therefore can be used to embed classical logic into intuitionistic logic or intuitionistic logic into minimal logic. Such translations have been defined for first-order logic.

In this paper, we define a translation, parameterized by monad operators, for higher-order logic. In particular, the property that any formula and its translation are equivalent in the presence of the eliminated axiom holds under functional extensionality and propositional extensionality. We apply this translation to embed higher-order classical (respectively intuitionistic) logic into higher-order intuitionistic (respectively minimal) logic. By adapting Friedman's trick, we show that coherent formulas correspond to a constructive fragment of higher-order classical logic, meaning that we can transform classical proofs into intuitionistic proofs without modifying the proven statements.

**2012 ACM Subject Classification** Theory of computation → Constructive mathematics; Theory of computation → Proof theory; Theory of computation → Higher order logic

**Keywords and phrases** Higher-order logic, Intuitionistic logic, Kuroda's translation, Memo

**Digital Object Identifier** 10.4230/LIPIcs.FSCD.2025.34

**Acknowledgements** I would like to thank Marc Aiguier and Olivier Hermant for their helpful remarks and suggestions.

## 1 Introduction

Intuitionistic logic extends minimal logic with the principle of explosion, which states that any formula can be derived from a contradiction. In minimal logic, contradictions cannot be used to prove any formula. In that sense, minimal logic controls inconsistencies.

$$ \bot \Rightarrow A \qquad (\text{principle of explosion}) $$

$$ A \lor \neg A \qquad (\text{principle of excluded middle}) $$

Classical logic extends intuitionistic logic with the principle of excluded middle, which states that for any formula A, either A or its negation $\neg A$ is true. Crucially, intuitionistic logic has the disjunction property–if $A \lor B$ holds then either A holds or B holds–and the witness property–if $\exists x.A$ holds then there is a term t such that $A[x \leftarrow t]$ holds. In that sense, proofs in intuitionistic logic are constructive.

Provability in intuitionistic logic (respectively minimal logic) trivially entails provability in classical logic (respectively intuitionistic logic). Following Barr's theorem [2], classical provability entails intuitionistic provability for geometric formulas–which are formulas that can only be built using conjunctions, infinite disjunctions, and existential quantifiers. Although Barr's theorem originates from topos theory, a syntactic proof can be found in [17].

In the general case, however, classical provability does not entail intuitionistic provability. To get around this issue, many different embeddings of classical logic into intuitionistic logic have been proposed over the past century. These translations $A \mapsto A^*$ satisfy two properties:

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

(ii) $A^*$ and A are equivalent in classical logic (characterization).

<figure><img src="image_2.png" /></figure>

© Thomas Traversié;

licensed under Creative Commons License CC-BY 4.0

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025).

Editor: Maribel Fernández; Article No. 34; pp. 34:1–34:14

Leibniz International Proceedings in Informatics

<figure><img src="image_3.png" /></figure>

LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 34:2 Monad Translations for Higher-Order Logic

One approach to embed classical logic into intuitionistic logic is to define double-negation translations, that is to insert double negations inside formulas. Glivenko [11] showed that, for any formula *A* that is provable in propositional logic, there exists an intuitionistic proof of its double-negation $\neg\neg A$. Kolmogorov [13], Gödel [12], Gentzen [10], and Kuroda [14] defined double-negation translations for first-order logic. Additionally, Kolmogorov's translation and the Gödel-Gentzen translation embed classical logic into minimal logic.

Friedman [9] developed a transformation of intuitionistic formulas that is parameterized by a formula *R*. The composition of a double-negation translation and Friedman's translation gives rise to a translation from classical logic to intuitionistic logic, in which the double negation is replaced by the operator $A \mapsto (A \Rightarrow R) \Rightarrow R$. The version of Barr's theorem where we only have finitary geometric formulas—called coherent formulas—can be proved using Friedman's translation [18].

So as to generalize even more the double-negation translations, it is possible to resort to *monad operators* instead of double negations. Monad operators are unary connectives *T* that satisfy $A \Rightarrow TA$ and $(A \Rightarrow TB) \Rightarrow (TA \Rightarrow TB)$ for any formulas *A* and *B*. They are called lax modalities in [1], nuclei in [22] and strong monads in [6], and they originate from propositional lax logic [7], topology and category theory. Monad operators have been used to generalize the Gödel-Gentzen translation [6] and Kuroda's translation [22]. These translations eliminate particular axioms, depending on the chosen monad operator, for example the principle of excluded middle or the principle of explosion. Such generic translations are therefore relevant to embed classical logic into intuitionistic logic or intuitionistic logic into minimal logic.

The well-known double-negation translations and their generalizations with monad operators have been defined for *first-order logic*. Brown and Rizkallah [3] showed that Kolmogorov's translation and the Gödel-Gentzen translation cannot be naturally extended to higher-order logic, and they proved that Kuroda's translation can be extended so that the soundness property holds. When we assume both functional extensionality and propositional extensionality, the characterization property also holds [21].

**Contribution.** In this paper, we define a Kuroda-style monad translation for higher-order logic. Depending on the choice of the monad operator, this translation either embeds higher-order classical logic into higher-order intuitionistic logic or embeds higher-order intuitionistic logic into higher-order minimal logic.

Like the extension of double-negation translation to higher-order logic [21], the characterization property holds under functional extensionality and propositional extensionality. Moreover, we underscore conditions under which the soundness property holds in the presence of both functional extensionality and propositional extensionality.

We refine the monad translation for factorizable monad operators, that are monad operators that satisfy $(TA \Rightarrow TB) \Rightarrow T(A \Rightarrow B)$. The factorizable monad translation directly abstracts Kuroda's translation with factorizable monad operators instead of double negations, and it introduces less monad operators in the formulas than the monad translation. It can be used to embed higher-order classical logic into higher-order intuitionistic logic.

When considering higher-order coherent formulas, the monad translation can be used to show that classical provability entails intuitionistic provability and that intuitionistic provability entails minimal provability. In particular, we are able to constructivize any classical proof of a statement that only involves higher-order coherent formulas.

**Outline.** We recall in Section 2 the necessary preliminaries about higher-order logic and monad operators. The monad translation for higher-order logic is defined in Section 3. In Section 4, we show that this translation satisfies the soundness and characterization
properties, and we examine its behavior in the presence of equality. We illustrate how the
monad translation can be used with different monad operators to define embeddings between
logics in Section 5, and we study the particular case of higher-order coherent formulas in
Section 6. In Section 7, we refine the translation for factorizable monad operators.

2 Preliminaries

The syntax and inference rules of higher-order logic are recalled in Section 2.1. The basic
notions about monad operators are summarized in Section 2.2.

**2.1 Higher-Order Logic**

Higher-order logic is modeled using Church's simple type theory [4]. Types are defined inductively: `ι` is the type of individuals, `o` is the type of propositions, and if `τ` and `σ` are types then `τ → σ` is a type. For every type `τ`, let `V_τ` be the set of variables of type `τ` and `C_τ` be a set of constants of type `τ`. The set of variables `V := ⋃_τ V_τ` and the set of constants `C := ⋃_τ C_τ` are assumed to be disjoint. For any set of constants `C`, the sets `Λ_c^τ` of terms of type `τ` are defined by induction:

For every $x \in V_\tau$, $x \in \Lambda_\tau^C$.

For every $c \in C_\tau$, $c \in \Lambda_\tau^C$.

For every $x \in V_\tau$ and $t \in \Lambda_\sigma^C$, then $(\lambda x. t) \in \Lambda_{\tau \to \sigma}^C$.

For every $t \in \Lambda_{\tau \to \sigma}^C$ and $u \in \Lambda_\tau^C$, then $(t \ u) \in \Lambda_\sigma^C$.

`λx. t` is a `λ`-abstraction and `t u` is an application. Computation is introduced in this `λ`-calculus thanks to the `β`-reduction rule (`λx. t`) `u ↦ t[x ← u]`, where `t[x ← u]` corresponds to the term `t` in which `x` has been substituted by `u`. We denote `≡_β` the congruence generated by `β`-reduction. We write `FV(t₁, ..., tₙ)` for the set of free variables that occur in the terms `t₁, ..., tₙ`.

Formulas are terms of type `o`. There are particular constants defining the logical connectives and quantifiers: contradiction `⊥` of type `o`, implication `⇒`, conjunction `∧` and disjunction `∨` of type `o` `→` `o`, and quantifiers `∀τ` and `∃τ` of type `(τ → o) → o`. For convenience, terms of the form `∀τ (λx. A)` and `∃τ (λx. A)` are simply abbreviated as `∀x.A` and `∃x.A`. The negation is defined by `¬A := A ⇒ ⊥` and the logical biconditional `⇔` is defined by `A ⇔ B := (A ⇒ B) ∧ (B ⇒ A)`. Contexts `Γ` are finite sequences of formulas.

In the rest of this paper, we consider a logic L which is either minimal logic (ML), intuitionistic logic (IL), or classical logic (CL). The natural deduction rules for CL are given in Figure 1. In IL, we do not consider the principle of excluded middle PEM, and in ML we neither consider PEM nor the principle of explosion BOT-E. We write Γ ⊢_L A when Γ ⊢ A is derivable in the logic L.

We can also define, for every type τ, an equality symbol `=`τ of type `τ → τ → o`. The symbols are infix, and we write `t = u` when there is no ambiguity on the type τ. The natural deduction rules for equality are given in Figure 2. We write Γ ⊢_L* A with * ∈ {e, cp, cf, efp} when Γ ⊢_L A is derivable with additional inference rules: with EQ-I and EQ-E when e occurs in *, with PROPEXT when p occurs in *, and with FUNEXT when f occurs in *.
34:4 Monad Translations for Higher-Order Logic

<figure><img src="image_4.png" /><figcaption>Figure 1 Natural deduction rules for classical logic.</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Figure 2 Natural deduction rules for equality.</figcaption></figure>

2.2 Monad Operators

We say that *T* is a unary connective when it is a closed term of type *o* → *o*. A unary connective *T* is a monad operator of *L* when the judgments (unit) and (bind) hold for any formulas *A* and *B*.

$$
\vdash_L A \Rightarrow TA \qquad (\text{unit})
$$

$$
\vdash_L (A \Rightarrow TB) \Rightarrow (TA \Rightarrow TB) \qquad (\text{bind})
$$

We use the terminology “monad operator” to avoid any confusion with monads in the sense
of category theory. Monad operators are called lax modalities in [1] and nuclei in [22]. This
definition of monad operators is equivalent to the axiomatization of strong monads in [6].
Following the Curry-Howard correspondence, monad operators coincide with the notion of
monad in programming languages [15], for instance in Haskell.
► **Example 1.** There are many monad operators of minimal logic:

■ $TA := A \lor \bot$,

■ $T_R A := (A \Rightarrow R) \Rightarrow R$, with parameter $R$, which corresponds to the continuation monad,

■ $TA := \neg\neg A$, which is a special case of the previous one with $R := \bot$,

■ $T_R A := (A \Rightarrow R) \Rightarrow A$, with parameter $R$, which corresponds to the Peirce monad [6].

We recall some formulas about monad operators that will be used in the rest of the paper.

► **Proposition 2.** Let $T$ be a monad operator of $L$, and $A$ and $B$ be formulas.

1. $\vdash_L TTA \Leftrightarrow TA$

2. $\vdash_L (A \Rightarrow B) \Rightarrow (TA \Rightarrow TB)$

3. $\vdash_L T(A \land B) \Leftrightarrow (TA \land TB)$

4. $\vdash_L T(A \Rightarrow B) \Rightarrow (TA \Rightarrow TB)$

5. $\vdash_L T(A \Rightarrow TB) \Leftrightarrow (TA \Rightarrow TB)$

6. $\vdash_L T(A \lor B) \Leftrightarrow T(TA \lor TB)$

7. $\vdash_L T(\forall x.TA) \Leftrightarrow \forall x.TA$

8. $\vdash_L T(\exists x.TA) \Leftrightarrow T(\exists x.A)$

*Proof.* We only show the most interesting cases.

■ **Item 3 (⇒):** We have $\vdash_L (A \land B) \Rightarrow A$ and $\vdash_L (A \land B) \Rightarrow B$. Using Item 2 we easily derive $\vdash_L T(A \land B) \Rightarrow (TA \land TB)$.

■ **Item 3 (⇔):** Using (bind), we directly have $\vdash_L (A \Rightarrow T(A \land B)) \Rightarrow TA \Rightarrow T(A \land B)$ and $\vdash_L (B \Rightarrow T(A \land B)) \Rightarrow TB \Rightarrow T(A \land B)$. Using these two facts and (unit), we easily derive $\vdash_L TA \Rightarrow TB \Rightarrow T(A \land B)$. We conclude $\vdash_L (TA \land TB) \Rightarrow T(A \land B)$.

■ **Item 4:** We know that $\vdash_L ((A \Rightarrow B) \land A) \Rightarrow B$. We derive $\vdash_L T((A \Rightarrow B) \land A) \Rightarrow TB$ using Item 2. By Item 3, we get $\vdash_L (T(A \Rightarrow B) \land TA) \Rightarrow TB$, therefore we conclude $\vdash_L T(A \Rightarrow B) \Rightarrow (TA \Rightarrow TB)$.

■ **Item 5 (⇒):** We have $\vdash_L T(A \Rightarrow TB) \Rightarrow (TA \Rightarrow TTB)$ using Item 4. We conclude $\vdash_L T(A \Rightarrow TB) \Rightarrow (TA \Rightarrow TB)$ using Item 1.

■ **Item 5 (⇔):** Using (unit), we derive $\vdash_L (TA \Rightarrow TB) \Rightarrow (A \Rightarrow TB)$ and $\vdash_L (A \Rightarrow TB) \Rightarrow T(A \Rightarrow TB)$. It follows $\vdash_L (TA \Rightarrow TB) \Rightarrow T(A \Rightarrow TB)$.

■ **Item 6 (⇔):** Using (bind), we get $\vdash_L (A \Rightarrow T(A \lor B)) \Rightarrow (TA \Rightarrow T(A \lor B))$ and $\vdash_L (B \Rightarrow T(A \lor B)) \Rightarrow (TB \Rightarrow T(A \lor B))$. Using (unit), we derive $\vdash_L TA \Rightarrow T(A \lor B)$ and $\vdash_L TB \Rightarrow T(A \lor B)$. It follows $\vdash_L (TA \lor TB) \Rightarrow T(A \lor B)$. We conclude using (bind).

■ **Item 7 (⇒):** We easily show $\vdash_L (\forall x.TA) \Rightarrow TA[x \leftarrow y]$ for a fresh variable $y$. Using (bind) we get $\vdash_L T(\forall x.TA) \Rightarrow TA[x \leftarrow y]$. We derive $T(\forall x.TA) \vdash_L TA[x \leftarrow y]$ and therefore $T(\forall x.TA) \vdash_L \forall x.TA$. We conclude $\vdash_L T(\forall x.TA) \Rightarrow \forall x.TA$.

## 3 Monad Translation

The standard double-negation translations [13, 12, 10, 14] have been defined for first-order logic. Several translations generalize them to monad operators [1, 6, 22] and extend them to higher-order logic [3, 21]. We want to define a translation that does both.

Kolmogorov's translation [13] and the Gödel-Gentzen translation [12, 10] cannot be extended to higher-order logic directly [3], because they do not preserve $\beta$-conversion. For example, let us take the Gödel-Gentzen translation of $(\lambda R. R \land Q) P \hookrightarrow P \land Q$. The translation of $(\lambda R. R \land Q) P$ is $(\lambda R. \neg\neg R \land \neg\neg Q) \neg\neg P$, which $\beta$-reduces to $\neg\neg\neg\neg P \land \neg\neg Q$, while the translation of $P \land Q$ is $\neg\neg P \land \neg\neg Q$. Unlike Kolmogorov's translation and the Gödel-Gentzen translation, Kuroda's translation [14] preserves $\beta$-conversion and can be directly extended to higher-order logic [3, 21].
34:6 Monad Translations for Higher-Order Logic

Moreover, a Kuroda-style monad translation [22] has been defined for first-order logic. It corresponds to Kuroda's translation, in which we insert monad operators instead of double negations. It also introduces additional monad operators after implications, and such modification is necessary to generalize Kuroda's translation to any monad operator. We will see in Section 7 how to remove this constraint for particular monad operators.

We define here a Kuroda-style monad translation for higher-order logic, taking advantage of the ideas developed in [21] and [22].

**Definition 3 (Monad translation for higher-order logic).** Let A be a formula in higher-order logic and T be a monad operator. Its monad translation is $A^T := TA_T$, where $t \mapsto t_T$ is inductively defined by:

$$
\begin{align*}
x_T &:= x \\
c_T &:= \left\{ \begin{array}{ll} \lambda p. \quad \forall x.T(p \ x) & \text{if } c = \forall \\ \lambda p. \quad \lambda q. \ p \Rightarrow Tq & \text{if } c = \Rightarrow \\ c & \text{otherwise} \end{array} \right. \\
(\lambda x. \ t)_T &:= \lambda x. \ t_T \\
(t \ u)_T &:= t_T \ u_T
\end{align*}
$$

In first-order logic, we have $(A[z \leftarrow w])^T = A^T[z \leftarrow w]$. As we are in higher-order logic, the substituted term $w$ may be modified by the translation. We would intuitively expect $(A[z \leftarrow w])^T = A^T[z \leftarrow w^T]$, but we actually have $(A[z \leftarrow w])^T = A^T[z \leftarrow w_T]$, because the monad operator in front of the formula is inserted after the inductive translation. It follows that the translation $t \mapsto t_T$ commutes with substitution, but not $A \mapsto A^T$. Both translations $t \mapsto t_T$ and $A \mapsto A^T$ preserve convertibility.

**Proposition 4.** For any term $t$, we have $(t[z \leftarrow w])_T = t_T[z \leftarrow w_T]$.

**Proof.** By induction on the term $t$. ◀

**Corollary 5.** For any higher-order formula $A$, we have $(A[z \leftarrow w])^T = A^T[z \leftarrow w_T]$.

In higher-order logic, terms are considered modulo $\beta$-convertibility. It follows that the translation must preserve $\beta$-convertibility for it to preserve provability.

**Proposition 6.** For any terms $t$ and $u$, if $t \equiv_{\beta} u$ then $t_T \equiv_{\beta} u_T$.

**Proof.** By definition $((\lambda x. t) u)_T = (\lambda x. t_T) u_T$, and we have $(\lambda x. t_T) u_T \leftrightarrow t_T[x \leftarrow u_T]$. Using Proposition 4, we get $((\lambda x. t) u)_T \equiv_{\beta} (t[x \leftarrow u])_T$. Closure by context, convexity, symmetry, and transitivity are immediate. ◀

**Corollary 7.** For any higher-order formulas $A$ and $B$, if $A \equiv_{\beta} B$ then $A^T \equiv_{\beta} B^T$.

## 4 Monad Embedding

The monad translation generalizes double-negation translations with monad operators instead of double negations. Likewise, the monad translation eliminates the use of a particular formula [1, 6], called T-elimination, while double-negation translations eliminate the use of the principle of excluded middle.

$$TA \Rightarrow A \qquad (T\text{-elimination})$$
More formally, we extend the logic L with the inference rule T-ELIM, and we write $Γ ⊢_{L+T} A$ when $Γ ⊢ A$ is derivable using the rules of L and T-ELIM.

$$ \overline{Γ ⊢ TA \Rightarrow A} \quad \text{T-ELIM} $$

The monad translation eliminates any use of the T-ELIM inference rule–this is the soundness property. The characterization property states that any formula and its translation are equivalent assuming T-ELIM.

When extending the double-negation elimination to higher-order logic [21], the characterization property does not trivially hold, but does hold when we consider functional extensionality and propositional extensionality. The same reasoning applies for the extension of the monad translation to higher-order logic.

**► Theorem 8 (Monad embedding).** Let $T$ be a monad operator of L such that we have $شد_۱ (TA)_T \Leftrightarrow TA_T$ for any formula A. Let $Γ, A$ be higher-order formulas.

1. If $Γ ⊢_{L+T} A$ then $Γ_T ⊢_L A^T$.

2. $شد_{L+T}^e A^T \Leftrightarrow A$.

**► Remark 9.** For Kolmogorov's translation and the Gödel-Gentzen translation, the soundness property is stated with $Γ^T$ instead of $Γ_T$. When considering Kuroda's translation, we can actually omit the monad operators at the head of the formulas of the context. The version with $Γ^T$ is provable as well.

**Proof of Theorem 8(1).** We proceed by induction on the derivation. Most of the cases are direct applications of Proposition 2. CONV derives from Corollary 7. We only show the most interesting cases:

- OR-E: Suppose that $Γ_T ⊢_L T(A_T ∨ B_T)$ and $Γ_T, A_T ⊢_L TC_T$ and $Γ_T, B_T ⊢_L TC_T$. To prove $Γ_T ⊢_L TC_T$, it suffices to have $Γ_T ⊢_L T(A_T ∨ B_T) ⇒ TC_T$.

Using the second and third hypotheses, we derive $Γ_T ⊢_L (A_T ∨ B_T) ⇒ TC_T$. Using (bind) we get $Γ_T ⊢_L T(A_T ∨ B_T) ⇒ TC_T$ and we conclude the case.

- ALL-I: Suppose $Γ_T ⊢_L TA_T$. We derive $Γ_T ⊢_L ∀x.TA^T$, that is $Γ_T ⊢_L (∀x.A)_T$. We conclude using (unit).

- ALL-E: Suppose $Γ_T ⊢_L T (∀x.TA_T)$. Using Proposition 2(7), we get $Γ_T ⊢_L ∀x.TA_T$. From ALL-E we obtain $Γ_T ⊢_L (TA_T)[x ← t_T]$. We conclude with Corollary 5.

- Ex-I: Suppose $Γ_T ⊢_L T(A[x ← t])_T$. Using Corollary 5, we get $Γ_T ⊢_L TA_T[x ← t_T]$. From Ex-I we obtain $Γ_T ⊢_L ∃x.TA_T$. We conclude using (unit) and Proposition 2(8).

- Ex-E: Suppose $Γ_T ⊢_L T (∃x.A_T)$ and $Γ_T, A_T ⊢_L TC_T$. To conclude the proof, it suffices to have $Γ_T ⊢_L T (∃x.A_T) ⇒ TC_T$.

We have $Γ_T, ∃x.A_T ⊢_L ∃x.A_T$ (by Ax) and $Γ_T, ∃x.A_T, A_T ⊢_L TC_T$ (by weakening of the second hypothesis). Using Ex-E, we derive $Γ_T, ∃x.A_T ⊢_L TC_T$ and therefore $Γ_T ⊢_L (∃x.A_T) ⇒ TC_T$. Using (bind), we obtain $Γ_T ⊢_L T (∃x.A_T) ⇒ TC_T$ and we conclude the case.

- Bot-E: Suppose $Γ_T ⊢_L T ⊥$. As we are in intuitionistic logic, we have $Γ_T ⊢_L ⊥ ⇒ A_T$. We deduce $Γ_T ⊢_L T ⊥ ⇒ TA_T$ using Proposition 2(2). We conclude $Γ_T ⊢_L TA_T$.

- PEM: As we are in classical logic, we have $Γ_T ⊢_L A_T ∨ (A_T ⇒ ⊥)$. Using (unit), we derive $Γ_T ⊢_L A_T ∨ (A_T ⇒ T ⊥)$ and then we conclude $Γ_T ⊢_L T(A_T ∨ (A_T ⇒ T ⊥))$.

- T-ELIM: We have $(TA ⇒ A)_T = ((TA)_T ⇒ TA_T)$. We know $شد_۱ (TA)_T \Leftrightarrow TA_T$, so we derive $Γ_T ⊢_L (TA ⇒ A)_T$. We conclude $Γ_T ⊢_L T (TA ⇒ A)_T$ using (unit).

<figure><img src="image_6.png" /></figure>
34:8 Monad Translations for Higher-Order Logic

Before proving the second item of Theorem 8, we show the following lemma, stating that any term and its translation are equal, assuming T-ELIM, functional extensionality and propositional extensionality.

► **Lemma 10.** For any term $t$, we have $\vdash_{L+T}^{\mathcal{E}fp} t_T = t$.

**Proof.** We proceed by induction on the term $t$. We directly have $\vdash_{L+T}^{\mathcal{E}fp} x_T = x$ and $\vdash_{L+T}^{\mathcal{E}fp} c_T = c$ for $c \notin \{\forall, \Rightarrow\}$. For $c \in \{\forall, \Rightarrow\}$, we derive $\vdash_{L+T}^{\mathcal{E}fp} c_T = c$ from PROPEXT, FUNEXT, T-ELIM and (unit). We have $\vdash_{L+T}^{\mathcal{E}fp} (t u)_T = t u$ using the induction hypotheses and EQ-E. We derive $\vdash_{L+T}^{\mathcal{E}fp} (\lambda x. t)_T = \lambda x. t$ using the induction hypothesis and FUNEXT. ◀

**Proof of Theorem 8(2).** We derive $\vdash_{L+T}^{\mathcal{E}fp} A_T \Leftrightarrow A$ using Lemma 10, and then we conclude $\vdash_{L+T}^{\mathcal{E}fp} A^T \Leftrightarrow A$ using (unit) and T-ELIM. ◀

We proved that the monad translation satisfies the soundness and characterization properties. For the characterization property, we had to introduce symbols of equality and to assume both functional extensionality and propositional extensionality. But does the soundness property still hold in the presence of equality?

The proof of the soundness property does not naturally extend when we consider the symbols and inference rules of equality. Let us consider the formulas

$$ \forall x \forall y. T(x = y) \Rightarrow x = y \qquad (\Delta^{\mathcal{E}f}) $$

$$ \forall x \forall y. (Tx = Ty) \Rightarrow x = y \qquad (\Delta^{\mathcal{E}p}) $$

regarding $T$ and equality predicates. We write $\Delta^{\mathcal{E}fp}$ for the context $\Delta^{\mathcal{E}f}$, $\Delta^{\mathcal{E}p}$. When proving the soundness property in the presence of equality, the first formula $\Delta^{\mathcal{E}f}$ is useful for the FUNEXT case and the second formula $\Delta^{\mathcal{E}p}$ is useful for the PROPEXT case.

► **Theorem 11 (Soundness for equality).** Let $T$ be a monad operator of $L$ such that we have $\vdash_L (TA)_T \Leftrightarrow TA_T$ for any formula $A$. Let $\Gamma, A$ be higher-order formulas.

1. If $\Gamma \vdash_{L+T}^{\mathcal{E}} A$ then $\Gamma_T \vdash_L^{\mathcal{E}} A^T$.

2. For $* \in \{\mathcal{E}f, \mathcal{E}p, \mathcal{E}fp\}$, if $\Gamma \vdash_{L+T}^{\mathcal{E}} A$ then $\Delta^*, \Gamma_T \vdash_L^{\mathcal{E}} A^T$.

**Proof.** For the first item, we complete the proof of Theorem 8 with the following cases:

- **EQ-I:** We directly use EQ-I and (unit).

- **EQ-E:** Suppose $\Gamma_T \vdash_L^* TA_T[x \leftarrow u_T]$ and $\Gamma_T \vdash_L^* T(u_T = v_T)$. Using EQ-E, we derive $\vdash_L^* A_T[x \leftarrow u_T] \Rightarrow (u_T = v_T) \Rightarrow A_T[x \leftarrow v_T]$. Therefore, we get $\vdash_L^* TA_T[x \leftarrow u_T] \Rightarrow T(u_T = v_T) \Rightarrow TA_T[x \leftarrow v_T]$ using Proposition 2(2) and Proposition 2(4). We conclude $\Gamma_T \vdash_L^* TA_T[x \leftarrow v_T]$.

For the second item, most cases are those of the first item that are reused using weakening on $\Delta^*$. The remaining cases are:

- **FUNEXT:** Suppose $\Delta^*, \Gamma_T \vdash_L^* T(f_T x = g_T x)$. Since $x \notin FV(\Gamma, f, g)$, we directly have $x \notin FV(\Gamma_T, f_T, g_T)$. We get $\Delta^*, \Gamma_T \vdash_L^* f_T x = g_T x$ using $\Delta^{\mathcal{E}f}$. We conclude using FUNEXT and (unit).

- **PROPEXT:** Suppose $\Delta^*, \Gamma_T \vdash_L^* T(A_T \Rightarrow TB_T)$ and $\Delta^*, \Gamma_T \vdash_L^* T(B_T \Rightarrow TA_T)$. Using Proposition 2(5), we get $\Delta^*, \Gamma_T \vdash_L^* TA_T \Rightarrow TB_T$ and $\Delta^*, \Gamma_T \vdash_L^* TB_T \Rightarrow TA_T$. Using PROPEXT we derive $\Delta^*, \Gamma_T \vdash_L^* TA_T = TB_T$. We conclude using $\Delta^{\mathcal{E}p}$ and (unit). ◀

When extending Kuroda's double-negation translation to higher-order logic [21], we only considered the formula $\Delta^{\mathcal{E}f}$. The generalization to any monad operator requires us to additionally consider the formula $\Delta^{\mathcal{E}p}$. In Section 7, we will see that this additional assumption can be dropped when considering factorizable monad operators.
# 5 Embeddings between Logics

Such monad translation can be directly applied with particular monad operators to embed classical logic into intuitionistic logic or intuitionistic logic into minimal logic.

There are many classical laws, such as the principle of excluded middle, the double-negation elimination, Peirce's law, or Clavius's law. All these laws are equivalent in intuitionistic logic.

$$ \neg\neg A \Rightarrow A \qquad (\text{double-negation elimination}) $$

$$ (\neg A \Rightarrow A) \Rightarrow A \qquad (\text{Clavius's law}) $$

$$ ((A \Rightarrow B) \Rightarrow A) \Rightarrow A \qquad (\text{Peirce's law}) $$

The T-elimination principle corresponds to the double-negation elimination when we choose $TA := (A \Rightarrow \bot) \Rightarrow \bot$ and to Clavius's law when we choose $TA := (A \Rightarrow \bot) \Rightarrow A$. For these monad operators, the T-ELIM inference rule is therefore equivalent to PEM, and eliminating any use of T-ELIM in the derivations means transforming classical provability into intuitionistic provability. When $T_R A := (A \Rightarrow R) \Rightarrow A$, the T-elimination principle only corresponds to an instance of Peirce's law with $B := R$.

**► Corollary 12 (Embeddings of classical logic into intuitionistic logic).** Let $\Gamma, A$ be higher-order formulas.

1. If $\Gamma \vdash_{\text{CL}} A$ then $\Gamma_T \vdash_{\text{IL}} A^T$ with $TA := (A \Rightarrow \bot) \Rightarrow \bot$.

2. If $\Gamma \vdash_{\text{CL}} A$ then $\Gamma_T \vdash_{\text{IL}} A^T$ with $TA := (A \Rightarrow \bot) \Rightarrow A$.

3. If $\Gamma \vdash_{\text{CL}} A$ then there exists a formula $R$ such that $\Gamma_{T_R} \vdash_{\text{IL}} A^{T_R}$ with $T_R A := (A \Rightarrow R) \Rightarrow A$. Moreover, for each of the above, we have $\vdash_{\text{CL}} A^T \Leftrightarrow A$.

**Proof.** We apply Theorem 8 with $L := \text{IL}$. T-ELIM is equivalent to PEM, so $\text{IL}+T$ corresponds to CL. For the third item, we have to give the correct parameter $R$. The derivation $\Gamma \vdash_{\text{CL}} A$ is finite, so Peirce's law is used a finite number of times with formulas $B_1, \dots, B_n$ of free variables $\vec{x}_1, \dots, \vec{x}_n$. Such free variables could be captured later in the derivation. As remarked by Escardó and Oliva [6], $T_{R_1} \wedge R_2 A \Rightarrow A \vdash_{\text{IL}} (T_{R_1} A \Rightarrow A) \wedge (T_{R_2} A \Rightarrow A)$. With the additional remark that $T_{\forall x.R} A \Rightarrow A \vdash_{\text{IL}} T_{R[x \leftarrow t]} A \Rightarrow A$, we define $R$ to be the conjunction $\forall \vec{x}_1.B_1 \wedge \dots \wedge \forall \vec{x}_n.B_n$, so that the monad translation eliminates the $n$ instances of Peirce's law that occur in the derivation. ◀

When $TA := A \lor \bot$, the T-elimination principle is equivalent to the principle of explosion, and the T-ELIM inference rule is therefore equivalent to the BOT-E inference rule. In that case, eliminating any use of T-ELIM in the derivations means transforming intuitionistic provability into minimal provability.

**► Corollary 13 (Embedding of intuitionistic logic into minimal logic).** Let $\Gamma, A$ be higher-order formulas. If $\Gamma \vdash_{\text{IL}} A$ then $\Gamma_T \vdash_{\text{ML}} A^T$ with $TA := A \lor \bot$. Moreover, we have $\vdash_{\text{IL}} A^T \Leftrightarrow A$.

**Proof.** We apply Theorem 8 with $L := \text{ML}$. T-ELIM is equivalent to BOT-E, so $\text{ML}+T$ corresponds to $\text{IL}$. ◀

# 6 Fragment of Coherent Formulas

Coherent formulas are formulas that can only be built using conjunctions, disjunctions and existential quantifiers. Because monad operators are only inserted after universal quantifiers and implications, it follows that $A_T = A$ for any coherent formula $A$. We lift to higher-order logic two tricks for coherent formulas that rely on this observation.
34:10 Monad Translations for Higher-Order Logic

The first trick [5, 22] allows us to derive minimal provability from intuitionistic provability when the context is empty and when the formula is coherent.

**Corollary 14.** Let $\Gamma, A$ be higher-order coherent formulas. If $\vdash_{\mathbf{IL}} A$ then $\vdash_{\mathbf{ML}} A$.

**Proof.** Suppose $\vdash_{\mathbf{IL}} A$. We apply Theorem 8 with $TA := A \lor \bot$, and we derive $\vdash_{\mathbf{ML}} TA_T$, that is $\vdash_{\mathbf{ML}} A \lor \bot$. We know that minimal logic has the disjunction property, and that we cannot prove $\bot$. Hence, we conclude $\vdash_{\mathbf{ML}} A$. ◀

The second trick [18, 22] allows us to derive intuitionistic provability from classical provability when the formulas involved are coherent. It corresponds to a weaker version–with finite disjunctions–of Barr’s theorem [2] extended to higher-order logic.

**Theorem 15.** Let $\Gamma, A$ be higher-order coherent formulas. If $\Gamma \vdash_{\mathbf{CL}} A$ then $\Gamma \vdash_{\mathbf{IL}} A$.

To prove this result, we adapt to higher-order logic Palmgren’s idea [18] of using Friedman’s translation [9]. As an intermediary lemma, we prove that, for higher-order logic, Friedman’s translation transforms classical proofs into intuitionistic proofs. Remark that we cannot directly apply Theorem 8, as the T-elimination principle does not correspond to a classical law when $TA := (A \Rightarrow R) \Rightarrow R$.

**Lemma 16.** Let $TA := (A \Rightarrow R) \Rightarrow R$ with parameter $R$. Let $\Gamma, A$ be higher-order formulas. If $\Gamma \vdash_{\mathbf{CL}} A$ then $\Gamma \vdash_{\mathbf{IL}} A^T$.

**Proof.** We proceed by induction on the derivation. All the cases are similar to the cases of Theorem 8, except that we do not need the T-ELIM case anymore, and that we change the PEM case. We prove $\Gamma_T \vdash_{\mathbf{IL}} T(A \lor \neg A)_T$ using

$$ \frac{\frac{\frac{\Gamma_T, B \Rightarrow R, A_T, \bot \Rightarrow R \vdash_{\mathbf{IL}} A_T}{\Gamma_T, B \Rightarrow R, A_T, \bot \Rightarrow R \vdash_{\mathbf{IL}} B}}{\Gamma_T, B \Rightarrow R, A_T, \bot \Rightarrow R \vdash_{\mathbf{IL}} R} \qquad \begin{array}{l} \text{AX} \\ \text{OR-IL} \\ \text{IMP-E with } B \Rightarrow R \end{array}}{\frac{\frac{\Gamma_T, B \Rightarrow R \vdash_{\mathbf{IL}} A_T \Rightarrow ((\bot \Rightarrow R) \Rightarrow R)}{\Gamma_T, B \Rightarrow R \vdash_{\mathbf{IL}} B}}{\Gamma_T, B \Rightarrow R \vdash_{\mathbf{IL}} R}} \qquad \begin{array}{l} \text{IMP-I} \times 2 \\ \text{OR-IR} \\ \text{IMP-E with } B \Rightarrow R \end{array}}{\Gamma_T \vdash_{\mathbf{IL}} ((A \lor (A \Rightarrow ((\bot \Rightarrow R) \Rightarrow R))) \Rightarrow R) \Rightarrow R} \qquad \text{IMP-I} $$

where $B$ is an abbreviation for the formula $A_T \lor (A_T \Rightarrow ((\bot \Rightarrow R) \Rightarrow R))$. ◀

**Proof of Theorem 15.** Suppose $\Gamma \vdash_{\mathbf{CL}} A$. Without loss of generality, we assume that $\Gamma$ and $A$ have no free variables, as we can replace them by fresh constants. We apply Lemma 16, and we derive $\Gamma_{T_R} \vdash_{\mathbf{IL}} T_R A_{T_R}$, that is $\Gamma \vdash_{\mathbf{IL}} (A \Rightarrow R) \Rightarrow R$. Choosing $R := A$, we get $\Gamma \vdash_{\mathbf{IL}} A$. ◀

In other words, coherent formulas correspond to a constructive fragment of higher-order classical logic. Constructive fragments of classical logic have been studied for propositional logic [11, 12] and first-order logic [19]. This is the first time, to our knowledge, that such results are proved for higher-order logic.

7 Refinement for Factorizable Monad Operators

So far, we have generalized Kuroda’s translation to any monad operator, at the expense of the insertion of additional monad operators after implications. In this section, we refine the translation for factorizable monad operators. Monad operators of $\mathbf{L}$ are factorizable when they satisfy the (factorization) judgment for any propositions $A$ and $B$.

$$ \vdash_{\mathbf{L}} (TA \Rightarrow TB) \Rightarrow T(A \Rightarrow B) \qquad \text{(factorization)} $$
For instance, (factorization) holds for $T_R A := (A \Rightarrow R) \Rightarrow A$ in minimal logic and for $TA := (A \Rightarrow \bot) \Rightarrow \bot$ in intuitionistic logic.

## 7.1 Factorizable Monad Translation

For factorizable monad operators, we do not need to insert a monad operator in the implication case of the translation [22]. In that sense, the factorizable monad translation is a direct abstraction of Kuroda's translation, in which double negations have been replaced by factorizable monad operators.

**► Definition 17 (Factorizable monad translation for higher-order logic).** Let $A$ be a formula in higher-order logic and $T$ be a factorizable monad operator. Its factorizable monad translation is $A^{\tilde{T}} := TA_{\tilde{T}}$, where $t \mapsto t_{\tilde{T}}$ is inductively defined by:

$$ 
\begin{align*}
x_{\tilde{T}} &:= x \\
c_{\tilde{T}} &:= \begin{cases} \lambda p. \forall x.T(p x) & \text{if } c = \forall \\ c & \text{otherwise} \end{cases} \\
(\lambda x. t)_{\tilde{T}} &:= \lambda x. t_{\tilde{T}} \\
(t u)_{\tilde{T}} &:= t_{\tilde{T}} u_{\tilde{T}}
\end{align*}
$$

The translation $t \mapsto t_{\tilde{T}}$ and $A \mapsto A^{\tilde{T}}$ satisfy the same properties as $t \mapsto t_T$ and $A \mapsto A^T$ concerning substitution and convertibility.

**► Proposition 18.** Let $t$ and $u$ be terms, and $A$ and $B$ be higher-order formulas.

1. $(t[z \leftarrow w])_{\tilde{T}} = t_{\tilde{T}}[z \leftarrow w_{\tilde{T}}]$.

2. $(A[z \leftarrow w])^{\tilde{T}} = A^{\tilde{T}}[z \leftarrow w_{\tilde{T}}]$.

3. If $t \equiv_{\beta} u$ then $t_{\tilde{T}} \equiv_{\beta} u_{\tilde{T}}$.

4. If $A \equiv_{\beta} B$ then $A^{\tilde{T}} \equiv_{\beta} B^{\tilde{T}}$.

*Proof.* We adapt the proofs of Proposition 4, Corollary 5, Proposition 6 and Corollary 7. ◀

<figure><img src="image_7.png" /></figure>

## 7.2 Factorizable Monad Embedding

The factorizable monad translation satisfies the soundness and characterization properties. It only applies to factorizable monad operators, but it simplifies the monad translation, as it introduces fewer monad operators while satisfying the same result.

**► Theorem 19 (Factorizable monad embedding).** Let $T$ be a factorizable monad operator of $L$ such that $\vdash_L (TA)_{\tilde{T}} \Leftrightarrow TA_{\tilde{T}}$ for any formula $A$. Let $\Gamma, A$ be higher-order formulas.

1. If $\Gamma \vdash_{L+T} A$ then $\Gamma_{\tilde{T}} \vdash_L A^{\tilde{T}}$.

2. $\vdash_{L+T} A^{\tilde{T}} \Leftrightarrow A$.

*Proof.* We prove the first item by induction on the derivation. Most of the cases are the same as for Theorem 8. CONV derives from Proposition 18. We only show the proof of the cases that differ:

- IMP-I: Suppose that $\Gamma_{\tilde{T}}, A_{\tilde{T}} \vdash_L TB_{\tilde{T}}$. We get $\Gamma_{\tilde{T}} \vdash_L A_{\tilde{T}} \Rightarrow TB_{\tilde{T}}$, and we derive $\Gamma_{\tilde{T}} \vdash_L TA_{\tilde{T}} \Rightarrow TB_{\tilde{T}}$ using (bind). We conclude $\Gamma_{\tilde{T}} \vdash_L T(A_{\tilde{T}} \Rightarrow B_{\tilde{T}})$ using (factorization).

- IMP-E: Suppose that $\Gamma_{\tilde{T}} \vdash_L T(A_{\tilde{T}} \Rightarrow B_{\tilde{T}})$ and $\Gamma_{\tilde{T}} \vdash_L TA_{\tilde{T}}$. We get $\Gamma_{\tilde{T}} \vdash_L TA_{\tilde{T}} \Rightarrow TB_{\tilde{T}}$ using Proposition 2(4). We conclude $\Gamma_{\tilde{T}} \vdash_L TB_{\tilde{T}}$ using IMP-E.
■ **T-ELIM**: We directly have $\Gamma_{\tilde{T}} \vdash_L TTA_{\tilde{T}} \Rightarrow TA_{\tilde{T}}$ using Proposition 2(1). We derive $\Gamma_{\tilde{T}} \vdash_L T(TA_{\tilde{T}} \Rightarrow A_{\tilde{T}})$ using (factorization). Since we know $\vdash_L (TA)_{\tilde{T}} \Leftrightarrow TA_{\tilde{T}}$, we conclude $\Gamma_{\tilde{T}} \vdash_L T(TA \Rightarrow A)_{\tilde{T}}$.

For the second item, we show $\vdash_{L+T}^{\epsilon,fp} t_{\tilde{T}} = t$ by adapting the proof of Lemma 10. It follows that $\vdash_{L+T}^{\epsilon,fp} A_{\tilde{T}} \Leftrightarrow A$. We conclude $\vdash_{L+T}^{\epsilon,fp} A^{\tilde{T}} \Leftrightarrow A$ using (unit) and T-ELIM). ◀

In the presence of equality, the soundness property for the factorizable monad translation is simplified compared to the one for the monad translation. We can drop the formula $\Delta^{\epsilon p}$ of Theorem 11, as the PROPEXT case can now be proved without any additional hypothesis.

**Theorem 20 (Soundness for equality).** Let $T$ be a factorizable monad operator of $L$ such that $\vdash_L (TA)_{\tilde{T}} \Leftrightarrow TA_{\tilde{T}}$ for any formula $A$. Let $\Gamma, A$ be higher-order formulas.

1. For $* \in \{e, cp\}$, if $\Gamma \vdash_{L+T}^* A$ then $\Gamma_{\tilde{T}} \vdash_L^* A^{\tilde{T}}$.

2. For $* \in \{ef, cfp\}$, if $\Gamma \vdash_{L+T}^* A$ then $\Delta^{\epsilon f}, \Gamma_{\tilde{T}} \vdash_L^* A^{\tilde{T}}$.

*Proof.* For the first item, we complete the proof of Theorem 19 with the following cases:

■ **EQ-I** and **EQ-E**: The proofs are the same as for Theorem 11.

■ **PROPEXT**: Suppose $\Gamma_{\tilde{T}} \vdash_L^* T(A_{\tilde{T}} \Rightarrow B_{\tilde{T}})$ and $\Gamma_{\tilde{T}} \vdash_L^* T(B_{\tilde{T}} \Rightarrow A_{\tilde{T}})$. Using PROPEXT we have $\vdash_L^* (A_{\tilde{T}} \Rightarrow B_{\tilde{T}}) \Rightarrow (B_{\tilde{T}} \Rightarrow A_{\tilde{T}}) \Rightarrow (A_{\tilde{T}} = B_{\tilde{T}})$, and we get $\vdash_L^* T(A_{\tilde{T}} \Rightarrow B_{\tilde{T}}) \Rightarrow T(B_{\tilde{T}} \Rightarrow A_{\tilde{T}}) \Rightarrow T(A_{\tilde{T}} = B_{\tilde{T}})$ using Proposition 2(2) and Proposition 2(4). We conclude $\Gamma_{\tilde{T}} \vdash_L^* T(A_{\tilde{T}} = B_{\tilde{T}})$.

For the second item, we reuse most cases of the first item using weakening on $\Delta^{\epsilon f}$. The case **FUNEXT** corresponds to the one of Theorem 11, with $\Delta^{\epsilon f}$ instead of $\Delta^*$.

Unlike the monad translation of Section 3, the factorizable monad translation allows us to fully recover the specific behavior of the extension of Kuroda’s double-negation translation to higher-order logic [21]. Specifically, monad operators are not inserted after implications, and the extra assumption $\Delta^{\epsilon p}$ is not needed for the soundness property in the presence of propositional equality.

## 7.3 Additional Embeddings between Logics

The embeddings of classical logic into intuitionistic logic of Corollary 12 are also valid with the factorizable monad translation. These embeddings introduce fewer monad operators than the monad translation.

**Corollary 21 (Embeddings of classical logic into intuitionistic logic).** Let $\Gamma, A$ be higher-order formulas.

1. If $\Gamma \vdash_{CL} A$ then $\Gamma_{\tilde{T}} \vdash_{IL} A^{\tilde{T}}$ with $TA := (A \Rightarrow \bot) \Rightarrow \bot$.

2. If $\Gamma \vdash_{CL} A$ then $\Gamma_{\tilde{T}} \vdash_{IL} A^{\tilde{T}}$ with $TA := (A \Rightarrow \bot) \Rightarrow A$.

3. If $\Gamma \vdash_{CL} A$ then there exists a formula $R$ such that $\Gamma_{\tilde{T}_R} \vdash_{IL} A^{\tilde{T}_R}$ with $T_R A := (A \Rightarrow R) \Rightarrow A$. Moreover, for each of the above, we have $\vdash_{CL}^{\epsilon,fp} A^{\tilde{T}} \Leftrightarrow A$.

*Proof.* The proof is the one of Corollary 12, but using Theorem 19 instead of Theorem 8. ◀

**Remark 22.** Kuroda’s translation embeds classical logic into intuitionistic logic. It can also embed classical logic into minimal logic when the classical inference rule considered is either PEM or DNE1.

$$ \underline{\Gamma \vdash A \lor \neg A} \quad \text{PEM} $$

$$ \frac{\Gamma \vdash \neg\neg A}{\Gamma \vdash A} \quad \text{DNE1} $$

$$ \underline{\Gamma \vdash \neg\neg A \Rightarrow A} \quad \text{DNE2} $$
But Kuroda's translation does not embed classical logic into minimal logic when we consider DNE2. As noted by Ferreira and Oliva [8], the modified Kuroda's translation, in which double negations are also inserted after implications, does embed classical logic into minimal logic, regardless of the classical inference rule considered. This is because the double-negation operator $TA := (A \Rightarrow \bot) \Rightarrow \bot$ satisfies the (factorization) property in intuitionistic logic, but not in minimal logic.

## 8 Conclusion and Future Work

We defined two monad embeddings for higher-order logic: the monad translation and the factorizable monad translation. The former broadens the scope of Kuroda's translation to any monad operator, but it additionally introduces monad operators after implications as a trade-off. The latter directly generalizes Kuroda's translation to factorizable monad operators. For both translations, the soundness property holds. As we are in higher-order logic, the characterization property holds when we assume both functional extensionality and propositional extensionality. We gave conditions so that the soundness property holds in the presence of functional extensionality and propositional extensionality.

These results generalize to monad operators the approach taken for extending Kuroda's translation to higher-order logic [21], and they extend to higher-order logic the approach taken for generalizing the double-negation translations to monad operators [1, 6, 22]. The monad translation and the factorizable monad translation entail various embeddings–depending on the monad operator and on the translation–of higher-order classical logic into higher-order intuitionistic logic, and of higher-order intuitionistic logic into higher-order minimal logic.

For higher-order coherent formulas, we even showed that intuitionistic provability entails minimal provability, and that classical provability entails intuitionistic provability. Coherent formulas therefore correspond to a constructive fragment of higher-order classical logic: for this fragment, we have provided an algorithm that transforms any classical proof into an intuitionistic proof.

Although originating from topos theory, Barr's theorem admits proof-theoretical demonstrations for the first-order finitary case [18, 16] and the first-order infinitary case [20, 17]. We gave a proof of the higher-order finitary case, by extending Palmgren's idea [18] of using Friedman's translation. The higher-order infinitary case remains to be investigated. In particular, simple type theory–used to model higher-order logic–is not sufficient to model an infinitary disjunction.

## References

1. Peter Aczel. The Russell-Prawitz modality. *Mathematical Structures in Comp. Sci.*, 11(4):541-554, August 2001. doi:10.1017/S0960129501003309.

2. Michael Barr. Toposes without points. *Journal of Pure and Applied Algebra*, 5(3):265-280, 1974. doi:10.1016/0022-4049(74)90037-1.

3. Chad E. Brown and Christine Rizkallah. Glivenko and Kuroda for simple type theory. *The Journal of Symbolic Logic*, 79(2):485-495, 2014. doi:10.1017/JSL.2013.10.

4. Alonzo Church. A Formulation of the Simple Theory of Types. *The Journal of Symbolic Logic*, 5(2):56-68, 1940. doi:10.2307/2266170.

5. Almudena Colacito, Dick de Jongh, and Ana Lucia Vargas. Subminimal negation. *Soft Computing*, 21:165-174, 2016. doi:10.1007/s00500-016-2391-8.

6. Martín Escardó and Paulo Oliva. The Peirce translation. *Annals of Pure and Applied Logic*, 163(6):681-692, 2012. Computability in Europe 2010. doi:10.1016/j.apal.2011.11.002.
34:14 Monad Translations for Higher-Order Logic

7 Matt Fairtlough and Michael Mendler. Propositional Lax Logic. *Information and Computation*, 137:1-33, 1997. doi:10.1006/inco.1997.2627.

8 Gilda Ferreira and Paulo Oliva. On the Relation Between Various Negative Translations. In Ulrich Berger, Hannes Diener, Peter Schuster, and Monika Seisenberger, editors, *Logic, Construction, Computation*, pages 227-258. De Gruyter, Berlin, Boston, 2012. doi:10.1515/9783110324921.227.

9 Harvey Friedman. Classically and intuitionistically provably recursive functions. In Gert H. Müller and Dana S. Scott, editors, *Higher Set Theory*, pages 21-27, Berlin, Heidelberg, 1978. Springer Berlin Heidelberg.

10 Gerhard Gentzen. Die Widerspruchsfreiheit der Reinen Zahlentheorie. *Mathematische Annalen*, 112:493-565, 1936.

11 Valery Glivenko. Sur quelques points de la logique de M. Brouwer. *Bulletins de la classe des sciences*, 15:183-188, 1928.

12 Kurt Gödel. Zur intuitionistischen Arithmetik und Zahlentheorie. *Ergebnisse eines Mathematischen Kolloquiums*, 4:34-38, 1933.

13 Andrey Nikolaevich Kolmogorov. O principe tertium non datur. *Matematicheski Sbornik*, 32:646-667, 1925.

14 Sigekatu Kuroda. Intuitionistische Untersuchungen der formalistischen Logik. *Nagoya Mathematical Journal*, 2:35-47, 1951. doi:10.1017/S0027763000010023.

15 Eugenio Moggi. Notions of computation and monads. *Information and Computation*, 93(1):55-92, 1991. Selections from 1989 IEEE Symposium on Logic in Computer Science. doi:10.1016/0890-5401(91)90052-4.

16 Sara Negri. Contraction-free sequent calculi for geometric theories with an application to Barr's theorem. *Archive for Mathematical Logic*, 42:389-401, May 2003. doi:10.1007/s001530100124.

17 Sara Negri. Geometric rules in infinitary logic. In Ofer Arieli and Anna Zamansky, editors, *Arnon Avron on Semantics and Proof Theory of Non-Classical Logics*, pages 265-293. Springer International Publishing, Cham, 2021. doi:10.1007/978-3-030-71258-7_12.

18 Erik Palmgren. An Intuitionistic Axiomatisation of Real Closed Fields. *Mathematical Logic Quarterly*, 48(2):297-299, 2002. doi:10.1002/1521-3870(200202)48:2\%3C297::AID-MALQ297\%3E3.O.CO;2-G.

19 Luiz Carlos Pereira and Edward Hermann Haeusler. On constructive fragments of classical logic. In Heinrich Wansing, editor, *Dag Prawitz on Proofs and Meaning*, pages 281-292. Springer International Publishing, Cham, 2015. doi:10.1007/978-3-319-11041-7_12.

20 Michael Rathjen. Remarks on Barr's Theorem: Proofs in Geometric Theories. In Dieter Probst and Peter Schuster, editors, *Concepts of Proof in Mathematics, Philosophy, and Computer Science*, pages 347-374. De Gruyter, Berlin, Boston, 2016. doi:10.1515/9781501502620-019.

21 Thomas Traversié. Kuroda's Translation for Higher-Order Logic. Submitted, April 2024. doi:10.48550/arXiv.2404.19503.

22 Benno van den Berg. A Kuroda-style j-translation. *Archive for Mathematical Logic*, 58(5-6):627-634, August 2019. doi:10.1007/s00153-018-0656-x.