General handwaving about semantics in logic.

1 files changed, 81 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index eacec62..74e36e4 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3885,6 +3885,87 @@ mettre un seul devant toute la formule (traduction de Glivenko).
 
 \end{frame}
 %
+\section{Sémantique du calcul propositionnel intuitionniste}
+\begin{frame}
+\frametitle{Qu'est-ce qu'une « sémantique » en logique ?}
+
+De façon très (trop ?) vague :
+
+\smallskip
+
+\itempoint Une \textbf{logique} $\mathsf{L}$ est définie par un
+certain nombre de règles (axiomes, modes d'inférence)
+\alert{syntactique} opérant sur des « formules » et définit une notion
+de \textbf{théorème} comme les formules ayant une \textbf{preuve}
+selon ces règles.  On note (qqch comme) $\mathsf{L} \vdash \varphi$
+pour « $\varphi$ est un théorème [= est démontrable]
+selon $\mathsf{L}$ ».
+
+\medskip
+
+\itempoint Un \textbf{modèle} pour $\mathsf{L}$ est une structure
+mathématique générale qui donne un « sens » au symboles utilisés dans
+$\mathsf{L}$ et qui notamment déclare certaines formules comme
+\textbf{vraies} (noté $\mathcal{M} \vDash \varphi$).  Une
+\textbf{sémantique} est un ensemble de modèles (formés sur le même
+schéma).  On dit que la sémantique $\mathsf{S}$ \textbf{valide} une
+formule $\varphi$ lorsque $\varphi$ est vraie dans chacun de ses
+modèles (on note $\mathsf{S} \vDash \varphi$).
+
+\medskip
+
+On dit que
+\begin{itemize}
+\item $\mathsf{S}$ est \textbf{correcte} pour $\mathsf{L}$ lorsque
+  $\mathsf{L} \vdash \varphi$ implique $\mathsf{S} \vDash \varphi$
+  (« tout théorème est vrai dans tout modèle »).  On veut toujours
+  ça !
+\item $\mathsf{S}$ est \textbf{complète} pour $\mathsf{L}$ lorsque
+  $\mathsf{S} \vDash \varphi$ implique $\mathsf{L} \vdash \varphi$
+  (« toute formule vraie dans tout modèle est un théorème »).
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Exemples de sémantiques}
+
+\itempoint La sémantique des \textbf{tableaux de vérité booléens} est
+\alert{correcte et complète} pour le calcul propositionnel
+\alert{classique} : $\varphi$ est démontrable \alert{ssi} toute
+affectation de « vrai » ou « faux » à chacune de ses variables donne
+« vrai ».
+
+\smallskip
+
+Pour le calcul propositionnel \alert{intuitionniste}, elle n'est
+\alert{que correcte}.
+
+\medskip
+
+\itempoint Le plan réel $\mathbb{R}^2$ est un modèle des axiomes de la
+géométrie euclidienne.  Ce modèle est une sémantique correcte et
+complète à lui seul : un énoncé géométrique est démontrable à partir
+des axiomes \alert{ssi} il est vrai dans $\mathbb{R}^2$.
+
+\medskip
+
+\itempoint $\mathbb{N}$ est un modèle de ce qu'on appellera
+l'« \textbf{arithmétique de Peano du premier ordre} » $\mathsf{PA}$
+(c'est le « modèle souhaité » de $\mathsf{PA}$).  Ce modèle pris tout
+seul est une sémantique correcte mais \alert{non complète} (théorème
+d'\alert{incomplétude} de Gödel : il y a des énoncés vrais dans
+$\mathbb{N}$ mais non démontrables dans $\mathsf{PA}$).
+
+\medskip
+
+\itempoint En revanche, si on élargit les modèles aux « modèles du
+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}
+%
 % TODO:
 % - Kripke
 % - CPS et fragment négatif