From 18cab2596f0973227c4889b0458b0888437cc9cb Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 2 Dec 2023 20:22:39 +0100
Subject: Classical logic.

---
 transp-inf110-02-typage.tex | 74 +++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 71 insertions(+), 3 deletions(-)

(limited to 'transp-inf110-02-typage.tex')

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 5e8e2d4..9b95039 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1565,8 +1565,8 @@ $\neg(A\land\neg A)$&$\neg\neg(A\lor\neg A)$\\
 \begin{frame}
 \frametitle{Quelques non-tautologies}
 
-Rappelons qu'\textcolor{blue}{on ne permet pas de raisonnement par
-  l'absurde} dans notre logique.
+{\footnotesize Rappelons qu'\textcolor{blue}{on ne permet pas de
+    raisonnement par l'absurde} dans notre logique.\par}
 
 \bigskip
 
@@ -1585,7 +1585,10 @@ calcul propositionnel \emph{classique}) :
 \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)$
+\item $\neg A \lor \neg\neg A$ (« tiers exclu faible »)
+\item $(\neg\neg A \Rightarrow A) \Rightarrow (A \lor \neg A)$ {\tiny
+  (même si $(\neg\neg A \Rightarrow A)$ pour \emph{tout} $A$ donne $A
+  \lor \neg A$ pour tout $A$)}
 \end{itemize}
 
 \bigskip
@@ -1649,4 +1652,69 @@ $\neg\neg\neg\neg A$ à $\neg\neg A$, etc.).
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Logique classique}
+
+La logique \textbf{classique} ou \textbf{booléenne} modifie la règle
+\[
+\inferrule*[left={$\bot$Élim}]{\Gamma\vdash \bot}{\Gamma\vdash Q}
+\quad\quad\quad
+\text{~en~}
+\quad\quad\quad
+\inferrule*[left={Absurde}]{\Gamma,{\color{mydarkgreen}\neg Q}\vdash \bot}{\Gamma\vdash Q}
+\]
+
+\bigskip
+
+Elle est donc \alert{plus forte} (= a plus de tautologies) que la
+logique intuitionniste.
+
+\bigskip
+
+\itempoint\textbf{Théorème} {\footnotesize (« complétude de la
+  sémantique booléenne du calcul propositionnel classique »)} : $P$
+est une tautologie de la logique classique \alert{ssi} pour toute
+substitution de $\bot$ ou $\top$ à chacune des variables
+propositionnelles de $P$ a la valeur de vérité $\top$.
+
+\bigskip
+
+Tableaux de vérité :
+
+\smallskip
+
+\begin{tabular}{c||c||c}
+$
+\begin{array}{c|cc}
+\land&\bot&\top\\\hline
+\bot&\bot&\bot\\
+\top&\bot&\top\\
+\end{array}
+$
+&
+$
+\begin{array}{c|cc}
+\lor&\bot&\top\\\hline
+\bot&\bot&\top\\
+\top&\top&\top\\
+\end{array}
+$
+&
+$
+\begin{array}{c|cc}
+A \Rightarrow B&B=\bot&B=\top\\\hline
+A=\bot&\top&\top\\
+A=\top&\bot&\top\\
+\end{array}
+$
+\end{tabular}
+
+\end{frame}
+%
+% TODO:
+% - substitution des variables propositionnelles par des formules
+% - substitution d'équivalences
+% - Curry-Howard
+% - Kriple
+%
 \end{document}
-- 
cgit v1.2.3