Exercise on comparison of double-negation elimination and excluded middle.

1 files changed, 243 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 6b1f15b..10a5e8b 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -30,6 +30,12 @@
 %
 \newcommand{\dbllangle}{\mathopen{\langle\!\langle}}
 \newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}}
+\newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}}
+\newcommand{\dottedland}{\mathbin{\dot\land}}
+\newcommand{\dottedlor}{\mathbin{\dot\lor}}
+\newcommand{\dottedtop}{\mathord{\dot\top}}
+\newcommand{\dottedbot}{\mathord{\dot\bot}}
+\newcommand{\dottedneg}{\mathop{\dot\neg}}
 %
 \DeclareUnicodeCharacter{00A0}{~}
 %
@@ -1814,6 +1820,7 @@ $\neg\neg A\Rightarrow\neg\neg B$ et $A\Rightarrow\neg\neg B$ sont
 tous les trois équivalents (en logique intuitionniste).
 \end{corrige}
 
+%
 
 \exercice\ (${\star}{\star}{\star}$)\par\nobreak
 
@@ -1856,6 +1863,7 @@ terme de type $(A\land B \Rightarrow C) \Rightarrow D$ (où on rappelle
 $D = (A\Rightarrow C) \lor (B\Rightarrow C)$).
 \end{corrige}
 
+%
 
 \exercice\ (${\star}$)\par\nobreak
 
@@ -1886,6 +1894,7 @@ prouvables classiquement (leur tableau de vérité n'est pas entièrement
 vrai).
 \end{corrige}
 
+%
 
 \exercice\ (${\star}$)\par\nobreak
 
@@ -1970,6 +1979,240 @@ preuve en question :
  end)})
 \end{corrige}
 
