From c205701f31a6feb379ba086ec661941ddd276be2 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 2 Dec 2023 19:27:11 +0100
Subject: Examples of non-tautologies.

---
 transp-inf110-02-typage.tex | 40 +++++++++++++++++++++++++++++++++++++---
 1 file changed, 37 insertions(+), 3 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 0142fef..43e4dfa 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1541,9 +1541,8 @@ $A\land(B\lor C) \Leftrightarrow (A\land B)\lor (A\land C)$
 \hline
 $\top$&$\bot \Rightarrow C$\\
 \hline
-$\top\land A \Leftrightarrow A$&$\bot \land A \Leftrightarrow \bot$\\
-\hline
-$\top\lor A \Leftrightarrow \top$&$\bot \lor A \Leftrightarrow A$\\
+$\top\land A \Leftrightarrow A$\quad\quad\quad$\bot \land A \Leftrightarrow \bot$
+&$\top\lor A \Leftrightarrow \top$\quad\quad\quad$\bot \lor A \Leftrightarrow A$\\
 \hline
 $\neg A \land \neg B \Leftrightarrow \neg(A\lor B)$&$\neg A \lor \neg B \mathrel{\color{red}\Rightarrow} \neg(A\land B)$\\
 \hline
@@ -1555,10 +1554,45 @@ $(\neg\neg A\land \neg\neg B) \Leftrightarrow \neg\neg (A\land B)$
 $(A\Rightarrow B) \mathrel{\color{red}\Rightarrow} (\neg B\Rightarrow \neg A)$
 &$\neg A \Leftrightarrow \neg\neg\neg A$\\
 \hline
+$\neg(A\land\neg A)$&$\neg\neg(A\lor\neg A)$\\
+\hline
 \end{tabular}
 
 \par}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Quelques non-tautologies}
+
+Rappelons qu'\textcolor{blue}{on ne permet pas de raisonnement par
+  l'absurde} dans notre logique.
+
+\bigskip
+
+Les énoncés suivants \alert{ne sont pas} des tautologies du calcul
+propositionnel intuitionniste (même s'ils \emph{sont} valables en
+calcul propositionnel \emph{classique}) :
+\begin{itemize}
+\item $((A\Rightarrow B)\Rightarrow A)\Rightarrow A$ (« loi de Peirce »)
+\item $A \lor \neg A$ (« tiers exclu »)
+\item $\neg\neg A \Rightarrow A$ (« élimination de la double
+  négation »)
+\item $\neg(A\land B) \Rightarrow \neg A\lor\neg B$ (une des « lois de
+  De Morgan »)
+\item $(A\Rightarrow B) \Rightarrow \neg A\lor B$ {\footnotesize (la
+  réciproque est bien valable intuitionnistement)}
+\item $(\neg B\Rightarrow \neg A) \Rightarrow (A\Rightarrow B)$
+  {\footnotesize (même remarque)}
+\item $(A\Rightarrow B) \lor (B\Rightarrow A)$ (« loi de Dummett »)
+\item $(\neg\neg A \Rightarrow A) \Rightarrow (A \lor \neg A)$
+\end{itemize}
+
+\bigskip
+
+{\footnotesize\textcolor{brown}{Mais comment sait-on que quelque chose
+    \emph{n'est pas} une tautologie, au juste ?}\par}
+
 \end{frame}
 %
 \end{document}
-- 
cgit v1.2.3