diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 29 |
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 |