# Arithmetic as a theory modulo

Gilles Dowek, Benjamin Werner

► To cite this version:

Gilles Dowek, Benjamin Werner. Arithmetic as a theory modulo. 2005. hal-04242432

HAL Id: hal-04242432

https://inria.hal.science/hal-04242432v1

Preprint submitted on 15 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
Arithmetic as a theory modulo

Gilles Dowek and Benjamin Werner

Projet LogiCal

Pôle Commun de Recherche en Informatique du Plateau de Saclay

École polytechnique, INRIA, CNRS and Université de Paris-Sud

LIX, École polytechnique, 91128 Palaiseau Cedex, France

`{Gilles.Dowek,Benjamin.Werner}@polytechnique.fr`

**Abstract.** We present constructive arithmetic in Deduction modulo with rewrite rules only.

In natural deduction and in sequent calculus, the cut elimination theorem and the analysis of the structure of cut free proofs is the key to many results about predicate logic with no axioms: analyticity and non-provability results, completeness results for proof search algorithms, decidability results for fragments, constructivity results for the intuitionistic case...

Unfortunately, the properties of cut free proofs do not extend in the presence of axioms and the cut elimination theorem is not as powerful in this case as it is in pure logic. This motivates the extension of the notion of cut for various axiomatic theories such as arithmetic, Church's simple type theory, set theory and others. In general, we can say that a new axiom will necessitate a specific extension of the notion of cut: there still is no notion of cut general enough to be applied to any axiomatic theory. Deduction modulo [2, 3] is one attempt, among others, towards this aim.

In deduction modulo, a theory is not a set of axioms but a set of axioms combined with a set of rewrite rules. For instance, the axiom $\forall x x + 0 = x$ can be replaced by the rewrite rule $x + 0 \longrightarrow x$. The point is that replacing the axiom by the rewrite rule introduces short-cuts in the corresponding proofs, which avoid axiomatic cuts. When the set of rewrite rules is empty, one is simply back to regular predicate logic. On the other hand, when the set of axioms is empty we have theories expressed by rewrite rules only. For such theories, cut free proofs are similar to cut free proofs in pure logic, in particular they end with an introduction rule. Thus, when a theory can be expressed in deduction modulo with rewrite rules only and, in addition, cuts can be eliminated modulo these rewrite rules, the theory has most of the properties of pure logic. This leads to the question of which theories can be expressed with rewrite rules only, in such a way that cut-elimination holds.

It is known that several theories can be expressed in such a setting, for instance all equational theories, type theory, set theory, etc... But arithmetic was an important example of a theory that lacked such a presentation. The goal of this paper is to show that arithmetic can indeed be presented in deduction mod-
ulo without axioms in such a way that cut elimination holds. The cut elimination result is built using the generic tools introduced in [3].

When considering arithmetic, it is customary to keep the cut-elimination argument predicative. We show that these generic tools also make it possible to build a predicative proof.

It should be noticed that second-order arithmetic can be embedded in simple type theory with the axiom of infinity and thus that it can be expressed in deduction modulo. Our presentation of first-order arithmetic in deduction modulo uses many ideas coming from second-order arithmetic. However, our presentation of arithmetic has exactly the power of first-order arithmetic.

# 1 Deduction modulo

## 1.1 Identifying propositions

In deduction modulo, the notions of language, term and proposition are those of predicate logic. But, a theory is formed with a set of axioms $\Gamma$ and a congruence $\equiv$ defined on propositions. Such a congruence may be defined by a rewrite system on terms and on propositions (as propositions contain binders — quantifiers — these rewrite systems are in fact *combinatory reduction systems* [10]). 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 proposition, hence it is stated

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

All the rules of intuitionistic natural deduction may be stated in a similar way (see Figure 1).

For example, we can define a congruence with the following rewrite system

$$ \begin{align*} 0 + y &\rightarrow y \\ S(x) + y &\rightarrow S(x + y) \\ 0 \times y &\rightarrow 0 \\ S(x) \times y &\rightarrow x \times y + y \end{align*} $$

In the theory formed with a set of axioms $\Gamma$ containing the axiom $\forall x \ x = x$ and this congruence, we can prove, in natural deduction modulo, that the number 4 is even

$$ \frac{\overline{\Gamma \vdash \forall x \ x = x} \quad \text{axiom}}{\overline{\Gamma \vdash \mathbf{2} \times \mathbf{2} = \mathbf{4}} \quad \langle x, x = x, \mathbf{4} \rangle \quad \forall \text{-elim}} \\ \overline{\Gamma \vdash \exists x \ \mathbf{2} \times x = \mathbf{4}} \quad \langle x, \mathbf{2} \times x = \mathbf{4}, \mathbf{2} \rangle \quad \exists \text{-intro} $$
$\overline{\Gamma \vdash_A B}$ axiom if $A \in \Gamma$ and $A \equiv B$

$\frac{\Gamma, A \vdash_A B}{\Gamma \vdash_A C} \Rightarrow$-intro if $C \equiv (A \Rightarrow B)$

$\frac{\Gamma \vdash_A C \quad \Gamma \vdash_A A}{\Gamma \vdash_B B} \Rightarrow$-elim if $C \equiv (A \Rightarrow B)$

$\frac{\Gamma \vdash_A A \quad \Gamma \vdash_A B}{\Gamma \vdash_C C} \wedge$-intro if $C \equiv (A \wedge B)$

$\frac{\Gamma \vdash_A C}{\Gamma \vdash_A A} \wedge$-elim if $C \equiv (A \wedge B)$

$\frac{\Gamma \vdash_A C}{\Gamma \vdash_B B} \wedge$-elim if $C \equiv (A \wedge B)$

$\frac{\Gamma \vdash_A A}{\Gamma \vdash_A C} \vee$-intro if $C \equiv (A \vee B)$

$\frac{\Gamma \vdash_B B}{\Gamma \vdash_C C} \vee$-intro if $C \equiv (A \vee B)$

$\frac{\Gamma \vdash_D D \quad \Gamma, A \vdash_C C \quad \Gamma, B \vdash_C C}{\Gamma \vdash_C C} \vee$-elim if $D \equiv (A \vee B)$

$\frac{\Gamma \vdash_A A}{\Gamma \vdash_A A} \top$-intro if $A \equiv \top$

$\frac{\Gamma \vdash_B B}{\Gamma \vdash_A A} \bot$-elim if $B \equiv \bot$

$\frac{\Gamma \vdash_A A}{\Gamma \vdash_B B} \langle x, A \rangle \forall$-intro if $B \equiv (\forall x A)$ and $x \notin FV(\Gamma)$

$\frac{\Gamma \vdash_B B}{\Gamma \vdash_C C} \langle x, A, t \rangle \forall$-elim if $B \equiv (\forall x A)$ and $C \equiv (t/x)A$

$\frac{\Gamma \vdash_C C}{\Gamma \vdash_B B} \langle x, A, t \rangle \exists$-intro if $B \equiv (\exists x A)$ and $C \equiv (t/x)A$

$\frac{\Gamma \vdash_C C \quad \Gamma, A \vdash_B B}{\Gamma \vdash_B B} \langle x, A \rangle \exists$-elim if $C \equiv (\exists x A)$ and $x \notin FV(\Gamma B)$

<caption>**Fig. 1.** Natural deduction modulo</caption>
Substituting the variable $x$ by the term $2$ in the proposition $2 \times x = 4$ yields the proposition $2 \times 2 = 4$, that is congruent to $4 = 4$. The transformation of one proposition into the other, that requires several proof steps in usual formulations of natural deduction, is dropped from the proof in deduction modulo.

In this example, the rewrite rules apply to terms only. Deduction modulo permits also to consider rules rewriting atomic propositions to arbitrary ones. For instance, in the theory of integral domains, we can take the rule

$$x \times y = 0 \rightarrow x = 0 \lor y = 0$$

that rewrites an atomic proposition to a disjunction.

Notice that, in the proof above, we do not need the axioms of addition and multiplication. Indeed, these axioms are now redundant: since the terms $0 + y$ and $y$ are congruent, the axiom $\forall y 0 + y = y$ is congruent to the axiom of equality $\forall y y = y$. Hence, it can be dropped. Thus, rewrite rules replace axioms.

This equivalence between rewrite rules and axioms is expressed by the equivalence lemma that for every congruence $\equiv$, we can find a theory $\mathcal{T}$ such that $\Gamma \vdash \equiv A$ is provable in deduction modulo if and only if $\mathcal{T}, \Gamma \vdash A$ is provable in ordinary predicate logic [2]. Hence, deduction modulo is not a true extension of predicate logic, but rather an alternative formulation of predicate logic. Of course, the provable propositions are the same in both cases, but the proofs are very different.

## 1.2 Model of a theory modulo

A model of a congruence $\equiv$ is a model such that if $A \equiv B$ then for all assignments, $A$ and $B$ have the same denotation. A model of a theory modulo $\Gamma, \equiv$ is a model of the theory $\Gamma$ and of the congruence $\equiv$. Unsurprisingly, the completeness theorem extends to classical deduction modulo [6] and a proposition is provable in the theory $\Gamma, \equiv$ if and only if it is valid in all the models of $\Gamma, \equiv$.

## 1.3 Normalization in deduction modulo

