Cours 3 : Déduction naturelle

Déduction naturelle : Pas utilisée en pratique

Syntaxe :
\underbrace{𝛤}_{\text{ensemble fini de formules}} \vdash \underbrace{𝜑}_{formule}

Jugement

NB :

  • $𝛤$ pourrait être un multi-ensemble ⟶ utile en logique intuitionniste
  • Attention, la relation $\vdash$ est une surcharge, concernant la syntaxe, de la relation vue dans les précédents cours !
Sémantique :

$I \vDash 𝛤 \vdash 𝜑$ ssi pour tout $𝜓∈𝛤$, si $I \vDash 𝜓$ alors $I \vDash 𝜑$

$𝛤 \vdash 𝜑$ valide :

si pour tout $I$, $I \vDash 𝛤 \vdash 𝜑$

Règles d’inférence de $NK_0$

 
$𝛤 \vdash \top$

Ax :

 
$𝛤, 𝜑 \vdash 𝜑$

Aff :

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

Absurde :

$𝛤, ¬ 𝜑 \vdash \bot$
$𝛤 \vdash 𝜑$

Intersection :

$𝛤 \vdash 𝜑_1$ $𝛤 \vdash 𝜑_2$
$𝛤 \vdash 𝜑_1 ∧ 𝜑_2$  

AND Élimination gauche :

$𝛤 \vdash 𝜑_1 ∧ 𝜑_2$
$𝛤 \vdash 𝜑_2$

AND Élimination droite :

$𝛤 \vdash 𝜑_1 ∧ 𝜑_2$
$𝛤 \vdash 𝜑_1$

OR Introduction gauche :

$𝛤 \vdash 𝜑_1$
$𝛤 \vdash 𝜑_1 ∨ 𝜑_2$

OR Introduction droite :

$𝛤 \vdash 𝜑_2$
$𝛤 \vdash 𝜑_1 ∨ 𝜑_2$

Élimination :

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

Aussi : règles de négation, d’implication (2 règles), de non $𝜑 ∨ ¬𝜑$

Implication Introduction :

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

Implication Élimination :

$𝛤 \vdash 𝜑 ⟹ 𝜓$ $𝛤 \vdash 𝜑$
$𝛤 \vdash 𝜓$  

Nég Introduction :

$𝛤, 𝜑 \vdash \bot$
$𝛤 \vdash ¬𝜑$

Nég Élimination :

$𝛤 \vdash 𝜑$ $𝛤 \vdash ¬𝜑$
$𝛤 \vdash \bot$  

Prop : le système d’inférence $NK_0$ est correct.

Les jugements dérivables sont valides

Dém : Par récurrence sur la preuve.


Th de Complétude :

Si $𝛤\vDash 𝜑$, alors $𝛤 \vdash 𝜑$ est dérivable dans $NK_0$

Exs :

$𝜑 \vdash ¬¬𝜑$

$𝜑, ¬𝜑 \vdash 𝜑$ $𝜑, ¬𝜑 \vdash ¬ 𝜑$ Ax
  $𝜑, ¬𝜑 \vdash \bot$  
  $𝜑 \vdash ¬¬𝜑$  

$¬¬𝜑 \vdash 𝜑$

$¬¬𝜑, ¬𝜑 \vdash ¬𝜑$ $¬¬𝜑, ¬𝜑 \vdash ¬¬𝜑$ Ax
  $¬¬𝜑, ¬𝜑 \vdash \bot$  
  $¬¬𝜑 \vdash 𝜑$  

Lemme : Si $𝛤, 𝜑 \vdash 𝜓$ et $𝛤 \vdash 𝜑$ sont dérivables, alors $𝛤 \vdash 𝜓$ est dérivable

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

Lemme 2 : $¬ (𝜑∨𝜓) \vdash ¬𝜑$ et $¬ (𝜑∨𝜓) \vdash ¬𝜓$ sont dérivables dans $NK_0$

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

Déduction naturelle intuitionniste $NJ_0$ : on remplace la règle “Abs” (raisonnement par l’absurde), par la règle $\bot \, E$ (Élimination de $\bot$) :

$𝛤 \vdash \bot$
$𝛤 \vdash 𝜑$
NJ_0 = NK_0 - (Abs) + (\bot E)

NB : Avec la règle d’affaiblissement, $(Abs) ⟹ (\bot E)$ dans $NK_0$


Th : Complétude

Si $𝛤 \vdash 𝜑$ est valide, alors $𝛤 \vdash 𝜑$ est prouvable.

Lemme : Soit $𝛤\vdash 𝜑$ valide tq pour toute var. prop. $A$ de $𝛤 \vdash 𝜑$, $\lbrace A, \lnot A \rbrace ∩𝛤 ≠ ∅$,

alors : $𝛤\vdash 𝜑$ est prouvable dans $NJ_0$

Preuve : par récurrence sur $(\vert 𝛤 \vert, \vert 𝜑 \vert)$ pour l’ordre lexicographique.


Lemme : Le règle suivante, $(¬L)$, est dérivable dans $NJ_0$ :

$(¬L)$:

$𝛤\vdash 𝜑$
$𝛤, ¬𝜑 \vdash \bot$

Dém : avec (Ax) et (Aff)


$(DN)$ (Double négation):

$𝛤\vdash ¬¬𝜑$
$𝛤 \vdash 𝜑$

$(TE)$ (Tiers Exclus):

 
$𝛤 \vdash 𝜑∨¬𝜑$

$NJ_0 + Abs$,$NJ_0 + NE$, $NJ_0 + TE$ sont équivalents


Preuve du th de complétude :

par réc sur

t(𝛤\vdash 𝜑) ≝ \vert \lbrace A \mid A \text{ apparaît dans } 𝛤\vdash 𝜑 \text{ et } \lbrace A, \lnot A \rbrace ∩𝛤 = ∅ \rbrace \vert

(le cas de base relevant du lemme précédent)

Leave a comment