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

Leave a comment