Replacing axioms by rewrite rules in a theory changes the structure of proofs and in particular some theories may have the normalization property when expressed with axioms and not when expressed with rewrite rules. For instance, from the normalization theorem for predicate logic, we get that any proposition that is provable with the axiom $A \Leftrightarrow (B \land (A \Rightarrow \perp))$ has a normal proof. But if we transform this axiom into the rule $A \rightarrow B \land (A \Rightarrow \perp)$ (Crabbé's rule [1]) the proposition $B \Rightarrow \perp$ has a proof, but no normal proof.

We have proved a normalization theorem: proofs normalize in a theory modulo if this theory bears a pre-model [3]. A pre-model is a many-valued model whose truth values are reducibility candidates, i.e. sets of proof-terms. Hence we first define proof-terms, then reducibility candidates and finally pre-models.

**Definition 1 (Proof-term).** We write $t, u...$ for terms of the language. Proof-terms denoted by $\pi, \sigma...$ and are inductively defined as follows.
$$
\begin{array}{l@{\qquad}l}
\pi ::= & \alpha \\
& \lambda\alpha \pi \mid (\pi \pi') \\
& \langle\pi, \pi'\rangle \mid \text{fst}(\pi) \mid \text{snd}(\pi) \\
& i(\pi) \mid j(\pi) \mid \delta(\pi_1, \alpha\pi_2, \beta\pi_3) \\
& I \\
& \delta_{\perp}(\pi) \\
& \lambda x \pi \mid (\pi t) \\
& \langle t, \pi\rangle \mid \delta_{\exists}(\pi, x\alpha\pi')
\end{array}
$$

Each proof-term construction corresponds to an intuitionistic natural deduc-
tion rule: terms of the form α express proofs built with the axiom rule, terms
of the form λα π and (π π') express proofs built with the introduction and
elimination rules of the implication, terms of the form ⟨π, π'⟩ and fst(π), snd(π)
express proofs built with the introduction and elimination rules of the conjunc-
tion, terms of the form i(π), j(π) and δ(π₁, απ₂, βπ₃) express proofs built with
the introduction and elimination rules of the disjunction, the term I expresses
the proof built with the introduction rule of the truth, terms of the form δ⊥(π)
express proofs built with the elimination rule of the contradiction, terms of the
form λx π and (π t) express proofs built with the introduction and elimination
rules of the universal quantifier and terms of the form ⟨t, π⟩ and δ∃(π, xαπ') ex-
press proofs built with the introduction and elimination rules of the existential
quantifier.

**Definition 2 (Reduction).** Reduction on proof-terms is defined as the con-
textual closure of the following rules that eliminate cuts step by step.

$$
\begin{align*}
(\lambda\alpha \pi_1 \pi_2) \triangleright (\pi_2/\alpha)\pi_1 & \qquad (\lambda x \pi t) \triangleright (t/x)\pi \\
fst(\langle\pi_1, \pi_2\rangle) \triangleright \pi_1 & \qquad snd(\langle\pi_1, \pi_2\rangle) \triangleright \pi_2 \\
\delta(i(\pi_1), \alpha\pi_2, \beta\pi_3) \triangleright (\pi_1/\alpha)\pi_2 & \qquad \delta(j(\pi_1), \alpha\pi_2, \beta\pi_3) \triangleright (\pi_1/\beta)\pi_3 \\
\delta_{\exists}(\langle t, \pi_1 \rangle, \alpha x \pi_2) \triangleright (t/x, \pi_1/\alpha)\pi_2 &
\end{align*}
$$

We write $\triangleright^*$ for the reflexive-transitive closure of the relation $\triangleright$.

In the following, the techniques are usual for normalization proofs by reducibility.
The setting, however, is different.

**Definition 3 (Reducibility candidates).** A proof-term is said to be neutral if it is a proof variable or an elimination (i.e. of the form (π π'), fst(π), snd(π), δ(π₁, απ₂, βπ₃), δ⊥(π), (π t), δ∃(π, xαπ')), but not an introduction. A set R of proof-terms is a reducibility candidate if

- whenever $\pi \in R$, then $\pi$ is strongly normalizable,

- whenever $\pi \in R$ and $\pi \triangleright^* \pi'$ then $\pi' \in R$,

- whenever $\pi$ is neutral and if for every $\pi'$ such that $\pi \triangleright^1 \pi'$, $\pi' \in R$ then $\pi \in R$.

We write $\mathcal{CR}$ for the set of all reducibility candidates.
**Definition 4.** Let $\mathcal{SN}$ be the set of all strongly normalizable proof terms and $\perp$ be the set of all strongly normalizing proof terms whose normal form is neutral.

It is easy to check that both $\mathcal{SN}$ and $\perp$ are reducibility candidates. Furthermore, they are respectively the maximal and minimal reducibility candidate with respect to inclusion.

**Definition 5 (Pre-model).** A pre-model $\mathcal{M}$ for a many-sorted language $\mathcal{L}$ is given by:

- for every sort $s$ a set $M_s$,

- for every function symbol $f$ of rank $\langle s_1, \dots, s_n, s_{n+1} \rangle$ a mapping $\hat{f}$ from $M_{s_1} \times \dots \times M_{s_n}$ to $M_{s_{n+1}}$,

- for every predicate symbol $P$ of rank $\langle s_1, \dots, s_n \rangle$ a mapping $\hat{P}$ from $M_{s_1} \times \dots \times M_{s_n}$ to $\mathcal{CR}$.

**Definition 6 (Denotation in a pre-model).** Let $\mathcal{M}$ be a pre-model, $\phi$ an assignment mapping any variable $x$ of sort $s$ to an element of $M_s$ and let $t$ be a term of sort $s$. We define the object $\llbracket t \rrbracket_\phi \in M_s$ by induction over the structure of $t$.

- $\llbracket x \rrbracket_\phi = \phi(x)$,

- $\llbracket f(t_1, \dots, t_n) \rrbracket_\phi = \hat{f}(\llbracket t_1 \rrbracket_\phi, \dots, \llbracket t_n \rrbracket_\phi)$.

Let $A$ be a proposition and $\phi$ a well-sorted assignment as above. We define the reducibility candidate $\llbracket A \rrbracket_\phi$ by induction over the structure of $A$.

If $A$ is an atomic proposition $P(t_1, \dots, t_n)$ then $\llbracket A \rrbracket_\phi = \hat{P}(\llbracket t_1 \rrbracket_\phi, \dots, \llbracket t_n \rrbracket_\phi)$.

When $A$ is a non-atomic proposition, its interpretation is defined by the following, usual, equations:

$$ \llbracket B \Rightarrow C \rrbracket_\phi = \{ \pi \in \mathcal{SN} | \pi \triangleright^* \lambda \alpha \pi' \Rightarrow \forall \sigma \in \llbracket B \rrbracket_\phi (\sigma/\alpha) \pi' \in \llbracket C \rrbracket_\phi \} $$

$$ \llbracket B \lor C \rrbracket_\phi = \{ \pi \in \mathcal{SN} \mid \pi \triangleright^* i(\pi_1) \Rightarrow \pi_1 \in \llbracket B \rrbracket_\phi \land \pi \triangleright^* j(\pi_2) \Rightarrow \pi_2 \in \llbracket C \rrbracket_\phi \} $$

$$ \llbracket B \land C \rrbracket_\phi = \{ \pi \in \mathcal{SN} | \pi \triangleright^* \langle \pi_1, \pi_2 \rangle \Rightarrow (\pi_1 \in \llbracket B \rrbracket_\phi \land \pi_2 \in \llbracket C \rrbracket_\phi) \} $$

$$ \llbracket \top \rrbracket_\phi = \mathcal{SN} $$

$$ \llbracket \bot \rrbracket_\phi = \mathcal{SN} $$

$$ \llbracket \exists x B \rrbracket_\phi = \{ \pi \in \mathcal{SN} | \pi \triangleright^* \langle t, \pi' \rangle \Rightarrow \exists X \in M_s \pi' \in \llbracket B \rrbracket_{\phi, X/x} \} $$

$$ \llbracket \forall x B \rrbracket_\phi = \{ \pi \in \mathcal{SN} | \pi \triangleright^* \lambda x \pi' \Rightarrow \forall X \in M_s \forall t \in \mathcal{T} (t/x) \pi' \in \llbracket B \rrbracket_{\phi, X/x} \} $$

where $\mathcal{T}$ is the set of terms of the language.

**Definition 7.** A pre-model is said to be a pre-model of a congruence $\equiv$ if when $A \equiv B$ then for every assignment $\phi$, $\llbracket A \rrbracket_\phi = \llbracket B \rrbracket_\phi$.

**Theorem 1 (Normalization).** [3] If a congruence $\equiv$ has a pre-model all proofs modulo $\equiv$ strongly normalize.

In this article we will be able to shorten some proofs using the following remark; it simply states that the previous definition can also be reformulated in a more conventional way.
**Proposition 1.** A proof term $\sigma$ belongs to $[[A \Rightarrow B]]_\phi$ if and only if for any proof term $\pi \in [[A]]_\phi$, $(\sigma \pi) \in [[B]]_\phi$.

A proof term $\sigma$ belongs to $[[\forall x_s A]]_\phi$ if and only if for any term $t$ of the language and any element $X$ of $M_s$, $(\sigma t) \in [[A]]_{\phi, X/t}$.

*Proof.* We only detail the first case, both proofs bear no originality. Suppose that for any $\pi \in [[A]]_\phi$, $(\sigma \pi) \in [[B]]_\phi$. Since $[[B]]_\phi$ is a reducibility candidate, it is not empty it contains all the variables, so we know that such a $\pi$ exists. Thus $(\sigma \pi)$ is $\mathcal{SN}$ and so is $\sigma$. Now, if $\sigma \triangleright^* \lambda\alpha\sigma'$ then for any $\pi \in [[A]]_\phi$, we know that $(\sigma \pi) \in [[B]]_\phi$ and $(\sigma \pi) \triangleright^* (\pi/\alpha)\sigma'$. So $(\pi/\alpha)\sigma' \in [[B]]_\phi$. The converse condition is well-known.

## 2 A completeness result for intuitionistic predicate logic

We recall in this section a completeness theorem for intuitionistic predicate logic, using a notion of model based on Heyting algebras.

**Definition 8 (Complete lattice).** A structure $\langle B, \leq, \min, \max, \cap, \cup, \bigcap, \bigcup \rangle$ is a complete lattice if $\leq$ is an order relation:

$$- x \leq x,$$

$$- x \leq y \Rightarrow y \leq x \Rightarrow x = y,$$

$$- x \leq y \Rightarrow y \leq z \Rightarrow x \leq z,$$

min and max are minimum and maximum elements:

$$- \min \leq x,$$

$$- x \leq \max,$$

$x \cap y$ is the greatest lowerbound of $x$ and $y$ and $x \cup y$ is the least upperbound of $x$ and $y$:

$$- x \cap y \leq x,$$

$$- x \cap y \leq y,$$

$$- z \leq x \Rightarrow z \leq y \Rightarrow z \leq x \cap y,$$

$$- x \leq x \cup y,$$

$$- y \leq x \cup y,$$

$$- x \leq z \Rightarrow y \leq z \Rightarrow x \cup y \leq z,$$

$\cap$ and $\cup$ (infinite greatest lowerbound and least upperbound) are functions from $\wp(B)$ to $B$ such that:

$$- x \in a \Rightarrow \bigcap a \leq x,$$

$$- (\forall x \in a \ c \leq x) \Rightarrow c \leq \bigcap a,$$

$$- x \in a \Rightarrow x \leq \bigcup a,$$

$$- (\forall x \in a \ x \leq c) \Rightarrow \bigcup a \leq c.$$

**Definition 9 (Complete Heyting algebra).** A structure $\langle B, \leq, \cap, \cup, \min, \max, \bigcap, \bigcup, \rightarrow \rangle$ is a complete Heyting algebra if it is a complete lattice and:
$$ - x \leq y \rightarrow z \Leftrightarrow x \cap y \leq z. $$

**Definition 10 (Intuitionistic model).** Let $\mathcal{L}$ be a language an intuitionistic model of $\mathcal{L}$ is formed with:

- a set $E$,

- a complete Heyting algebra $B$,

- for each function symbol $f$ of arity $n$ a function $\hat{f}$ from $E^n$ to $E$,

- for each predicate symbol $P$ of arity $n$ a function $\hat{P}$ from $E^n$ to $B$.

**Definition 11 (Denotation).** Given a model $\mathcal{M}$, a proposition $A$ and an assignment $\phi$, we define $|A|_{\phi}$ as follows:

- $|x|_{\phi} = \phi(x)$,

- $|f(t_1, ..., t_n)|_{\phi} = \hat{f}(|t_1|_{\phi}, ..., |t_n|_{\phi})$,

- $|P(t_1, ..., t_n)|_{\phi} = \hat{P}(|t_1|_{\phi}, ..., |t_n|_{\phi})$,

- $|\perp|_{\phi} = \min$,

- $|\top|_{\phi} = \max$,

- $|A \Rightarrow B|_{\phi} = |A|_{\phi} \rightarrow |B|_{\phi}$,

- $|A \wedge B|_{\phi} = |A|_{\phi} \cap |B|_{\phi}$,

- $|A \vee B|_{\phi} = |A|_{\phi} \cup |B|_{\phi}$,

- $|\forall x A|_{\phi} = \bigcap \{|A|_{\phi, v/x} | v \in E\}$,

- $|\exists x A|_{\phi} = \bigcup \{|A|_{\phi, v/x} | v \in E\}$.

**Definition 12 (Validity).** A proposition $A$ is valid in the model $\mathcal{M}$, or $\mathcal{M}$ is a model of $A$ ($\mathcal{M} \models A$), if for every assignment $\phi$, $|A|_{\phi}$ is equal to $\max$.

**Theorem 2.** (Soundness and completeness) [13] A sequent $\Gamma \vdash A$ is intuitionistically provable if and only if the proposition $A$ is valid in all models of $\Gamma$.

# 3 An alternative presentation of arithmetic

Heyting arithmetic is usually presented as a theory in predicate logic with the axioms of Definition 13 below. Before we give a presentation of arithmetic in deduction modulo, we shall give an alternative presentation $HA_{Class}$ of arithmetic in predicate logic in Definition 17 below and prove the equivalence with $HA$. This equivalence is proved in several steps using two intermediate theory. Let us first recall the usual presentation of arithmetic.

## 3.1 Heyting arithmetic

**Definition 13 (HA).** The language of the theory HA is formed with the symbols $0, S, +, \times$ and $=$. The axioms are the axioms of equality corresponding to these symbols and the propositions

$$ \forall x \forall y (S(x) = S(y) \Rightarrow x = y) $$

$$ \forall x \neg(0 = S(x)) $$

$$ ((0/x)P \Rightarrow \forall y ((y/x)P \Rightarrow (S(y)/x)P) \Rightarrow \forall n (n/x)P) $$

$$ \forall y (0 + y = y) \qquad \forall x \forall y (S(x) + y = S(x + y)) $$

$$ \forall y (0 \times y = 0) \qquad \forall x \forall y (S(x) \times y = x \times y + y) $$
## 3.2 Heyting arithmetic with a Pred symbol

Our first step on the way to $HA_{Class}$ is the theory $HA_{Pred}$.

**Definition 14 (HA$_{Pred}$).** The theory HA$_{Pred}$ is the extension of HA with with a symbol Pred and the axioms

$$Pred(0) = 0$$

$$Pred(S(x)) = x$$

$$\forall x \forall y (x = y \Rightarrow Pred(x) = Pred(y))$$

We prove that $HA_{Pred}$ is a conservative extension of HA.

**Proposition 2.** *The proposition*

$$\forall x (x = 0 \lor \exists y x = S(y))$$

is provable in HA.

*Proof.* Using the induction scheme.

**Proposition 3.** *The proposition*

$$\forall x \exists y ((x = 0 \Rightarrow y = 0) \land \forall z (x = S(z) \Rightarrow y = z))$$

is provable in HA.

*Proof.* Using Proposition 2, we prove it for the case $x = 0$ and $x = S(x')$. For $x = 0$ we have to prove

$$\exists y ((0 = 0 \Rightarrow y = 0) \land \forall z (0 = S(z) \Rightarrow y = z))$$

which is provable with $y = 0$ and for $x = S(x')$

$$\exists y ((S(x') = 0 \Rightarrow y = 0) \land \forall z (S(x') = S(z) \Rightarrow y = z))$$

which is provable for $y = x'$.

**Proposition 4.** *The theory HA$_{Pred}$ is a conservative extension of HA.*

*Proof.* By Skolem theorem for constructive logic (see for instance [5]), as the proposition

$$\forall x \exists y ((x = 0 \Rightarrow y = 0) \land \forall z (x = S(z) \Rightarrow y = z))$$

is provable, the extension of HA with the axiom

$$\forall x ((x = 0 \Rightarrow Pred(x) = 0) \land \forall z (x = S(z) \Rightarrow Pred(x) = z))$$
is conservative. We prove that the three extra axioms of HA<sub>Pred</sub> are consequences of this proposition. For the first, from

$$ \forall x ((x = 0 \Rightarrow Pred(x) = 0) \land \forall z (x = S(z) \Rightarrow Pred(x) = z)) $$

we deduce

$$ 0 = 0 \Rightarrow Pred(0) = 0 $$

and thus

$$ Pred(0) = 0 $$

For the second, from

$$ \forall x ((x = 0 \Rightarrow Pred(x) = 0) \land \forall z (x = S(z) \Rightarrow Pred(x) = z)) $$

we deduce

$$ \forall z (S(x) = S(z) \Rightarrow Pred(S(x)) = z) $$

hence

$$ S(x) = S(x) \Rightarrow Pred(S(x)) = x $$

and

$$ Pred(S(x)) = x $$

For the third, using Proposition 2, we prove it for the case $y = 0$ and $y = S(y')$. For $y = 0$, we have to prove

$$ x = 0 \Rightarrow Pred(x) = 0 $$

and for $y = S(y')$, we have to prove

$$ x = S(y') \Rightarrow Pred(x) = y' $$

and both propositions are consequences of the proposition above.

### 3.3 The theory HA<sub>N</sub>

We consider now a theory whose domain of discourse is not restricted to natural numbers, that that may contain other objects. Thus, we introduce a predicate symbol N to characterize natural numbers. We also introduce a predicate Null to characterize 0.

**Definition 15 (HA<sub>N</sub>).* The language of the theory HA<sub>N</sub> is formed with the symbols 0, S, +, ×, =, Pred, Null and N. The axioms are the axioms of equality (including those related to Pred, Null and N) and the propositions

$$ (0/x)P \Rightarrow \forall y (N(y) \Rightarrow (y/x)P \Rightarrow (S(y)/x)P) \Rightarrow \forall n (N(n) \Rightarrow (n/x)P) $$
<table>
  <tr>
    <td>$N(0)$</td>
    <td>$\forall x (N(x) \Rightarrow N(S(x)))$</td>
  </tr>
  <tr>
    <td>$Pred(0) = 0$</td>
    <td>$\forall x (Pred(S(x)) = x)$</td>
  </tr>
  <tr>
    <td>$Null(0)$</td>
    <td>$\forall x (\neg Null(S(x)))$</td>
  </tr>
  <tr>
    <td>$\forall y (0 + y = y)$</td>
    <td>$\forall x \forall y (S(x) + y = S(x + y))$</td>
  </tr>
  <tr>
    <td>$\forall y (0 \times y = 0)$</td>
    <td>$\forall x \forall y (S(x) \times y = x \times y + y)$</td>
  </tr>
</table>

In the induction scheme, all the symbols, including Pred, Null and N may
occur in the proposition P

We define a translation from the language of HA<sub>Pred</sub> to the language of HA<sub>N</sub>.

**Definition 16 (Translation).**

- $|P| = P$, if $P$ is atomic, $|\top| = \top$, $|\bot| = \bot$, $|A \land B| = |A| \land |B|$, $|A \lor B| =$
$|A| \lor |B|$, $|A \Rightarrow B| = |A| \Rightarrow |B|,$

- $|\forall x A| = \forall x (N(x) \Rightarrow |A|)$, $|\exists x A| = \exists x (N(x) \land |A|)$.

Now we want to prove that HA<sub>Pred</sub> and HA<sub>N</sub> are equivalent, in the sense
that a proposition A is provable in HA<sub>Pred</sub> if and only if its translation |A| is
provable in HA<sub>N</sub>.

We first prove that HA<sub>N</sub> is an extension of HA<sub>Pred</sub>.

**Proposition 5.** If A is an axiom of HA<sub>Pred</sub> then |A| is provable in HA<sub>N</sub>.

*Proof.* The translations of the axioms of equality of HA<sub>Pred</sub> are obvious consequences the axioms of equality of HA<sub>N</sub>.

By the axioms of equality we have

$$
\forall x \forall y (S(x) = S(y) \Rightarrow Pred(S(x)) = Pred(S(y)))
$$

hence

$$
\forall x \forall y (S(x) = S(y) \Rightarrow x = y)
$$

and

$$
\forall x (N(x) \Rightarrow \forall y (N(y) \Rightarrow (S(x) = S(y) \Rightarrow x = y)))
$$

By the axioms of equality we have

$$
\forall x (0 = S(x) \Rightarrow (\mathrm{Null}(0) \Rightarrow \mathrm{Null}(S(x))))
$$

hence

$$
\forall x \neg(0 = S(x))
$$

and

$$
\forall x (N(x) \Rightarrow \neg(0 = S(x)))
$$

Finally, Let P be an arbitrary proposition in the language of HA<sub>Pred</sub>. Then the relativization of instance of the induction scheme corresponding to the proposition P is an instance of the induction scheme of HA<sub>N</sub>.

The relativization of the axioms of addition, multiplication and predeces-
sor of HA<sub>Pred</sub> are consequences of the axioms of addition, multiplication and
predecessor of HA<sub>N</sub>.
**Proposition 6.** *The propositions*

1. $\forall x \forall y ((N(x) \land N(y)) \Rightarrow N(x + y))$

2. $\forall x \forall y ((N(x) \land N(y)) \Rightarrow N(x \times y))$

3. $\forall x (N(x) \Rightarrow N(Pred(x)))$

are provable in HA$_N$.

*Proof.* For proposition 1, we introduce $N(x)$ and $N(y)$ and we prove $N(x + y)$. An instance of the induction scheme is

$$N(0 + y) \Rightarrow \forall x (N(x + y) \Rightarrow (N(S(x) + y))) \Rightarrow \forall x (N(x) \Rightarrow N(x + y))$$

Thus we are reduced to prove

$$\begin{array}{l} N(0 + y) \\ \forall x (N(x + y) \Rightarrow (N(S(x) + y))) \\ N(x) \end{array}$$

that can be proved with the hypotheses, the axioms of addition, the axioms of equality and the axiom $\forall x (N(x) \Rightarrow (N(S(x))))$. Proposition 2 is proved in the same way with the help of Proposition 2.

For proposition 3, an instance of the induction scheme is

$$N(Pred(0)) \Rightarrow \forall x (N(Pred(x) \Rightarrow N(Pred(S(x))))) \Rightarrow \forall x (N(x) \Rightarrow N(Pred(x)))$$

Thus we are reduced to prove

$$\begin{array}{l} N(Pred(0)) \\ \forall x (N(Pred(x)) \Rightarrow N(Pred(S(x)))) \end{array}$$

the first proposition can be proved with the axioms of predecessor, the axioms of equality and the axiom $N(0)$. We prove the second by induction. For $x = 0$ we have to prove

$$(N(Pred(0)) \Rightarrow N(Pred(S(0))))$$

that is equivalent to $N(0) \Rightarrow N(0)$ that is obviously provable. Then assume the proposition holds for $x$, we prove it for $S(x)$:

$$\forall x (N(Pred(S(x))) \Rightarrow N(Pred(S(S(x)))))$$

that is equivalent to

$$N(x) \Rightarrow N(S(x))$$

that is a consequence of the axiom $\forall x (N(x) \Rightarrow N(S(x)))$.

**Proposition 7.** Let $t$ be a term in the language $0, S, +, \times, Pred$ whose variables are $x_1, ..., x_n$. Then the sequent $N(x_1), ..., N(x_n) \vdash N(t)$ is provable.

*Proof.* By induction on term structure, using Proposition 6, and the fact that $N(0)$ and $\forall x (N(x) \Rightarrow N(S(x)))$ are axioms.
**Proposition 8.** If the sequent HA<sub>N</sub>, Γ, N(x) ⊢ A is provable and x is free neither in Γ nor in A, then the sequent HA<sub>N</sub>, Γ ⊢ A is provable.

*Proof.* We instantiate all free occurrences of x in the proof by 0 and get a proof of HA<sub>N</sub>, Γ, N(0) ⊢ A. As N(0) is an axiom of HA<sub>N</sub> we do not need to repeat it.

**Proposition 9.** Let A be a closed proposition in the language of HA<sub>Pred</sub>. If A is provable in HA<sub>Pred</sub> then |A| is provable in HA<sub>N</sub>.

*Proof.* We prove, more generally, that if the sequent HA<sub>Pred</sub>, Γ ⊢ A is provable then the sequent HA<sub>N</sub>, |Γ|, N(x<sub>1</sub>), ..., N(x<sub>n</sub>) ⊢ |A|, where x<sub>1</sub>, ..., x<sub>n</sub> are the free variables of Γ and A, is provable.

We proceed by induction on the structure of the proof of the sequent HA<sub>Pred</sub>, Γ ⊢ A using Proposition 5 for axioms, Proposition 7 for quantifier rules and Proposition 8 to eliminate spurious hypotheses after each rule.

- If the last rule of the proof of HA<sub>Pred</sub>, Γ ⊢ A is the elimination of the implication

$$ \frac{\frac{\pi_1}{\text{HA}_{\text{Pred}}, \Gamma \vdash C \Rightarrow D} \qquad \frac{\pi_2}{\text{HA}_{\text{Pred}}, \Gamma \vdash C}}{\text{HA}_{\text{Pred}}, \Gamma \vdash D} $$

then, by induction hypothesis, we get proofs of HA<sub>N</sub>, N(x<sub>1</sub>), ..., N(x<sub>n</sub>), N(y<sub>1</sub>), ..., N(y<sub>p</sub>), |Γ| ⊢ |C| ⇒ |D| and HA<sub>N</sub>, N(x<sub>1</sub>), ..., N(x<sub>n</sub>), |Γ| ⊢ |C|. By weakening, we get a proof of the sequent HA<sub>N</sub>, N(x<sub>1</sub>), ..., N(x<sub>n</sub>), N(y<sub>1</sub>), ..., N(y<sub>p</sub>), |Γ| ⊢ |C|. Using an elimination of the implication, we get a proof of HA<sub>N</sub>, N(x<sub>1</sub>), ..., N(x<sub>n</sub>), N(y<sub>1</sub>), ..., N(y<sub>p</sub>), |Γ| ⊢ |D| and using Proposition 8, we eliminate the spurious hypotheses in this proof.

- If the last rule of the proof of HA<sub>Pred</sub>, Γ ⊢ A is the elimination of the universal quantifier

$$ \frac{\pi}{\text{HA}_{\text{Pred}}, \Gamma \vdash \forall x C} \qquad \frac{\text{HA}_{\text{Pred}}, \Gamma \vdash (t/x)C}{\text{HA}_{\text{Pred}}, \Gamma \vdash (t/x)C} $$

then, by induction hypothesis, we get a proof of HA<sub>N</sub>, N(x<sub>1</sub>), ..., N(x<sub>n</sub>), |Γ| ⊢ ∀x (N(x) ⇒ |C|). Let y<sub>1</sub>, ..., y<sub>p</sub> be the variables of t that are not in x<sub>1</sub>, ..., x<sub>n</sub>. By weakening, we get a proof of HA<sub>N</sub>, N(x<sub>1</sub>), ..., N(x<sub>n</sub>), N(y<sub>1</sub>), ..., N(y<sub>p</sub>), |Γ| ⊢ ∀x (N(x) ⇒ |C|). By Proposition 7 and weakening we have a proof of HA<sub>N</sub>, N(x<sub>1</sub>), ..., N(x<sub>n</sub>), N(y<sub>1</sub>), ..., N(y<sub>p</sub>), |Γ| ⊢ N(t). Using an elimination of the universal quantifier and an elimination of the implication, we get a proof of HA<sub>N</sub>, N(x<sub>1</sub>), ..., N(x<sub>n</sub>), N(y<sub>1</sub>), ..., N(y<sub>p</sub>), |Γ| ⊢ |(t/x)C| and using Proposition 8, we eliminate the spurious hypotheses in this proof.

The other cases are similar.

We then prove that the extension is conservative.

**Proposition 10.** Let A be a closed proposition in the language of HA<sub>Pred</sub>. If |A| is provable in HA<sub>N</sub> then A is provable in HA<sub>Pred</sub>.
*Proof.* Assume that $|A|$ is valid in all models of $HA_N$. We want to prove that $A$ is valid in all models of $HA_{Pred}$.

Consider a model $\mathcal{M}$ of $HA_{Pred}$. Let $\mathcal{N}$ be the model whose domain is the same as $\mathcal{M}$, the denotations of the symbols of $HA_{Pred}$ being the same as in $\mathcal{M}$. The denotation of the symbol Null maps $a$ to $\hat{=} (a, \emptyset)$ and $N$ denoting the function taking the value max everywhere.

Then we prove that $\mathcal{N}$ is a model of $HA_N$.

As $\mathcal{N}$ is a model the axioms of equality of all the symbols of $HA_{Pred}$. It is routine to check that it is also a model of the axioms of equality for the symbols Null and $N$ as the propositions

$$x = y \Rightarrow x = 0 \Rightarrow y = 0$$

and

$$x = y \Rightarrow \top \Rightarrow \top$$

are valid in $\mathcal{M}$ and hence in $\mathcal{N}$.

Let us prove that it is a model of the induction scheme of $HA_N$. Consider an instance $I$ of the induction scheme of $HA_N$ for the proposition $A$. Consider the proposition $A'$ obtained by replacing all the propositions of the form $Null(t)$ by $t = 0$ and all the propositions of the form $N(t)$ by $\top$ and then and all atomic propositions $(Pred(t)/y)P$ by $\forall y (((t = 0 \land y = 0) \lor t = S(y)) \Rightarrow P)$ until there is no symbol $Pred$ left. Then, by induction over the structure of $A$, for all assignments $\phi$, $[[A]]_\phi = [[A']]]_\phi$. The only point to check is that the propositions $(Pred(t)/y)P$ and $\forall y (((t = 0 \land y = 0) \lor (t = S(y) \Rightarrow P))$ have the same denotation. This is because the equivalence

$$(Pred(t)/y)P \Leftrightarrow \forall y (((t = 0 \land y = 0) \lor t = S(y)) \Rightarrow P)$$

is provable. Indeed, the equivalence

$$(Pred(t)/y)P \Leftrightarrow \forall y (y = Pred(t) \Rightarrow P)$$

is provable and the equivalence

$$y = Pred(x) \Leftrightarrow ((x = 0 \land y = 0) \lor x = S(y))$$

can be proved by induction on $x$. Consider the instance $I'$ of the induction scheme of $HA_{Pred}$ for the proposition $A'$. This proposition has the same denotation in $\mathcal{M}$ and in $\mathcal{N}$ this it is valid in $\mathcal{N}$, and it is easy to check that $I$ and $I'$ have the same denotation in $\mathcal{N}$. Thus $I$ is valid in $\mathcal{N}$.

The other axioms of $HA_N$ are obviously valid in $\mathcal{N}$.

Thus $\mathcal{N}$ is a model of $HA_N$ and $|A|$ is valid in $\mathcal{N}$. By construction of $\mathcal{N}$, $A$ and $|A|$ have the same denotation in $\mathcal{N}$, hence $A$ is valid in $\mathcal{N}$ and thus also in $\mathcal{M}$.

*Remark 1.* The variant of $HA_N$ where the induction scheme is replaced by the weaker axiom

$$(0/x)P \Rightarrow \forall y ((y/x)P \Rightarrow (S(y)/x)P) \Rightarrow \forall n (N(n) \Rightarrow (n/x)P)$$
is equivalent. First this scheme is an obvious consequence of the induction scheme of HA$_N$. Conversely, the instance of the induction scheme of HA$_N$ corresponding to the proposition P is a consequence of the instance of this scheme corresponding to the proposition N(x) ∧ P.

### 3.4 A sort for classes of numbers

Finally, we introduce a second sort for classes of natural numbers and use these number classes to express equality and the induction scheme.

**Definition 17 (HA$_{Class}$).**

The theory HA$_{Class}$ is a many sorted theory with two sorts $ι$ and $κ$. The language contains a constant 0 of sort $ι$, function symbols S and Pred of rank $\langleι, ι\rangle$ and $+$ and $×$ of rank $\langleι, ι, ι\rangle$, predicate symbols $=$ of rank $\langleι, ι\rangle$, Null and N of rank $\langleι\rangle$ and $\in$ of rank $\langleι, κ\rangle$ and for each proposition P in the language 0, S, Pred, $+$, $×$, $=$, Null and N and whose free variables are among x, y$_1$, ..., y$_n$ of sort $ι$, a function symbol $f_{x,y_1,...,y_n,P}$ of rank $\langleι, ..., ι, κ\rangle$. The symbol $f_{x,y_1,...,y_n,P}$ is written $f_P$ when the variables x, y$_1$, ..., y$_n$ are clear from the context. The axioms are

$$ 
\begin{array}{l}
\forall y \forall z (y = z \Leftrightarrow \forall p (y \in p \Rightarrow z \in p)) \\
\forall n (N(n) \Leftrightarrow \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)) \\
\forall x \forall y y_1 \dots \forall y_n (x \in f_{x,y_1,...,y_n} P(y_1, ..., y_n) \Leftrightarrow P)
\end{array}
$$

$$ Pred(0) = 0 \qquad \forall x (Pred(S(x)) = x) $$

$$ Null(0) \qquad \forall x (\neg Null(S(x))) $$

$$ \forall y (0 + y = y) \qquad \forall x \forall y (S(x) + y = S(x + y)) $$

$$ \forall y (0 \times y = 0) \qquad \forall y (S(x) \times y = x \times y + y) $$

We first prove that HA$_{Class}$ is an extension of HA$_N$.

**Proposition 11.** All the propositions provable in HA$_N$ are provable in HA$_{Class}$.

*Proof.* We check that all the axioms of HA$_N$ are provable in HA$_{Class}$.

- The proposition $x = x$ is equivalent to

$$ \forall p (x \in p \Rightarrow x \in p) $$

that is provable.

- Let P be a proposition in the language of HA$_N$. To prove the proposition

$$ y = z \Rightarrow ((y/x)P \Rightarrow (z/x)P) $$

we introduce the propositions $y = z$ and $(y/x)P$ and we prove $(z/x)P$.
The proposition $y = z$ is equivalent to

$$ \forall p (y \in p \Rightarrow z \in p) $$

we apply it to the term associated to $P$ and we get $(y/x)P \Rightarrow (z/x)P$ we deduce $(z/x)P$.

- $N(0)$ is equivalent to $\forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow 0 \in p)$ that is provable

- To prove $N(y) \Rightarrow N(S(y))$, we assume $N(y)$ and we prove $N(S(y))$.

The proposition $N(S(y))$ is equivalent to

$$ \forall p (0 \in p \Rightarrow \forall z (N(z) \Rightarrow z \in p \Rightarrow S(z) \in p) \Rightarrow S(y) \in p) $$

We introduce $p_0$ and prove

$$ (0 \in p_0 \Rightarrow \forall z (N(z) \Rightarrow z \in p_0 \Rightarrow S(z) \in p_0) \Rightarrow S(y) \in p_0) $$

We introduce the hypotheses $0 \in p_0$, $\forall z (N(z) \Rightarrow z \in p_0 \Rightarrow S(z) \in p_0)$ and we prove

$$ S(y) \in p_0 $$

We have $N(y)$, i.e.

$$ \forall p (0 \in p \Rightarrow \forall z (z \in p \Rightarrow S(z) \in p) \Rightarrow y \in p) $$

we deduce

$$ (0 \in p_0 \Rightarrow \forall z (N(z) \Rightarrow z \in p_0 \Rightarrow S(z) \in p_0) \Rightarrow y \in p_0) $$

we deduce

$$ y \in p_0 $$

we deduce

$$ S(y) \in p_0 $$

- To prove $(0/x)P \Rightarrow \forall y (N(y) \Rightarrow (y/x)P \Rightarrow (S(y)/x)P) \Rightarrow \forall n (N(n) \Rightarrow (n/x)P)$ we introduce hypotheses $(0/x)P, \forall y (N(y) \Rightarrow (y/x)P \Rightarrow (S(y)/x)P), N(n)$ and we prove $(n/x)P$.

We have $N(n)$, i.e.

$$ \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) $$

we apply it to the term associated to $P$, and we get

$$ (0/x)P \Rightarrow \forall y (N(y) \Rightarrow (y/x)P \Rightarrow (S(y)/x)P) \Rightarrow (n/x)P $$

we deduce $(n/x)P$

- The axioms of Pred and Null and the axioms of addition and multiplication are axioms of HA<sub>Class</sub>.

We then prove that the extension is conservative.
**Proposition 12.** Let A be a proposition in the language of HA<sub>N</sub>, if A is provable in HA<sub>Class</sub> then it is provable in HA<sub>N</sub>.

*Proof.* The proposition A is valid in all models of HA<sub>Class</sub>. We want to prove that it is valid in all models of HA<sub>N</sub>. Let M be a model of HA<sub>N</sub>. Let M be the domain of M and B be its Heyting algebra.

A function $F$ from $M$ to $B$ is said to be definable if there exists a proposition $P$ in the language of HA<sub>N</sub> with free variables $x, y_1, \dots, y_n$ and an assignment $\phi = b_1/y_1, \dots, b_n/y_n$ such that for every $a$, $F(a) = [P]_{\phi,a/x}$.

We construct a model $\mathcal{N}$ of HA<sub>Class</sub> as follows. We take $N_l = M$ and $N_\kappa$ be the set of definable functions from $M$ to $B$. All the symbols of HA<sub>N</sub> have the same denotation in $\mathcal{N}$ as in $\mathcal{M}$. The symbol $\in$ denotes the function mapping $a$ and $f$ to $f(a)$.

If $f$ is the symbol associated to $P$ then $f$ denotes the function mapping $b_1, \dots, b_n$ to the function mapping $a$ to $[P]_{a/x, b_1/y_1, \dots, b_n/y_n}$. This model is obviously a model of the axioms of Pred and Null, of the axioms of addition and multiplication and of the conversion scheme.

Let us check that it is a model of the axioms

$$y = z \Leftrightarrow \forall p (y \in p \Rightarrow z \in p)$$

and

$$N(n) \Leftrightarrow \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

Let us start with the first of these propositions. For every $P$ in the language of HA<sub>N</sub>, the proposition

$$y = z \Rightarrow (y/x)P \Rightarrow (z/x)P$$

is provable in HA<sub>N</sub>, hence it is valid in $\mathcal{M}$ and thus in $\mathcal{N}$, i.e. for every $c, d$ and $\phi$

$$[y = z \Rightarrow (y/x)P \Rightarrow (z/x)P]_{\phi,c/y,d/z} = \max$$

Thus for every $c, d, P$ and $\phi$ we have

$$[y = z]_{c/y,d/z} \leq [(y/x)P \Rightarrow (z/x)P]_{\phi,c/y,d/z}$$

Hence, for every $c$ and $d$, we have

$$[y = z]_{c/y,d/z} \leq \bigcap_{P, \phi} [(y/x)P \Rightarrow (z/x)P]_{\phi,c/y,d/z}$$

$$[y = z]_{c/y,d/z} \leq [\forall p (y \in p \Rightarrow z \in p)]_{c/y,d/z}$$

$$[y = z \Rightarrow \forall p (y \in p \Rightarrow z \in p)]_{c/y,d/z} = \max$$

and the proposition

$$y = z \Rightarrow \forall p (y \in p \Rightarrow z \in p)$$

is valid in $\mathcal{N}$.
Then we prove that the converse is also valid. The proposition

$$ (y = y \Rightarrow y = z) \Rightarrow y = z $$

is provable in HA<sub>N</sub>, hence it is valid in M and thus in N, i.e. for every c and d

$$ \llbracket (y = y \Rightarrow y = z) \Rightarrow y = z \rrbracket_{c/y,d/z} = \max $$

and

$$ \llbracket ((y/x)w = x \Rightarrow (z/x)w = x) \Rightarrow y = z \rrbracket_{c/w,c/y,d/z} = \max $$

Thus

$$ \llbracket ((y/x)w = x \Rightarrow (z/x)w = x) \rrbracket_{c/w,c/y,d/z} \le \llbracket y = z \rrbracket_{c/y,d/z} $$

Hence, we have

$$ \bigcap_{P, \phi} \llbracket (y/x)P \Rightarrow (z/x)P \rrbracket_{\phi, c/y, d/z} \le \llbracket y = z \rrbracket_{c/y, d/z} $$

$$ \llbracket \forall p (y \in p \Rightarrow z \in p) \rrbracket_{c/y,d/z} \le \llbracket y = z \rrbracket_{c/y,d/z} $$

$$ \llbracket \forall p (y \in p \Rightarrow z \in p) \Rightarrow y = z \rrbracket_{c/y,d/z} = \max $$

and the proposition

$$ \forall p (y \in p \Rightarrow z \in p) \Rightarrow y = z $$

is valid in N.

Let us now prove that the second proposition is also valid. For every P in the language of HA<sub>N</sub>, the proposition

$$ N(n) \Rightarrow ((0/z)P \Rightarrow \forall y (N(y) \Rightarrow (y/z)P \Rightarrow (S(y)/z)P) \Rightarrow (n/z)P) $$

is provable in HA<sub>N</sub>, hence it is valid in M and thus in N, i.e. for every a and φ

$$ \llbracket N(n) \Rightarrow ((0/z)P \Rightarrow \forall y (N(y) \Rightarrow (y/z)P \Rightarrow (S(y)/z)P) \Rightarrow (n/z)P) \rrbracket_{\phi,a/n} = \max $$

Thus for every a, P and φ, we have

$$ \llbracket N(n) \rrbracket_{a/n} \le \llbracket ((0/z)P \Rightarrow \forall y (N(y) \Rightarrow (y/z)P \Rightarrow (S(y)/z)P) \Rightarrow (n/z)P) \rrbracket_{\phi,a/n} $$

Hence for every a we have

$$ \llbracket N(n) \rrbracket_{a/n} \le \bigcap_{P, \phi} \llbracket ((0/z)P \Rightarrow \forall y (N(y) \Rightarrow (y/z)P \Rightarrow (S(y)/z)P) \Rightarrow (n/z)P) \rrbracket_{\phi, a/n} $$

$$ \llbracket N(n) \rrbracket_{a/n} \le \llbracket \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) \rrbracket_{a/n} $$

$$ \llbracket N(n) \Rightarrow \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) \rrbracket_{a/n} = \max $$

Thus, the proposition

$$ N(n) \Rightarrow \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) $$
is valid in $\mathcal{N}$.

Then we prove that the converse is also valid. The proposition

$$ (N(0) \Rightarrow \forall y (N(y) \Rightarrow N(y) \Rightarrow N(S(y))) \Rightarrow N(n)) \Rightarrow N(n) $$

is provable in $HA_N$, hence it is valid in $\mathcal{M}$ and thus in $\mathcal{N}$, i.e. for every $a$

$$ \llbracket (N(0) \Rightarrow \forall y (N(y) \Rightarrow N(y) \Rightarrow N(S(y))) \Rightarrow N(n)) \Rightarrow N(n) \rrbracket_{a/n} = \max $$

$$ \llbracket (N(0) \Rightarrow \forall y (N(y) \Rightarrow N(y) \Rightarrow N(S(y))) \Rightarrow N(n)) \rrbracket_{a/n} \leq \llbracket N(n) \rrbracket_{a/n} $$

Hence we have

$$ \bigcap_{P, \phi} \llbracket (0/z)P \Rightarrow \forall y (N(y) \Rightarrow (y/z)P \Rightarrow (S(y)/z)P) \Rightarrow (n/z)P) \rrbracket_{\phi, a/n} \leq \llbracket N(n) \rrbracket_{a/n} $$

$$ \llbracket \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) \rrbracket_{a/n} \leq \llbracket N(n) \rrbracket_{a/n} $$

