diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 81 |
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 |