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)$