diff options
| -rw-r--r-- | exercices-inf110.tex | 243 |
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} + % % |