From 8d9b259203eac848f2e9092abeba9d5b3f358bbf Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 27 Nov 2023 23:06:49 +0100
Subject: Syntax of propositional calculus.
---
transp-inf110-02-typage.tex | 41 +++++++++++++++++++++++++++++++++++++++--
1 file 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
@@ -1296,6 +1297,42 @@ On distingue :
vérité ».
\end{itemize}
+\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}
--
cgit v1.2.3