More about Kripke frames and semantics.

1 files changed, 159 insertions, 3 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index e548e6f..5d43757 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -37,6 +37,7 @@
 \newcommand{\dottedlor}{\mathbin{\dot\lor}}
 \newcommand{\dottedtop}{\mathord{\dot\top}}
 \newcommand{\dottedbot}{\mathord{\dot\bot}}
+\newcommand{\dottedneg}{\mathop{\dot\neg}}
 \mathchardef\emdash="07C\relax
 \newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}}
 \setlength{\derivskip}{4pt}
@@ -1748,7 +1749,8 @@ logique intuitionniste.
   sémantique booléenne du calcul propositionnel classique »)} : $P$
 est une tautologie de la logique classique \alert{ssi} pour toute
 substitution de $\bot$ ou $\top$ à chacune des variables
-propositionnelles de $P$ a la valeur de vérité $\top$.
+propositionnelles de $P$ a la valeur de vérité $\top$.  (Voir
+transp. \ref{truth-table-semantics} plus loin pour précisions.)
 
 \bigskip
 
@@ -4012,6 +4014,7 @@ elle est peu maniable et/ou un peu triviale !
 \end{frame}
 %
 \begin{frame}
+\label{truth-table-semantics}
 \frametitle{Sémantique 0 : tableaux de vérité}
 
 {\footnotesize (Reprise de ce qui a déjà été dit.)\par}
