diff options
| -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} |