From 56663f84db4f3b78c8afb93c8742b573822485d5 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 16 Dec 2023 20:35:31 +0100
Subject: More exercises in intiotionistic propositional logic.

---
 exercices-inf110.tex | 88 +++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 87 insertions(+), 1 deletion(-)

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 3e988db..70cce79 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -15,6 +15,7 @@
 \usepackage{mathrsfs}
 \usepackage{wasysym}
 \usepackage{url}
+\usepackage{flagderiv}
 %
 \usepackage{graphics}
 \usepackage[usenames,dvipsnames]{xcolor}
@@ -1708,7 +1709,7 @@ la portée de définition de la fonction dans un langage fonctionnel.
 %
 %
 
-\section{Correspondance de Curry-Howard}
+\section{Correspondance de Curry-Howard et calcul propositionnel intuitionniste}
 
 
 \exercice\ (${\star}{\star}$)\par\nobreak
@@ -1856,6 +1857,91 @@ $D = (A\Rightarrow C) \lor (B\Rightarrow C)$).
 \end{corrige}
 
 
+\exercice\ (${\star}$)\par\nobreak
+
+Montrer que la formule (de Gödel-Dummett)
+\[
+(A\Rightarrow B) \lor (B\Rightarrow A)
+\]
+est prouvable en calcul propositionnel classique et \emph{n'est pas}
+prouvable en calcul propositionnel intuitionniste.
+
+\begin{corrige}
+Elle est prouvable en logique classique comme on le voit en
+considérant son tableau de vérité : le seul cas où $A\Rightarrow B$
+est faux est celui où $A$ est vrai et $B$ est faux, et le seul cas où
+$B\Rightarrow A$ est faux est celui où $B$ est vrai et $A$ est faux :
+on ne peut donc pas être dans ces deux cas à la fois.  (Si on préfère,
+$A\Rightarrow B$ équivaut classiquement à $\neg A \lor B$, et
+$B\Rightarrow A$ équivaut classiquement à $A \lor \neg B$, donc la
+disjonction des deux équivaut classiquement à $\neg A \lor B \lor A
+\lor \neg B$, qui est classiquement vrai.)
+
+Elle n'est pas prouvable en logique intuitionniste à cause de la
+propriété de la disjonction : si on avait $\vdash (A\Rightarrow B)
+\lor (B\Rightarrow A)$, on aurait $\vdash A\Rightarrow B$ ou bien
+$\vdash B\Rightarrow A$ ; mais ni $A\Rightarrow B$ ni $B\Rightarrow A$
+seul n'est prouvable intuitionnistement car elles ne sont même pas
+prouvables classiquement (leur tableau de vérité n'est pas entièrement
+vrai).
+\end{corrige}
+
+
+\exercice\ (${\star}$)\par\nobreak
+
+Montrer en calcul propositionnel intuitionniste que
+\[
+A\lor B \Rightarrow ((A\Rightarrow B) \Rightarrow B) \land
+((B\Rightarrow A) \Rightarrow A)
+\]
+
+\begin{corrige}
+Voici une preuve complète écrite dans le style « drapeau » :
+\bgroup\normalsize
+\begin{footnotesize}
+\begin{flagderiv}[exercise-pseudodisjunction-proof]
+\assume{mainhyp}{A\lor B}{}
+\assume{parta}{A}{}
+\assume{parta-left-subhyp}{A\Rightarrow B}{}
+\step{parta-left-subconc}{B}{$\Rightarrow$Élim sur \ref{parta-left-subhyp} et \ref{parta}}
+\conclude{parta-left}{(A\Rightarrow B) \Rightarrow B}{$\Rightarrow$Int de \ref{parta-left-subhyp} dans \ref{parta-left-subconc}}
+\assume{parta-right-subhyp}{B\Rightarrow A}{}
+\conclude{parta-right}{(B\Rightarrow A) \Rightarrow A}{$\Rightarrow$Int de \ref{parta-right-subhyp} dans \ref{parta}}
+\step{parta-conc}{((A\Rightarrow B) \Rightarrow B) \land
+((B\Rightarrow A) \Rightarrow A)}{$\land$Int sur \ref{parta-left}, \ref{parta-right}}
+\done
+\assume{partb}{B}{}
+\assume{partb-right-subhyp}{B\Rightarrow A}{}
+\step{partb-right-subconc}{A}{$\Rightarrow$Élim sur \ref{partb-right-subhyp} et \ref{partb}}
+\conclude{partb-right}{(B\Rightarrow A) \Rightarrow A}{$\Rightarrow$Int de \ref{partb-right-subhyp} dans \ref{partb-right-subconc}}
+\assume{partb-left-subhyp}{A\Rightarrow B}{}
+\conclude{partb-left}{(A\Rightarrow B) \Rightarrow B}{$\Rightarrow$Int de \ref{partb-left-subhyp} dans \ref{partb}}
+\step{partb-conc}{(((A\Rightarrow B) \Rightarrow B) \land
+(B\Rightarrow A) \Rightarrow A)}{$\land$Int sur \ref{partb-left}, \ref{partb-right}}
+\done
+\step{mainconc}{(((A\Rightarrow B) \Rightarrow B) \land
+(B\Rightarrow A) \Rightarrow A)}{$\lor$Élim sur \ref{mainhyp} de \ref{parta} dans \ref{parta-conc} et de \ref{partb} dans \ref{partb-conc}}
+\conclude{}{A\lor B \Rightarrow ((A\Rightarrow B) \Rightarrow B) \land
+((B\Rightarrow A) \Rightarrow A)}{$\Rightarrow$Int de \ref{mainhyp} dans \ref{mainconc}}
+\end{flagderiv}
+\end{footnotesize}
+\egroup
+
+La voici écrite informellement en langage naturel :
+
+Supposons $A\lor B$.  Considérons d'abord le cas $A$.  Si on a
+$A\Rightarrow B$ alors $B$, ce qui montre $(A\Rightarrow B)\Rightarrow
+B$ ; par ailleurs, de $A$ on tire aussi $(B\Rightarrow A)\Rightarrow
+A$ ; on a donc montré $((A\Rightarrow B) \Rightarrow B) \land
+((B\Rightarrow A) \Rightarrow A)$.  Le cas $B$ est exactement analogue
+par symétrie (à l'ordre des conclusions près dans la conjonction
+finale).  Dans les deux cas de la disjonction on a montré
+$(A\Rightarrow B)\Rightarrow B$.  Donc finalement $A\lor B \Rightarrow
+((A\Rightarrow B) \Rightarrow B) \land ((B\Rightarrow A) \Rightarrow
+A)$.
+\end{corrige}
+
+
 %
 %
 %
-- 
cgit v1.2.3