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

Teacher: Gilles Dowek

Ex1

What is the proof-term associated to the proof

? Reduce it to its irreducible form.

Irreducible form:

Ex2

Or:

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

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

1.

$\chi$ is interpreted as the characteristic function of $\mathbb{N}\mathrm{\setminus }\{0\}$. The proof is exactly the same as the one of theorem 4.10, except that: « The interpretations of the symbols $0$, $S$, $+$, $\times$, and $Pred$ are defined in the obvious way. »

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

2.

Proof of $\forall xN(x)\Rightarrow \exists yN(y)\wedge (y=\chi (x))$ by induction.

• if $x=0$: $y=0$ is a witness
• if $x>0$: $y=1$ is suitable

where the ${\rho }_i$’s are the Parigot’s numbers

Now we use the induction scheme (with the rewriting rule of $N$), with $c\stackrel{\scriptscriptstyle\mathrm{def}}{=}\{x\mid \exists yN(y)\wedge y=\chi (x)\}$

When you apply this proof to $7$, you get $⟨1,⟨{\rho }_1,ref{l}_1⟩⟩$.