From a96bca145d8b48d7fed74b94a3e1f5efd9ce3029 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Thu, 14 Dec 2023 18:15:40 +0100
Subject: Examples in open sets semantics.

---
 transp-inf110-02-typage.tex | 56 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 54 insertions(+), 2 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 25c5720..3dc9c75 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4321,10 +4321,62 @@ complète pour le calcul propositionnel intuitionniste :
 \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.
+  simplement de $\mathbb{R}^n$} pour un $n \geq 1$ donné, alors
+  $\varphi$ est démontrable en calcul propositionnel intuitionniste.
 \end{itemize}
 
+\medskip
+
+\itempoint La sémantique des ouverts modélise plus ou moins
+l'intuition que la vérité est une « notion locale » (si quelque chose
+est vrai en un point, c'est vrai autour de ce point).
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Sémantique des ouverts : exemples}
+
+\itempoint Soit $U = \mathopen{]}0,1\mathclose{[}$ dans $X =
+    \mathbb{R}$.  Alors
+\begin{itemize}
+\item $\dottedneg U = \mathopen{]}-\infty,0\mathclose{[} \cup
+  \mathopen{]}1,+\infty\mathclose{[}$
+\quad\itempoint $\dottedneg\dottedneg U = \mathopen{]}0,1\mathclose{[} = U$
+\quad\itempoint $(\dottedneg\dottedneg U \dottedlimp U) = \mathbb{R}$
+\item $U \dottedlor \dottedneg U = \mathbb{R}\setminus\{0,1\}$
+\quad\itempoint $((\dottedneg\dottedneg U \dottedlimp U) \dottedlimp
+(U \dottedlor \dottedneg U)) = \mathbb{R}\setminus\{0,1\}$
+\end{itemize}
+Par correction, ceci montre que $((\neg\neg A \Rightarrow A)
+\Rightarrow (A \lor \neg A))$ n'est pas prouvable en logique
+intuitionniste.
+
+\bigskip
+
+{\footnotesize
+
+\itempoint Dans $X = \mathbb{R}^2$, soit $U = \{(x_1,x_2) : x_1<0
+\text{~et~} x_2<0\}$ et $V_1 = \{x_1>0\}$ et $V_2 = \{x_2>0$\}.
+\begin{itemize}
+\item $\dottedneg U = \{(x_1,x_2) : x_1>0 \text{~ou~} x_2>0\} =
+  V_1\dottedlor V_2$
+\quad\itempoint Donc $(\dottedneg U \dottedlimp (V_1\dottedlor V_2)) =
+\mathbb{R}^2$
+\item $(\dottedneg U \dottedlimp V_1) = \{(x_1,x_2) : x_1<0
+  \text{~ou~} x_2>0\}$
+\item $(\dottedneg U \dottedlimp V_2) = \{(x_1,x_2) : x_1>0
+  \text{~ou~} x_2<0\}$
+\item $(\dottedneg U \dottedlimp V_1) \dottedlor (\dottedneg U
+  \dottedlimp V_2) = \mathbb{R}^2 \setminus\{(0,0)\}$
+\end{itemize}
+Ceci montre que $(\neg A \Rightarrow B_1) \lor (\neg A \Rightarrow
+B_2) \Rightarrow (\neg A \Rightarrow (B_1\lor B_2))$ (« axiome de
+Kreisel-Putnam ») n'est pas prouvable en logique intuitionniste (et
+\textit{a fortiori} $(C \Rightarrow B_1) \lor (C \Rightarrow B_2)
+\Rightarrow (C \Rightarrow (B_1\lor B_2))$ ne l'est pas).
+
+\par}
+
 \end{frame}
 %
 % TODO:
-- 
cgit v1.2.3