From abc0cec0510aaffdec6bca8e68bb1eaf008c16df Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 2 Dec 2023 19:45:25 +0100
Subject: Proof of negation vs reduction ad absurdum.

---
 transp-inf110-02-typage.tex | 54 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

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
@@ -1593,6 +1593,60 @@ calcul propositionnel \emph{classique}) :
 {\footnotesize\textcolor{brown}{Mais comment sait-on que quelque chose
     \emph{n'est pas} une tautologie, au juste ?}\par}
 
+\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}
-- 
cgit v1.2.3