diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 40 |
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} |