Relative normalization

Gilles Dowek, Alexandre Miquel

► To cite this version:

Gilles Dowek, Alexandre Miquel. Relative normalization. 2007. hal-04259519v2

HAL Id: hal-04259519

https://inria.hal.science/hal-04259519v2

Preprint submitted on 30 Oct 2023

**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 CC BY 4.0 - Attribution - International License
# Relative normalization

Gilles Dowek¹ and Alexandre Miquel²

¹ École polytechnique and INRIA
LIX, École polytechnique, 91128 Palaiseau cedex, France
Gilles.Dowek@polytechnique.fr

² Université Paris 7,
PPS, 175 Rue du Chevaleret, 75013 Paris, France
Alexandre.Miquel@pps.jussieu.fr

Gödel's second incompleteness theorem forbids to prove, in a given theory $\mathcal{U}$, the consistency of many theories—in particular, of the theory $\mathcal{U}$ itself—as well as it forbids to prove the normalization property for these theories, since this property implies their consistency. When we cannot prove in a theory $\mathcal{U}$ the consistency of a theory $\mathcal{T}$, we can try to prove a relative consistency theorem, that is, a theorem of the form:

> If $\mathcal{U}$ is consistent then $\mathcal{T}$ is consistent.

Following the same spirit, we show in this paper how to prove relative normalization theorems, that is, theorems of the form:

> If $\mathcal{U}$ is 1-consistent, then $\mathcal{T}$ has the normalization property.

## 1 An abstract consistency result

To prove that a theory $\mathcal{T}$ is consistent provided the theory $\mathcal{U}$ is, we usually assume given a model of $\mathcal{U}$ and we build a model of $\mathcal{T}$. When the domain of the model of $\mathcal{T}$ is a subset of the domain of the model of $\mathcal{U}$—which is called an internal model—we can however proceed in a slightly different way: instead of mapping a formula $A$ of $\mathcal{T}$ to a truth value $[[A]]_\phi$ (depending on an assignment $\phi$) we can translate it into a formula $A^*$ of $\mathcal{U}$ that expresses that the truth value associated to $A$ is 1. And instead of proving that $\mathcal{T} \vdash A$ entails $[[A]]_\phi = 1$, we prove that $\mathcal{T} \vdash A$ entails $\mathcal{U} \vdash A^*$. Finally, if $\perp^*$ is $\perp$ (or any equivalent formula in $\mathcal{U}$) and if the theory $\mathcal{U}$ is consistent, then the theory $\mathcal{T}$ is consistent too.

Unlike the method based on model extrusion, the method by which formulæ of $\mathcal{T}$ are directly translated as formulæ of $\mathcal{U}$ does not require to take care of the free variables of $A$ with an assignment: free variables of $A$ just remain free variables of $A^*$, after being possibly renamed.

This way of proving the consistency of $\mathcal{T}$ is quite different from proving in $\mathcal{U}$ the existence of a model of $\mathcal{T}$, as we do not need to define a domain of interpretation: all the universe of discourse of the theory $\mathcal{U}$—or part of it—can serve as domain. Thus this method can be applied also in cases where the existence of a model of $\mathcal{T}$ can not be proved in $\mathcal{U}$.

**Definition 1.** — An interpretation of a theory $\mathcal{T}$ in a theory $\mathcal{U}$ is given by
- a function which maps each sort `s` of `T` to a sort `s*` of `U` with a relativization predicate `s*(x)` in `U` (with `x` of sort `s*`), such that `U ⊢ ∃x s*(x)`.

- a function which maps each variable `x` of sort `s` in `T` to a variable `x*` of sort `s*` in `U`;

- a function which maps each formula `A` of `T` with free variables `x₁, ..., xₙ` of sorts `s₁, ..., sₙ` in `T` to a formula `A*` of `U` whose free variables occur among the variables `x₁*, ..., xₙ*`.

for which we require that

1. for all sorts `s` of `T` we have `U ⊢ ∃x s*(x)`;

2. for all formulæ `A` and `B` of `T` whose free variables occur among the variables `x₁, ..., xₙ` of sorts `s₁, ..., sₙ` in `T` we have:

$$U \vdash \bot^* \Leftrightarrow \bot$$

$$U \vdash \top^* \Leftrightarrow \top$$

$$U \vdash s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \Rightarrow ((A \wedge B)^* \Leftrightarrow (A^* \wedge B^*))$$

$$U \vdash s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \Rightarrow ((A \vee B)^* \Leftrightarrow (A^* \vee B^*))$$

$$U \vdash s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \Rightarrow ((A \Rightarrow B)^* \Leftrightarrow (A^* \Rightarrow B^*))$$

$$U \vdash s_1^*(x_1^*) \wedge \dots \wedge s_{n-1}^*(x_{n-1}^*) \Rightarrow ((\forall x_n A)^* \Leftrightarrow \forall x_n^* (s_n^*(x_n^*) \Rightarrow A^*))$$

$$U \vdash s_1^*(x_1^*) \wedge \dots \wedge s_{n-1}^*(x_{n-1}^*) \Rightarrow ((\exists x_n A)^* \Leftrightarrow \exists x_n^* (s_n^*(x_n^*) \wedge A^*))$$

