diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r-- | transp-inf110-02-typage.tex | 38 |
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} |