summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-14 15:12:26 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-14 15:12:26 +0100
commit90252bf926e8a6727ba1dfd5a3d22167b49f4d20 (patch)
tree6d6a22d25cfdf6e9eacad08fdcd149dc40340bf4
parent6901d599346dea164b4f9065c6829bf937d6bd08 (diff)
downloadinf110-lfi-90252bf926e8a6727ba1dfd5a3d22167b49f4d20.tar.gz
inf110-lfi-90252bf926e8a6727ba1dfd5a3d22167b49f4d20.tar.bz2
inf110-lfi-90252bf926e8a6727ba1dfd5a3d22167b49f4d20.zip
Truth-table semantics.
-rw-r--r--transp-inf110-02-typage.tex142
1 files changed, 142 insertions, 0 deletions
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}
@@ -3966,6 +3971,143 @@ 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:
% - Kripke
% - CPS et fragment négatif