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(-)

(limited to 'transp-inf110-02-typage.tex')

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