$$ \llbracket \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) \Rightarrow N(n) \rrbracket_{a/n} = \max $$

and the proposition

$$ \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) \Rightarrow N(n) $$

is valid in $\mathcal{N}$.

Thus the model $\mathcal{N}$ is a model of $HA_{Class}$, thus $A$ is valid in $\mathcal{N}$. Hence it is valid in $\mathcal{M}$.

*Remark 2.* The variant of $HA_{Class}$ such where the axiom

$$ N(n) \Leftrightarrow \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) $$

is replaced by

$$ N(n) \Leftrightarrow \forall p (0 \in p \Rightarrow \forall y (y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) $$

is also a conservative extension of $HA_N$.

We favor the first formulation that allows more natural induction proofs (see Section 7).

# 4 Arithmetic in deduction modulo

## 4.1 The theory HA$_{→}$

**Definition 18 (The theory HA$_{→}$).** The language of the theory HA$_{→}$ is the same as that of the theory HA$_{Class}$. This theory has no axioms and the rewrite rules

$$ \begin{array}{l} y = z \longrightarrow \forall p (y \in p \Rightarrow z \in p) \\ N(n) \longrightarrow \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) \end{array} $$

$$ x \in f_{x, y_1, \dots, y_n, P}(y_1, \dots, y_n) \longrightarrow P $$

