TD 4 : Systèmes de preuve classique et inuitionniste

Énoncé

EX 1

1.

$(NK_0)$ :

   
$¬𝜑 \vdash ¬𝜑$ $¬¬𝜑 \vdash ¬¬𝜑$
$¬¬𝜑, ¬𝜑 \vdash ¬𝜑$ $¬¬𝜑, ¬𝜑 \vdash ¬¬𝜑$
$¬¬𝜑, ¬𝜑 \vdash \bot$  
$¬¬𝜑 \vdash 𝜑$  
$\vdash ¬¬𝜑 ⟶ 𝜑$  

Dans $(NJ_0)$ : on est obligé d’utiliser l’absurde, donc prouvable dans $(NJ_0)$.

$(LK_0)$ :

   
$𝜑 \vdash 𝜑$  
$\vdash ¬𝜑, 𝜑$  
$¬¬𝜑 \vdash 𝜑$  
$\vdash ¬¬𝜑 ⟶ 𝜑$  

2.

$(NK_0)$

   
$𝜑, ¬𝜑 \vdash 𝜑$ $𝜑, ¬𝜑 \vdash ¬𝜑$
$𝜑, ¬𝜑 \vdash \bot$  
$𝜑 \vdash ¬¬𝜑$  
$\vdash 𝜑 ⟶ ¬¬𝜑$  

$(LK_0)$

 
$𝜑\vdash 𝜑$
$𝜑, ¬𝜑 \vdash \bot$
$𝜑 \vdash ¬¬𝜑$
$\vdash 𝜑 ⟶ ¬¬𝜑$

3.

$(LK_0)$

 
$𝜑\vdash 𝜑$
$\vdash 𝜑, ¬𝜑$
$\vdash 𝜑 ∨ ¬𝜑$

$(NK_0)$

     
    $¬(𝜑 ∨ ¬𝜑), 𝜑 \vdash 𝜑$
  $¬(𝜑 ∨ ¬𝜑), 𝜑 \vdash ¬(𝜑 ∨ ¬𝜑)$ $¬(𝜑 ∨ ¬𝜑), 𝜑 \vdash (𝜑 ∨ ¬𝜑)$
  $¬(𝜑 ∨ ¬𝜑), 𝜑 \vdash \bot$  
  $¬(𝜑 ∨ ¬𝜑) \vdash ¬𝜑 $  
$¬(𝜑 ∨ ¬𝜑) \vdash ¬(𝜑 ∨ ¬𝜑)$ $¬(𝜑 ∨ ¬𝜑) \vdash (𝜑 ∨ ¬𝜑) $  
$¬(𝜑 ∨ ¬𝜑) \vdash \bot$    
$\vdash 𝜑 ∨ ¬𝜑$    

EX 2

1.

On peut se passer de la règle d’affaiblissement, puisque les axiomes sont de la forme :

 
$𝛤, 𝜑 \vdash 𝜑$

quitte rajouter les formules $𝜓$ supprimées par l’affaiblissement

$𝛤 \vdash 𝜑$
$𝛤, 𝜓 \vdash 𝜑$

dans $𝛤$.

2.

On obtient $NK’$ à partir de $NK$ en supprimant le $∨$ et en ajoutant la règle de $∧$-élimination (i.e la règle de $∨$-élimination où $∨$ est remplacé par $∧$), et on garde la sémantique standard.

Or, celle-ci reste correcte vis-à-vis de la sémantique standard.


Preuve : Par induction sur la taille de l’arbre de preuve.

  • $𝛤 \vDash^n 𝜑∨𝜓$
  • $𝛤, 𝜑 \vDash^n 𝜃$
  • $𝛤, 𝜓 \vDash^n 𝜃$

? $𝛤 \vDash^n 𝜃$

soit $I \vDash^n 𝛤$

donc $I \vDash^n 𝜑 ∨𝜓$

donc $I \vDash^n 𝜑$ et $I \vDash^n 𝜓$

donc $I \vDash^n 𝜃$


Donc la correction de $NK’$ vis-à-vis de la sémantique non-standard est établie.

3.

𝜑 = \top ∨ ¬ \top

EX 3

Règle de coupure (Cut) :

$𝛤, 𝜑 \vdash 𝛥$ $𝛤’\vdash 𝛥’, 𝜑$
$𝛤, 𝛤’ \vdash 𝛥, 𝛥’$  

