diff options
author | David A. Madore <david+git@madore.org> | 2023-12-02 18:51:48 +0100 |
---|---|---|
committer | David A. Madore <david+git@madore.org> | 2023-12-02 18:51:48 +0100 |
commit | 6a328e50a9485b9bea7e7c8c3e5a6a30dc5ca235 (patch) | |
tree | 8d75bb91c6ca01f9db053bfc075c4902c2f4df70 /transp-inf110-02-typage.tex | |
parent | 274f1d328dca636784b45d1bf198692b751c7828 (diff) | |
download | inf110-lfi-6a328e50a9485b9bea7e7c8c3e5a6a30dc5ca235.tar.gz inf110-lfi-6a328e50a9485b9bea7e7c8c3e5a6a30dc5ca235.tar.bz2 inf110-lfi-6a328e50a9485b9bea7e7c8c3e5a6a30dc5ca235.zip |
Some important tautologies.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r-- | transp-inf110-02-typage.tex | 58 |
1 files changed, 58 insertions, 0 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index fdb603d..0142fef 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1503,4 +1503,62 @@ Présentation « drapeau », plus proche de l'écriture naturelle, commode \end{frame} % +\begin{frame} +\frametitle{Quelques tautologies du calcul propositionnel intuitionniste} + +\itempoint Lorsque $\vdash P$ (sans hypothèse), on dit que $P$ est +\textbf{valide} dans le calcul propositionnel intuitionniste, ou est +une \textbf{tautologie} de celui-ci. + +\medskip + +{\footnotesize + +Quelques tautologies importantes (« $P\Leftrightarrow Q$ » abrège +« $P \Rightarrow Q$ et $Q \Rightarrow P$ ») : + +\begin{tabular}{|c|c|} +\hline +$A\Rightarrow B\Rightarrow A$&$(A\Rightarrow B\Rightarrow C) +\Rightarrow (A\Rightarrow B)\Rightarrow A\Rightarrow C$\\ +\hline +$A\land B \Rightarrow A$\quad\quad\quad$A\land B \Rightarrow B$&$A\Rightarrow A\lor B$\quad\quad\quad$B \Rightarrow A\lor B$\\ +\hline +$A\Rightarrow B\Rightarrow A\land B$&$(A\Rightarrow C)\Rightarrow(B\Rightarrow C)\Rightarrow A\lor B\Rightarrow C$\\ +\hline +$A\land B \Leftrightarrow B\land A$&$A\lor B \Leftrightarrow B\lor A$\\ +\hline +$(A\land B)\land C \Leftrightarrow A\land(B\land C)$&$(A\lor B)\lor C \Leftrightarrow A\lor(B\lor C)$\\ +\hline +$(A\Rightarrow B)\land (A\Rightarrow C) \Leftrightarrow (A\Rightarrow B\land C)$ +&$(A\Rightarrow C)\land (B\Rightarrow C) \Leftrightarrow (A\lor B \Rightarrow C)$\\ +\hline +$(A\Rightarrow B)\lor (A\Rightarrow C) \mathrel{\color{red}\Rightarrow} (A\Rightarrow B\lor C)$ +&$(A\Rightarrow C)\lor (B\Rightarrow C) \mathrel{\color{red}\Rightarrow} (A\land B \Rightarrow C)$\\ +\hline +$A\land(B\lor C) \Leftrightarrow (A\land B)\lor (A\land C)$ +&$A\lor(B\land C) \mathrel{\color{olive}\Leftrightarrow} (A\lor B)\land (A\lor 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$\\ +\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 +$A \mathrel{\color{red}\Rightarrow} \neg\neg A$&$(\neg\neg A\Rightarrow \neg\neg B) \Leftrightarrow \neg\neg (A\Rightarrow B)$\\ +\hline +$(\neg\neg A\land \neg\neg B) \Leftrightarrow \neg\neg (A\land B)$ +&$(\neg\neg A\lor \neg\neg B) \mathrel{\color{red}\Rightarrow} \neg\neg (A\lor B)$\\ +\hline +$(A\Rightarrow B) \mathrel{\color{red}\Rightarrow} (\neg B\Rightarrow \neg A)$ +&$\neg A \Leftrightarrow \neg\neg\neg A$\\ +\hline +\end{tabular} + +\par} + +\end{frame} +% \end{document} |