$$ \mathrm{Pred}(0) \longrightarrow 0 $$

$$ \mathrm{Pred}(S(x)) \longrightarrow x $$

$$ \mathrm{Null}(0) \longrightarrow \top $$

$$ \mathrm{Null}(S(x)) \longrightarrow \bot $$

$$ 0 + y \longrightarrow y $$

$$ S(x) + y \longrightarrow S(x + y) $$

$$ 0 \times y \longrightarrow 0 $$

$$ S(x) \times y \longrightarrow x \times y + y $$
**Proposition 13.** The theory HA$_{→}$ is a conservative extension of HA.

*Proof.* It is equivalent to HA$_{Class}$.

*Remark 3.* The variant of HA$_{→}$ where the rule

$$N(n) \rightarrow \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

is replaced by

$$N(n) \rightarrow \forall p (0 \in p \Rightarrow \forall y (y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

is also a conservative extension of HA.

# 5 Cut elimination

In this section, we build a pre-model to show that HA$_{→}$ has the cut elimination property.

**Proposition 14.** The theory HA$_{→}$ has the cut elimination property.

*Proof.* We build a pre-model as follows. We take $M_t = \mathbb{N}$, $M_\kappa = \mathcal{CR}^\mathbb{N}$. The denotations of 0, $S$, $+$, $\times$, $Pred$ are obvious. We take $\hat{Null}(n) = \mathcal{SN}$. The denotation of $\in$ is the function mapping $n$ and $f$ to $f(n)$. Then we can define the denotation of

$$\forall p (y \in p \Rightarrow z \in p)$$

and the denotation of = accordingly.

To define the denotation of $N$, for each function $f$ of $\mathcal{CR}^\mathbb{N}$ we can define an interpretation $\mathcal{M}_f$ of the language of the proposition

$$\forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

where the symbol $N$ is interpreted by the function $f$. We define the function $\Phi$ from $\mathcal{CR}^\mathbb{N}$ to $\mathcal{CR}^\mathbb{N}$ mapping $f$ to the function mapping the natural number $x$ to the candidate

$$[\forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)]_{x/n}^{\mathcal{M}_f}$$

The order on $\mathcal{CR}^\mathbb{N}$ defined by $f \subseteq g$ if for all $n$, $f(n) \subseteq g(n)$ is a complete order and the function $\Phi$ is monotonous as the occurrence of $N$ is positive in

$$\forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

Hence it has a fixpoint $g$. We interpret the symbol $N$ by the function $g$.

Finally, the denotation of the symbols of the form $f_P$ is defined in the obvious way.

This pre-model is a pre-model of each rule of HA$_{→}$ by construction.

*Remark 4.* Building a premodel for the variant of HA$_{→}$ with the rule

$$N(x) \rightarrow \forall p (0 \in p \Rightarrow \forall y (y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

is even simpler, we do not need to use the fixpoint theorem and we just define the denotation of the proposition $N(n)$ as the denotation of

$$\forall p (0 \in p \Rightarrow \forall y (y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$
# 6 A predicative cut elimination proof

The normalization proof of the previous section is essentially obtained by mapping arithmetic into second order arithmetic and then applying the usual normalization proof of second order arithmetic.

This proof is impredicative, indeed, to define the reducibility candidates interpreting the propositions $t = u$ and $N(t)$ we use a quantification over the set $M_κ$ of functions mapping natural number to reducibility candidates.

We shall now see that it is possible to build also a predicative proof. In this proof, we restrict the set $M_κ$ to contain only some functions from natural numbers to candidates, typically definable functions. Then these functions can be replaced by indices, for instance, a natural number and the quantification over functions from natural numbers to candidates can be replaced by a simple quantification over natural numbers. The difficulty here is that to define the denotation of = and $N$ we must use quantification on elements of the set $M_κ$. To define this set we need to define the notion of definable functions and as the symbols = and $N$ occur in the language, to define this notion we need to use the denotation of the symbols = and $N$. To break this circularity, we give another definition of the interpretation of $t = u$ and $N(t)$ that does not use quantification over the elements of $M_κ$. Then the rewrite rules are not valid by construction anymore and we have to check their validity a posteriori.

Thus, we shall start by constructing the reducibility candidates $E$ and $E'$ used for interpreting equality and $P_n$ used for interpreting the symbol $N$.

## 6.1 The construction of some candidates

**Definition 19.** Let $A$ be a set of strongly normalizing terms. The set $[A]$ is inductively defined by

- if $\pi \in A$ then $\pi \in [A]$,

- if $\pi \in [A]$ and $\pi \triangleright^* \pi'$ then $\pi' \in [A]$,

- if $\pi$ is an elimination and all its one step reducts are in $[A]$ then $\pi \in [A]$.

**Proposition 15.** Let $A$ be a set of strongly normalizing proof-terms. The set $[A]$ is a reducibility candidate and it is the smallest reducibility candidate containing $A$.

*Proof.* The set $[A]$ obviously verifies conditions 2 and 3 of Definition 3. Furthermore, all elements of $A$ are $SN$, all reducts of elements of $SN$ are $SN$, and if all one step reducts of $\pi$ are $SN$, then $\pi \in SN$. Therefore $[A] \subseteq SN$ and thus $[A]$ is a reducibility candidate.

Now let $C$ be a reducibility candidate containing $A$. Given an element $\sigma$ of $[A]$, by induction over the proof that $\sigma \in [A]$, it is immediate to show that $\sigma \in C$.

**Definition 20.** The smallest reducibility candidate $\perp$ can be defined by $\perp = [\emptyset]$. For each strongly normalizing proof-term $\sigma$ we define $C_\sigma$, the smallest reducibility candidate containing $\sigma$, by $C_\sigma = \{\sigma\}$.
**Definition 21.**

$$ 
\begin{aligned}
E &= \{ \pi \in \mathcal{SN} \mid \forall t \ \forall \sigma \in \mathcal{SN} \ (\pi \ t \ \sigma) \in C_{\sigma} \} \\
E' &= \{ \pi \in \mathcal{SN} \mid \forall t \ \forall \sigma \in \mathcal{SN} \ (\pi \ t \ \sigma) \in \mathbb{P} \}
\end{aligned}
$$

Let $P = (P_i)_{i \in \mathbb{N}}$ and $Q = (Q_i)_{i \in \mathbb{N}}$ be two sequences of reducibility candidates, recall that the order defined by $P \subseteq Q$ if for all $n$, $P_n \subseteq Q_n$ is a complete order.

**Definition 22.** Let $\sigma_0$ and $\sigma_S$ be two proof terms and $P$ be a sequence of reducibility candidates, we define the family of candidates $C_n^{\sigma_0, \sigma_S, P}$ by induction on $n$.

$$ C_0^{\sigma_0, \sigma_S, P} = [\{\pi \mid \pi = \sigma_0 \wedge \pi \in \mathcal{SN}\}] $$

$$ C_{n+1}^{\sigma_0, \sigma_S, P} = [\{(\sigma_S \ t \ \rho \ \pi) \in \mathcal{SN} \mid \rho \in P_n \wedge \pi \in C_n^{\sigma_0, \sigma_S, P}\}] $$

It is easy to check that if $P \subseteq Q$ then $C_n^{\sigma_0, \sigma_S, P} \subseteq C_n^{\sigma_0, \sigma_S, Q}$.

**Definition 23 (P-Peano pair).** A pair of proof-terms $\langle \sigma_0, \sigma_S \rangle$ is called a P-Peano pair if

- $\sigma_0$ is $\mathcal{SN}$,

- $\sigma_S$ is $\mathcal{SN}$ and for every term $t$, for every natural number $n$, every proof-term $\rho \in P_n$, and for every proof-term $\pi$ in $C_n^{\sigma_0, \sigma_S, P}$, the term $(\sigma_S \ t \ \rho \ \pi)$ is $\mathcal{SN}$.

It is easy to check that if $P \subseteq Q$ then $(\langle \sigma_0, \sigma_S \rangle$ is a P-Peano pair $\Leftarrow \langle \sigma_0, \sigma_S \rangle$ is a Q-Peano pair).

Finally we define a family of candidates $\Phi(P)$.

**Definition 24.**

$$ (\Phi(P))_n = \{ \pi \in \mathcal{SN} \mid \forall t \forall \sigma_0 \forall \sigma_S \ \langle \sigma_0, \sigma_S \rangle \text{ is a P-Peano pair} \Rightarrow (\pi \ t \ \sigma_0 \ \sigma_S) \in C_n^{\sigma_0, \sigma_S, P} \}. $$

It is easy to check that is $P \subseteq Q$ then $\Phi(P) \subseteq \Phi(Q)$, i.e. that the function $\Phi$ is monotonous.

As this function is monotonous, it has a least fixpoint. Let $(P_i)_{i \in \mathbb{N}}$ be the least fixed point of $\Phi$. By definition

$$ P_n = \{ \pi \in \mathcal{SN} \mid \forall t \forall \sigma_0 \forall \sigma_S \ \langle \sigma_0, \sigma_S \rangle \text{ is a P-Peano pair} \Rightarrow (\pi \ t \ \sigma_0 \ \sigma_S) \in C_n^{\sigma_0, \sigma_S, P} \}. $$

Now that the family $P$ is defined we just write a Peano pair for a P-Peano pair and $C_n^{\sigma_0, \sigma_S}$ for $C_n^{\sigma_0, \sigma_S, P}$.
## 6.2 A pre-model

As in the impredicative construction, we take $M_t = \mathbb{N}$, we interprete the symbols $0, S, +, \times, \text{Pred}$ in the obvious way and we take $\hat{\text{Null}}(n) = \mathcal{SN}$. Then, we define the interpretation of the symbols = and $N$ as follows.

$$ 
\begin{align*}
\hat{=} (n, n) &= E \\
\hat{=} (n, m) &= E' \text{ if } n \neq m \\
\hat{N} (n) &= P_n
\end{align*}
$$

Before we define the set $M_\kappa$ and the interpretation of the symbol $\in$, we introduce a notion of definable function from the set of natural numbers to the set of candidates.

**Definition 25 (Definable function).** A function $f$ from $\mathbb{N}$ to $\mathcal{CR}$ is said to be definable if there exists a proposition $P$ in the language of $\text{HA} \dashv\dashv$ without the symbol $\in$ and an assignment $\phi$ such that for all $n$ $f(n) = [P]_{\phi,n/x}$.

We then define the set $M_\kappa$, as the (countable) set of functions from $\mathbb{N}$ to $\mathcal{CR}$ containing

- definable functions,

- constant functions taking the value $C_\sigma$ for some proof-term $\sigma$,

- and functions mapping $k$ to $C_k^{\sigma_0, \sigma_S}$ for some proof-terms $\sigma_0$ and $\sigma_S$.

Finally, we complete the construction of the pre-model by defining the denotation of $\in$ as the obvious application function and the denotation of the symbols of the form $f_P$ accordingly. The validity of all the rewrite rules of $\text{HA} \dashv\dashv$ is routine, except that of the rules

$$ y = z \longrightarrow \forall p (y \in p \Rightarrow z \in p) $$

and

$$ N(x) \longrightarrow \forall p (0 \in p \Rightarrow (\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p) $$

**Proposition 16.** *The rule*

$$ y = z \longrightarrow \forall p (y \in p \Rightarrow z \in p) $$

*is valid in this pre-model.*

*Proof.* We consider two cases whether $\phi(y) = \phi(z)$ or not.

- If $\phi(y) = \phi(z)$, then $[y = z]_\phi = E$ and we have to prove $[\forall p (y \in p \Rightarrow z \in p)]_\phi = E$. Consider a proof-term $\pi$ in $[\forall p (y \in p \Rightarrow z \in p)]_\phi$, we prove that it is an element of $E$. By definition, $\pi \in \mathcal{SN}$. Consider a term $t$ of sort $\kappa$ and a strongly normalizing proof-term $\sigma$. We have to prove that $(\pi \ t \ \sigma) \in C_\sigma$.
Let $f$ be the constant function equal to $C_\sigma$. This function is an element of $M_\kappa$. We have $\sigma \in C_\sigma = [y \in p]_{\phi,f/p}$. Thus, as $\pi$ is in $[\forall p (y \in p \Rightarrow z \in p)]_\phi$ Proposition 1 ensures that $(\pi t \sigma) \in [z \in p]_{\phi,f/p}$, i.e. $(\pi t \sigma) \in C_\sigma$.

Conversely, consider a proof-term $\pi$ in $E$, we prove that it is an element of $[\forall p (y \in p \Rightarrow z \in p)]_\phi$. By definition $\pi \in \mathcal{SN}$. Consider a term $t$ of sort $\kappa$ and an object $f$ in $M_\kappa$. We have to prove that $(\pi t) \in [y \in p \Rightarrow z \in p]_{\phi,f/p}$. As $\pi$ is strongly normalizing, so is $(\pi t)$. Consider now a proof-term $\sigma \in [y \in p]_{\phi,f/p}$. We have to prove that $(\pi t \sigma) \in [z \in p]_{\phi,f/p}$. Notice that, as $\sigma$ is an element of $[y \in p]_{\phi,f/p}$ and $\phi(y) = \phi(z)$, $\sigma$ is also an element of $[z \in p]_{\phi,f/p}$ and thus of $C_\sigma \subseteq [z \in p]_{\phi,f/p}$. Since $\pi \in E$, $(\pi t \sigma) \in C_\sigma \subseteq [z \in p]_{\phi,f/p}$, i.e. $(\pi t \sigma) \in [z \in p]_{\phi,f/p}$.

If $\phi(y) \neq \phi(z)$, then $[y = z]_\phi = E'$ and we have to prove that $[\forall p (y \in p \Rightarrow z \in p)]_\phi = E'$. Consider a proof-term $\pi$ in $[\forall p (y \in p \Rightarrow z \in p)]_\phi$, we prove that it is an element of $E'$. By definition, $\pi \in \mathcal{SN}$. Consider a term $t$ of sort $\kappa$ and a strongly normalizing proof-term $\sigma$. We have to prove that $(\pi t \sigma) \in \perp$. Let $f$ be the function equal to $C_\sigma$ on $\phi(y)$ and to $\perp$ elsewhere. This function is definable, thus it is an element of $M_\kappa$. We have $\sigma \in C_\sigma = [y \in p]_{\phi,f/p}$. Thus, as $\pi$ is an element of $[\forall p (y \in p \Rightarrow z \in p)]_\phi$, we have $(\pi t \sigma) \in [z \in p]_{\phi,f/p}$, i.e. $(\pi t \sigma) \in \perp$.

Conversely, consider an proof-term $\pi$ in $E'$, we prove that it is an element of $[\forall p (y \in p \Rightarrow z \in p)]_\phi$. By definition $\pi \in \mathcal{SN}$. Consider a term $t$ of sort $\kappa$ and an object $f$ in $M_\kappa$. We have to prove that $(\pi t) \in [y \in p \Rightarrow z \in p]_{\phi,f/p}$. As $\pi$ is strongly normalizing, so is $(\pi t)$. Consider now a proof-term $\sigma$ in $[y \in p]_{\phi,f/p}$; we know $\sigma$ is $\mathcal{SN}$. Since $\pi \in E'$, $(\pi t \sigma) \in \perp \subseteq [z \in p]_{\phi,f/p}$, i.e. $(\pi t \sigma) \in [z \in p]_{\phi,f/p}$.

**Proposition 17.** Let $\langle\sigma_0, \sigma_S\rangle$ be a Peano pair and $f$ be the function of $M_\kappa$ mapping $k$ to $C_k^{\sigma_0, \sigma_S}$. Then

$$ \sigma_0 \in [0 \in p]_{f/p} $$

$$ \sigma_S \in [\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)]_{f/p} $$

*Proof.* As the pair $\langle\sigma_0, \sigma_S\rangle$ is Peano, the term $\sigma_0$ is $\mathcal{SN}$. Thus it is in $C_0^{\sigma_0, \sigma_S} = [0 \in p]_{f/p}$. As the pair $\langle\sigma_0, \sigma_S\rangle$ is Peano, the term $\sigma_S$ is $\mathcal{SN}$. Let $t$ be a term and $n$ a natural number, we have to prove that $(\sigma_S t) \in [N(y) \Rightarrow y \in p \Rightarrow S(y) \in p]_{f/p,n/y}$. Let $\rho$ be a proof-term in $P_n$, we have to prove that $(\sigma_S t \rho) \in [y \in p \Rightarrow S(y) \in p]_{f/p,n/y}$. As the pair $\langle\sigma_0, \sigma_S\rangle$ is Peano, the term $(\sigma_S t \rho)$ is $\mathcal{SN}$. Let $\pi$ be a proof-term in $[y \in p]_{f/p,n/y} = C_n^{\sigma_0, \sigma_S}$, we have to prove that $(\sigma_S t \rho \pi) \in [S(y) \in p]_{f/p,n/y}$. As the pair $\langle\sigma_0, \sigma_S\rangle$ is Peano, the term $(\sigma_S t \rho \pi)$ is $\mathcal{SN}$ and is in $C_{n+1}^{\sigma_0, \sigma_S}$, i.e. in $[S(y) \in p]_{n/y,f/p}$.

**Proposition 18.** Let $f$ be an arbitrary function mapping natural numbers to reducibility candidates and $\sigma_0$ and $\sigma_S$ two proof-terms such that $\sigma_0 \in [0 \in p]_{f/p}$ and $\sigma_S \in [\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p]_{f/p}$ then for all $n$ $C_n^{\sigma_0, \sigma_S} \subseteq [y \in p]_{n/y,f/p}$.

*Proof.* By induction on $n$. For $n = 0$ we have $\sigma_0 \in [0 \in p]_{f/p}$ and thus $C_0^{\sigma_0, \sigma_S} \subseteq [y \in p]_{0/y,f/p}$. Assume the result holds for $n$. To prove that it holds for $n + 1$,
we prove that all the generators of $C_{n+1}^{\sigma_0, \sigma_S}$ are in $[[y \in p]]_{n+1/y,f/p}$. Consider such a term: given a term $t$, a proof term $\rho \in P_n$, a proof-term $\pi' \in C_n^{\sigma_0, \sigma_S}$ and let $\pi = (\sigma_S \ t \ \rho \ \pi')$. we have to check that $\pi \in [[y \in p]]_{n+1/y,f/p}$.

By induction hypothesis $\pi' \in [[y \in p]]_{n/y,f/p}$, hence $\pi \in [[S(y) \in p]]_{n/y,f/p} = [[y \in p]]_{n+1/y,f/p}$.

**Proposition 19.** Let $f$ be an arbitrary function mapping natural numbers to reducibility candidates and $\sigma_0$ and $\sigma_S$ two proof-terms such that $\sigma_0 \in [[0 \in p]]_{f/p}$ and $\sigma_S \in [[\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)]]_{f/p}$. Then, $\langle \sigma_0, \sigma_S \rangle$ is a Peano pair.

*Proof.* The proof-term $\sigma_0$ is in $[[0 \in p]]_{f/p}$ thus it is $SN$. The proof-term $\sigma_S$ is in $[[\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)]]_{f/p}$ thus it is $SN$. Let $t$ be a term and $n$ a natural number. Since $\sigma_S$ is in $[[\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)]]_{f/p}$ the proof-term $\sigma_S$ $t$ is in $[[N(y) \Rightarrow y \in p \Rightarrow S(y) \in p]]_{n/y,f/p}$. Let $\rho$ be a proof-term of $P_n$. It follows that $(\sigma_S \ t \ \rho) \in [[y \in p \Rightarrow S(y) \in p]]_{n/y,f/p}$. Let $\pi$ be a proof-term of $C_n^{\sigma_0, \sigma_S}$. By Proposition 18, we have $\pi \in [[y \in p]]_{n/y,f/p}$ and hence $(\sigma_S \ t \ \rho \ \pi) \in [[S(y) \in p]]_{n/y,f/p} \subseteq SN$.

**Proposition 20.** *The rule*

$$N(x) \rightarrow \forall p (0 \in p \Rightarrow (\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p)$$

is valid in this pre-model.

*Proof.* We have to prove that for all $n$ in $\mathbb{N}$

$$P_n = [[\forall p (0 \in p \Rightarrow (\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p)]]_{n/x}$$

Consider a proof-term $\pi$ in $[[\forall p (0 \in p \Rightarrow (\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p)]]_{n/x}$, we prove that it is an element of $P_n$. By definition $\pi$ is $SN$. Let $t$ be a term of sort $\kappa$ and consider an arbitrary function $f$ of $M_\kappa$, the term $(\pi t)$ is in $[[0 \in p \Rightarrow (\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p]]_{n/x,f/p}$. Let $\sigma_0$ be a $SN$ proof-term. Consider a function $f$ of $M_\kappa$ such that $f(0)$ contains $\sigma_0$. As $\pi$ is in $[[\forall p (0 \in p \Rightarrow (\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p)]]_{n/x}$ and $\sigma_0 \in [[0 \in p]]_{f/p}$, the term $(\pi t \sigma_0)$ is in $[[[\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p]]_{n/x,f/p}$. Consider a proof-term $\sigma_S$ such that $\langle \sigma_0, \sigma_S \rangle$ is a Peano pair. Let $f$ be the function of $M_\kappa$ mapping $k$ to $C_k^{\sigma_0, \sigma_S}$. By Proposition 17, we have $\sigma_0 \in [[0 \in p]]_{f/p}$ and $\sigma_S \in [[\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)]]_{f/p}$. As, moreover $(\pi t \sigma_0) \in [[(\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p]]_{n/x,f/p}$, we have $(\pi t \sigma_0 \sigma_S) \in [[x \in p]]_{n/x,f/p} = C_n^{\sigma_0, \sigma_S}$.

Conversely, consider a proof-term $\pi$ in $P_n$, we prove that it is an element of $[[\forall p (0 \in p \Rightarrow (\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p)]]_{n/x}$. Let $t$ be a term of sort $\kappa$ and $f$ a function of $M_\kappa$. We have to prove $(p/t)\pi' \in [[0 \in p \Rightarrow (\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)) \Rightarrow x \in p]]_{n/x,f/p}$. Let $\sigma_0$ and $\sigma_S$ be, respectively, elements of $[[0 \in p]]_{f/p}$ and $[[\forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p)]]_{f/p}$. We have to prove $(\pi t \sigma_0 \sigma_S) \in [[x \in p]]_{n/x}$. By Proposition 19, the pair $\langle \sigma_0, \sigma_S \rangle$ is Peano. Thus, $(\pi t \sigma_0 \sigma_S) \in C_n^{\sigma_0, \sigma_S}$ and using Proposition 18 $(\pi t \sigma_0 \sigma_S) \in [[x \in p]]_{n/x,f/p}$.
**Remark 5. (Making the proof predicative).** The pre-model construction above is not yet predicative as to define the reducibility candidate associated to proposition $\forall p A$ we use quantification over $M_\kappa$ that is a set of functions mapping natural numbers to reducibility candidates. However as the set $M_\kappa$ is countable, it is not difficult to associate a natural number to each of its elements and to define a function $U$ that maps each number to the associated function. Then we can replace $M_\kappa$ by $\mathbb{N}$ and define the interpretation of $\in$ as the function mapping $n$ and $m$ to $U(m)(n)$. The construction obtained this way is predicative. For instance, it could be formalized in Martin-Löf's Type Theory with one universe.

**Remark 6.** For the variant of HA$_\to$ with the rule

$$N(n) \to \forall p (0 \in p \Rightarrow \forall y (y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

the proof is simpler as we do not need to apply the fixpoint theorem. If $\sigma_0$ and $\sigma_S$ be two proof terms, we define the family of candidates $C_n^{\sigma_0, \sigma_S}$ by induction on $n$ without the parameter $P$. Peano pairs and the family $P_n$ can be defined directly and the rest of the proof is similar.

# 7 The system T

More traditional cut elimination proofs for arithmetic use the normalization of Gödel system T. We show here that the normalization of system T also can be obtained as a corollary of the normalization theorem of [3] although the system T contains a specific rewrite rule on proofs and [3] allows only specific rewrite rules on terms and propositions but uses fixed rewrite rules on proofs.

## 7.1 The theory T

Consider the symbol $nat = f_{N(x)}$ and $\to = f_{x \in y \Rightarrow x \in z}$. In HA$_\to$, we have

$$x \in nat \to N(x)$$

$$x \in (y \to z) \to x \in y \Rightarrow x \in z$$

and of course

$$N(n) \to \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

We can drop the first rule, replacing all propositions of the form $N(x)$ the proposition $x \in nat$ and we get this way the rewrite system with two rules

$$n \in nat \to \forall p (0 \in p \Rightarrow \forall y (y \in nat \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p)$$

$$x \in (y \to z) \to x \in y \Rightarrow x \in z$$

In this system, we get rid of all terms of type $\iota$. We get the following theory

**Definition 26 (The theory $\mathcal{T}$).**

$$\varepsilon(nat) \to \forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p))$$

$$\varepsilon(y \to z) \to \varepsilon(y) \Rightarrow \varepsilon(z)$$
## 7.2 Cut elimination

**Proposition 21.** The theory $\mathcal{T}$ has the cut elimination property.

*Proof.* We construct a pre-model as follows. The domain of the pre-model is the set $\mathcal{C}\mathcal{R}$ of all reducibility candidates. We first interprete the symbol $\varepsilon$ by $\hat{\varepsilon}(a) = a$.

For each reducibility candidate $C$ we can define an interpretation $\mathcal{M}_C$ of the language of the proposition $\forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p))$ where the symbol nat is interpreted by $C$ and the candidate $\Phi(C)$

$$[\forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p))]^{\mathcal{M}_C}$$

As the occurrence of $\varepsilon(nat)$ in $\forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p))$ is positive, the function $\Phi$ is monotonous hence it has a fixpoint $C_0$. We complete the construction of the pre-model by $nat = C_0$ and $\dashv(C, C') = C \dashv C'$.

## 7.3 A predictive cut elimination proof

**Definition 27.** Let $\sigma_0$ and $\sigma_S$ be two proof terms and $P$ be a reducibility candidate, we define the family of candidates $C_n^{\sigma_0, \sigma_S, P}$ by induction on $n$.

$$C_0^{\sigma_0, \sigma_S, P} = [\{\pi \mid \pi = \sigma_0 \wedge \pi \in \mathcal{S}N\}]$$

$$C_{n+1}^{\sigma_0, \sigma_S, P} = [\{\pi \mid \exists \sigma' \exists \sigma'' \exists \rho \in P_n \exists \pi' \in C_n^{\sigma_0, \sigma_S, P} (\sigma_S \triangleright^* \lambda \alpha \sigma'$$

$$\wedge (\rho/\beta)\sigma' \mathcal{S}N \wedge (\rho/\beta)\sigma' \triangleright^* \lambda \alpha \sigma'' \wedge (\pi'/\alpha)\sigma'' \mathcal{S}N \wedge \pi = (\pi'/\alpha)\sigma'')]$$

$$\text{We define } C^{\sigma_0, \sigma_S} = \bigcup_n C_n^{\sigma_0, \sigma_S}.$$

It is easy to check that is $P \subseteq Q$ then $C^{\sigma_0, \sigma_S, P} \subseteq C^{\sigma_0, \sigma_S, Q}$.

**Definition 28 (P-Peano pair).** A pair of proof-terms $\langle\sigma_0, \sigma_S\rangle$ is called a P-Peano pair if

- $\sigma_0$ is $\mathcal{S}N$,

- $\sigma_S$ is $\mathcal{S}N$ and for every proof-term $\sigma'$ such that $\sigma_S \triangleright^* \lambda \beta \sigma'$, every natural number $n$, every proof-term $\rho \in P_n$, $(\rho/\beta)\sigma'$ is $\mathcal{S}N$ and for every term such $\sigma''$ such that $(\rho/\beta)\sigma' \triangleright^* \lambda \alpha \sigma''$ and for every proof-term $\pi'$ in $C^{\sigma_0, \sigma_S, P}$, the term $(\pi/\alpha)\sigma''$ is $\mathcal{S}N$.

It is easy to check that is $P \subseteq Q$ then $(\langle\sigma_0, \sigma_S\rangle$ is a P-Peano pair $\Leftarrow \langle\sigma_0, \sigma_S\rangle$ is a Q-Peano pair).

Finally we define a candidates $\Phi(P)$.

**Definition 29.**

$$\Phi(P) = \{\pi \in \mathcal{S}N \mid \pi \triangleright^* \lambda p \pi' \Rightarrow (t/p)\pi' \in \mathcal{S}N \wedge$$

$$(t/p)\pi' \triangleright^* \lambda \alpha \pi'' \Rightarrow$$

$$\forall \sigma_0 \in \mathcal{S}N (\sigma_0/\alpha)\pi'' \in \mathcal{S}N$$

$$\wedge (\sigma_0/\alpha)\pi'' \triangleright^* \lambda \beta \pi''' \Rightarrow$$

$$\forall \sigma_S \langle\sigma_0, \sigma_S\rangle \text{ is a P-Peano pair} \Rightarrow (\sigma_S/\beta)\pi''' \in C^{\sigma_0, \sigma_S, P}.$$
It is easy to check that is $P \subseteq Q$ then $\Phi(P) \subseteq \Phi(Q)$, i.e. that the function $\Phi$ is monotonous.

As this function is monotonous, it has a least fixpoint. Let $(P_i)_{i \in \mathbb{N}}$ be the least fixpoint of $\Phi$. By definition

$$
\begin{align*}
P = \{ \pi \in \mathcal{SN} \mid & \pi \triangleright^* \lambda p \pi' \Rightarrow (t/p)\pi' \in \mathcal{SN} \wedge \\
& (t/p)\pi' \triangleright^* \lambda \alpha \pi'' \Rightarrow \\
& \phantom{(t/p)\pi' \triangleright^* \lambda \alpha \pi''} \forall \sigma_0 \in \mathcal{SN} (\sigma_0/\alpha)\pi'' \in \mathcal{SN} \\
& \wedge (\sigma_0/\alpha)\pi'' \triangleright^* \lambda \beta \pi''' \Rightarrow \\
& \phantom{(t/p)\pi' \triangleright^* \lambda \alpha \pi''} \forall \sigma_S \langle \sigma_0, \sigma_S \rangle \text{ is a P-Peano pair} \Rightarrow (\sigma_S/\beta)\pi'''' \in C^{\sigma_0, \sigma_S, P} \}
\end{align*}
$$

Now that the candidate $P$ is defined we just write a Peano pair for a $P$-Peano pair and $C^{\sigma_0, \sigma_S}$ for $C^{\sigma_0, \sigma_S, P}$.

We then define the set $M$, as the set of reducibility candidates containing

- $P$,

- $C^{\sigma_0, \sigma_S}$ for some proof-terms $\sigma_0$ and $\sigma_S$

- and that is closed by $\Rightarrow$.

We define the denotation of $\varepsilon$ as the identity and the denotation nat as the candidate $P$, and the denotation of $\to$ as the function $\Rightarrow$.

The validity of all the rule

$$ \varepsilon(y \to z) \longrightarrow \varepsilon(y) \Rightarrow \varepsilon(z) $$

is routine, we check the one of the rule

$$ \varepsilon(\mathrm{nat}) \longrightarrow \forall p (\varepsilon(p) \Rightarrow (\varepsilon(\mathrm{nat}) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p)) $$

**Proposition 22.** Let $\langle \sigma_0, \sigma_S \rangle$ be a Peano pair. Then

$$ \sigma_0 \in [\varepsilon(p)]_{C^{\sigma_0, \sigma_S}/p} $$

$$ \sigma_S \in [\varepsilon(\mathrm{nat}) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)]_{C^{\sigma_0, \sigma_S}/p} $$

*Proof.* As the pair $\langle \sigma_0, \sigma_S \rangle$ is Peano, the term $\sigma_0$ is $\mathcal{SN}$. Thus it is in $C^{\sigma_0, \sigma_S} = [\varepsilon(p)]_{C^{\sigma_0, \sigma_S}/p}$. As the pair $\langle \sigma_0, \sigma_S \rangle$ is Peano, the term $\sigma_S$ is $\mathcal{SN}$. Assume it reduces to $\lambda\beta\sigma'$ and let $\rho$ be a proof-term in $P$, we have to prove that $(\rho/\beta)\sigma' \in [\varepsilon(p) \Rightarrow \varepsilon(p)]_{C^{\sigma_0, \sigma_S}/p}$. As the pair $\langle \sigma_0, \sigma_S \rangle$ is Peano, the term $(\rho/\beta)\sigma'$ is $\mathcal{SN}$ Assume it reduces to $\lambda\alpha\sigma''$ and let $\pi$ be a proof-term in $[\varepsilon(p)]_{C^{\sigma_0, \sigma_S}/p} = C^{\sigma_0, \sigma_S}$, we have to prove that $(\pi/\alpha)\sigma'' \in [\varepsilon(p)]_{C^{\sigma_0, \sigma_S}/p}$. As the pair $\langle \sigma_0, \sigma_S \rangle$ is Peano, the term $(\pi/\alpha)\sigma''$ is $\mathcal{SN}$. Thus it is in $C^{\sigma_0, \sigma_S}$, i.e. in $[\varepsilon(p)]_{C^{\sigma_0, \sigma_S}/p}$.

**Proposition 23.** Let $c$ be an arbitrary reducibility candidates and $\sigma_0$ and $\sigma_S$ two proof-terms such that $\sigma_0 \in [\varepsilon(p)]_{c/p}$ and $\sigma_S \in [(\varepsilon(\mathrm{nat}) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p))]_{c/p}$, we have $C^{\sigma_0, \sigma_S} \subseteq [\varepsilon(p)]_{c/p}$.
**Proof.** By induction on $n$ we prove that $C_n^{\sigma_0, \sigma_S} \subseteq [\varepsilon(p)]_{c/p}$. For $n=0$ we have $\sigma_0 \in [\varepsilon(p)]_{c/p}$ and thus $C_0^{\sigma_0, \sigma_S} \subseteq [\varepsilon(p)]_{c/p}$. Assume the result holds for $n$. To prove that it holds for $n+1$, we prove that all the generators of $C_{n+1}^{\sigma_0, \sigma_S}$ are in $[\varepsilon(p)]_{c/p}$. Consider such a term $\pi$. There are proof-terms $\sigma'$ and $\sigma''$, and a proof term $\rho$ in $P$ and a proof-term $\pi'$ in $C_n^{\sigma_0, \sigma_S}$ such that $\sigma_S \triangleright^* \lambda\beta \sigma'$, $(\rho/\beta)\sigma'$ is $\mathcal{SN}$, $(\rho/\beta)\sigma' \triangleright^* \lambda\alpha \sigma''$, $(\pi'/\alpha)\sigma''$ is $\mathcal{SN}$, and $\pi = (\pi'/\alpha)\sigma''$. By induction hypothesis $\pi' \in [\varepsilon(p)]_{c/p}$ hence $\pi \in [\varepsilon(p)]_{c/p}$.

**Proposition 24.** Let $c$ be an arbitrary reducibility candidate and $\sigma_0$ and $\sigma_S$ two proof-terms such that $\sigma_0 \in [\varepsilon(p)]_{c/p}$ and $\sigma_S \in [\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)]_{c/p}$. Then, $\langle\sigma_0, \sigma_S\rangle$ is a Peano pair.

**Proof.** The proof-term $\sigma_0$ is in $[\varepsilon(p)]_{c/p}$ thus it is $\mathcal{SN}$. The proof-term $\sigma_S$ is in $[\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)]_{c/p}$ thus it is $\mathcal{SN}$. Assume it reduces to $\lambda\beta \sigma'$ and let $\rho$ a proof-term of $P$. As $\sigma_S$ is in $[\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)]_{c/p}$ the proof-term $(\rho/\beta)\sigma'$ is in $[\varepsilon(p) \Rightarrow \varepsilon(p)]_{n/y,c/p}$. Thus it is $\mathcal{SN}$. Assume it reduces to $\lambda\alpha\sigma''$ and let $\pi$ is a member of $C^{\sigma_0, \sigma_S}$. By Proposition 23, the proof-term $\pi$ is in $[\varepsilon(p)]_{c/p}$ and thus as $(\rho/\beta)\sigma'$ is in $[\varepsilon(p) \Rightarrow \varepsilon(p)]_{c/p}$, the proof term $(\pi/\alpha)\sigma''$ is in $[\varepsilon(p)]_{c/p}$. Thus it is $\mathcal{SN}$.

**Proposition 25.** The rule

$$ \varepsilon(nat) \longrightarrow \forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p)) $$

is valid in this pre-model.

**Proof.** We have to prove that

$$ P = [\forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p))] $$

