From 90252bf926e8a6727ba1dfd5a3d22167b49f4d20 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Thu, 14 Dec 2023 15:12:26 +0100
Subject: Truth-table semantics.

---
 transp-inf110-02-typage.tex | 142 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 142 insertions(+)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 74e36e4..e548e6f 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -32,6 +32,11 @@
 \newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
 \newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
 \newcommand{\cps}{\mathrm{CPS}}
+\newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}}
+\newcommand{\dottedland}{\mathbin{\dot\land}}
+\newcommand{\dottedlor}{\mathbin{\dot\lor}}
+\newcommand{\dottedtop}{\mathord{\dot\top}}
+\newcommand{\dottedbot}{\mathord{\dot\bot}}
 \mathchardef\emdash="07C\relax
 \newcommand{\mpdotsabove}[1]{\inferrule*{\vdots}{#1}}
 \setlength{\derivskip}{4pt}
@@ -3964,6 +3969,143 @@ premier ordre » (« modèles au sens de Tarski »), la sémantique devient
 complète (théorème de \alert{complétude} de Gödel pour la logique du
 premier ordre : tout énoncé vrai dans tout modèle est démontrable).
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Sémantiques du calcul propositionnel intuitionniste ?}
+
+\itempoint On a vu les \alert{règles syntaxiques} du calcul
+propositionnel intuitionniste (déduction naturelle, ou calcul des
+séquents).  Mais quel est le \textbf{sens} des connecteurs ?
+
+\medskip
+
+\begin{itemize}
+\item En logique classique, c'est facile : la sémantique des tableaux
+  de vérité est correcte et complète, donc on peut considérer qu'elle
+  définit le sens.
+\item En logique intuitionniste, on n'a donné pour l'instant qu'une
+  interprétation intuitive (Brouwer-Heyting-Kolmogorov) des
+  connecteurs.
+\end{itemize}
+
+\medskip
+
+\itempoint Avoir une sémantique (correcte) complète, ou « moins
+incomplète » que celle des tableaux de vérité permet de prouver qu'une
+formule logique n'est \alert{pas démontrable} (si elle n'est pas
+validée par cette sémantique).
+
+\medskip
+
+{\footnotesize
+
+\itempoint On peut considérer \alert{Curry-Howard} comme une
+sémantique : le « sens » de $\Rightarrow,\land,\lor,\top,\bot$ est
+donné par les opérations sur les types d'un langage de programmation,
+et les énoncés validés par le modèle sont ceux dont le type est
+habité.  Elle est complète si le langage est le $\lambda$CST.  Mais
+elle est peu maniable et/ou un peu triviale !
+
+\par}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Sémantique 0 : tableaux de vérité}
+
+{\footnotesize (Reprise de ce qui a déjà été dit.)\par}
+
+\medskip
+
+\itempoint On définit $\mathbb{B} := \{0,1\}$, $\dottedtop = 1$,
+$\dottedbot = 0$ et $\dottedland, \dottedlor, \dottedlimp \colon
+\mathbb{B}^2 \to \mathbb{B}$ par les tableaux de vérité usuels :
+
+\smallskip
+
+\begin{tabular}{c@{\hskip 30bp}c@{\hskip 30bp}c}
+$
+\begin{array}{c|cc}
+\dottedland&0&1\\\hline
+0&0&0\\
+1&0&1\\
+\end{array}
+$
+&
+$
+\begin{array}{c|cc}
+\dottedlor&0&1\\\hline
+0&0&1\\
+1&1&1\\
+\end{array}
+$
+&
+$
+\begin{array}{c|cc}
+A \dottedlimp B&B=0&B=1\\\hline
+A=0&1&1\\
+A=1&0&1\\
+\end{array}
+$
+\end{tabular}
+
+\medskip
+
+\itempoint Si $\varphi$ est une formule propositionnelle en $r$
+variables, ceci définit une fonction $\dot\varphi \colon \mathbb{B}^r
+\to \mathbb{B}$ par composition.
+
+\medskip
+
+\itempoint Un \textbf{modèle booléen} du calcul propositionnel est une
+affectation $\{\mathrm{variables}\} \to \mathbb{B}$ : chaque formule
+$\varphi$ a donc une valeur de vérité ($0$ ou $1$) dans le modèle,
+donnée par $\dot\varphi$.  On dit que $\mathcal{M} \vDash \varphi$
+lorsque c'est $1$.
+
+\medskip
+
+\itempoint On dit que la sémantique booléenne valide $\varphi$ lorsque
+$\mathcal{M} \vDash \varphi$ pour tout modèle (i.e., $\dot\varphi$
+vaut constamment $1$).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Correction et complétude classique des tableaux de vérité}
+
+\textbf{Théorème :} la sémantique booléenne est \alert{correcte et
+  complète} pour le calcul propositionnel classique.
+
+\medskip
+
+\underline{Esquisse de preuve :}
+
+\smallskip
+
+\itempoint\underline{Correction :} on montre par induction sur la
+preuve que si $\eta_1,\ldots,\eta_r \vdash \varphi$ alors $\dot\varphi
+= 1$ dans tout modèle où $\dot\eta_1 = \cdots = \dot\eta_r = 1$ : la
+vérification est très facile sur chaque règle du calcul
+propositionnel.
+
+\medskip
+
+\itempoint\underline{Complétude :} on démontre \alert{classiquement}
+$\vdash A_i \lor \neg A_i$ pour chaque variable $A_i$, puis on utilise
+l'élimination du $\lor$ pour se placer dans chacun des $2^r$ cas
+possibles (i.e., avec $A_i$ ou $\neg A_i$ dans les hypothèses).  Dans
+chaque cas on a $A_i \Leftrightarrow \top$ ou $A_i \Leftrightarrow
+\bot$ pour chaque variable, donc en suivant les tableaux de vérité on
+a $\varphi$ (vraie).  L'élimination du $\lor$ montre alors $\varphi$
+vraie.\qed
+
+\bigskip
+
+\alert{Intuitionnistement}, la correction vaut toujours, mais plus la
+complétude ($A\lor\neg A$ n'est pas démontrable).
+
 \end{frame}
 %
 % TODO:
-- 
cgit v1.2.3