@@ -4108,9 +4111,162 @@ complétude ($A\lor\neg A$ n'est pas démontrable).
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Sémantique 1 : cadres de Kripke}
+
+\textbf{Définitions :}
+\begin{itemize}
+\item un \textbf{cadre de Kripke} est {\footnotesize (dans ce
+  contexte)} un ensemble partiellement ordonné $(W,\leq)$ ; les
+  éléments de $W$ s'appellent les \textbf{mondes} ; si $w\leq w'$, on
+  dit que $w'$ est \textbf{accessible} depuis $w$ ;
+\item dans un cadre de Kripke, une \textbf{affectation de vérité} est
+  une fonction $p\colon W \to \mathbb{B}$ (où $\mathbb{B} = \{0,1\}$)
+  telle que si $p(w) = 1$ et $w\leq w'$ alors $p(w') = 1$ (i.e., $p$
+  est croissante, on dit aussi « permanente ») ;
+\item on définit des opérations $\dottedland, \dottedlor, \dottedlimp$
+  sur les affectations de vérité :
+\begin{itemize}
+\item $(q_1\dottedland q_2)(w) = 1$ ssi $q_1(w) = 1$ et $q_2(w) = 1$ ;
+\item $(q_1\dottedlor q_2)(w) = 1$ ssi $q_1(w) = 1$ ou $q_2(w) = 1$ ;
+\item $(q_1\dottedlimp q_2)(w) = 1$ ssi pour tout $w' \geq w$ t.q.
+  $q_1(w') = 1$, on a $q_2(w') = 1$ ;
+\item $\dottedtop(w) = 1$ partout ;
+\quad\itempoint $\dottedbot(w) = 0$ partout.
+\end{itemize}
+\item un \textbf{modèle de Kripke} est {\footnotesize (dans ce
+  contexte)} un cadre de Kripke $(W,\leq)$ muni d'une affectation de
+  vérité pour chaque variable propositionnelle ;
+\item $\varphi$ est \textbf{validée} par le modèle de Kripke lorsque
+  $\dot\varphi$ vaut $1$ dans tout monde $w$.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Cadres de Kripke (suite)}
+
+{\footnotesize Recopie : \itempoint $(q_1\dottedland q_2)(w) = 1$ ssi
+  $q_1(w) = 1$ et $q_2(w) = 1$ ;\quad\itempoint $(q_1\dottedlor
+  q_2)(w) = 1$ ssi $q_1(w) = 1$ ou $q_2(w) = 1$ ;\quad\itempoint
+  $(q_1\dottedlimp q_2)(w) = 1$ ssi pour tout $w' \geq w$ t.q.
+  $q_1(w') = 1$, on a $q_2(w') = 1$.\par}
+
+\medskip
+
+Par exemple :
+\begin{itemize}
+\item $\dottedneg p$ (c'est-à-dire $p\dottedlimp \dottedbot$) vaut $1$
+  dans le monde $w$ lorsque $p$ vaut $0$ dans \alert{tout monde
+    accessible} depuis $w$ ;
+\item $p\dottedlor\dottedneg p$ vaut $1$ dans le monde $w$ lorsque $p$
+  vaut $0$ dans \alert{tout monde accessible} depuis $w$ ou bien $1$
+  dans $w$ (donc dans tout monde accessible depuis $w$, par
+  permanence) : \textcolor{teal}{$p$ est « décidé » à vrai ou à
+    faux} ;
+\item $\dottedneg \dottedneg p$ vaut $1$ dans le monde $w$ lorsque
+  $\forall w'\geq w.\, \exists w''\geq w'.\, p(w'')=1$
+  \textcolor{teal}{(« dans tout futur possible, $p$ finit par devenir
+    vrai »)}.
+\end{itemize}
+
+\bigskip
+
+\itempoint La sémantique de Kripke modélise plus ou moins l'intuition
+selon laquelle « $A \Rightarrow B$ » ne signifie pas juste « soit $A$
+est vrai soit $B$ est faux » (sens en logique classique) mais bien
+« dans tout monde possible où $A$ est vrai, $B$ l'est ».
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Sémantique des cadres de Kripke}
+
+\textbf{Définitions} (suite) :
+\begin{itemize}
+\item {\footnotesize (déjà dit :)} $\varphi$ est \textbf{validée} par
+  le \alert{modèle} de Kripke (= valide dedans, = valable) lorsque
+  $\dot\varphi$ vaut $1$ dans tout monde $w$ ;
+\item $\varphi$ est \textbf{validée} par le \alert{cadre} de Kripke
+  lorsqu'elle est validée par toute affectation de vérité pour chacune
+  de ses variables (= tout modèle sur ce cadre) ;
+\item $\varphi$ est \textbf{validée} par \alert{la sémantique de
+  Kripke} lorsque $\varphi$ est validée par tout cadre (i.e., tout
+  modèle de Kripke).
+\end{itemize}
+
+\bigskip
+
+\textbf{Théorème} (Kripke) : la sémantique de Kripke est correcte et
+complète pour le calcul propositionnel intuitionniste :
+\begin{itemize}
+\item\underline{correction :} tout théorème propositionnel
+  intuitionniste est valide dans tout modèle de Kripke,
+\item\underline{complétude :} toute formule propositionnelle valide
+  dans tout modèle de Kripke est démontrable en calcul propositionnel
+  intuitionniste.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Cadres de Kripke : remarques}
+
+La sémantique de Kripke n'est complète que quand on considèe
+\alert{tous les cadres}.  Si on se limite aux modèles sur un cadre
+donné, ils peuvent valider des formules non démontrables.
+\begin{itemize}
+\item Le cadre réduit à un singleton valide la logique classique :
+  c'est exactement la sémantique booléenne ;
+\item Si $(W,\leq)$ est totalement ordonné, il valide la formule
+  $(A\Rightarrow B) \lor (B\Rightarrow A)$ {\footnotesize
+  (\underline{preuve :} sinon il y a un monde $w$ dans lequel
+  $p_A(w)=1$ mais $p_B(w)=0$ et un $w'$ dans lequel $p_A(w')=0$ mais
+  $p_B(w')=1$ ; mais si $w\leq w'$ ceci contredit la permanence de
+  $p_A$ et si $w\geq w'$ ceci contredit la permanence de
+  $p_B$~\qedsymbol)} qui n'est pas prouvable en logique
+  propositionnelle intuitionniste.
+\item Le cadre le plus simple après un singleton est $(\{0,1\},\leq)$,
+  qui correspond à une logique à trois valeurs de vérité, avec les
+  tableaux suivants.
+\end{itemize}
+
+{\footnotesize
+
+\begin{tabular}{c@{\hskip 30bp}c@{\hskip 30bp}c}
+$
+\begin{array}{c|ccc}
+\dottedland&0&?&1\\\hline
+0&0&0&0\\
+?&0&?&?\\
+1&0&?&1\\
+\end{array}
+$
+&
+$
+\begin{array}{c|ccc}
+\dottedlor&0&?&1\\\hline
+0&0&?&1\\
+?&?&?&1\\
+1&1&1&1\\
+\end{array}
+$
+&
+$
+\begin{array}{c|ccc}
+A \dottedlimp B&B=0&B={?}&B=1\\\hline
+A=0&1&1&1\\
+A={?}&0&1&1\\
+A=1&0&?&1\\
+\end{array}
+$
+\end{tabular}
+
+\par}
+
+\end{frame}
+%
 % TODO:
-% - Kripke
-% - CPS et fragment négatif
 % - inférence de type de Hindley-Milner
 %
 \end{document}