Brouwer-Heyting-Kolmogorov interpretation of logical connectives.

1 files changed, 28 insertions, 1 deletions

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
@@ -1856,8 +1856,35 @@ 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