3. for all axioms `A` of `T` we have: `U ⊢ A*` (assuming that the axioms of `T` are closed formulæ).

A simple way to define the underlying translation `A ↦ A*` of such an interpretation is to define it structurally on formulæ, by first defining the formula `A*` for each atomic formula `A` of `T`, and then by extending the definition inductively to all formulæ using the equations

$$(A \Rightarrow B)^* \equiv (A^* \Rightarrow B^*)$$

$$(A \wedge B)^* \equiv (A^* \wedge B^*)$$

$$(A \vee B)^* \equiv (A^* \vee B^*)$$

$$\top^* \equiv \top$$

$$(\forall x A)^* \equiv \forall x^* (s^*(x^*) \Rightarrow A^*)$$

$$(\exists x A)^* \equiv \exists x^* (s^*(x^*) \wedge A^*)$$

(assuming that `s` is the sort of the variable `x`). In this case, the conditions required in item 1 of the definition above come for free, but the soundness of all the axioms of `T` in `U` still has to be checked separately.

Notice that the definition of the notion of interpretation (of a theory into another one) does not say anything about the translation of terms. The reason is that in some cases, it is desirable to interpret a theory with a rich term language (such as Peano arithmetic) into a theory with a poor one (such as set theory), so that we can not expect that terms of `T` are always interpreted as terms of `U`.

However, interpretations are usually structural on terms too, which means that they come with a translation `t ↦ t*` on terms such that

- for all terms `t` of sort `s` whose free variables occur among the variables `x₁, ..., xₙ` of sorts `s₁, ..., sₙ` in the theory `T`, one has:

$$U \vdash s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \Rightarrow s^*(t^*)$$
- for all well-formed terms of $\mathcal{T}$ of the form $f(t_1, \dots, t_n)$ (where $f$ is an arbitrary function symbol of $\mathcal{T}$), one has:<fnref n="1" />

$$ (f(t_1, \dots, t_n))^* = (f(x_1, \dots, x_n))^* \{x_1^* := t_1^*; \dots; x_n^* := t_n^*\}. $$

The main interest of the notion of interpretation (in the sense of Def. 1) is that it provides a way to translate each theorem of $\mathcal{T}$ into a theorem of $\mathcal{U}$:

**Proposition 1.** — Given an interpretation $*$ of a theory $\mathcal{T}$ in a theory $\mathcal{U}$ and a formula $A$ of $\mathcal{T}$ whose free variables occur among the variables $x_1, \dots, x_n$ of sorts $s_1, \dots, s_n$ in $\mathcal{T}$, if $\mathcal{T} \vdash A$ then

$$ \mathcal{U} \vdash s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \Rightarrow A^* $$

*Proof.* By induction on the structure of the proof of $\mathcal{T} \vdash A$.

**Theorem 1.** — If the theory $\mathcal{T}$ has an interpretation in $\mathcal{U}$, and if the theory $\mathcal{U}$ is consistent, then $\mathcal{T}$ is consistent too.

*Proof.* Assume $\mathcal{T} \vdash \perp$. From Prop. 1 we get $\mathcal{U} \vdash \perp^*$ and thus $\mathcal{U} \vdash \perp$ using the equivalence $\mathcal{U} \vdash \perp^* \Leftrightarrow \perp$. □

Notice that this way of proving the consistency of a theory directly extends to intuitionistic logic.

# 2 Normalization

## 2.1 Deduction modulo

We want to be able to speak abstractly of the normalization of proofs in an arbitrary theory $\mathcal{T}$ and also to be able to deduce some corollaries from the fact that $\mathcal{T}$ has the normalization property, in particular, the consistency of $\mathcal{T}$, the disjunction and the witness property for constructive proofs, etc. It is well-known that predicate logic is not an appropriate for defining such a notion of normalization as each axiomatic theory $\mathcal{T}$ requires a specific notion of reduction. Thus we use an extension of predicate logic called *Deduction modulo* [1].

In Deduction modulo, a theory is formed by a set of axioms $\Gamma$ and a congruence $\equiv$ defined on formulæ. Then, the deduction rules take this congruence into account. For instance, the *modus ponens* is not stated as usual

$$ \frac{A \Rightarrow B \quad A}{B} $$

as the first premise need not be exactly $A \Rightarrow B$ but may be only congruent to this formula, hence it is stated

$$ \frac{C \quad A}{B} \quad \text{if } C \equiv A \Rightarrow B $$

<footnote n="1">¹ This condition says that each function symbol $f$ of $\mathcal{T}$ is translated as a macro in $\mathcal{U}$.</footnote>
All the rules of natural deduction may be stated in a similar way. Many theories, such as arithmetic, simple type theory and set theory can be expressed with a congruence and no axioms.

Replacing axioms by a congruence changes the structure of proofs and in particular some theories may have the normalization property when expressed with axioms and not when expressed with a congruence. In counterpart, when theory formed with a congruence and no axioms has the normalization property, then we can deduce that it is consistent, constructive proofs have the disjunction and the witness property, various proof search methods are complete, etc.

## 2.2 Pre-models

A theory in Deduction modulo has the normalization property if it has what we call a pre-model [2]. A pre-model is a many-valued model whose truth values are reducibility candidates, that is, particular sets of strongly normalizable proof-terms whose definition is given below.