Consider a proof-term $\pi$ in $[\forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p))]$, we prove that it is an element of $P$. By definition $\pi$ is $\mathcal{SN}$. Assume it reduces to $\lambda p \pi'$ and let $t$ be a term. Consider an arbitrary reducibility candidate $c$ of $M$, the term $(t/p)\pi'$ is in $[\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p)]_{c/p}$, thus it is $\mathcal{SN}$. Assume it reduces to $\lambda\alpha\pi''$ and let $\sigma_0$ be a $\mathcal{SN}$ proof-term. Consider a candidate $c$ of $M$ that contains $\sigma_0$. As $\pi$ is in $[\forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p))]_{c/p}$ and $\sigma_0 \in [\varepsilon(p)]_{c/p}$, the term $(\sigma_0/\alpha)\pi''$ is in $[(\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p)]_{c/p}$ and thus it is $\mathcal{SN}$. Assume it reduces to $\lambda\beta\pi'''$ and consider a proof-term $\sigma_S$ such that $\langle\sigma_0, \sigma_S\rangle$ is a Peano pair. Let $c$ be the candidate $C^{\sigma_0, \sigma_S}$. By Proposition 22, we have $\sigma_0 \in [0 \in p]_{c/p}$ and $\sigma_S \in [\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)]_{c/p}$. As, moreover $(\sigma_0/\alpha)\pi''$ is in $[(\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p)]_{c/p}$, we have $(\sigma_S/\beta)\pi''' \in [\varepsilon(p)]_{c/p} = C^{\sigma_0, \sigma_S}$.

