TD 5 : Sémantique de Kripke

Énoncé

EX 1

${\cal K} ≝ (W, ≤, I)$

Montrons par induction structurelle sur $𝜑$ que :

pour toute formule $𝜑$, si ${\cal K}, 𝛼 \Vdash 𝜑$, alors pour tout $𝛽 ≥𝛼$, $𝛽 \Vdash 𝜑$

  • Si $𝜑∈V$ :

    ${\cal K}, 𝛼 \Vdash 𝜑$ équivaut à $𝜑∈I(𝛼)$, d’où

    \[I(𝛽) \supset I(𝛼) \ni 𝜑\]

    et

    \[{\cal K}, 𝛽 \Vdash 𝜑\]

  • Si $𝜑 = 𝜓_1 ∨ 𝜓_2$ :

    ${\cal K}, 𝛼 \Vdash 𝜑$ équivaut à ${\cal K}, 𝛼 \Vdash 𝜓_1$ ou ${\cal K}, 𝛼 \Vdash 𝜓_2$, d’où ${\cal K}, 𝛽 \Vdash 𝜓_1$ ou ${\cal K}, 𝛽 \Vdash 𝜓_2$ (par hypothèse d’induction), et on conclut.

  • Si $𝜑 = 𝜓_1 ∨ 𝜓_2$ : idem

  • Si $𝜑 = ¬ 𝜓$ :

    ${\cal K}, 𝛼 \Vdash 𝜑$ équivaut à : pour tout $𝛽 ≥𝛼$, ${\cal K}, 𝛽 \not\Vdash 𝜓$.

    Soit $𝛽 ≥𝛼$.

    Pour tout $𝛾 ≥ 𝛽$, $𝛾 ≥ 𝛼$ par transitivité, donc on conclut.

  • Si $𝜑 = 𝜓_1 ⟶ 𝜓_2$ : on procède de manière analogue au cas précédent.

EX 2

1.

  digraph {
    rankdir=BT;
    1[label="𝜔_1:∅ "];
    2[label="𝜔_2:P "];
    1 -> 2;
  }
  • ${\cal K}, 𝜔_1 \not\Vdash P$ clairement
  • ${\cal K}, 𝜔_1 \not\Vdash ¬P$ car $¬(𝜔_2 \not\Vdash P)$

2.

  digraph {
    rankdir=BT;
    1[label="𝜔_1:∅ "];
    2[label="𝜔_2:P "];
    1 -> 2;
  }

  • ${\cal K}, 𝜔_1 \not\Vdash ¬¬P⟶P$ car

    • ${\cal K}, 𝜔_1 \Vdash ¬¬P$

    ⟺ $∀𝜔≥𝜔_1, {\cal K}, 𝜔 \not\Vdash ¬P$

    ⟺ $∀𝜔≥𝜔_1, ∃𝜔’≥𝜔, {\cal K}, 𝜔’ \Vdash P$

    C’est le cas avec $𝜔’=𝜔_2$

3.

  digraph {
    rankdir=BT;
    1[label="𝜔_1:∅"];
    2[label="𝜔_2:P"];
    3[label="𝜔_3:Q"];
    1 -> {2, 3};
  }

  • ${\cal K}, 𝜔_1 \not\Vdash (P⟶Q) ∨ (Q⟶P)$ car

    • ${\cal K}, 𝜔_1 \not\Vdash (P⟶Q)$ puisque $𝜔_2 ≥ 𝜔_1$ et ${\cal K}, 𝜔_2 \not\Vdash (P⟶Q)$

    • ${\cal K}, 𝜔_1 \not\Vdash (Q⟶P)$ puisque $𝜔_3 ≥ 𝜔_1$ et ${\cal K}, 𝜔_3 \not\Vdash (Q⟶P)$

4.

  digraph {
    rankdir=BT;
    1[label="𝜔_1:∅"];
    2[label="𝜔_2:P"];
    3[label="𝜔_3:∅"];
    1 -> {2, 3};
  }

  • ${\cal K}, 𝜔_1 \not\Vdash ¬P ∨ ¬¬P$ car

    • ${\cal K}, 𝜔_1 \not\Vdash ¬P$ puisque $𝜔_2 ≥ 𝜔_1$ et ${\cal K}, 𝜔_2 \Vdash P$

    • ${\cal K}, 𝜔_1 \not\Vdash ¬¬P$ puisque $𝜔_3 ≥ 𝜔_1$ et ${\cal K}, 𝜔_3 \not\Vdash P$

5.

  digraph {
    rankdir=BT;
    1[label="𝜔_1:∅ "];
    2[label="𝜔_2:P "];
    1 -> 2;
  }

  • ${\cal K}, 𝜔_1 \not\Vdash ¬(¬P ∧ ¬Q)⟹P∨Q$ car

    • ${\cal K}, 𝜔_1 \not\Vdash P$ et ${\cal K}, 𝜔_1 \not\Vdash Q$

    • ${\cal K}, 𝜔_1 \not\Vdash ¬(¬P ∧ ¬Q)$ car il existe un $𝜔≥𝜔_1$ tel que ${\cal K}, 𝜔 \not\Vdash ¬P$, ou il existe un $𝜔≥𝜔_1$ tel que ${\cal K}, 𝜔 \not\Vdash ¬P$

6.

  digraph {
    rankdir=BT;
    1[label="𝜔_1:Q "];
    2[label="𝜔_2:P,Q "];
    1 -> 2;
  }

EX 3

1.

