diff options
author | David A. Madore <david+git@madore.org> | 2023-11-27 23:06:49 +0100 |
---|---|---|
committer | David A. Madore <david+git@madore.org> | 2023-11-27 23:06:49 +0100 |
commit | 8d9b259203eac848f2e9092abeba9d5b3f358bbf (patch) | |
tree | cdf0eb6cade4b25d6fc8b567e9dbfb1602726801 /transp-inf110-02-typage.tex | |
parent | ece1b6e6ae5c0a7c350ca8421138f9911dd71427 (diff) | |
download | inf110-lfi-8d9b259203eac848f2e9092abeba9d5b3f358bbf.tar.gz inf110-lfi-8d9b259203eac848f2e9092abeba9d5b3f358bbf.tar.bz2 inf110-lfi-8d9b259203eac848f2e9092abeba9d5b3f358bbf.zip |
Syntax of propositional calculus.
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r-- | transp-inf110-02-typage.tex | 41 |
1 files changed, 39 insertions, 2 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 881ec13..45d1ca2 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -1262,7 +1262,7 @@ On prouve alors successivement : % \section{Le calcul propositionnel intuitionniste} \begin{frame} -\frametitle{Le calcul propositionnel intuitionniste : présentation sommaire} +\frametitle{Le calcul propositionnel : présentation sommaire} \itempoint Le \textbf{calcul propositionnel} est une forme de logique qui ne parle que de « propositions » (énoncés logiques) : pas de @@ -1285,7 +1285,8 @@ abréviation de $P \Rightarrow \bot$ (soit : « $P$ est absurde »). \medskip -On distingue : +On distingue {\footnotesize (les règles précises seront décrites plus + loin)} : \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 @@ -1298,4 +1299,40 @@ On distingue : \end{frame} % +\begin{frame} +\frametitle{Le calcul propositionnel : syntaxe} + +\itempoint Une \textbf{formule} du calcul propositionnel est +(inductivement) : +\begin{itemize} +\item une \textbf{variable propositionnelle} ($A$, $B$, $C$...), +\item l'application d'un connecteur : $(P\Rightarrow Q)$, $(P\land + Q)$, $(P\lor Q)$ où $P,Q$ sont deux formules, ou encore $\top$, + $\bot$. +\end{itemize} + +\medskip + +\itempoint Conventions d'écriture : +\begin{itemize} +\item $\neg P$ abrège « $(P \Rightarrow \bot)$ » ; +\item on omet certaines parenthèses : $\neg$ est prioritaire sur + $\land$ qui est prioritaire sur $\lor$ qui est prioritaire sur + $\Rightarrow$ {\footnotesize (\textcolor{purple}{ne pas abuser de + l'omission des parenthèses, merci})} ; +\item $\land$ et $\lor$ associent à gauche disons (ça n'aura pas + d'importance) ; mais $\Rightarrow$ associe à droite : $P \Rightarrow + Q\Rightarrow R$ signifie $(P\Rightarrow(Q\Rightarrow R))$ ; +\item parfois : $P \Leftrightarrow Q$ pour $(P\Rightarrow Q) \land + (Q\Rightarrow P)$ {\footnotesize (priorité encore plus basse ?)}. +\end{itemize} + +\medskip + +\itempoint Si $P_1,\ldots,P_r, Q$ sont des formules, $P_1,\ldots,P_r +\vdash Q$ s'appelle un \textbf{séquent}, à comprendre comme « sous les +hypothèses $P_1,\ldots,P_r$, on a $Q$ ». + +\end{frame} +% \end{document} |