summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-02 19:27:11 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-02 19:27:11 +0100
commitc205701f31a6feb379ba086ec661941ddd276be2 (patch)
tree25501f41e7e9e3e625790c9070850a669559443e /transp-inf110-02-typage.tex
parent6a328e50a9485b9bea7e7c8c3e5a6a30dc5ca235 (diff)
downloadinf110-lfi-c205701f31a6feb379ba086ec661941ddd276be2.tar.gz
inf110-lfi-c205701f31a6feb379ba086ec661941ddd276be2.tar.bz2
inf110-lfi-c205701f31a6feb379ba086ec661941ddd276be2.zip
Examples of non-tautologies.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex40
1 files 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}