# Exercises 3: Term associated to a proof, Leivant/Krivine/Parigot arithmetic

Teacher: Gilles Dowek

## Ex1

What is the proof-term associated to the proof

$\infer[⇒ \text{-elim}]{⊢ ∃x \; (P(x) ⇒ P(x))}{ \infer[⇒ \text{-intro}]{⊢ ∃x \; (P(x) ⇒ P(x)) ⇒ ∃ x \; (P(x) ⇒ P(x))}{ \infer[ax]{∃x \; (P(x) ⇒ P(x)) ⊢ ∃ x \; (P(x) ⇒ P(x))}{\phantom{∃x \; (P(x) ⇒ P(x)) ⊢ ∃ x \; (P(x) ⇒ P(x))}} } & \infer[∃ \text{-intro}]{⊢ ∃x \, (P(x) ⇒ P(x))}{ \infer[⇒ \text{-intro}]{⊢ P(c) ⇒ P(c)}{ \infer[ax]{P(c) ⊢ P(c)}{\phantom{P(c) ⊢ P(c)}} } } }$

? Reduce it to its irreducible form.

$\infer[⇒ \text{-elim}]{⊢ (λ α: A. α) \; ⟨c, λ β: P(c).β⟩: ∃x \; (P(x) ⇒ P(x))}{ \infer[⇒ \text{-intro}]{⊢ λ(α: A). α : ∃x \; (P(x) ⇒ P(x)) ⇒ ∃ x \; (P(x) ⇒ P(x))}{ \infer[ax]{α: \overbrace{∃x \; (P(x) ⇒ P(x))}^{≝ \, A} ⊢ α: ∃ x \; (P(x) ⇒ P(x))}{\phantom{α: ∃x \; (P(x) ⇒ P(x)) ⊢ α: ∃ x \; (P(x) ⇒ P(x))}} } & \infer[∃ \text{-intro}]{⊢ ⟨c, λ(β: P(c)).β⟩: ∃x \, (P(x) ⇒ P(x))}{ \infer[⇒ \text{-intro}]{⊢ λ(β: P(c)).β: P(c) ⇒ P(c)}{ \infer[ax]{β: P(c) ⊢ β: P(c)}{\phantom{β: P(c) ⊢ β: P(c)}} } } }$

Irreducible form:

$\infer[∃ \text{-intro}]{⊢ ∃x \, (P(x) ⇒ P(x))}{ \infer[⇒ \text{-intro}]{⊢ P(c) ⇒ P(c)}{ \infer[ax]{P(c) ⊢ P(c)}{\phantom{P(c) ⊢ P(c)}} } }$

## Ex2

$χ(0) ⟶ 0\\ χ(S(n)) ⟶ S(0) \qquad ⊛$

Or:

$∀x \; ∃y \; (x=0 ⇒ y=0 ∧ ∃ z \; (x= S \, z) ⇒ y=1)\\ ∀ x \; N(x) ⇒ ∃y \; N(y) ∧ (x=0 ⇒ y=0 ∧ (∃ z \; x= S \, z) ⇒ y=1)$

the second version being a little bit better, as induction scheme can be defined as a rewrite rule, and not as an axiom:

$N(t) ⟶ ∀c \; (0 ∈ c ∧ ∀x \; N(x) ⇒ (x ∈ c ⇒ S(x) ∈ c) ⇒ t ∈ c)$

With the two rewriting rules $⊛$, we will show:

$∀x \; N(x) ⇒ ∃y \; N(y) ∧ (y = χ(x))\\ ∀ x \; N(x) ⇒ N(χ(x))$

### 1.

$χ$ is interpreted as the characteristic function of $ℕ \backslash \lbrace 0 \rbrace$. The proof is exactly the same as the one of theorem 4.10, except that: « The interpretations of the symbols $0$, $S$, $+$, $×$, and $Pred$ are defined in the obvious way. »

With super-consistency, we have termination of proof reduction.

### 2.

Proof of $∀x \; N(x) ⇒ ∃y \; N(y) ∧ (y = χ(x))$ by induction.

• if $x=0$: $y=0$ is a witness
• if $x > 0$: $y=1$ is suitable
$π_0 = ⟨0, ⟨ρ_0, refl_0⟩⟩\\ π_s = λα, β, β'. ⟨1, ⟨ρ_1, refl_1⟩⟩ \\ : ∀x \; N(x) ⇒ (∃y \; N(y) ∧ (y = χ(x))) ⇒ (∃y \; N(y) ∧ (y = χ(S \, x)))$

where the $ρ_i$’s are the Parigot’s numbers

Now we use the induction scheme (with the rewriting rule of $N$), with $c ≝ \lbrace x \; \mid \; ∃ y \, N(y) ∧ y = χ(x)\rbrace$

$λx, γ: N(x). (γ \, c \, π_0 \, π_1)$

When you apply this proof to $7$, you get $⟨1, ⟨ρ_1, refl_1⟩⟩$.

Tags:

Updated: