Cours 2 : Logique intuitionniste et sémantique de Kripke

Calcul des séquents

Séquent $𝛤 \vdash 𝛥$ :

$𝛤, 𝛥$ multiensembles de formules

NB : Pourquoi multiensembles ? cf. Logique linéaire ⟶ on a besoin de compter le nombre de fois qu’on a une hypothèse.

---

$I⊆P$ :

$I \vDash 𝛤\vdash 𝛥$ :

si

• ou bien : $∃𝜑∈𝛤 ; I \not\vDash 𝜑$
• ou bien : $∃𝜑∈𝛥; I \vDash 𝜑$

NB :

\[𝛤\underbrace{,}_{\text{un "et"}} 𝛥 \vdash 𝜑\underbrace{,}_{\text{un "ou"}} 𝜓\]

Système $LK_0$ :

Th : Correction et complétude de $LK_0$

---

Règle du Cut :

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

Th : Élimination des coupures

$𝛤 \vdash 𝛥$ est prouvable dans $LK_0 + Cut$

ssi

$𝛤 \vdash 𝛥$ est prouvable dans $LK_0$

Preuve : Correction de $LK_0+Cut$, et complétude de $LK_0$

Th : Propriété de la sous-formule

Si $𝜋$ est un preuve de $𝛤 \vdash 𝛥$ dans $LK_0$ (sans Cut) et si $𝛤’ \vdash 𝛥’$ apparaît dans $𝜋$, alors pour tout $𝜑’ ∈ 𝛤’∪𝛥’$, $∃𝜑∈𝛤∪𝛥$ tq $𝜑’$ est une sous-formule de $𝜑$

Preuve : dans $LK_0$, on ne fait que “casser” des formules. On fait apparaître une nouvelle $𝜑$ avec la règle Cut.

NB : permet de montrer syntaxiquement qu’on ne peut pas avoir une preuve de $\bot$ _____

$LJ_0$

(Ax)

$𝛤, 𝜑 \vdash 𝜑 (, 𝛥)$

---

($\bot L$)

$𝛤, \bot \vdash 𝜑 (, 𝛥)$

---

($\top R$)

$𝛤 \vdash \top (, 𝛥)$

---

($∧ L$)

$𝛤, 𝜑_1, 𝜑_2 \vdash \top 𝜓 (, 𝛥)$
$𝛤 \vdash \top (, 𝛥)$

---

($∨ L$)

$𝛤, 𝜑_1 \vdash \top 𝜓 (, 𝛥)$	$𝛤, 𝜑_2 \vdash \top 𝜓 (, 𝛥)$
$𝛤, 𝜑_1 ∨ 𝜑_2 \vdash \top 𝜓, (, 𝛥)$

---

Th :

1. $LJ_0+Cut = LJ_0$
2. $LJ_0$ a la propriété de la sous-formule

---

Modèles de Kripke

\[K ≝ (W, ≤_k, 𝛼_k)\]

• $W$ est un ensemble de mondes
• $≤_K$ est un ordre partiel sur les mondes

• $𝛼_K : W ⟶ 2^P$ où

  • $𝛼_K$ est croissante : si $w ≤ w’$, alors $𝛼(w)⊆𝛼(w’)$

Sémantique de Kripke

Pour $K$ fixé.

Sémantique : idem à précédemment, à la différence près que

\[w \Vdash 𝜑_1 ⟹ 𝜑_2\]

ssi

pour tout $w’≥w$, si $w’ \Vdash 𝜑_1$ alors $w’ \Vdash 𝜑_2$

---

$K, w \Vdash 𝛤$ :

ssi c’est le cas pour toute $𝜑∈𝛤$

$K, w \Vdash (𝛤 \vdash 𝜑)$ :

ssi $K, w \Vdash 𝛤$ implique $K, w \Vdash 𝜑$

---

TH :

1. $LJ_0$ est correct
2. $LJ_0 ⟹$ (règle d’axiome + règles avec $⟹$) est complet