1 files changed, 54 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 43e4dfa..5e8e2d4 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1595,4 +1595,58 @@ calcul propositionnel \emph{classique}) :
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Preuve de la négation vs raisonnement par l'absurde}
+
+\itempoint Rappel : la négation $\neg A$ abrège $A \Rightarrow \bot$
+{\footnotesize(« si $A$ est vrai alors \textsc{absurdité} »)}.
+
+\bigskip
+
+Bien distinguer :
+
+\medskip
+
+\itempoint d'une part la \textbf{preuve de la négation} de $A$ :
+
+\smallskip
+
+\textcolor{teal}{« Supposons $A$ [vrai].  Alors (...), ce qui est
+  absurde.  Donc $A$ est faux. »}
+
+\smallskip
+
+qui \alert{est valable} intuitionnistement : c'est prouver $A
+\Rightarrow \bot$ par la règle $\Rightarrow$Intro,
+
+\medskip
+
+\itempoint et la \textbf{preuve par l'absurde} de $A$ d'autre part :
+
+\smallskip
+
+\textcolor{teal}{« Supposons $A$ faux [i.e., $\neg A$].  Alors (...),
+  ce qui est absurde.  Donc $A$ est vrai. »}
+
+\smallskip
+
+qui \alert{n'est pas valable} intuitionnistement : tout ce qu'on peut
+en tirer est $\neg\neg A$.
+
+\bigskip
+
+\itempoint On peut lire $\neg A$ comme « $A$ est faux » et $\neg\neg
+A$ comme « $A$ n'est pas faux ».
+
+\smallskip
+
+{\footnotesize
+
+\itempoint Noter que $\neg\neg\neg A$ équivaut à $\neg A$ (donc
+$\neg\neg\neg\neg A$ à $\neg\neg A$, etc.).
+
+\par}
+
+\end{frame}
+%
 \end{document}