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⟩⟩$.