Conversely, consider a proof-term $\pi$ in $P$, we prove that it is an element of $[\forall p (\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p))]$. By definition $\pi$ is $\mathcal{SN}$. Assume it reduces to $\lambda p \pi'$ and let $t$ be a term and $c$ a candidate of $M$. We have to prove $(p/t)\pi' \in [\varepsilon(p) \Rightarrow (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p)) \Rightarrow \varepsilon(p)]_{c/p}$. As $\pi$ is in $P$, the proof-term $(t/p)\pi'$ is $\mathcal{SN}$. Assume it reduces to $\lambda\alpha\pi''$ and let $\sigma_0$ be a proof-term of $[0 \in p]_{c/p}$. We have to prove $(\sigma_0/\alpha)\pi'' \in [(\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p))]_{c/p}$.
$\varepsilon(p)) \Rightarrow \varepsilon(p)]_{c/p}$. As $\pi$ is in $P$, $(\sigma_0/\alpha)\pi''$ is $\mathcal{S}\mathcal{N}$. Assume it reduces to $\lambda\beta\pi'''$ and consider a proof-term $\sigma_S \in [\forall y (\varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p))]_{c/p}$. We have to prove $(\sigma_S/\beta)\pi''' \in [x \in p]_{n/x,c/p}$. By Proposition 24, the pair $\langle\sigma_0, \sigma_S\rangle$ is Peano. Thus, $(\sigma_S/\beta)\pi''' \in C^{\sigma_0, \sigma_S}$ and using Proposition 23 $(\sigma_S/\beta)\pi''' \in [\varepsilon(p)]_{c/p}$.

