diff options
Diffstat (limited to 'exercices-inf110.tex')
| -rw-r--r-- | exercices-inf110.tex | 88 |
1 files changed, 87 insertions, 1 deletions
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} + + % % % |