diff options
| author | David A. Madore <david+git@madore.org> | 2023-12-03 11:09:18 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2023-12-03 11:09:18 +0100 |
| commit | b620eb841333f53f725cbad829e57142a0c72e73 (patch) | |
| tree | 8bb024248f4b06d7cb5bfa9110838d71f45f703b | |
| parent | 7642c21489594995bc78be6afe22cbae30239368 (diff) | |
| download | inf110-lfi-b620eb841333f53f725cbad829e57142a0c72e73.tar.gz inf110-lfi-b620eb841333f53f725cbad829e57142a0c72e73.tar.bz2 inf110-lfi-b620eb841333f53f725cbad829e57142a0c72e73.zip | |
A few more important tautologies.
| -rw-r--r-- | transp-inf110-02-typage.tex | 6 |
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 |