diff options
author | David A. Madore <david+git@madore.org> | 2023-12-02 19:45:25 +0100 |
---|---|---|
committer | David A. Madore <david+git@madore.org> | 2023-12-02 19:45:25 +0100 |
commit | abc0cec0510aaffdec6bca8e68bb1eaf008c16df (patch) | |
tree | f14313c7dcbac7e018c4637c3706f44c5ce7bb0c /transp-inf110-02-typage.tex | |
parent | c205701f31a6feb379ba086ec661941ddd276be2 (diff) | |
download | inf110-lfi-abc0cec0510aaffdec6bca8e68bb1eaf008c16df.tar.gz inf110-lfi-abc0cec0510aaffdec6bca8e68bb1eaf008c16df.tar.bz2 inf110-lfi-abc0cec0510aaffdec6bca8e68bb1eaf008c16df.zip |
Proof of negation vs reduction ad absurdum.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r-- | transp-inf110-02-typage.tex | 54 |
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} |