**Definition 2 (Proof-term).** Proof-terms are inductively defined as follows:

$$
\begin{array}{l@{\qquad}l}
\pi ::= \alpha & (\text{Axiom}) \\
| \lambda\alpha\pi | (\pi\pi') & (\Rightarrow\text{-intro, } \Rightarrow\text{-elim}) \\
| \langle\pi, \pi'\rangle | \text{fst}(\pi) | \text{snd}(\pi) & (\wedge\text{-intro, } \wedge\text{-elim}_{1,2}) \\
| i(\pi) | j(\pi) | (\delta\pi_1\alpha\pi_2\beta\pi_3) & (\forall\text{-intro}_{1,2}, \forall\text{-elim}) \\
| I & (\top\text{-intro}) \\
| (\delta\perp\pi) & (\perp\text{-elim}) \\
| \lambda x\pi | (\pi t) & (\forall\text{-intro}, \forall\text{-elim}) \\
| \langle t, \pi\rangle | (\delta\exists\pi x\alpha\pi') & (\exists\text{-intro}, \exists\text{-elim})
\end{array}
$$

Each proof-term constructor corresponds to an inference rule of intuitionistic natural deduction (see above). A proof-term built using a constructor that corresponds to an introduction rule—that is, a proof-term of the form $\lambda\alpha\pi, \langle\pi, \pi'\rangle$, $i(\pi)$, $j(\pi)$, $I$, $\lambda x\pi$ or $\langle t, \pi\rangle$—is called an *introduction*. Similarly, a proof-term built using a constructor that corresponds to an elimination rule—that is, a proof-term of the form $(\pi\pi')$, $\text{fst}(\pi)$, $\text{snd}(\pi)$, $(\delta\pi_1\alpha\pi_2\beta\pi_3)$, $(\delta\perp\pi)$, $(\pi t)$ or $(\delta\exists\pi x\alpha\pi')$—is called an *elimination*.

**Definition 3 (Reduction).** Reduction on proof-terms is defined by the following rules that eliminate cuts step by step.

$$
\begin{array}{l@{\qquad}l}
(\lambda\alpha \pi_1 \pi_2) & \triangleright \pi_1(\alpha \leftarrow \pi_2) \\
\text{fst}(\langle\pi_1, \pi_2\rangle) & \triangleright \pi_1 \\
\text{snd}(\langle\pi_1, \pi_2\rangle) & \triangleright \pi_2 \\
(\delta i(\pi_1) \alpha\pi_2 \beta\pi_3) & \triangleright \pi_2(\alpha \leftarrow \pi_1) \\
(\delta j(\pi_1) \alpha\pi_2 \beta\pi_3) & \triangleright \pi_3(\beta \leftarrow \pi_1) \\
(\lambda x\pi t) & \triangleright \pi(x \leftarrow t) \\
(\delta\exists \langle t, \pi_1\rangle \alpha x \pi_2) & \triangleright \pi_2(x \leftarrow t, \alpha \leftarrow \pi_1)
\end{array}
$$
**Definition 4 (Reducibility candidates).** A set $\mathcal{R}$ of proof-terms is a re-
ducibility candidate if:

- if $\pi \in \mathcal{R}$, then $\pi$ is strongly normalizable;

- if $\alpha$ is a variable, then $\alpha \in \mathcal{R}$;

- if $\pi \in \mathcal{R}$ and $\pi \triangleright \pi'$, then $\pi' \in \mathcal{R}$;

- if $\pi$ is an elimination and if $\pi' \in \mathcal{R}$ for all $\pi'$ such that $\pi \triangleright^1 \pi'$, then $\pi \in \mathcal{R}$.

The set of reducibility candidates is written $\mathcal{C}$.

**Definition 5 (Pre-model).** A pre-model $\mathcal{M}$ (of a given signature) is given by

- A nonempty set (still) written $\mathcal{M}$ and called the domain of $\mathcal{M}$ (or several domains $\mathcal{M}_\sigma$ for many-sorted theories);

- For each function symbol $f$ of arity $n$, a function $f^{\mathcal{M}} : \mathcal{M}^n \to \mathcal{M}$;

- For each predicate symbol $p$ of arity $n$, a function $p^{\mathcal{M}} : \mathcal{M}^n \to \mathcal{C}$.

If $\mathcal{P}$ is an atomic formula and $\phi$ is a assignment on a premodel $\mathcal{M}$, the
reducibility candidate $\llbracket \mathcal{P} \rrbracket_\phi$ is defined in the obvious way. This definition extends
to all formulæ as follows:

- A proof-term is an element of $\llbracket A \Rightarrow B \rrbracket_\phi$ if it is strongly normalizable and when it reduces to a proof-term of the form $\lambda\alpha \pi_1$, then for every $\pi'$ in $\llbracket A \rrbracket_\phi$, $[\pi'/\alpha]\pi_1$ is an element of $\llbracket B \rrbracket_\phi$.

- A proof-term is an element of $\llbracket A \wedge B \rrbracket_\phi$ if it is strongly normalizable and when it reduces to a proof-term of the form $\langle \pi_1, \pi_2 \rangle$, then $\pi_1$ and $\pi_2$ are elements of $\llbracket A \rrbracket_\phi$ and $\llbracket B \rrbracket_\phi$.

- A proof-term is an element of $\llbracket A \vee B \rrbracket_\phi$ if it is strongly normalizable and when it reduces to a proof-term of the form $i(\pi_1)$ (resp. $j(\pi_2)$) then $\pi_1$ (resp. $\pi_2$) is an element of $\llbracket A \rrbracket_\phi$ (resp. $\llbracket B \rrbracket_\phi$).

- A proof-term is an element of $\llbracket \top \rrbracket_\phi$ if it is strongly normalizable.

- A proof-term is an element of $\llbracket \bot \rrbracket_\phi$ if it is strongly normalizable.

- A proof-term is an element of $\llbracket \forall x \ A \rrbracket_\phi$ if it is strongly normalizable and when it reduces to a proof-term of the form $\lambda x \ \pi_1$ then for every term $t$ and every element $v$ of $\mathcal{M}$, $[t/x]\pi_1$ is an element of $\llbracket A \rrbracket_{\phi+\langle x,v \rangle}$, where $\phi + \langle x,v \rangle$ is the function that coincides with $\phi$ everywhere except on $x$ where it takes value $v$.

- A proof-term is an element of $\llbracket \exists x \ A \rrbracket_\phi$ if it is strongly normalizable and when it reduces to a proof-term of the form $\langle t, \pi_1 \rangle$ there exists an element $v$ of $\mathcal{M}$ such that $\pi_1$ is an element of $\llbracket A \rrbracket_{\phi+\langle x,v \rangle}$.

A pre-model $\mathcal{M}$ is a pre-model of a congruence $\equiv$ if for all formulæ $A$ and $B$ such that $A \equiv B$, we have $\llbracket A \rrbracket_\phi = \llbracket B \rrbracket_\phi$ for all assignments $\phi$.

The theorem that if a theory has a pre-model then it has the normalization
property is proved in two steps. We first check that (1) for each formula $A$ and
assignment $\phi$, the set $\llbracket A \rrbracket_\phi$ is a reducibility candidate and then that (2) proofs
of $A$ are all members of the set $\llbracket A \rrbracket_\phi$. The proof of (1) is an induction over the
structure of formulæ and the proof of (2) an induction over the structure of
proofs. We need to prove, for each deduction rule a lemma such as:
If $\pi_1 \in \llbracket A \Rightarrow B \rrbracket_\phi$ and $\pi_2 \in \llbracket A \rrbracket_\phi$, then $(\pi_1, \pi_2) \in \llbracket B \rrbracket_\phi$.

Then, as all elements of a reducibility candidate strongly normalize we conclude that all proofs of a formula A strongly normalize [2].

## 2.3 A theory of syntactic constructions

To relativize the pre-model construction of $\mathcal{T}$ w.r.t. a theory $\mathcal{U}$, we need to express all the syntactic constructions of the proof-language of $\mathcal{T}$ in $\mathcal{U}$. The proof-language of $\mathcal{T}$ is complex: it contains proof-variables, proof-terms, as well as the terms of the theory $\mathcal{T}$ (that appear in proof-terms). Moreover, we need to express usual syntactic operations, such as $\alpha$-conversion, substitution, etc.

For that let us consider a language of trees $\mathcal{L}$ generated by a finite number of constructors, that is, an algebra of closed terms generated by a finite number of function symbols written $c_1, \dots, c_N$—the constructors of $\mathcal{L}$—whose arities are written $k_1, \dots, k_N$. In what follows, we assume that the language $\mathcal{L}$ provides two constructors 0 (of arity 0) and $s$ (of arity 1) to encode natural numbers.

It is well-known that the latter assumption is sufficient to ensure that all syntactic constructions (such as variables, terms, proof-terms, etc.) can be encoded in $\mathcal{L}$, by the mean of Gödel numberings. However, the cost of these numberings can be avoided by taking a richer language $\mathcal{L}$, in which syntactic constructions can be encoding more directly.

Once the language $\mathcal{L}$ has been fixed, the class of all functions that can be defined by primitive recursion on $\mathcal{L}$ is well-defined too.

From the language $\mathcal{L}$, we build a (mono-sorted) first-order theory $\mathcal{S}$, which we call the *theory of syntactic constructions*. This theory is defined as follows:

1. The function symbols of $\mathcal{S}$ are the constructors $c_1, \dots, c_N$ plus, for each primitive recursive definition of a $n$ary function on syntactic trees, a function symbol $f$ of arity $n$.

2. The only predicate symbol of the theory $\mathcal{S}$ is equality.

3. The axioms of $\mathcal{S}$ are:

- The equality axioms, that is: convexity, symmetry and transitivity of equality, as well as congruence axioms for all function symbols $f$:

$$ 
\begin{align*}
x &= x \\
x &= y \land x = z \Rightarrow y = z \\
x_1 &= y_1 \land \dots \land x_n = y_n \quad \Rightarrow \quad f(x_1, \dots, x_n) = f(y_1, \dots, y_n)
\end{align*}
$$

- Axioms expressing injectivity and non-confusion for constructors:

$$ 
\begin{align*}
c_i(x_1, \dots, x_{k_i}) &= c_i(y_1, \dots, y_{k_i}) \Rightarrow x_1 = y_1 \land \dots \land x_{k_i} = y_{k_i} \\
c_i(x_1, \dots, x_{k_i}) &= c_j(y_1, \dots, y_{k_j}) \Rightarrow \perp
\end{align*}
$$

(for all $i, j \in [1..N]$ such that $i \neq j$).

- For each primitive recursive definition of a function represented by a function symbol $f$, the axioms expressing its equational theory.
- For each formula $A(x)$ possibly depending on a variable $x$ (as well as other parameters that are left implicit), the induction principle:

$$ \bigwedge_{i=1}^{N} \left( \forall x_1 \dots \forall x_{k_i} A(c_i(x_1, \dots, x_{k_i})) \right) \Rightarrow \forall x A(x). $$

In what follows, we assume that the usual syntactic structures of $\mathcal{T}$ are represented in the theory $\mathcal{S}$ using the following predicates:

<table><tr><td>Nat(x)</td><td>x is a natural number</td></tr><tr><td>Le(x, y)</td><td>x is less than or equal to y</td></tr><tr><td>Sort(x)</td><td>x is a sort</td></tr><tr><td>TermVar(x, y)</td><td>x is a term variable of sort y</td></tr><tr><td>Term(x, y)</td><td>x is a term of sort y</td></tr><tr><td>ProofVar(x)</td><td>x is a proof variable</td></tr><tr><td>Proof(x)</td><td>x is a proof</td></tr><tr><td>Elim(x)</td><td>x is a proof that ends with an elimination rule</td></tr><tr><td>Red(x, y)</td><td>the proof x reduces in one step to the proof y</td></tr><tr><td>Redn(x, n, y)</td><td>the proof x reduces in n steps to the proof y</td></tr></table>

Note that all the relations above are primitive recursive.

From these relations, we can define important (and non primitive recursive) relations such as:

$$ \begin{align*} \text{Red}^*(x, y) &\equiv \exists n (\text{Nat}(n) \wedge \text{Redn}(x, n, y)) \\ \text{SN}(x) &\equiv \text{Proof}(x) \wedge \\ & \phantom{\equiv} \exists n (\text{Nat}(n) \wedge \forall y (\text{Proof}(y) \Rightarrow \neg \text{Redn}(x, n, y))) \end{align*} $$

(Intuition: a proof $\pi$ is strongly normalizable if there is a number $n \ge 0$ such that $\pi$ has no $n$-reduct.)

We assume that proof-terms (Def. 2) are represented as trees of $\mathcal{L}$ by the mean of constructors—or constructor aggregates—Axiom (arity 1), Imp_I (arity 2), Imp_E (arity 2), And_I (arity 2), And_E1 (arity 1), And_E2 (arity 1), Or_I1 (arity 1), Or_I2 (arity 1), Or_E (arity 5), Top_I (arity 0), Bot_E (arity 1), Forall_I (arity 2), Forall_E (arity 2), Exists_I (arity 2), Exists_E (arity 2) whose name are self-explanatory (see Def. 2 for the correspondence).

Finally, we write $TSubst$ (resp. $PSubst$) the ternary function symbol of $\mathcal{S}$ that computes term-substitution (resp. proof-substitution) inside a proof.

## 3 An abstract normalization result

We now want to relativize the pre-model construction. Hence, besides the theory $\mathcal{T}$ we want to prove the normalization of, we shall consider another theory $\mathcal{U}$ either in predicate logic or in deduction modulo.

**Definition 6.** — We say that a theory $\mathcal{U}$ expresses syntactic constructions if it comes with an interpretation (in the sense of Def. 1) of the theory $\mathcal{S}$ (defined in 2.3) into $\mathcal{U}$, which is structural on terms and formulæ (cf section 1).
From now on, we assume that $\mathcal{U}$ expresses all syntactic constructions, by the mean of an interpretation of the theory $\mathcal{S}$ that we write using `[^]` brackets ('the code of ...'). In particular, we write $[^t]$ the code of any tree $t \in \mathcal{L}$, including (representations of) variables, terms and proof-terms of the theory $\mathcal{T}$. The sort of $\mathcal{U}$ associated to the unique sort of $\mathcal{S}$ through the interpretation of $\mathcal{S}$ in $\mathcal{U}$ is written $[^{\mathcal{L}}]$, and the corresponding relativisation predicate is written $[^{\mathcal{L}}](x)$.

Each primitive recursive relation $R$ of arity $n$ on $\mathcal{L}$ is expressed in $\mathcal{S}$ as a relation still written $R(x_1, \dots, x_n)$ and defined by

$$R(x_1, \dots, x_n) \equiv f(x_1, \dots, x_n) = 1,$$

where $f$ is the function symbol of $\mathcal{S}$ associated to the characteristic function of $R$. Via the interpretation $[^]$, the primitive recursive relation $R$ is thus represented in $\mathcal{U}$ as a relation written $[^{\mathcal{R}}](x_1, \dots, x_n)$. It is important to notice that this representation is faithful when the theory $\mathcal{U}$ is consistent:

**Proposition 2.** — If $\mathcal{U}$ is consistent, then for all primitive recursive relations $R(t_1, \dots, t_n)$ on $\mathcal{L}$ and for all $t_1, \dots, t_n \in \mathcal{L}$ we have:

$$R(t_1, \dots, t_n) \quad \text{iff} \quad \mathcal{U} \vdash [\mathcal{R}]([^{t_1}], \dots,[^{t_n}])$$

In particular, we have: $t_1 = t_2$ iff $\mathcal{U} \vdash [t_1 = t_2]$ (for all $t_1, t_2 \in \mathcal{L}$).

*Proof. (Direct implication)* Assume that $R(t_1, \dots, t_n)$ holds. From the trace of the computation of the characteristic function $f$ of $R$ applied to $t_1, \dots, t_n$ we easily build a proof of $\mathcal{S} \vdash f(t_1, \dots, t_n) = 1$, from which we immediately get a proof of $\mathcal{U} \vdash [\mathcal{R}]([^{t_1}], \dots,[^{t_n}])$ through the interpretation of $\mathcal{S}$ in $\mathcal{U}$.

(Converse implication) Assume that $\mathcal{U} \vdash [\mathcal{R}]([^{t_1}], \dots,[^{t_n}])$. We distinguish two cases, depending on whether $R(t_1, \dots, t_n)$ holds or not.

- Either $R(t_1, \dots, t_n)$ holds. In this case we are done.

- Either $R(t_1, \dots, t_n)$ does not hold. From the trace of the computation of the characteristic function of $R$, we now get a proof of $\mathcal{S} \vdash f(t_1, \dots, t_n) = 0$, and thus a proof of $\mathcal{U} \vdash \neg [\mathcal{R}]([^{t_1}], \dots,[^{t_n}])$, which is impossible since $\mathcal{U}$ is consistent. Hence this case is absurd. $\square$

In what follows, we will need a stronger notion of consistency, namely:

**Definition 7 (1-consistency).** — We say that $\mathcal{U}$ is 1-consistent if for all primitive recursive relations $R(t_1, \dots, t_n)$ on $\mathcal{L}$, the derivability of

$$\mathcal{U} \vdash \exists x_1 \dots \exists x_n ([\mathcal{L}](x_1) \wedge \dots \wedge [\mathcal{L}](x_n) \wedge [\mathcal{R}](x_1, \dots, x_n))$$

entails the existence of trees $t_1, \dots, t_n \in \mathcal{L}$ such that $R(t_1, \dots, t_n)$.

The 1-consistency of a theory entails its consistency, but the converse does not hold in general.

**Definition 8 (Realizability translation).** — A realizability translation of a theory $\mathcal{T}$ in $\mathcal{U}$ is defined by
- a function which maps each sort `s` of `T` to a sort `s*` of `U` with a relativization predicate `s*(x)` in `U` (with `x` of sort `s*`);

- a function which maps each variable `x` of sort `s` in `T` to a variable `x*` of sort `s*` in `U`;

- a function which maps each function symbol `f` of rank `⟨s₁, ..., sₙ, s⟩` in `T` to a term `f*(z₁, ..., zₙ)` of sort `s*` in `U`, that (possibly) depends on variables `z₁, ..., zₙ` of sort `s₁*, ..., sₙ*`, respectively.

- a function which maps each predicate symbol `p` of rank `⟨s₁, ..., sₙ⟩` in `T` to a formula of `U` written `π ⊧ p(z₁, ..., zₙ)`, that possibly depends on variables `π, z₁, ..., zₙ` of sorts `[L]`, `s₁*, ..., sₙ*`, respectively.

Given a realizability translation of `T` in `U`, the translation of variables and function symbols is extended to all terms by setting:

$$ (x)^* = x^* \\ (f(t_1, \dots, t_n))^* \equiv f^*(z_1, \dots, z_n)(z_1 \leftarrow t_1^*, \dots, z_n \leftarrow t_n^*) $$

Notice that this translation transforms each term `t` of `T` with free variables `x₁, ..., xₙ` of sorts `s₁, ..., sₙ` into a term `t*` of `U` whose free variables occur among the variables `x₁*, ..., xₙ*` of sorts `s₁*, ..., sₙ*`.

Similarly, we extend the translation of predicate symbols to all formulæ by associating to each formula `A` of `T` with free variables `x₁, ..., xₙ` of sorts `s₁, ..., sₙ` a formula `π ⊧ A` of `U` with free variables `π, x₁*, ..., xₙ*` of sorts `[L]`, `s₁*, ..., sₙ*`. The formula `π ⊧ A` is recursively defined on `A` by the equations:

$$ \pi \Vdash p(t_1, \dots, t_n) \equiv (\pi \Vdash p(z_1, \dots, z_n))(z_1 \leftarrow t_1^*, \dots, z_n \leftarrow t_n^*) $$

$$ \pi \Vdash \top \equiv [SN](\pi) $$

$$ \pi \Vdash \bot \equiv [SN](\pi) $$

$$ \pi \Vdash A \Rightarrow B \quad \equiv \quad [SN](\pi) \wedge \\ \phantom{\pi \Vdash A \Rightarrow B \quad \equiv \quad} \forall \alpha \ \forall \pi' \ ([Red^*](\pi, [Imp_I](\alpha, \pi')) \Rightarrow \\ \phantom{\pi \Vdash A \Rightarrow B \quad \equiv \quad} \forall \phi \ (\phi \Vdash A \Rightarrow [PSubst](\pi', \alpha, \phi) \Vdash B)) $$

$$ \pi \Vdash A \wedge B \quad \equiv \quad [SN](\pi) \wedge \\ \phantom{\pi \Vdash A \wedge B \quad \equiv \quad} \forall \pi_1 \ \forall \pi_2 \ ([Red^*](p, [And_I](\pi_1, \pi_2))) \Rightarrow \pi_1 \Vdash A \wedge \pi_2 \Vdash B $$

$$ \pi \Vdash A \vee B \quad \equiv \quad [SN](\pi) \wedge \\ \phantom{\pi \Vdash A \vee B \quad \equiv \quad} \forall \pi_1 \ ([Red^*](\pi, [Or_I_1](\pi_1))) \Rightarrow \pi_1 \Vdash A) \wedge \\ \phantom{\pi \Vdash A \vee B \quad \equiv \quad} \forall \pi_2 \ ([Red^*](\pi, [Or_I_2](\pi_2))) \Rightarrow \pi_2 \Vdash B) $$

