From f7c363a563fb87edec9df488245a9be44deb9d58 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 5 Jan 2024 14:26:25 +0100
Subject: Another exercise on Kripke semantics.

---
 exercices-inf110.tex | 110 +++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 106 insertions(+), 4 deletions(-)

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 44f9c50..e6c7867 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -2383,10 +2383,14 @@ flèches explicites pour le rappeler).
 Soit $p$ l'affectation de vérité qui vaut $1$ en $u_0$ et $0$ en
 chacun de $v_0,u_1,v_1,u_2$.  Pour ce $p$, calculer l'affectation de
 vérité de $((\neg\neg p \Rightarrow p)\Rightarrow(p\lor\neg p))
-\Rightarrow(\neg p\lor\neg\neg p)$.  En déduire que la formule
-$((\neg\neg A \Rightarrow A)\Rightarrow(A\lor\neg A)) \Rightarrow(\neg
-A\lor\neg\neg A)$ n'est pas démontrable en calcul propositionnel
-intuitionniste.
+\Rightarrow(\neg p\lor\neg\neg p)$ (c'est-à-dire plus exactement
+$((\dottedneg\dottedneg p \dottedlimp
+p)\dottedlimp(p\dottedlor\dottedneg p)) \dottedlimp(\dottedneg
+p\dottedlor\dottedneg\dottedneg p)$, où les points rappellent qu'on
+parle de l'interprétation des connecteurs données par la sémantique de
+Kripke).  En déduire que la formule $((\neg\neg A \Rightarrow
+A)\Rightarrow(A\lor\neg A)) \Rightarrow(\neg A\lor\neg\neg A)$ n'est
+pas démontrable en calcul propositionnel intuitionniste.
 
 \begin{corrige}
 On calcule successivement l'affectation de vérité de chacune des
@@ -2427,6 +2431,104 @@ n'est pas démontrable.
 \end{corrige}
 
 
