An exercise showing that Scott's formula is not provable.

1 files changed, 80 insertions, 0 deletions

diff --git a/controle-20260126.tex b/controle-20260126.tex
index 617e33b..3f5e45e 100644
--- a/controle-20260126.tex
+++ b/controle-20260126.tex
@@ -549,6 +549,86 @@ Qed.
 
 \exercice
 
+Dans cet exercice, on veut montrer que la « formule de Scott », à
+savoir la formule propositionnelle suivante :
+\[
+((\neg\neg A \Rightarrow A) \,\Rightarrow\, (A \lor \neg A))
+\;\Rightarrow\; (\neg\neg A \lor \neg A)
+\]
+n'est pas un théorème du calcul propositionnel intuitionniste.
+
+Pour cela, on introduit l'espace topologique $X = \mathbb{R}$ et
+l'ouvert suivant :
+\[
+\begin{aligned}
+U \;&=\; \left\{ x\in \mathbb{R} \;:\; x>0 \;\text{~et~}\; \forall
+n\in\mathbb{N}.(x\neq 2^{-n}) \right\}\\
+&=\; \mathbb{R}_{>0} \setminus \{1,\frac{1}{2},\frac{1}{4},\frac{1}{8},\ldots\}\\
+&=\; \mathopen]1;+\infty\mathclose[
+\;\cup\; \mathopen]\frac{1}{2};1\mathclose[
+\;\cup\; \mathopen]\frac{1}{4};\frac{1}{2}\mathclose[
+\;\cup\; \mathopen]\frac{1}{8};\frac{1}{4}\mathclose[
+\;\cup\; \cdots\\
+\end{aligned}
+\]
+(On rappellera brièvement pourquoi $U$ est bien un ouvert.)
+
+Donner la valeur, pour la sémantique des ouverts de $X$, de chaque
+sous-formule de la formule de Scott dans laquelle $A$ a été remplacé
+par $U$, et en déduire pourquoi la formule de Scott n'est pas
+démontrable.  On représentera chaque ensemble graphiquement en plus
+d'expliciter sa valeur avec des symboles.
+
+(Il est recommandé de faire particulièrement au point $0$ et, pour
+éviter les erreurs, de bien s'assurer qu'on a affaire à un ouvert à
+chaque fois.)
+
+\begin{corrige}
+D'abord, $U$ est un ouvert parce que c'est une réunion d'intervalles
+ouverts.
+
+On trouve successivement :
+\begin{itemize}
+\item L'ensemble $\dottedneg U$ est l'ensemble $\mathbb{R}_{<0} =
+  \mathopen]-\infty;0\mathclose[$ des réels strictement négatifs.
+\item L'ensemble $\dottedneg\dottedneg U$ est l'ensemble
+  $\mathbb{R}_{>0} = \mathopen]0;+\infty\mathclose[$ des réels
+    strictement positifs.
+\item L'ensemble $\dottedneg\dottedneg U \dottedlimp U$ est l'ensemble
+  $\{ x\in \mathbb{R} \;:\; x\neq 0 \;\text{~et~}\; \forall
+  n\in\mathbb{N}.(x\neq 2^{-n}) \}$ des réels non nuls qui ne sont pas
+  un $2^{-n}$, ensemble qui est aussi la réunion de $U$ et de
+  $\mathopen]-\infty;0\mathclose[$.  (Le seul point véritablement
+    problématique est $0$, mais il ne peut pas appartenir à l'ouvert
+    car les $2^{-n}$ n'y sont pas, et si un ouvert contient $0$ il
+    doit contenir un intervalle ouvert autour de $0$, donc tous les
+    $2^{-n}$ à partir d'un certain rang.)
+\item L'ensemble $U \dottedlor \dottedneg U$ est le même ensemble
+  $U \cup \mathopen]-\infty;0\mathclose[$ qu'au point précédent.
+\item L'ensemble $(\dottedneg\dottedneg U \dottedlimp U) \dottedlimp
+  (U \dottedlor \dottedneg U)$ est $\mathbb{R}$ tout entier,
+  précisément parce que les deux points précédents donnent le même
+  ouvert.
+\item L'ensemble $\dottedneg\dottedneg U \dottedlor \dottedneg U$ est
+  l'ensemble $\mathopen]-\infty;0\mathclose[ \cup
+    \mathopen]0;+\infty\mathclose[ = \mathbb{R}\setminus\{0\}$ des
+    réels non nuls.
+\item L'ensemble associé à la formule de Scott tout entière est le
+  même ensemble $\mathbb{R}\setminus\{0\}$ qu'au point précédent.
+\end{itemize}
+Comme on a trouvé autre chose que $\mathbb{R}$, par correction de la
+sémantique des ouverts sur $X = \mathbb{R}$, la formule de Scott ne
+peut pas être démontrable en calcul propositionnel intuitionniste.
+\end{corrige}
+
+
+
+%
+%
+%
+
+\exercice
+
 \textbf{Rappels de quelques définitions habituelles.}  On rappelle
 qu'un \textbf{mot binaire [fini]} est une suite finie (éventuellement
 vide, c'est-à-dire de longueur nulle) de $0$ et de $1$.  On notera