From b620eb841333f53f725cbad829e57142a0c72e73 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Sun, 3 Dec 2023 11:09:18 +0100 Subject: A few more important tautologies. --- transp-inf110-02-typage.tex | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'transp-inf110-02-typage.tex') 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 -- cgit v1.2.3