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)