## 7.4 Application to the system T

**Definition 30 (The system T).** The system T is the extension of simply typed lambda-calculus with a constant 0, a unary function symbol S and a ternary function symbol $\text{Rec}^A$ for each type A and the rules

$$ \text{Rec}(a, f, 0) \longrightarrow a $$

$$ \text{Rec}(a, f, S(b)) \longrightarrow (f \ b \ \text{Rec}(a, f, b)) $$

Proof normalization for the theory $\mathcal{T}$ implies normalization for the system T. Indeed, types of the system T are terms of the theory $\mathcal{T}$ and terms of type A in the system T can be translated into proofs of $\varepsilon(A)$ in the theory $\mathcal{T}$ (Parigot's numbers [11]):

$$ - |x| = x, |u| |v| = |u| |v|, |\lambda x : A u| = \lambda x : \varepsilon(A) |u|, $$

$$ - |0| = \lambda p \ \lambda x : \varepsilon(p) \ \lambda f : \varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p) x, $$

$$ - |S(n)| = \lambda p \ \lambda x : \varepsilon(p) \ \lambda f : \varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p) (f |n| (|n| p x f)), $$

$$ - |\text{Rec}^A(x, f, n)| = (|n| A x f). $$

It is routine to check that if $t \to^1 u$ in the system T then $|t| \to^+ |u|$ in the theory $\mathcal{T}$. Indeed

