summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-02 20:22:39 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-02 20:22:39 +0100
commit18cab2596f0973227c4889b0458b0888437cc9cb (patch)
treea6342a01c882eed798fa0299bb604004ad876c56 /transp-inf110-02-typage.tex
parentabc0cec0510aaffdec6bca8e68bb1eaf008c16df (diff)
downloadinf110-lfi-18cab2596f0973227c4889b0458b0888437cc9cb.tar.gz
inf110-lfi-18cab2596f0973227c4889b0458b0888437cc9cb.tar.bz2
inf110-lfi-18cab2596f0973227c4889b0458b0888437cc9cb.zip
Classical logic.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex74
1 files changed, 71 insertions, 3 deletions
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}