Add an exercise on the semantics of the propositional calculus.

1 files changed, 93 insertions, 0 deletions

diff --git a/controle-20250129.tex b/controle-20250129.tex
index 74b2d52..b78c71c 100644
--- a/controle-20250129.tex
+++ b/controle-20250129.tex
@@ -485,6 +485,99 @@ Qed.
 %
 %
 
+\exercice
+
+En utilisant une des sémantiques vues en cours pour le calcul
+propositionnel intuitionniste, montrer que la formule suivante n'est
+pas démontrable en calcul propositionnel intuitionniste :
+\[
+\big(((A\Rightarrow B)\Rightarrow B) \land ((B\Rightarrow A)\Rightarrow A)\big)
+\; \Rightarrow \;
+(A\lor B)
+\]
+
+(\emph{Indications :} Si on souhaite utiliser la sémantique des
+ouverts, on pourra utiliser deux demi-droites de même origine dans la
+droite réelle.  Si on souhaite utiliser la sémantique de Kripke, on
+pourra prendre le cadre $\{u,v,w\}$ avec l'ordre engendré par les
+seules relations $u\leq v$ et $u\leq w$, et considérer les
+affectations de vérité valant $1$ uniquement dans le monde $v$
+respectivement $w$.  Si on souhaite utiliser la sémantique de la
+réalisabilité propositionnelle, on remarquera qu'un programme $e$ qui
+réalise cette formule pour $A=\mathbb{N}$ et $B=\varnothing$ doit
+renvoyer un élément de la forme $\langle 0,\emdash\rangle$ si on
+l'applique à $\langle c,c\rangle$ avec $c$ le code de Gödel d'une
+fonction constante quelconque, et que pour $A=\varnothing$ et
+$B=\mathbb{N}$ il doit renvoyer $\langle 1,\emdash\rangle$.)
+
+La formule en question est-elle démontrable en calcul propositionnel
+classique ?  (On ne demande pas forcément d'en exhiber une
+démonstration.)
+
+\begin{corrige}
+\emph{Avec la sémantique des ouverts :} Travaillons sur les ouverts de
+$X = \mathbb{R}$.  Posons $U = \{t\in\mathbb{R} : t<0\}$ et $V =
+\{t\in\mathbb{R} : t>0\}$.  Ce sont bien des ouverts.  Alors
+$(U\dottedlimp V) = V$ donc $((U\dottedlimp V)\dottedlimp V) =
+\mathbb{R}$.  Symétriquement, $((V\dottedlimp U)\dottedlimp U) =
+\mathbb{R}$.  En revanche, $U\dottedlor V = \mathbb{R}\setminus\{0\}$.
+On en déduit pour la formule tout entière que $\big(((U\dottedlimp
+V)\dottedlimp V) \land ((V\dottedlimp U)\dottedlimp U)\big) \;
+\dottedlimp \; (U\lor B)$ vaut $\mathbb{R}\setminus\{0\}$ : comme ceci
+n'est pas $X$ tout entier, la formule n'est pas prouvable (par
+correction de la sémantique des ouverts de $X$).
+
+\emph{Avec la sémantique de Kripke :} Travaillons dans le cadre de
+Kripke $\{u,v,w\}$ avec pour seules relations non-triviales $u\leq v$
+et $u\leq w$.  Soit $p$ l'affectation de vérité valant $1$ en $v$ et
+$0$ partout ailleurs, et $q$ celle valant $1$ en $w$ et $0$ partout
+ailleurs.  Ce sont bien des affectations de vérité (c'est-à-dire ici
+que si elles valent $1$ en $u$, ce qui ne se produit jamais, elles
+valent $1$ partout).  On vérifie alors que $(p\dottedlimp q) = q$ donc
+$((p\dottedlimp q)\dottedlimp q) = 1$.  Symétriquement,
+$((q\dottedlimp p)\dottedlimp p) = 1$.  En revanche, $p\dottedlor q$
+vaut $1$ en $v$ et $w$ mais $0$ en $u$.  On en déduit pour la formule
+tout entière que $\big(((p\dottedlimp q)\dottedlimp q) \land
+((q\dottedlimp p)\dottedlimp p)\big) \; \dottedlimp \; (p\lor q)$ vaut
+$1$ en $v$ et $w$ mais $0$ en $u$ : comme ceci n'est pas $1$ partout,
+la formule n'est pas prouvable (par correction de la sémantique de
+Kripke).
+
+\emph{Avec la sémantique de la réalisabilité propositionnelle :}
+Supposons que $e$ réalise la formule.  Si $A = \mathbb{N}$ et $B =
+\varnothing$, alors $(A \dottedlimp B) = \varnothing$ donc $((A
+\dottedlimp B) \dottedlimp B) = \mathbb{N}$, et $(B \dottedlimp A) =
+\mathbb{N}$ donc $((A \dottedlimp B) \dottedlimp B) = \mathbb{N}
+\dottedlimp \mathbb{N}$ est l'ensemble des codes de Gödel des
+fonctions récursives totales $\mathbb{N}\to\mathbb{N}$.  Fixons $c$ un
+tel code de Gödel, disons celui du programme qui renvoie
+immédiatement $0$.  Alors $\langle c,c\rangle$ est dans $((A
+\dottedlimp B) \dottedlimp B) \dottedland ((A \dottedlimp B)
+\dottedlimp B)$, donc $\varphi_e(\langle c,c\rangle)$ doit être dans
+$A\dottedlor B$, et comme $B$ est vide, il est forcément de la forme
+$\langle 0,m\rangle$ avec $m\in A$.  Mais exactement le même
+raisonnement en échangeant $A$ et $B$ (qui ont un rôle symétrique)
+montre que si $A = \varnothing$ et $B = \mathbb{N}$ alors
+$\varphi_e(\langle c,c\rangle)$ doit être dans $A\dottedlor B$ et
+cette fois de la forme $\langle 1,n\rangle$ avec $n\in B$.  Comme
+$\varphi_e(\langle c,c\rangle)$ ne peut pas être à la fois de la forme
+$\langle 0,\emdash\rangle$ et $\langle 1,\emdash\rangle$, c'est que la
+formule n'est pas réalisable.  En particulier, elle n'est pas
+prouvable (par correction de la sémantique de la rélisabilité
+propositionnelle).
+
+Enfin, concernant la formule en logique classique, un simple tableau
+de vérité montre qu'elle est vraie dans chacun des quatre cas de
+figure, donc la formule est classiquement prouvable (par complétude de
+la sémantique booléenne pour la logique classique).
+\end{corrige}
+
+
+
+%
+%
+%
+
 %% \bigbreak
 %% \hbox to\hsize{\hrulefill}
 %% \smallskip