a).

   
$𝜑, 𝜓\vdash 𝜑$ $𝜑, 𝜓\vdash 𝜓$
$¬𝜑, 𝜑, 𝜓\vdash \bot$ $¬𝜓, 𝜑, 𝜓\vdash \bot$
$¬𝜑, (𝜑∧𝜓)\vdash \bot$ $¬𝜓, (𝜑∧𝜓)\vdash \bot$
$¬𝜑\vdash ¬(𝜑∧𝜓)$ $¬𝜓\vdash ¬(𝜑∧𝜓)$
$¬¬(𝜑∧𝜓), ¬𝜑\vdash \bot$ $¬¬(𝜑∧𝜓), ¬𝜓\vdash \bot$
$¬¬(𝜑∧𝜓)\vdash ¬¬𝜑$ $¬¬(𝜑∧𝜓)\vdash ¬¬𝜓$
$¬¬(𝜑∧𝜓), ¬¬(𝜑∧𝜓)\vdash (¬¬𝜑∧¬¬𝜓)$  
$¬¬(𝜑∧𝜓)\vdash (¬¬𝜑∧¬¬𝜓)$  
$¬¬(𝜑∧𝜓)\vdash (¬¬𝜑∧¬¬𝜓)$  
$\vdash ¬¬(𝜑∧𝜓)⟶(¬¬𝜑∧¬¬𝜓)$  
   
$𝜑\vdash 𝜑$ $𝜓\vdash 𝜓$
$𝜑, 𝜓\vdash (𝜑∧𝜓)$  
$¬(𝜑∧𝜓), 𝜑, 𝜓\vdash \bot$  
$¬(𝜑∧𝜓), 𝜑\vdash ¬𝜓$  
$¬¬𝜓, ¬(𝜑∧𝜓), 𝜑\vdash \bot$  
$¬¬𝜓, ¬(𝜑∧𝜓)\vdash ¬𝜑$  
$¬¬𝜑, ¬¬𝜓, ¬(𝜑∧𝜓)\vdash \bot$  
$(¬¬𝜑∧¬¬𝜓), ¬(𝜑∧𝜓)\vdash \bot$  
$(¬¬𝜑∧¬¬𝜓)\vdash ¬¬(𝜑∧𝜓)$  
$\vdash (¬¬𝜑∧¬¬𝜓) ⟶ ¬¬(𝜑∧𝜓)$  

b).

Supposons que

\[\vdash P ∨ Q ⟺ f(P, Q)\]

où $f(P, Q)$ est une formule n’utilisant que les connecteurs $\lbrace \bot, ∧, ¬, ⟶ \rbrace$

Montrons que

\[\vdash ¬¬(P∨Q)⟺(¬¬P∨¬¬Q)\]

en logique intuitionniste.

Ce qui revient à montrer que, modulo la règle Cut :

\[\vdash ¬¬f(P,Q)⟺f(¬¬P,¬¬Q)\]

Montrons

\[\begin{cases} ¬¬f(P,Q)\vdash f(¬¬P,¬¬Q) \\ f(¬¬P,¬¬Q) \vdash ¬¬f(P,Q) \end{cases}\]

Par induction structurelle sur $f(P,Q)$ :

  • Cas de base :

    • Si $f(P,Q) = P ⟶ Q$ ou $f(P,Q) = P ∧ Q$ : immédiat par 1.a)

    • Si $f(P,Q) = \bot$ alors le résultat s’ensuit puisque

 
$\bot \vdash \bot$
$\vdash ¬\bot$
$¬¬\bot \vdash \bot$

  • Si $f(P,Q) = ¬P$ : il est immédiat que $¬¬¬P \vdash ¬¬¬P$ (axiome)

  • Si $f(P,Q) = ¬Q$ : idem

  • Induction :

    • Si $f(P,Q) = f_1(P,Q) \circ f_2(P,Q)$ où $\circ ∈ \lbrace ⟶, ∧ \rbrace$:
    \[\vdash ¬¬(f_1(P,Q) \circ f_2(P,Q))⟺f_1(¬¬P,¬¬Q) \circ f_2(¬¬P, ¬¬Q)\]
   
$¬¬f_1(P,Q) \vdash f_1(¬¬P,¬¬Q)$ $¬¬ f_2(P,Q) \vdash f_2(¬¬P, ¬¬Q)$
  • Si $f(P,Q) = ¬f_1(P,Q)$ :

c).

  digraph {
    rankdir=BT;
    1[label="𝜔_1:∅"];
    2[label="𝜔_2:P"];
    3[label="𝜔_3:Q"];
    1 -> {2, 3};
  }

Sémantique de Tarski

Topologie sur $ℝ$, où les ouverts sont de la forme

\[]x,y[, x∈ℝ∪ \lbrace +∞ \rbrace, y∈ℝ∪ \lbrace -∞ \rbrace\]

Interprétation des formules : les ouverts.

  • $P_I = I(P)$
  • $\top = ℝ$
  • $\bot = ∅$
  • $(𝜑_1 ∨ 𝜑_2)_I = {𝜑_1}_I ∪ {𝜑_2}_I$
  • $(𝜑_1 ∧ 𝜑_2)_I = {𝜑_1}_I ∩ {𝜑_2}_I$
  • $(¬𝜑)_I = \overset{\circ}{\widehat{(𝜑_I)^c}}$
\[\bigcap_{𝜓∈𝛤} 𝜓_I ⊆ 𝜑_I\]

⟶ Algèbre de Heyting, Logique intuitionniste

Il y a complétude de cette sémantique pour le calcul des séquents intuitionniste

Montrons que le tiers-exclus n’est pas valide :

Il suffit de montrer que

\[(P∨¬P)_I ≠ ℝ\]

⟶ avec $(P)_I = ]-∞, 0[$

NB : Si on prend l’ensemble des parties, on tombe sur la logique classique ⟶ algèbre de Boole

Leave a comment