+\exercice\ (${\star}{\star}$)\par\nobreak
+
+Pour $n\in\mathbb{N}$, on considère le cadre de Kripke
+$\{w_0,\ldots,w_{n-1}\}$ formé de $n$ mondes totalement ordonnés par
+$w_i \leq w_j$ lorsque $i\geq j$ (le fait d'inverser l'ordre s'avérera
+plus commode pour l'écriture de la suite) :
+\begin{center}
+\begin{tikzpicture}[>=stealth']
+\node (wmax) at (-180bp,0bp) {$w_{n-1}$};
+\node (dots) at (-140bp,0bp) {$\cdots$};
+\node (w2) at (-100bp,0bp) {$w_2$};
+\node (w1) at (-50bp,0bp) {$w_1$};
+\node (w0) at (0bp,0bp) {$w_0$};
+\draw (wmax)--(dots);
+\draw[->] (dots)--(w2);
+\draw[->] (w2)--(w1);
+\draw[->] (w1)--(w0);
+\end{tikzpicture}
+\end{center}
+
+On définit aussi $n+1$ affectations de vérité $p_0,\ldots,p_n$ par
+$p_k(w_i) = 1$ lorsque $i<k$ et $p_k(w_i) = 0$ lorsque $i\geq k$
+(notamment, $p_0$ est l'affectation $\dottedbot$ et $p_n$ est
+l'affectation $\dottedtop$).  Pourquoi sont-ce les seules affectations
+de vérité sur ce cadre ?  Calculer les tableaux de $\dottedland,
+\dottedlor, \dottedlimp, \dottedneg$ sur $p_0,\ldots,p_n$.
+
+Donner un exemple de formule propositionnelle classiquement
+démontrable et qui n'est pas validée par ce cadre (si $n\geq 2$), et
+un exemple de formule propositionnelle validée par ce cadre et qui pas
+démontrable intuitionnistement.
+
+\begin{corrige}
+La contrainte sur une affectation de vérité sur un cadre de Kripke $W$
+est d'être permanente, i.e., si $p(w)=1$ alors $p(w')=1$ pour tout
+monde $w'$ accessible depuis $w$ (c'est-à-dire $w\leq w'$), autrement
+dit d'etre une fonction croissante $W \to \{0,1\}$.  Comme ici $W$ est
+simplement $\{0,\ldots,n-1\}$ avec l'ordre inversé, les seules
+fonctions décroissantes $\{0,\ldots,n-1\} \to \{0,1\}$ étant celles
+qui valent $1$ jusqu'à un certain point et $0$ ensuite, on obtient les
+$p_k$ qu'on a décrits.
+
+Le calcul de $\dottedland$ et $\dottedlor$ est facile puisqu'il se
+fait monde par monde : on a $(p_k \dottedland p_\ell)(w_i) = 1$
+lorsque $p_k(w_i) = 1$ et $p_\ell(w_i) = 1$, c'est-à-dire $i<k$ et
+$i<\ell$, ce qui équivaut à $i<\min(k,\ell)$, ce qui montre $p_k
+\dottedland p_\ell = p_{\min(k,\ell)}$ ; de même, on a $(p_k
+\dottedlor p_\ell)(w_i) = 1$ lorsque $p_k(w_i) = 1$ ou $p_\ell(w_i) =
+1$, c'est-à-dire $i<k$ ou $i<\ell$, ce qui équivaut à
+$i<\max(k,\ell)$, ce qui montre $p_k \dottedlor p_\ell =
+p_{\max(k,\ell)}$.
+
+Reste à traiter le cas de $\dottedlimp$.  Si $k\leq\ell$, alors
+$p_k(w_j) = 1$ implique $p_\ell(w_j) = 1$ (car $j<k$ implique
+$j<\ell$), et ce, pour tout $j$, ce qui montre $(p_k\dottedlimp
+p_\ell) = \dottedtop = p_n$ dans ce cas.  En revanche, si $k>\ell$, il
+faut distinguer deux cas : lorsque $j<\ell$, on a $p_k(w_j) = 1$ et
+$p_\ell(w_j) = 1$, ce qui montre que $(p_k\dottedlimp p_\ell)(w_i) =
+1$ pour $i<\ell$ ; mais comme $p_k(w_\ell) = 1$ et cependant
+$p_\ell(w_\ell) = 0$, on a $(p_k\dottedlimp p_\ell)(w_i) = 0$ pour
+$i\geq \ell$ ; c'est-à-dire que $(p_k\dottedlimp p_\ell) = p_\ell$
+dans ce cas.  Enfin, $\dottedneg q$ est simplement $q\dottedlimp
+\dottedbot$, c'est-à-dire $q\dottedlimp p_0$.
+
+Pour résumer :
+\[
+\begin{aligned}
+p_k \dottedland p_\ell &= p_{\min(k,\ell)} \\
+p_k \dottedlor p_\ell &= p_{\max(k,\ell)} \\
+(p_k \dottedlimp p_\ell) &=
+\left\{
+\begin{array}{ll}
+p_n&\text{~si $k\leq\ell$}\\
+p_\ell&\text{~si $k>\ell$}\\
+\end{array}
+\right.
+\\
+\dottedneg p_k &=
+\left\{
+\begin{array}{ll}
+p_n&\text{~si $k=0$}\\
+p_0&\text{~si $k>0$}\\
+\end{array}
+\right.
+\end{aligned}
+\]
+
+La formule $A\lor\neg A$, classiquement démontrable, n'est pas validée
+par ce cadre lorsque $n\geq 2$ (prendre $p_1$ pour $A$ : on trouve
+$p_1 \dottedlor \dottedneg p_1 = p_1$).  La formule $\neg
+A\lor\neg\neg A$, en revanche, est validée par ce cadre (car
+$\dottedneg\dottedneg p_k = p_n$ si $k>0$ et $p_0$ si $k=0$) mais
+n'est pas prouvable intuitionnistement (par la propriété de la
+disjonction : si elle était prouvable, soit $\neg A$ soit $\neg\neg A$
+le serait, or elles ne sont même pas prouvables classiquement).
+\end{corrige}
+
+
 %
 %
 %
-- 
cgit v1.2.3