diff options
| -rw-r--r-- | controle-20240126.tex | 145 |
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 |