summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-14 16:42:00 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-14 16:42:00 +0100
commit3a2fa75340fe92e66190eb84b555f7044ef39e4b (patch)
tree27ee4b1d649e24ce9756b79cfab57a15df35c9b9
parented9be5a414c1d3a249db6cb4b1c920689f848086 (diff)
downloadinf110-lfi-3a2fa75340fe92e66190eb84b555f7044ef39e4b.tar.gz
inf110-lfi-3a2fa75340fe92e66190eb84b555f7044ef39e4b.tar.bz2
inf110-lfi-3a2fa75340fe92e66190eb84b555f7044ef39e4b.zip
Semantics of open sets.
-rw-r--r--transp-inf110-02-typage.tex61
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
%