summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-03 11:09:18 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-03 11:09:18 +0100
commitb620eb841333f53f725cbad829e57142a0c72e73 (patch)
tree8bb024248f4b06d7cb5bfa9110838d71f45f703b /transp-inf110-02-typage.tex
parent7642c21489594995bc78be6afe22cbae30239368 (diff)
downloadinf110-lfi-b620eb841333f53f725cbad829e57142a0c72e73.tar.gz
inf110-lfi-b620eb841333f53f725cbad829e57142a0c72e73.tar.bz2
inf110-lfi-b620eb841333f53f725cbad829e57142a0c72e73.zip
A few more important tautologies.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex6
1 files changed, 5 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 06473c2..3178d29 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1519,9 +1519,12 @@ Quelques tautologies importantes (« $P\Leftrightarrow Q$ » abrège
\begin{tabular}{|c|c|}
\hline
-$A\Rightarrow B\Rightarrow A$&$(A\Rightarrow B\Rightarrow C)
+$A\Rightarrow A$\quad\quad\quad $A\Rightarrow B\Rightarrow A$&$(A\Rightarrow B\Rightarrow C)
\Rightarrow (A\Rightarrow B)\Rightarrow A\Rightarrow C$\\
\hline
+$(A\Rightarrow B\Rightarrow C) \Leftrightarrow (A\land B \Rightarrow C)$
+&$A\land A \mathrel{\color{olive}\Leftrightarrow} A$\quad\quad\quad$A\lor A \mathrel{\color{olive}\Leftrightarrow} A$\\
+\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$\\
@@ -1854,6 +1857,7 @@ juste qu'il « existe » classiquement.
\end{frame}
%
% TODO:
+% - Brouwer-Heyting-Kolmogorov
% - substitution des variables propositionnelles par des formules
% - substitution d'équivalences
% - Curry-Howard