summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-14 16:20:36 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-14 16:20:36 +0100
commited9be5a414c1d3a249db6cb4b1c920689f848086 (patch)
tree594ff610a5b803c0e9ace719d1d5082b77516a58
parent90252bf926e8a6727ba1dfd5a3d22167b49f4d20 (diff)
downloadinf110-lfi-ed9be5a414c1d3a249db6cb4b1c920689f848086.tar.gz
inf110-lfi-ed9be5a414c1d3a249db6cb4b1c920689f848086.tar.bz2
inf110-lfi-ed9be5a414c1d3a249db6cb4b1c920689f848086.zip
More about Kripke frames and semantics.
-rw-r--r--transp-inf110-02-typage.tex162
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}