summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-14 14:34:17 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-14 14:34:17 +0100
commit6901d599346dea164b4f9065c6829bf937d6bd08 (patch)
treed94dfdf53c331973e46c20903536fc37cb43fcdf
parent8658f79341e546996382a31223091db753f9fab0 (diff)
downloadinf110-lfi-6901d599346dea164b4f9065c6829bf937d6bd08.tar.gz
inf110-lfi-6901d599346dea164b4f9065c6829bf937d6bd08.tar.bz2
inf110-lfi-6901d599346dea164b4f9065c6829bf937d6bd08.zip
General handwaving about semantics in logic.
-rw-r--r--transp-inf110-02-typage.tex81
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