+%
+
+\exercice\ (${\star}{\star}$)\par\nobreak
+
+\textbf{(1)} Montrer en calcul propositionnel intuitionniste que $(A
+\lor \neg A) \Rightarrow (\neg\neg A \Rightarrow A)$.
+
+\textbf{(2)} Montrer que $(\neg\neg A \Rightarrow A) \Rightarrow (A
+\lor \neg A)$ n'est pas démontrable en calcul propositionnel
+intuitionniste.  \textit{(Cette question est sans doute plus facile à
+  traiter en utilisant l'une quelconque des sémantiques vues en cours
+  pour le calcul propositionnel intuitionniste.)}
+
+\textbf{(3)} Montrer qu'il revient au même, en calcul propositionnel
+intuitionniste, de postuler $P \lor \neg P$ pour \emph{toute}
+proposition $P$, ou bien de postuler $\neg\neg Q \Rightarrow Q$ pour
+\emph{toute} proposition $Q$.  (Pour le sens qui ne découle pas
+immédiatement de (1), on pourra démontrer la proposition $\neg\neg (P
+\lor \neg P)$ sans hypothèse.)
+
+\begin{corrige}
+\textbf{(1)} Voici une démonstration écrite en informellement en
+langage naturel : « Supposons $A \lor \neg A$, et on veut montrer
+$\neg\neg A \Rightarrow A)$.  Considérons d'abord le cas $A$ : alors
+certainement $\neg\neg A \Rightarrow A$.  Considérons maintenant le
+cas $\neg A$ : alors $\neg\neg A$ aboutit à une contradiction, d'où on
+peut tirer n'importe quelle conclusion et notamment $A$, bref,
+$\neg\neg A \Rightarrow A$ dans ce cas aussi.  Dans les deux cas de la
+disjonction on a montré $\neg\neg A \Rightarrow A$.  Donc finalement
+$(A \lor \neg A) \Rightarrow (\neg\neg A \Rightarrow A)$. »
+
+En Coq, cette preuve s'écrit :
+
+{\tt
+Parameter A : Prop.\\
+Theorem thm : (A\textbackslash /\textasciitilde A) -> (\textasciitilde\textasciitilde A->A).\\
+Proof.  intro H.  destruct H.  split.  intro H2.  exact H.
+intro H2.  exfalso.  apply H2.  exact H.  Qed.
+\par}
+
+Revoici la même démonstration écrite comme un $\lambda$-terme :
+\[
+\begin{aligned}
+\lambda(h:A\lor \neg A).\,
+(\texttt{match~}h\texttt{~with~}&\iota_1 h_0
+\mapsto \lambda(h_2:\neg\neg A).\,h_0,\\
+&\iota_2 h_1
+\mapsto \lambda(h_2:\neg\neg A).\,\texttt{exfalso}^{(A)}(h_2 h_1))
+\end{aligned}
+\]
+(ou en syntaxe Coq : \texttt{(fun H : A \textbackslash/ \textasciitilde\ A =>
+ match H with
+  or\_introl H0 => fun H2 : \textasciitilde\ \textasciitilde\ A => H0
+| or\_intror H1 => fun H2 : \textasciitilde\ \textasciitilde\ A => False\_ind A (H2 H1)
+ end)})
+
+\textbf{(2)} Pour prouver l'indémontrabitilité en calcul
+propositionnel intuitionniste de $(\neg\neg A \Rightarrow A)
+\Rightarrow (A \lor \neg A)$, on peut utiliser soit une approche
+sémantique, soit une approche syntaxique.  On va expliciter ces
+différentes approches.
+
+Commençons par l'approche sémantique.  Montrons ce résultat avec
+chacune des sémantiques vues en cours (n'importe laquelle suffit à
+établir le résultat !).
+
+Une preuve a été donnée en cours basée sur la sémantique des ouverts :
+si $U$ désigne l'ouvert $\mathopen{]}0,1\mathclose{[}$ dans $X =
+    \mathbb{R}$, alors $\dottedneg U =
+    \mathopen{]}-\infty,0\mathclose{[} \cup
+    \mathopen{]}1,+\infty\mathclose{[}$ donc $\dottedneg\dottedneg U =
+    \mathopen{]}0,1\mathclose{[} = U$ donc $(\dottedneg\dottedneg U
+    \dottedlimp U) = \mathbb{R}$ tandis que $(U \dottedlor \dottedneg
+    U) = \mathbb{R}\setminus\{0,1\}$, donc finalement
+    $((\dottedneg\dottedneg U \dottedlimp U) \dottedlimp (U \dottedlor
+    \dottedneg U)) = \mathbb{R}\setminus\{0,1\}$ ; or si $(\neg\neg A
+    \Rightarrow A) \Rightarrow (A \lor \neg A)$ était démontrable en
+    calcul propositionnel intuitionniste, on trouverait $X$ tout
+    entier quel que soit l'ouvert $U$ utilisé pour $A$ (par
+    \emph{correction} de la sémantique des ouverts).  Comme ce n'est
+    pas le cas, c'est que la proposition en question n'est pas
+    démontrable.
+
+Une autre preuve est fournie par le cadre de Kripke à trois mondes
+$\{u,v,w\}$ avec $u\leq v$ et $u\leq w$ (imaginer $v,w$ comme deux
+futurs possibles de $u$) et $p$ l'affectation de vérité $(u \mapsto 0,
+v\mapsto 0, w\mapsto 1)$ (imaginer une vérité encore indécidée et qui
+pourrait devenir fausse ou vraie), si bien que $\dottedneg p$ est
+l'affectation de vérité $(u \mapsto 0, v\mapsto 1, w\mapsto 0)$, donc
+$\dottedneg\dottedneg p$ est l'affectation de vérité $(u \mapsto 0,
+v\mapsto 0, w\mapsto 1)$ qui est la même que $p$ et
+$(\dottedneg\dottedneg p \dottedlimp p)$ est l'affectation de vérité
+constante $1$ (i.e., $\dottedtop$) ; en revanche, $(p \dottedlor
+\dottedneg p)$ est l'affectation de vérité $(u \mapsto 0, v\mapsto 1,
+w\mapsto 1)$, et $((\dottedneg\dottedneg p \dottedlimp p) \dottedlimp
+(p \dottedlor \dottedneg p))$ est également l'affectation de vérité
+$(u \mapsto 0, v\mapsto 1, w\mapsto 1)$.  Or si $(\neg\neg A
+\Rightarrow A) \Rightarrow (A \lor \neg A)$ était démontrable en
+calcul propositionnel intuitionniste, on trouverait constamment $1$
+quelle que soit l'affectation $p$ utilisé pour $A$ (par
+\emph{correction} de la sémantique des ouverts).  Comme ce n'est pas
+le cas, c'est que la proposition en question n'est pas démontrable.
+
+Une autre preuve est fournie par la sémantique de la réalisabilité
+propositionnelle : dans cette sémantique si $P$ est une partie
+quelconque de $\mathbb{N}$, alors $\dottedneg P$ est $\mathbb{N}$ si
+$P$ est vide et $\varnothing$ sinon, et $\dottedneg\dottedneg P$ est
+$\varnothing$ si $P$ est vide et $\mathbb{N}$ sinon.  Ainsi,
+$\dottedneg\dottedneg P \dottedlimp P$ est l'ensemble des programmes
+qui prennent un entier naturel quelconque en entrée et doivent
+renvoyer \emph{un élément de $P$ s'il y en a un}.  Par contraste, $P
+\dottedlor \dottedneg P$ est l'ensemble des couples $\langle
+0,n\rangle$ avec $n\in P$ ou bien de la forme $\langle 1,n\rangle$
+avec $n$ quelconque si $P=\varnothing$.  Un élément hypothétique de
+$((\dottedneg\dottedneg P \dottedlimp P) \dottedlimp (P \dottedlor
+\dottedneg P))$ pour tous les $P$ à la fois serait un programme qui
+prend en entrée un élément de $\dottedneg\dottedneg P \dottedlimp P$
+et renvoie un élément de $P \dottedlor \dottedneg P$.  Or pour $P =
+\varnothing$ (pour lequel $\dottedneg\dottedneg P \dottedlimp P$ vaut
+$\mathbb{N}$), ce programme doit renvoyer un couple de la forme
+$\langle 1,n\rangle$ quelle que soit son entrée ; mais pour $P =
+\varnothing$, ce même programme doit renvoyer un couple de la forme
+$\langle 0,n\rangle$ quand on lui passe un élément de
+$\dottedneg\dottedneg P \dottedlimp P$ (qui est l'ensemble des
+programmes qui terminent, et en tout cas n'est pas vide) : ceci est
+contradictoire.  Or si $(\neg\neg A \Rightarrow A) \Rightarrow (A \lor
+\neg A)$ était démontrable en calcul propositionnel intuitionniste, il
+devrait exister un programme appartenant à $((\dottedneg\dottedneg P
+\dottedlimp P) \dottedlimp (P \dottedlor \dottedneg P))$ pour tous
+les $P$ (par \emph{correction} de la sémantique de la réalisabilité
+propositionnelle).  Comme ce n'est pas le cas, c'est que la
+proposition en question n'est pas démontrable.
+
+Une quatrième preuve est fournie par la sémantique des problèmes finis
+de Medvedev : considérons les deux problèmes
+$(\{\bullet\},\{\bullet\})$ et $(\{\bullet\},\varnothing)$ (qui ont le
+même ensemble de candidats, et qui sont échangés par $\dottedneg$).
+Sur le premier, $\dottedneg\dottedneg P \dottedlimp P$ vaut
+$(\{\bullet\},\{\bullet\})$ (où on note abusivement $\bullet$ pour
+l'unique fonction $\{\bullet\} \to \{\bullet\}$) tandis que $P
+\dottedlor \dottedneg P$ vaut $(\{\bullet_1,\bullet_2\},
+\{\bullet_1\})$, donc $((\dottedneg\dottedneg P \dottedlimp P)
+\dottedlimp (P \dottedlor \dottedneg P))$ vaut
+$(\{\bullet_1,\bullet_2\}, \{\bullet_1\})$ (où on note abusivement
+$\bullet_i$ pour l'unique fonction $\{\bullet\} \to
+\{\bullet_1,\bullet_2\}$ envoyant $\bullet$ sur $\bullet_i$).  Sur le
+second problème, $\dottedneg\dottedneg P \dottedlimp P$ vaut
+$(\{\bullet\},\{\bullet\})$ tandis que $P \dottedlor \dottedneg P$
+vaut $(\{\bullet_1,\bullet_2\}, \{\bullet_2\})$, donc
+$((\dottedneg\dottedneg P \dottedlimp P) \dottedlimp (P \dottedlor
+\dottedneg P))$ vaut $(\{\bullet_1,\bullet_2\}, \{\bullet_2\})$.  Ces
+deux ensembles de solutions sont disjoints, donc il n'y a pas de
+solution commune.  Or si $(\neg\neg A \Rightarrow A) \Rightarrow (A
+\lor \neg A)$ était démontrable en calcul propositionnel
+intuitionniste, il devrait exister une solution appartenant à
+$((\dottedneg\dottedneg P \dottedlimp P) \dottedlimp (P \dottedlor
+\dottedneg P))$ pour tous les $P$ ayant un même ensemble de candidats
+(par \emph{correction} de la sémantique de la sémantique de Medvedev).
+Comme ce n'est pas le cas, c'est que la proposition en question n'est
+pas démontrable.
+
+Outre ces quatre preuves sémantiques, on peut aussi prouver
+l'idémontrabilité de $(\neg\neg A \Rightarrow A) \Rightarrow (A \lor
+\neg A)$ en calcul propositionnel intuitionniste de façon syntaxique,
+par la recherche d'une démonstration sans coupure, comme suit.
+
+Puisque $\vdash (\neg\neg A \Rightarrow A) \Rightarrow (A \lor \neg
+A)$ si et seulement si $\neg\neg A \Rightarrow A \vdash A \lor \neg A$
+(par les règles d'introduction et d'élimination du $\Rightarrow$ en
+déduction naturelle), il suffit de montrer qu'on n'a pas $\neg\neg A
+\Rightarrow A \vdash A \lor \neg A$.  Par l'existence d'une
+démonstration sans coupure (ou plus précisément, la propriété de la
+sous-formule), si on avait ce séquent, il y en aurait une
+démonstration dans laquelle toute formule qui apparaît est l'une des
+six suivantes : $\bot, A, \neg A, \neg\neg A, A\lor\neg A, \neg\neg A
+\Rightarrow A$.  Il s'agit donc de considérer tous les séquents ayant
+un sous-ensemble de ces six formules comme hypothèses et une de ces
+six formules comme conclusion : cela fait $2^6\times 6 = 384$
+possibilités, un peu fastidieux à lister complètement à la main, mais
+on peut se simplifier la tâcher en considérant les ensembles suivants
+(tous facilement démontrables) :
+\begin{itemize}
+\item ceux ayant la conclusion parmi les hypothèses,
+\item ceux ayant $\bot$ dans les hypothèses, ou bien à la fois $A$ et
+  $\neg A$, ou bien à la fois $\neg A$ et $\neg\neg A$, et une
+  conclusion quelconque,
+\item $\Gamma, A \vdash \neg\neg A$ (où $\Gamma$ est quelconque),
+\item $\Gamma, \neg\neg A, (A\lor\neg A) \vdash A$,
+\item $\Gamma, \neg\neg A, (\neg\neg A \Rightarrow A) \vdash A$,
+\item $\Gamma, A \vdash (A\lor\neg A)$,
+\item $\Gamma, \neg A \vdash (A\lor\neg A)$.
+\item $\Gamma, \neg\neg A, (\neg\neg A \Rightarrow A) \vdash A\lor\neg
+  A$,
+\item $\Gamma, A \vdash (\neg\neg A \Rightarrow A)$.
+\item $\Gamma, \neg A \vdash (\neg\neg A \Rightarrow A)$.
+\end{itemize}
+On peut ensuite se convaincre en examinant chaque règle de la logique
+(en calcul des séquents) qu'aucune application d'aucune règle à un de
+ces séquents ne donne de séquent nouveau (parmi ceux dont les
+hypothèses et la conclusion sont dans les six formules listées !).
+Les séquents qu'on vient de lister sont donc exactement tous les
+séquents valables dont les hypothèses et la conclusion sont dans les
+six formules listées.  Comme $\neg\neg A \Rightarrow A \vdash A \lor
+\neg A$ n'en fait pas partie, il n'est pas valable, pas plus que
+$\vdash (\neg\neg A \Rightarrow A) \Rightarrow (A \lor \neg A)$.
+
+(Cett approche syntaxique est nettement plus pénible que les approches
+sémantiques qu'on a vues.  Elle a cependant l'avantage de relever d'un
+algorithme systématique.)
+
+\textbf{(3)} Observons d'abord que si on postule $P \lor \neg P$ pour
+toute proposition $P$, alors on peut en déduire $\neg\neg Q
+\Rightarrow Q$ pour toute proposition $Q$ : ce sens-là est évident,
+car $\neg\neg Q \Rightarrow Q$ découle de $Q \lor \neg Q$ comme
+expliqué dans la question (1) (et en utilisant implicitement le fait
+qu'on peut substituer une proposition quelconque à une variable
+propositionnelle).
+
+Reste à traiter l'autre sens, i.e., montrer que si on postule
+$\neg\neg Q \Rightarrow Q$ pour toute proposition $Q$, alors on peut
+en déduire $P \lor \neg P$ pour toute proposition $P$.  Soit donc $P$
+une proposition quelconque (ou une variable propositionnelle, si on
+préfère).  Or $\neg(P \lor \neg P)$ équivaut à $\neg P \land \neg\neg
+P$ (ceci est une application de la tautologie $((A\lor B)\Rightarrow
+C) \Leftrightarrow (A\Rightarrow C) \land (B\Rightarrow C)$ en
+remplaçant $A$ par $P$, $B$ par $\neg P$ et $C$ par $\bot$) ; mais
+clairement $\neg P \land \neg\neg P$ implique $\bot$ (ceci est une
+application de la tautologie $A \land (A\Rightarrow B) \Rightarrow B$
+en remplaçant $A$ par $\neg P$ et $B$ par $\bot$) : donc on a montré
+$\neg\neg(P \lor \neg P)$ (sans hypothèse).  Si on postule $\neg\neg Q
+\Rightarrow Q$, il n'y a qu'à appliquer ce fait avec $Q$ valant $P
+\lor \neg P$ pour conclure $P \lor \neg P$.
+\end{corrige}
+
 
 %
 %