From c33435562d1c1506e17013bd0f05da8ba1ae914b Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 3 Dec 2023 17:46:12 +0100
Subject: Brouwer-Heyting-Kolmogorov interpretation of logical connectives.

---
 transp-inf110-02-typage.tex | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 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 3178d29..bebce81 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1854,10 +1854,37 @@ Dans tous les cas $f$ est calculable.\qed
 classiques) ne nous donne pas du tout d'algorithme !  Elle montre
 juste qu'il « existe » classiquement.
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{L'interprétation de Brouwer-Heyting-Kolmogorov}
+
+Interprétation \alert{informelle/intuitive} des connecteurs de la
+logique intuitionniste, due à A. Kolmogorov, A. Heyting, G. Kreisel,
+A. Troelstra et d'autres :
+
+\begin{itemize}
+\item un témoignage de $P\land Q$, est un témoignage de $P$ et un de $Q$,
+\item un témoignage de $P\lor Q$, est un témoignage de $P$ ou un de
+  $Q$, et la donnée duquel des deux on a choisi,
+\item un témoignage de $P\Rightarrow Q$ est un moyen de transformer
+  un témoignage de $P$ en un témoignage de $Q$,
+\item un témoignage de $\top$ est trivial, \quad \itempoint un
+  témoignage de $\bot$ n'existe pas,
+\item {\color{darkgray} un témoignage de $\forall x.P(x)$ est un moyen
+  de transformer un $x$ quelconque en un témoignage de $P(x)$,}
+\item {\color{darkgray} un témoignage de $\exists x.P(x)$ est la
+  donnée d'un certain $x_0$ et d'un témoignage de $P(x_0)$.}
+\end{itemize}
+
+\medskip
+
+{\footnotesize J'écris « témoignage », mais Kolmogorov parlait de
+  « solution » d'un problème, Heyting de « preuve », etc.\par}
+
 \end{frame}
 %
 % TODO:
-% - Brouwer-Heyting-Kolmogorov
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences
 % - Curry-Howard
-- 
cgit v1.2.3