Two more exercises on intuitionistic propositional calculus.

1 files changed, 145 insertions, 10 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index d3c885c..44f9c50 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -963,8 +963,7 @@ Autrement dit :
 
 En Python, avec de petites variations :
 
-{\tt
-\noindent
+{\tt\noindent
 def ackermann\_small(m,n,k):\\
 \strut\quad \# Returns A(m,n,k) value if m<=1 or n<=1 or k<=2\\
 \strut\quad if k==0: return m+n\\
@@ -1952,7 +1951,7 @@ A)$.
 
 En Coq, cette preuve s'écrit :
 
-{\tt
+{\tt\noindent
 Parameter A B C : Prop.\\
 Theorem thm : A\textbackslash /B -> ((A->B)->B) /\textbackslash\ ((B->A)->A).\\
 Proof.  intro H.  destruct H.  split.  intro H1.  apply H1.  exact H.
@@ -1993,12 +1992,12 @@ 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.)
+\textbf{(3)} Montrer qu'il revient pourtant 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
@@ -2013,7 +2012,7 @@ $(A \lor \neg A) \Rightarrow (\neg\neg A \Rightarrow A)$. »
 
 En Coq, cette preuve s'écrit :
 
-{\tt
+{\tt\noindent
 Parameter A : Prop.\\
 Theorem thm : (A\textbackslash /\textasciitilde A) -> (\textasciitilde\textasciitilde A->A).\\
 Proof.  intro H.  destruct H.  split.  intro H2.  exact H.
@@ -2214,6 +2213,142 @@ $\neg\neg(P \lor \neg P)$ (sans hypothèse).  Si on postule $\neg\neg Q
 \lor \neg P$ pour conclure $P \lor \neg P$.
 \end{corrige}
 
+%
+
+\exercice\label{exercise-negneg-conjunction}\ (${\star}{\star}$)\par\nobreak
+
+Montrer $\neg\neg A \land \neg\neg B \Rightarrow \neg\neg (A\land B)$
+en calcul propositionnel intuitionniste.  On écrira la preuve très
+soigneusement et on en donnera un $\lambda$-terme.
+
+\begin{corrige}
+Voici une preuve écrite informellement en langage naturel :
+
+Supposons $\neg\neg A\land\neg\neg B$ (donc à la fois $\neg\neg A$ et
+$\neg\neg B$), et on veut montrer $\neg\neg (A\land B)$.  Pour ça,
+supposons $\neg (A\land B)$ et on veut arriver à une contradiction.
+Supposons provisoirement qu'on ait $A$.  Si de plus on a $B$, alors on
+a $A\land B$, ce qui contredit $\neg (A\land B)$ : ceci montre $\neg
+B$ (toujours sous l'hypothèse $A$ !) ; mais commme on a $\neg\neg B$,
+on a une contradiction.  On a donc prouvé $\neg A$ ; mais comme on a
+$\neg\neg A$, on a une contradiction.
+
+La revoici écrite dans le style « drapeau » :
+\bgroup\normalsize
+\begin{footnotesize}
+\begin{flagderiv}[exercise-negneg-conjunction-proof]
+\assume{mainhyp}{\neg\neg A\land\neg\neg B}{}
+\assume{khyp}{\neg (A\land B)}{}
+\step{nna}{\neg\neg A}{$\land$Élim$_1$ sur \ref{mainhyp}}
+\assume{ahyp}{A}{}
+\step{nnb}{\neg\neg B}{$\land$Élim$_2$ sur \ref{mainhyp}}
+\assume{bhyp}{B}{}
+\step{conj}{A\land B}{$\land$Int sur \ref{ahyp}, \ref{bhyp}}
+\step{contrb}{\bot}{$\Rightarrow$Élim sur \ref{khyp} et \ref{conj}}
+\conclude{negb}{\neg B}{$\Rightarrow$Int de \ref{bhyp} dans \ref{contrb}}
+\step{contra}{\bot}{$\Rightarrow$Élim sur \ref{nnb} et \ref{negb}}
+\conclude{nega}{\neg A}{$\Rightarrow$Int de \ref{ahyp} dans \ref{contra}}
+\step{contr}{\bot}{$\Rightarrow$Élim sur \ref{nna} et \ref{nega}}
+\conclude{negk}{\neg\neg (A\land B)}{$\Rightarrow$Int de \ref{khyp} dans \ref{contr}}
+\conclude{mainconc}{\neg\neg A\land\neg\neg B \Rightarrow \neg\neg (A\land B)}{$\Rightarrow$Int de \ref{mainhyp} dans \ref{negk}}
+\end{flagderiv}
+\end{footnotesize}
+\egroup
+
+En Coq, cette preuve s'écrit :
+
+{\tt\noindent
+Parameter A : Prop.  Parameter B : Prop.\\
+Theorem thm : \textasciitilde\textasciitilde A /\textbackslash\ \textasciitilde\textasciitilde B -> \textasciitilde\textasciitilde(A/\textbackslash B).\\
+Proof.  intro H.  intro K.  destruct H as [H1w H2w].
+apply H1w.  intro H1.  apply H2w.  intro H2.
+apply K.  split.  exact H1.  exact H2.  Qed.
+\par}
+
+En voici un $\lambda$-terme de preuve :
+\[
+\lambda(h:\neg\neg
+A\land\neg\neg B). \penalty0\, \lambda(k:\neg(A\land B)). \penalty0\,
+(\pi_1 h) \penalty0 (\lambda(h_1:a). \penalty500\, (\pi_2 h)
+\penalty1000 (\lambda(h_2:B). \penalty1500\, k\langle h_1,
+h_2\rangle))
+\]
+(ou en syntaxe Coq : \texttt{fun (H :
+  \textasciitilde\ \textasciitilde\ A
+  /\textbackslash\ \textasciitilde\ \textasciitilde\ B) (K :
+  \textasciitilde\ (A /\textbackslash\ B)) => match H with conj H1w
+  H2w => H1w (fun H1 : A => H2w (fun H2 : B => K (conj H1 H2))) end} ;
+la forme est un peu différente parce que Coq utilise un \texttt{match}
+pour déstructurer une conjonction alors que nous avons utilisé $\pi_1$
+et $\pi_2$, mais une fois noté que $\pi_1 h$ et $\pi_2 h$
+correspondent à \texttt{H1w} et \texttt{H2w} c'est bien
+essentiellement le même terme).
+\end{corrige}
+
+%
+
+\exercice\ (${\star}{\star}{\star}$)\par\nobreak
+
+Montrer qu'il revient pourtant au même, en calcul propositionnel
+intuitionniste, de postuler $\neg P \lor \neg\neg P$ pour \emph{toute}
+proposition $P$ (« loi faible du tiers exclu »), ou bien de postuler
+$\neg (Q\land R) \Rightarrow \neg Q \lor \neg R$ pour \emph{toutes}
+propositions $Q,R$ (« quatrième loi de De Morgan »).  On pourra
+prendre connaissance de la conclusion de
+l'exercice \ref{exercise-negneg-conjunction}.
+
+Expliquer pourquoi $\neg (A\land B) \Rightarrow \neg A \lor \neg B$
+n'est pas démontrable en calcul propositionnel intuitionniste.
+
+\begin{corrige}
+Montrons d'abord que si on postule $\neg P \lor \neg\neg P$ pour toute
+proposition $P$, on peut en déduire $\neg (Q\land R) \Rightarrow \neg
+Q \lor \neg R$ pour toutes propositions $Q,R$.  Soient donc $Q,R$ deux
+propositions quelconques (ou variables propositionnelles, si on
+préfère), et on veut prouver $\neg (Q\land R) \Rightarrow \neg Q \lor
+\neg R$.  Supposons $\neg (Q\land R)$ et on veut prouver $\neg Q \lor
+\neg R$.  Appliquons notre postulat $\neg P \lor \neg\neg P$ avec $P$
+valant $Q$ puis $R$ successivement : on a $\neg Q \lor \neg\neg Q$ et
+$\neg R \lor \neg\neg R$ ; par la loi d'élimination du $\lor$, ceci
+nous permet de raisonner par cas (dans chaque cas, on cherche à
+prouver $\neg Q \lor \neg R$) : dans le cas où $\neg Q$, ainsi que
+dans le cas où $\neg R$, on a évidemment $\neg Q \lor \neg R$ ; il
+reste donc à traiter le cas où $\neg\neg Q$ et $\neg\neg R$.  Or
+$\neg\neg A \land \neg\neg B \Rightarrow \neg\neg (A\land B)$ est
+démontrable en calcul propositionnel intuitionniste
+(exercice \ref{exercise-negneg-conjunction}).  Donc on peut affirmer
+$\neg\neg (Q\land R)$, ce qui contredit $\neg (Q\land R)$, et une
+contradiction permet de tirer n'importe quelle conclusion, notamment
+$\neg Q \lor \neg R$.  Bref, dans chacun des cas on a bien prouvé
+$\neg Q \lor \neg R$.  On peut maintenant décharger la supposition
+$\neg (Q\land R)$ et affirmer que $\neg (Q\land R) \Rightarrow \neg Q
+\lor \neg R$ comme on voulait.
+
+Réciproquement, montrons que si on postule $\neg (Q\land R)
+\Rightarrow \neg Q \lor \neg R$ pour toutes propositions $Q,R$, on
+peut en déduire $\neg P \lor \neg\neg P$ pour toute proposition $P$.
+Soit donc $P$ une proposition quelconque (ou variable
+propositionnelle, si on préfère), et on veut prouver $\neg P \lor
+\neg\neg P$.  Appliquons notre postulat $\neg (Q\land R) \Rightarrow
+\neg Q \lor \neg R$ avec $Q$ valant $P$ et $R$ valant $\neg P$ : il
+nous donne $\neg (P\land \neg P) \Rightarrow \neg P \lor \neg\neg P$.
+Or $\neg (P\land \neg P)$ est évident (une preuve en est donnée par le
+$\lambda$-terme $\lambda(h:P\land\neg P). \penalty0\, (\pi_2 h)(\pi_1
+h)$), donc on a bien $\neg P \lor \neg\neg P$ comme ou voulait.
+
+Si $\neg (A\land B) \Rightarrow \neg A \lor \neg B$ était démontrable
+en calcul propositionnel intuitionniste, on pourrait remplacer les
+variables propositionnelles $A,B$ par des propositions $Q,R$
+quelconques.  Notamment, d'après ce qu'on vient de voir au paragraphe
+précédent, on pourrait démontrer $\neg P \lor \neg\neg P$ pour $P$ une
+proposition quelconque.  Mais $\neg C \lor \neg\neg C$ n'est
+certainement pas prouvable en calcul propositionnel intuitionniste :
+car s'il l'était, par la propriété de la disjonction, $\neg C$ ou bien
+$\neg\neg C$ le serait, ce qui n'est pas le cas (même classiquement,
+on ne peut pas prouver $\neg C$ seul, ni $\neg\neg C$ seul, qui peut
+prendre l'une ou l'autre valeur de vérité).
+\end{corrige}
+
 
 %
 %