$$ |\text{Rec}^A(x, f, 0)| = (|0| A x f) = (\lambda p \ \lambda x : \varepsilon(p) \ \lambda f : \varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p) x) A x f \longrightarrow^+ x $$

$$ \begin{aligned} |\text{Rec}^A(x, f, S(n))| &= (|S(n)| A x f) = (\lambda p \ \lambda x : \varepsilon(p) \ \lambda f : \varepsilon(nat) \Rightarrow \varepsilon(p) \Rightarrow \varepsilon(p) (f |n| (|n| p x f))) A x f \\ &\longrightarrow^+ (f |n| (|n| A x f)) = (f |n| |\text{Rec}^A(x, f, n)|) = |(f n \ \text{Rec}^A(x, f, n))| \end{aligned} $$

Here we reap the benefit of having chosen the rule

$$ N(n) \longrightarrow \forall p (0 \in p \Rightarrow \forall y (N(y) \Rightarrow y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) $$

and not

$$ N(n) \longrightarrow \forall p (0 \in p \Rightarrow \forall y (y \in p \Rightarrow S(y) \in p) \Rightarrow n \in p) $$

that would have given us only the termination of the variant of system T where the recursor is replaced by an iterator.
References

1. M. Crabbé. Non-normalisation de la théorie de Zermelo. Manuscript (1974).

2. G. Dowek, Th. Hardin, and C. Kirchner. Theorem proving modulo. *Journal of Automated Reasoning*, 31 (2003) pp. 33-72.

3. G. Dowek and B. Werner. Proof normalization modulo, *The Journal of Symbolic Logic*, 68, 4 (2003) pp. 1289-1316.

4. G. Dowek and B. Werner. Arithmetic as a theory modulo. Manuscript (2004).

5. G. Dowek and B. Werner. A constructive proof of Skolem theorem for constructive logic, Manuscript (2004).

6. G. Dowek. *La part du Calcul*. Habilitation thesis, Université de Paris 7 (1999).

7. J.Y. Girard. Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, *Thèse d'État*, Université de Paris 7 (1972).

8. J.Y. Girard, Y. Lafont and P. Taylor. *Proofs and Types*, Cambridge University Press (1989).

9. K. Gödel. Über eine bisher noch nicht benüzte Erweiterung des finiten Standpunktes, *Dialectica*, 12 (1958) pp. 280-287. Reproduced in S. Feferman *et al.* (eds.), *Collected Works*, vol. II, Oxford University Press (1990) pp. 241-251.

10. J.-W. Klop, V. van Oostrom and F. van Raamsdonk. Combinatory reduction systems: introduction and survey. *Theoretical Computer Science*, 121, (1993) pp. 279-308.

11. M. Parigot. Programming with proofs: A second order type theory. *European Symposium on Programming*, H. Ganzinger (ed.), Lecture Notes in Computer Science, 300, (1988) pp. 145-159.

12. D. Prawitz, Natural deduction. A proof-theoretical study. Almqvist & Wiksell (1965).

13. H. Rasiowa and R. Sikorski, *The mathematics of metamathematics*, Polish Scientific Publishers (1963).