1.

$(NK_0) ⟶ (LK_0)$

Par récurrence sur la taille de l’arbre de preuve :

Élimination du $∨$ :

$𝛤\vdash 𝜑 ∨ 𝜓$ $𝛤, 𝜑\vdash 𝜃$ $𝛤, 𝜓\vdash 𝜃$
$𝛤\vdash 𝜃$    

Par HR, on a une preuve dans $(LK_0)$ de

  • $𝛤\vdash 𝜑 ∨ 𝜓$
  • $𝛤, 𝜑\vdash 𝜃$
  • et $𝛤, 𝜓\vdash 𝜃$

On va utiliser une autre forme de la règle cut :

$𝛤, 𝜓 \vdash 𝜃$ $𝛤 \vdash 𝜓$
$𝛤 \vdash 𝜃$  

$𝛤, 𝜑 \vdash 𝜃$ $𝛤, 𝜓 \vdash 𝜃$  
$𝛤, 𝜑∨𝜓 \vdash 𝜃$   $𝛤 \vdash 𝜑∨𝜓$
$𝛤, 𝛤 \vdash 𝜃$    
$𝛤 \vdash 𝜃$    

Introduction du $∨$ :

$𝛤\vdash 𝜑$
$𝛤\vdash 𝜑 ∨ 𝜓$

Par HR, on a une preuve dans $(LK_0)$ de $𝛤 \vdash 𝜑$

Donc

$𝛤\vdash 𝜑$
$𝛤\vdash 𝜑, 𝜓$
$𝛤\vdash 𝜑 ∨ 𝜓$

dans $(LK_0)$

2.

Les règles à gauche (resp. droite) correspondent aux règles d’élimination (resp. d’introduction).

$(LK_0) ⟶ (NK_0)$

Par récurrence sur la taille de l’arbre de preuve :

Règle $∨_g$ :

$𝛤, 𝜑, ¬𝛥 \vdash \bot$ $𝛤, 𝜓, ¬𝛥 \vdash \bot$
$𝛤 𝜑∨𝜓, ¬𝛥 \vdash \bot$  

Par HR, on a une preuve dans $(NK_0)$ de

  • $𝛤, 𝜑, ¬𝛥 \vdash \bot$
  • $𝛤, 𝜓, ¬𝛥 \vdash \bot$
$𝛤, 𝜑∨𝜓, ¬𝛥\vdash 𝜑∨𝜓$ $𝛤, ¬𝛥, 𝜑 \vdash \bot$ $𝛤, ¬𝛥, 𝜓\vdash \bot$
$𝛤, 𝜑∨𝜓, ¬𝛥\vdash 𝜑∨𝜓$ $𝛤, 𝜑∨𝜓, ¬𝛥, 𝜑 \vdash \bot$ $𝛤, 𝜑∨𝜓, ¬𝛥, 𝜓\vdash \bot$
$𝛤, 𝜑∨𝜓, ¬𝛥\vdash \bot$    

$∨_d$ :

$𝛤\vdash 𝛥, 𝜑, 𝜓$
$𝛤\vdash 𝛥, 𝜑 ∨ 𝜓$

Par HR, on a une preuve dans $(LK_0)$ de $𝛤, ¬ 𝛥, ¬𝜑, ¬𝜓 \vdash \bot$

Donc

$𝛤\vdash 𝜑$ $𝜋$  
  $𝛤, ¬𝛥, ¬𝜑, ¬𝜓 \vdash \bot$  
  $𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓), ¬𝜑, ¬𝜓 \vdash \bot$  
  $𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓), ¬𝜑 \vdash 𝜓$  
  $𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓), ¬𝜑 \vdash (𝜑 ∨ 𝜓)$ $𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓), ¬𝜑 \vdash ¬(𝜑 ∨ 𝜓)$
  $𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓), ¬𝜑 \vdash \bot$  
  $𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓) \vdash 𝜑$  
$𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓) \vdash ¬(𝜑 ∨ 𝜓)$ $𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓) \vdash (𝜑 ∨ 𝜓)$  
$𝛤, ¬𝛥, ¬(𝜑 ∨ 𝜓) \vdash \bot$    

dans $(NK_0)$

Leave a Comment