Download Th`ese

3.5 Traductions
vables dans P-CPn d’après le lemme 3.5.2 ; ainsi nous dérivons Γ `np Pγ =κ Qγ
à l’aide du lemme 3.5.9 ;
A =β 0 B B =β 0 C
(βtrans ) par hypothèse de récurrence, nous avons Aγ =β 0
A =β 0 C
Bγ et Bγ =β 0 Cγ ; nous avons alors Aγ =β 0 Cγ par la règle (βtrans ) ; les
prédicats Pγ et Qγ sont motivables dans P-CPn d’après le lemme 3.5.2 ; ainsi
nous dérivons Γ `np Pγ =κ Qγ à l’aide du lemme 3.5.9 ;
`np µ·∀αι .A `np µ·B
(P-βred ) nous avons Pγ = (λαι .Aγ )Bγ ; d’après le
(λαι .A)B =β 0 [αι \B]·A
lemme 3.5.2, les formules Aγ et Bγ sont motivables dans P-CPn par la
substitution [γ\>] ; comme γ 6= α, la formule ∀αι .Aγ est motivable dans
P-CPn par la substitution [γ\>] ; ainsi nous avons Pγ =β 0 [α\Bγ ] · Aγ ; les
prédicat Pγ et ([α\B]·A)γ sont motivables d’après le lemme 3.5.2 ; d’après
le lemme 3.5.6, le jugement Γ `np [α\Bγ ] · Aγ =κ ([α\B]·A)γ est dérivable ;
ainsi le prédicat [α\Bγ ] · Aγ est motivable ; d’après le lemme 3.5.9, le jugement Γ `np Pγ =κ [α\Bγ ] · Aγ est dérivable ; nous dérivons le jugement
Γ `np Pγ =κ [α\B]·Aγ à l’aide de la règle (Ext) ; nous avons alors une
dérivation du jugement Γ `np Pγ =κ Qγ .
Nous pouvons maintenant prouver la première moitié de la propriété de préservation de la déductibilité par γ-traduction ; si un jugement est dérivable dans CCPn ,
alors sa traduction est dérivable dans P-CPn :
Lemme 3.5.11. Soit n un élément de J2; ωK. Pour tout jugement dérivable Γ `nc F ,
le jugement Γγ `np Fγ est dérivable, avec γ ? une variable fraı̂che pour Γ ∪ {F }.
Démonstration. Par récurrence sur la dérivation de Γ `nc F :
(Ax) d’après le lemme 3.5.2, les jugements `np [γ\>]Γγ sont dériΓ `nc >
vables ; ainsi le jugement Γγ `np >γ est dérivable par la règle (P-Ax) ;
F ∈Γ
(Hyp) d’après le lemme 3.5.2, les jugements `np [γ\>]Γγ sont dériΓ `nc F
vables ; ainsi le jugement Γγ `np Fγ est dérivable par la règle (P-Hyp) ;
Γ, A `nc B
(→i ) par hypothèse de récurrence, le jugement Γγ , Aγ `np Bγ est
Γ `nc A → B
dérivable ; le jugement Γγ `np Aγ → Bγ est dérivable à l’aide de la règle (→i ) ;
nous avons alors une dérivation du jugement Γγ `np A → B γ ;
Γ `nc A → B Γ `nc A
(→e ) par hypothèse de récurrence, les jugements
Γ `nc B
Γγ `np (A → B)γ et Γγ `np Aγ sont dérivables ; le jugement Γγ `np Bγ est
alors dérivable à l’aide de la règle (→i ) ;
93