$$ \pi \Vdash \forall x A(x) \quad \equiv \quad [SN](\pi) \wedge \\ \phantom{\pi \Vdash \forall x A(x) \quad \equiv \quad} \forall v \ \forall \pi' \ ([Red^*](\pi, [Forall_I](v, \pi')) \Rightarrow \\ \phantom{\pi \Vdash \forall x A(x) \quad \equiv \quad} \forall x^* \ \forall t \ (s^*(x^*) \wedge [Term](t, [s])) \Rightarrow \\ \phantom{\pi \Vdash \forall x A(x) \quad \equiv \quad} [TSubst](\pi', v, t) \Vdash A(x))) $$

$$ \pi \Vdash \exists x A(x) \quad \equiv \quad [SN](\pi) \wedge \\ \phantom{\pi \Vdash \exists x A(x) \quad \equiv \quad} \forall \pi' \ \forall t \ ([Red^*](\pi, [Exists_I](t, \pi')) \Rightarrow \\ \phantom{\pi \Vdash \exists x A(x) \quad \equiv \quad} \exists x^* (s^*(x^*) \wedge \pi' \Vdash A(x))) $$
We now need to express in the theory $\mathcal{U}$ that the 'set' (in its informal sense) of all proofs $\pi$ such that $\pi \Vdash A$ forms a reducibility candidate. Given a formula of $\mathcal{U}$ possibly depending on a variable $\pi$ of sort $[\mathcal{L}]$ we write

$$ 
\begin{align*}
CR_{\pi}(A(\pi)) &\equiv \forall \pi \ (A(\pi) \Rightarrow [\text{Proof}](\pi) \wedge [\text{SN}](\pi)) && \wedge \\
&\equiv \forall \alpha \ ([\text{ProofVar}](\alpha) \Rightarrow A([\text{Axiom}](\alpha))) && \wedge \\
&\equiv \forall \pi \ \forall \pi' \ (A(\pi) \wedge [\text{Red}](\pi, \pi') \Rightarrow A(\pi')) && \wedge \\
&\equiv \forall \pi \ ([\text{Elim}](\pi) \wedge \forall \pi' ([\text{Red}](\pi, \pi') \Rightarrow A(\pi')) \Rightarrow A(\pi))
\end{align*}
$$

We can now introduce the conditions which make that a realizability translation is a realizability interpretation:

**Definition 9 (Realizability interpretation).** — A realizability translation of $\mathcal{T}$ in $\mathcal{U}$ is a realizability interpretation if the following conditions hold:

1. For each sort $s$ of $\mathcal{T}$, we have $\mathcal{U} \vdash \exists x s^*(x)$;

2. For each function symbol $f$ of rank $\langle s_1, \dots, s_n, s \rangle$ in $\mathcal{T}$:

$$ \mathcal{U} \vdash \forall z_1 \dots \forall z_n (s_1^*(z_1) \wedge \dots \wedge s_n^*(z_n) \Rightarrow s^*(f^*(z_1, \dots, z_n))) $$

3. For each predicate symbol $p$ of rank $\langle s_1, \dots, s_n \rangle$ in $\mathcal{T}$:

$$ \mathcal{U} \vdash \forall z_1 \dots \forall z_n (s_1^*(z_1) \wedge \dots \wedge s_n^*(z_n) \Rightarrow CR_{\pi}(\pi \Vdash p(z_1, \dots, z_n))) $$

4. For all pairs of congruent formulæ $A \equiv A'$ with free variables $x_1, \dots, x_n$ of sorts $s_1, \dots, s_n$:

$$ \mathcal{U} \vdash \forall x_1^* \dots \forall x_n^* (s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \Rightarrow \forall \pi (\pi \Vdash A \Leftrightarrow \pi \Vdash A')) $$

Items 2 and 3 immediately extend to all terms and formulæ as follows:

**Proposition 3 (Typing).** — Given a realizability translation of $\mathcal{T}$ in $\mathcal{U}$:

- For all terms $t$ of sort $s$ in $\mathcal{T}$ with free variables $x_1, \dots, x_n$ of sorts $s_1, \dots, s_n$:

$$ \mathcal{U} \vdash \forall x_1^* \dots \forall x_n^* (s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \Rightarrow s^*(t)) $$

- For all formulæ $A$ of $\mathcal{T}$ with free variables $x_1, \dots, x_n$ of sorts $s_1, \dots, s_n$:

$$ \mathcal{U} \vdash \forall x_1^* \dots \forall x_n^* (s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \Rightarrow CR_{\pi}(\pi \Vdash A)) $$

**Corollary 1 (Normalization of realizers).** — For all formulæ $A$ of $\mathcal{T}$ with free variables $x_1, \dots, x_n$ of sorts $s_1, \dots, s_n$:

$$ \mathcal{U} \vdash \forall x_1^* \dots \forall x_n^* \forall \pi (s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \wedge \pi \Vdash A) \Rightarrow [\text{SN}](\pi) $$

We now extend the realizability relation to sequents as follows: given a sequent $A_1, \dots, A_k \vdash B$ of $\mathcal{T}$ and a variable $\pi$ of sort $[\mathcal{L}]$ in $\mathcal{U}$, we write

$$ \pi \Vdash (A_1, \dots, A_k \vdash B) \equiv [\text{Imp}_I]([\alpha_1], \dots, [\text{Imp}_I]([\alpha_k], \pi), \dots) \Vdash A_1 \Rightarrow \dots \Rightarrow A_k \Rightarrow B, $$

where $\alpha_1, \dots, \alpha_k$ are pairwise distinct proof-variables (of $\mathcal{T}$) that represent the assumptions $A_1, \dots, A_k$. Corollary 1 immediately extends to sequent realizers:
**Corollary 2.** — For all sequents $\Gamma \vdash A$ of $\mathcal{T}$ with free variables $x_1, \dots, x_n$ of sorts $s_1, \dots, s_n$:

$$ \mathcal{U} \vdash \forall x_1^* \dots \forall x_n^* \forall \pi (s_1^*(x_1^*) \wedge \dots \wedge s_n^*(x_n^*) \wedge \pi \Vdash (\Gamma \vdash A) \Rightarrow [SN](\pi)) $$

**Proposition 4 (Existence of a realizer).** — Let $(-)^*$ be a realizability interpretation of $\mathcal{T}$ in $\mathcal{U}$. If a sequent $A_1, \dots, A_k \vdash B$ of $\mathcal{T}$ with free variables $x_1, \dots, x_n$ of sorts $s_1, \dots, s_n$ has a proof $\pi$ in intuitionistic deduction modulo $\mathcal{T}$ with free proof-variables $\alpha_1 : A_1, \dots, \alpha_k : A_k$, then

$$ \mathcal{U} \vdash \forall x_1^* \dots \forall x_n^* (s_1^*(x_1^*) \wedge \dots \wedge s_k^*(x_n^*) \Rightarrow [\pi] \Vdash (A_1, \dots, A_k \vdash B)) $$

*Proof.* By induction on the derivation of $\pi : (A_1, \dots, A_n \vdash B)$.

**Theorem 2.** — If a theory $\mathcal{T}$ has a realizability interpretation in $\mathcal{U}$ and if $\mathcal{U}$ is 1-consistent, then $\mathcal{T}$ enjoys the strong normalization property.

*Proof.* Assume $\pi$ is a proof of $A_1, \dots, A_n \vdash B$ (in intuitionistic deduction modulo $\mathcal{T}$). From Prop. 4 we get

$$ \mathcal{U} \vdash \forall x_1^* \dots \forall x_k^* (s_1^*(x_1^*) \wedge \dots \wedge s_k^*(x_k^*) \Rightarrow [\pi] \Vdash (A_1, \dots, A_k \vdash B)), $$

hence

$$ \mathcal{U} \vdash \forall x_1^* \dots \forall x_k^* (s_1^*(x_1^*) \wedge \dots \wedge s_k^*(x_k^*) \Rightarrow [SN]([\pi])) $$

using Cor. 2, and finally

$$ \mathcal{U} \vdash [SN]([\pi]), $$

from the fact that all domains of interpretation of sorts are inhabited. The latter means that

$$ \mathcal{U} \vdash [Proof]([\pi]) \wedge \exists n ([Nat](n) \wedge [R](x, n)), $$

writing

$$ R(x, n) \equiv \forall y (Proof(y) \Rightarrow \neg Redn(x, n, y)) $$

the relation of $\mathcal{S}$ which expresses that $x$ has no $n$-reduct. But since this relation is primitive recursive, and since $\mathcal{U}$ is 1-consistent, we deduce that there exists a natural number $n$ such that $\pi$ has no $n$-reduct. Which means that $\pi$ is strongly normalizable. $\square$

## References

1. G. Dowek, Th. Hardin, and C. Kirchner. Theorem proving modulo. *Journal of Automated Reasoning*, 31:33–72, 2003.

2. G. Dowek and B. Werner. Proof normalization modulo. *The Journal of Symbolic Logic*, 68(4):1289–1316, 2003.