TD11 : $H A_{2}$ et Ackermann

EX 1

\frac{𝛤 ⊢ u : P [i := t]}{𝛤 ⊢ ⟨ t, u ⟩ : \exists i . P}

\frac{𝛤 ⊢ u : \exists i . P}{𝛤 ⊢ ⟨ t, u ⟩ : \exists i . P}

1.

a).

v_{0} ≝ 𝜆^{1} j . ⟨ s (j), 𝜆^{2} A . 𝜆 x, y, z . x j ⟩

b).

u_{0} = let ⟨ k, a ⟩ = h_{i} s (0) in ⟨ k, 𝜆^{2} A . 𝜆 x, y, z . y i k (a A x y z) ⟩

c).

u_{s} ≝ 𝜆^{1} j, p . let ⟨ k, a ⟩ = p in let ⟨ k^{'}, a^{'} ⟩_{a c k (i, k, k^{'})} = h_{i} k

⟨ k^{'}, 𝜆^{2} A . 𝜆 x, y, z . z i j k k^{'} (a A x y z) (a^{'} A x y z) ⟩

d).

v_{s} ≝ 𝜆 i . 𝜆 h_{i} . 𝜆 j . R u_{0} u_{s} j

e).

𝜆 i . R v_{0} v_{s} i

2.

n a t ≝ N ⟹ (N ⟹ N) ⟹ N

a).

E (𝜆 i . u) = 𝜆 x_{i} . E (u)

On veut $u ⟶ v$ donc $E (u) ⟶ E (v)$

EX 2. $𝜆 𝜎$ simule $𝜆$

1.

↑ \circ ⇑ (S) = ↑ \circ (1 \cdot (S \circ ↑)) ⟶ (S \circ ↑)

2.

Par réc sur $i$ :

Pour $i = 1$ : Par réc sur $q \geq 0$ :
- $1 [⇑^{0} (S)] =_{𝜎} 1 [S]$
- $\begin{matrix} (q + 1) [⇑^{q} (S)] =_{𝜎} ((q - 1) + 1) [1 \cdot (⇑^{q - 1} (S) \circ ↑)] \\ =_{𝜎} (q - 1) [↑] [1 \cdot (⇑^{q - 1} (S) \circ ↑)] =_{𝜎} (q - 1) [⇑^{q - 1} (S) \circ ↑] \\ \overset{H R}{=_{𝜎}} [S \circ ↑^{q}] \end{matrix}$
Pour $i \geq 2$ : Par réc sur $q \geq 0$ :
- $i [⇑^{0} (S)] =_{𝜎} 1 [S]$
- $\begin{matrix} (q + i) [⇑^{q} (S)] =_{𝜎} ((q - 1) + i + 1) [1 \cdot (⇑^{q - 1} (S) \circ ↑)] \\ =_{𝜎} (q - 1 + i) [↑] [1 \cdot (⇑^{q - 1} (S) \circ ↑)] =_{𝜎} (q - 1 + i) [⇑^{q - 1} (S) \circ ↑] \\ \overset{H R}{=_{𝜎}} i [S \circ ↑^{q}] \end{matrix}$

3.

Par réc sur $1 \leq i \leq q$ :

Pour $i = 1$ :
$\begin{matrix} 1 [⇑^{q} (S)] =_{𝜎} 1 [1 \cdot (⇑^{q - 1} (S) \circ ↑)] \\ =_{𝜎} 1 \end{matrix}$
Pour $1 \leq i < q$ :
$\begin{matrix} i [⇑^{q} (S)] = (i - 1) [↑] [1 \cdot (⇑^{q} (S) \circ ↑)] = (i - 1) [⇑^{q} (S) \circ ↑] [↑] \\ = (i - 1) [↑] = i \end{matrix}$

4.

Par induction sur $v$ :

Share on

EX 1

1.