A simple exercise on Kripke semantics.

1 files changed, 79 insertions, 1 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 10a5e8b..d3c885c 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -20,6 +20,7 @@
 \usepackage{graphics}
 \usepackage[usenames,dvipsnames]{xcolor}
 \usepackage{tikz}
+\usetikzlibrary{arrows}
 %
 \theoremstyle{definition}
 \newtheorem{comcnt}{Tout}[section]
@@ -2079,7 +2080,7 @@ $(u \mapsto 0, v\mapsto 1, w\mapsto 1)$.  Or si $(\neg\neg A
 \Rightarrow A) \Rightarrow (A \lor \neg A)$ était démontrable en
 calcul propositionnel intuitionniste, on trouverait constamment $1$
 quelle que soit l'affectation $p$ utilisé pour $A$ (par
-\emph{correction} de la sémantique des ouverts).  Comme ce n'est pas
+\emph{correction} de la sémantique de Kripke).  Comme ce n'est pas
 le cas, c'est que la proposition en question n'est pas démontrable.
 
 Une autre preuve est fournie par la sémantique de la réalisabilité
@@ -2217,4 +2218,81 @@ $\neg\neg(P \lor \neg P)$ (sans hypothèse).  Si on postule $\neg\neg Q
 %
 %
 %
+
+\section{Sémantique(s) du calcul propositionnel intuitionniste}
+
+
+\exercice\ (${\star}$)\par\nobreak
+
+On considère le cadre de Kripke dessiné ci-dessous, où une flèche $w
+\to w'$ signifie que $w \leq w'$ (« le monde $w'$ est accessible
+depuis le monde $w$ »), sachant que la relation $\leq$ doit bien sûr
+être réflexive et transitive (c'est la clôture réflexive-transitive de
+celle qui est représentée par les flèches : c'est-à-dire qu'on a bien
+sûr $u_0\leq u_0$ et $u_2\leq u_0$ par exemple, malgré l'absence de
+flèches explicites pour le rappeler).
+\begin{center}
+\begin{tikzpicture}[>=stealth']
+\node (u0) at (0bp,0bp) {$u_0$};
+\node (v0) at (35bp,-15bp) {$v_0$};
+\node (u1) at (0bp,-30bp) {$u_1$};
+\node (v1) at (35bp,-45bp) {$v_1$};
+\node (u2) at (0bp,-60bp) {$u_2$};
+\draw[->] (u1)--(u0);
+\draw[->] (u2)--(u1);
+\draw[->] (v1)--(v0);
+\draw[->] (u2)--(v0);
+\draw[->] (v1)--(u0);
+\end{tikzpicture}
+\end{center}
+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.
+
+\begin{corrige}
+On calcule successivement l'affectation de vérité de chacune des
+sous-formules de la formule proposée : on se rappelle que
+$q\Rightarrow r$ vaut $1$ en un monde $w$ lorsque dans tout monde $w'$
+accessible depuis $w$ pour lequel $q(w') = 1$ on a aussi $r(w') = 1$,
+et notamment, $\neg q$ vaut $q$ en un monde $w$ lorsque dans tout
+monde $w'$ accessible depuis $w$ on a $q(w') = 0$.  Par ailleurs, pour
+éviter de se trompre, on vérifie à tout stade que les affectations de
+vérité sont permanentes, c'est-à-dire que si $q(w) = 1$ on a $q(w') =
+1$ pour tout monde $w'$ accessible depuis $w$.  On obtient les
+résultats tabulés ci-dessous :
+
+\begin{center}
+\begin{tabular}{r|ccccc}
+Formule&$u_2$&$v_1$&$u_1$&$v_0$&$u_0$\\\hline
+$p$&$0$&$0$&$0$&$0$&$1$\\
+$\neg p$&$0$&$0$&$0$&$1$&$0$\\
+$p\lor \neg p$&$0$&$0$&$0$&$1$&$1$\\
+$\neg\neg p$&$0$&$0$&$1$&$0$&$1$\\
+$\neg p\lor \neg\neg p$&$0$&$0$&$1$&$1$&$1$\\
+$\neg\neg p \Rightarrow p$&$0$&$1$&$0$&$1$&$1$\\
+$(\neg\neg p \Rightarrow p)\Rightarrow (p\lor \neg p)$&$1$&$0$&$1$&$1$&$1$\\
+$((\neg\neg p \Rightarrow p)\Rightarrow (p\lor \neg p))
+\Rightarrow(\neg p\lor\neg\neg p)$&$0$&$1$&$1$&$1$&$1$\\
+\end{tabular}
+\end{center}
+
+On constate que l'affecatation de vérité de $((\neg\neg p \Rightarrow
+p)\Rightarrow (p\lor \neg p)) \Rightarrow(\neg p\lor\neg\neg p)$ n'est
+pas identiquement $1$ sur le cadre.  Or si $((\neg\neg A \Rightarrow
+A)\Rightarrow(A\lor\neg A)) \Rightarrow(\neg A\lor\neg\neg A)$ était
+démontrable en calcul propositionnel intuitionniste, on trouverait
+constamment $1$ dans tout cadre et en remplaçant $p$ par n'importe
+quelle affectation de vérité sur le cadre (par \emph{correction} de la
+sémantique de la sémantique de Kripke) : c'est donc que cette formule
+n'est pas démontrable.
+\end{corrige}
+
+
+%
+%
+%
 \end{document}