From ece1b6e6ae5c0a7c350ca8421138f9911dd71427 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 27 Nov 2023 22:48:03 +0100
Subject: Quick overview of intuitionistic propositional calculus.

---
 transp-inf110-02-typage.tex | 38 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 6e21de5..881ec13 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1258,6 +1258,44 @@ On prouve alors successivement :
 
 \par}
 
+\end{frame}
+%
+\section{Le calcul propositionnel intuitionniste}
+\begin{frame}
+\frametitle{Le calcul propositionnel intuitionniste : présentation sommaire}
+
+\itempoint Le \textbf{calcul propositionnel} est une forme de logique
+qui ne parle que de « propositions » (énoncés logiques) : pas de
+variables d'individus (p.ex. entiers naturels, ensembles…), \alert{pas
+  de quantification}.
+
+\medskip
+
+\itempoint Les \textbf{connecteurs logiques} sont : $\Rightarrow$
+(implication), $\land$ (conjonction logique : « et »), $\lor$
+(disjonction : « ou »), $\top$ (« vrai ») et $\bot$ (« faux » ou
+« absurde »).
+
+{\footnotesize Tous sont binaires sauf $\top$, $\bot$ (nullaires).\par}
+
+\smallskip
+
+On peut y ajouter $\neg$ (négation logique) unaire : $\neg P$ est une
+abréviation de $P \Rightarrow \bot$ (soit : « $P$ est absurde »).
+
+\medskip
+
+On distingue :
+\begin{itemize}
+\item la logique \textbf{classique} qui admet la règle du \alert{tiers
+  exclu} (« tertium non datur ») sous une forme ou une autre ; logique
+  usuelle des mathématiques ; on peut la modéliser par $2$ valeurs de
+  vérité (« vrai » et « faux ») ;
+\item la logique \textbf{intuitionniste}, plus \emph{faible}, qui
+  n'admet pas cette règle : il n'y a pas vraiment de « valeur de
+  vérité ».
+\end{itemize}
+
 \end{frame}
 %
 \end{document}
-- 
cgit v1.2.3