Semantics of open sets.

1 files changed, 61 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 5d43757..25c5720 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4266,6 +4266,67 @@ $
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Sémantique 2 : les ouverts en topologie}
+
+Fixons $X$ un espace topologique : si on ne sait pas ce que c'est,
+penser à un espace métrique ou simplement $\mathbb{R}^m$ avec sa
+topologie ordinaire.  On note $\mathcal{O}(X)$ la topologie de $X$,
+c'est-à-dire l'ensemble des ouverts de $X$.
+
+\medskip
+
+On définit les opérations suivantes sur $\mathcal{O}(X)$ :
+\begin{itemize}
+\item $U \dottedland V := U\cap V$
+\quad\itempoint $U \dottedlor V := U\cup V$
+\quad\itempoint $\dottedtop := X$
+\quad\itempoint $\dottedbot := \varnothing$
+\item $(U \dottedlimp V) := \operatorname{int}((X\setminus U) \cup V)$
+  (où $\operatorname{int}$ désigne l'intérieur) est l'ensemble des
+  points $x \in X$ tels qu'il y ait un ouvert $W \ni x$ t.q.  $(U\cap
+  W) \subseteq (V\cap W)$ {\footnotesize (= les points « au voisinage
+    desquels » $U \subseteq V$)}, ou, si on préfère, le plus grand
+  ouvert $W$ tel que $(U\cap W) \subseteq (V\cap W)$ ;
+\item notamment, $\dottedneg U := \operatorname{int}(X\setminus U)$,
+  plus grand ouvert disjoint de $U$ ;
+\item notamment, $\dottedneg \dottedneg U :=
+  \operatorname{int}(\operatorname{adh}(U))$ (intérieur de l'adhérence
+  de $U$, ou « régularisé » de $U$).
+\end{itemize}
+
+\medskip
+
+\itempoint Si $\varphi(A_1,\ldots,A_r)$ est une formule
+propositionnelle et $U_1,\ldots,U_r \in \mathcal{O}(X)$, on définit
+$\dot\varphi(U_1,\ldots,U_r)$ de façon évidente (par induction).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Sémantique des ouverts : correction et complétude}
+
+De façon surprenante, les opérations qu'on a définies sur les ouverts
+de $X$ fournissent un modèle du calcul propositionnel intuitionniste :
+
+\medskip
+
+\textbf{Théorème} (Tarski) : la sémantique des ouverts est correcte et
+complète pour le calcul propositionnel intuitionniste :
+\begin{itemize}
+\item\underline{correction :} si $\varphi(A_1,\ldots,A_r)$ est une
+  théorème du calcul propositionnel intuitionniste, alors quel que
+  soit $X$ et $U_1,\ldots,U_r$ ouverts de $X$, on a
+  $\dot\varphi(U_1,\ldots,U_r) = \dottedtop$ (l'espace tout entier) ;
+\item\underline{complétude :} réciproquement, si
+  $\dot\varphi(U_1,\ldots,U_r) = \dottedtop$ pour tous ouverts
+  $U_1,\ldots,U_r$ de tout espace topologique $X$, \alert{ou même
+  simplement de $\mathbb{R}^n$}, alors $\varphi$ est démontrable en
+  calcul propositionnel intuitionniste.
+\end{itemize}
+
+\end{frame}
+%
 % TODO:
 % - inférence de type de Hindley-Milner
 %