An exercise on semantics.

1 files changed, 145 insertions, 0 deletions

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 52c4e3e..6c40a27 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -113,6 +113,151 @@ Git: \input{vcline.tex}
 
 \exercice
 
+En utilisant l'une quelconque (au choix) 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(\neg(A\land B) \land \neg(B\land C) \land \neg(C\land A)\big)
+\;\Rightarrow\; \big(\neg A \lor \neg B \lor \neg C\big)
+\]
+
+(\emph{Indications :} si on préfère la sémantique de Kripke,
+considérer un monde permettant d'accéder à trois autres mondes, tous
+les trois inaccessibles depuis les uns les autres ; si on préfère la
+sémantique des ouverts, considérer trois secteurs angulaires ouverts
+dans le plan, ayant un même sommet et qui se jouxtent sans
+s'intersecter ; si on préfère la sémantique de la réalisabilité ou des
+problèmes finis, énoncer le fait qu'il est impossible de trouver une
+partie vide parmi trois, sans avoir accès à ces parties, même si on a
+la promesse qu'au moins deux d'entre elles sont vides ; pour la
+sémantique des problèmes finis, on prendra par ailleurs trois
+problèmes ayant un seul candidat chacun.)
+
+\begin{corrige}
+On donne quatre solutions possibles, une pour chaque sémantique vue en
+cours.
+
+\emph{Sémantique de Kripke :} On considère le cadre de Kripke
+suivant :
+\begin{center}
+\begin{tikzpicture}[>=stealth']
+\node (t) at (0bp,0bp) {$t$};
+\node (u) at (35bp,30bp) {$u$};
+\node (v) at (35bp,0bp) {$v$};
+\node (w) at (35bp,-30bp) {$w$};
+\draw[->] (t)--(u);
+\draw[->] (t)--(v);
+\draw[->] (t)--(w);
+\end{tikzpicture}
+\end{center}
+Soient $p$ (resp. $q$, resp. $r$) l'affectation de vérité qui vaut $1$
+en $u$ (resp. $v$, resp. $w$) et $0$ partout ailleurs.  Alors chacun
+de $p\dottedland q$, $q\dottedland r$ et $r\dottedland p$ est
+identiquement $0$ donc $\dottedneg(p\dottedland q) \dottedland
+\dottedneg(q\dottedland r) \dottedland \dottedneg(r\dottedland p)$ est
+identiquement $1$.  En revanche, $\dottedneg p$ vaut $1$ dans les
+mondes $v$ et $w$ et $0$ dans les mondes $t$ et $u$, et de façon
+analogue pour $\dottedneg q$ et $\dottedneg r$ avec la permutation
+cyclique évidente.  Donc $\dottedneg p \dottedlor \dottedneg q
+\dottedlor \dottedneg r$ vaut $0$ dans le monde $t$ et $1$ dans les
+trois mondes $u,v,w$.  Par conséquent, il en va de même de
+$(\dottedneg(p\dottedland q) \dottedland \dottedneg(q\dottedland r)
+\dottedland \dottedneg(r\dottedland p)) \dottedlimp (\dottedneg p
+\dottedlor \dottedneg q \dottedlor \dottedneg r)$.  Si la formule
+proposée avait été démontrable, on aurait trouvé constamment $1$ (par
+\emph{correction} de la sémantique de Kripke) : ce n'est pas le cas,
+donc la formule n'est pas démontrable.
+
+\emph{Sémantique des ouverts :} Considérons dans $\mathbb{R}^2$ trois
+secteurs angulaires ouverts $U,V,W$, chacun ayant l'origine comme
+sommet et d'angle $\frac{2\pi}{3}$, et qui se jouxtent par une
+droite : par exemple, soit $U$ le secteur formé des nombres complexes
+non nuls dont l'argument (choisi entre $0$ et $2\pi$) est strictement
+compris entre $0$ et $\frac{2\pi}{3}$, soit $V$ celui dont l'argument
+est strictement compris entre $\frac{2\pi}{3}$ et $\frac{4\pi}{3}$ et
+soit $W$ celui dont l'argument est strictement compris entre
+$\frac{4\pi}{3}$ et $2\pi$.  Avec ces choix, les trois secteurs sont
+disjoints, donc chacun de $U\dottedland V$, $V\dottedland W$ et
+$W\dottedland U$ est vide donc $\dottedneg(U\dottedland V) \dottedland
+\dottedneg(V\dottedland W) \dottedland \dottedneg(W\dottedland U)$ est
+plein.  En revanche, $\dottedneg U$, $\dottedneg V$ et $\dottedneg W$
+sont des secteurs ouverts ayant l'origine pour sommet et d'angle
+$\frac{4\pi}{3}$ (par exemple, $\dottedneg U$ est l'intérieur de
+l'adhérence de $V\cup W$, et symétriquement pour les autres), donc
+aucun ne contient l'origine, donc $\dottedneg U \dottedlor \dottedneg
+V \dottedlor \dottedneg W$ non plus : c'est même précisément le
+complémentaire de l'origine.  Par conséquent,
+$(\dottedneg(U\dottedland V) \dottedland \dottedneg(V\dottedland W)
+\dottedland \dottedneg(W\dottedland U)) \dottedlimp (\dottedneg U
+\dottedlor \dottedneg V \dottedlor \dottedneg W)$ est aussi le
+complémentaire de l'origine.  Si la formule proposée avait été
+démontrable, on aurait trouvé tout $\mathbb{R}^2$ (par
+\emph{correction} de la sémantique des ouverts) : ce n'est pas le cas,
+donc la formule n'est pas démontrable.
+
+\emph{Sémantique de la réalisabilité :} Supposons qu'il existe un
+\emph{même} programme $e$ qui réalise la formule qu'on considère
+quelles que soient les parties $P,Q,R \subseteq \mathbb{N}$ mises à la
+place des variables propositionnelles $A,B,C$.  Notons que (au moins)
+deux des trois parties $P,Q,R$ sont vides, alors
+$\dottedneg(P\dottedland Q)$, $\dottedneg(Q\dottedland R)$ et
+$\dottedneg(R\dottedland P)$ sont égales à $\mathbb{N}$, donc $\langle
+0,0,0\rangle$ est dans $\dottedneg(P\dottedland Q) \dottedland
+\dottedneg(Q\dottedland R) \dottedland \dottedneg(R\dottedland P)$.
+Considérons $\varphi_e(\langle 0,0,0\rangle)$ : il est bien défini
+(car il existe des parties $P,Q,R$ comme on l'a dit) et doit
+appartenir à $\dottedneg P \dottedlor \dottedneg Q \dottedlor
+\dottedneg R$, c'est-à-dire qu'il doit indiquer une partie vide parmi
+$P,Q,R$.  Mais ce n'est pas possible sans aucune information sur les
+parties !  Pour être tout à fait précis, supposons (sans perte de
+généralité, puisque le problème est symétrique) qu'il renvoie un
+élément de $\dottedneg P$ : alors en considérant le cas $P =
+\mathbb{N}$ et $Q = \varnothing$ et $R = \varnothing$ on a une
+contradiction.  Or si la formule proposée avait été démontrable, il
+existerait un $e$ qui la réalise quelles que soient les parties (par
+\emph{correction} de la sémantique des la réalisabilité) : on vient de
+voir que ce n'est pas le cas, donc la formule n'est pas démontrable.
+
+\emph{Sémantique des problèmes finis :} Considérons trois problèmes
+dont l'ensemble des candidats est un singleton, appelons-les $E :=
+(\{\bullet_p\}, P)$, $F := (\{\bullet_q\}, Q)$ et $G :=
+(\{\bullet_r\}, R)$ où chacun des ensembles de solutions $P,Q,R$ est
+soit vide soit le singleton écrit juste avant.  Alors l'ensemble des
+candidats de $\dottedneg(E\dottedland F) \dottedland
+\dottedneg(F\dottedland G) \dottedland \dottedneg(G\dottedland E)$ est
+un singleton, appelons-le $\{\bullet_0\}$, et ce singleton est
+solution lorsque (au moins) deux des trois parties $P,Q,R$ sont vides.
+L'ensemble des candidats de chacun de $\dottedneg E$, $\dottedneg F$,
+$\dottedneg G$ est un singleton, disons $\{\bullet_{p'}\}$,
+$\{\bullet_{q'}\}$, $\{\bullet_{r'}\}$ respectivement, donc celui de
+$\dottedneg E \dottedlor \dottedneg F \dottedlor \dottedneg G$ est
+$\{\bullet_{p'}, \bullet_{q'}, \bullet_{r'}\}$.  Supposons qu'il
+existe un \emph{même} candidat $f$ qui soit solution du problème
+$(\dottedneg(E\dottedland F) \dottedland \dottedneg(F\dottedland G)
+\dottedland \dottedneg(G\dottedland E)) \dottedlimp (\dottedneg E
+\dottedlor \dottedneg F \dottedlor \dottedneg G)$.  C'est une fonction
+censée envoyer $\bullet_0$, s'il est solution, sur une solution du
+problème $\dottedneg E \dottedlor \dottedneg F \dottedlor \dottedneg
+G$, c'est-à-dire qu'il doit indiquer une partie vide parmi $P,Q,R$.
+Mais ce n'est pas possible sans aucune information sur les parties !
+Pour être tout à fait précis, supposons (sans perte de généralité,
+puisque le problème est symétrique) qu'il renvoie $\bullet_{p'}$ :
+alors en considérant le cas $P = \{\bullet_p\}$ et $Q = \varnothing$
+et $R = \varnothing$ on a une contradiction.  Or si la formule
+proposée avait été démontrable, il existerait un $f$ qui soit solution
+quels que soient $P,Q,R$ (par \emph{correction} de la sémantique des
+la réalisabilité) : on vient de voir que ce n'est pas le cas, donc la
+formule n'est pas démontrable.
+\end{corrige}
+
+
+%
+%
+%
+
+\exercice
+
 \textbf{Motivations :} On s'intéresse dans cet exercice à la notion de
 \emph{réel calculable}, qu'on va définir comme une formalisation
 possible d'un nombre réel exact pouvant être manipulé par un