Quick overview of intuitionistic propositional calculus.

1 files changed, 38 insertions, 0 deletions

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
@@ -1260,4 +1260,42 @@ On prouve alors successivement :
 
 \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}