From 5dd88ad420e92182d807c7b5ce81eeb37c061d30 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 4 Dec 2023 11:44:04 +0100
Subject: More discussion of the logical connectors.

---
 transp-inf110-02-typage.tex | 57 +++++++++++++++++++++++++++++++++++++++++----
 1 file changed, 53 insertions(+), 4 deletions(-)

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

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 5083da9..7e4c691 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1339,6 +1339,38 @@ On distingue {\footnotesize (les règles précises seront décrites plus
 \vdash Q$ s'appelle un \textbf{séquent}, à comprendre comme « sous les
 hypothèses $P_1,\ldots,P_r$, on a $Q$ ».
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Le calcul propositionnel intuitionniste : connecteurs}
+
+\itempoint Chaque connecteur logique a des règles
+d'\textbf{introduction} permettant de \alert{démontrer} ce connecteur,
+et des règles d'\textbf{élimination} permettant de l'\alert{utiliser}.
+
+\bigskip
+
+En français, et un peu informellement :
+\begin{itemize}
+\item pour introduire $\Rightarrow$ : on démontre $Q$ \alert{sous
+  l'hypothèse} $P$, ce qui donne $P\Rightarrow Q$ (hypothèse
+  déchargée) ;
+\item pour éliminer $\Rightarrow$ : si on a $P\Rightarrow Q$ et $P$,
+  on a $Q$ (\textit{modus ponens}) ;
+\item pour introduire $\land$ : on démontre $Q_1$ et $Q_2$, ce qui
+  donne $Q_1\land Q_2$ ; pour l'éliminer : si on a $Q_1 \land Q_2$ on
+  en tire $Q_1$ resp. $Q_2$ ;
+\item pour introduire $\lor$ : on démontre $Q_1$ et $Q_2$, ce qui
+  donne $Q_1\land Q_2$ ;
+\item pour éliminer $\lor$ : si on a $P_1 \lor P_2$, on démontre $Q$
+  successivement sous les hypothèses $P_1$ et $P_2$, ce qui donne $Q$
+  (hypothèses déchargées) ;
+\item pour introduire $\top$, c'est trivial, et on ne peut pas
+  l'éliminer ;
+\item pour éliminer $\bot$, on tire la conclusion qu'on veut
+  (\textit{ex falso quodlibet}), et on ne peut pas l'introduire.
+\end{itemize}
+
 \end{frame}
 %
 \begin{frame}
@@ -1387,6 +1419,13 @@ $\bot$
 \label{example-propositional-proofs}
 \frametitle{Exemples de démonstrations}
 
+Indiquant à côté de chaque barre une abréviation de la règle utilisée
+(« $\Rightarrow$Int » pour introduction de $\Rightarrow$,
+« $\land$Élim$_2$ » pour la 2\textsuperscript{e} règle d'élimination
+de $\land$, etc.) :
+
+\bigskip
+
 {\footnotesize
 \[
 \inferrule*[left={$\Rightarrow$Int},right=\hphantom{Int}]{
@@ -1429,11 +1468,11 @@ $\bot$
 \frametitle{Présentation différente}
 
 On peut aussi n'écrire que les conclusions (partie droite du
-signe $\vdash$), à condition d'indiquer pour chaque hypothèse
+signe « $\vdash$ »), à condition d'indiquer pour chaque hypothèse
 déchargée à quel endroit elle l'a été (ceci sacrifie de la lisibilité
 pour un gain de place) :
 
-\bigskip
+\medskip
 
 {\footnotesize
 \[
@@ -1451,7 +1490,7 @@ pour un gain de place) :
 \]
 \par}
 
-\bigskip
+\medskip
 
 {\footnotesize
 \[
@@ -1471,6 +1510,12 @@ pour un gain de place) :
 \]
 \par}
 
+\medskip
+
+{\footnotesize\textbf{N.B.} : une même hypothèse \emph{peut} être
+  déchargée à plusieurs endroits ($u$ dans le 1\textsuperscript{er}
+  exemple).\par}
+
 \end{frame}
 %
 \begin{frame}
@@ -1511,7 +1556,7 @@ Présentation « drapeau », plus proche de l'écriture naturelle, commode
 \frametitle{Quelques tautologies du calcul propositionnel intuitionniste}
 
 \itempoint Lorsque $\vdash P$ (sans hypothèse), on dit que $P$ est
-\textbf{valide} dans le calcul propositionnel intuitionniste, ou est
+\textbf{valable} dans le calcul propositionnel intuitionniste, ou est
 une \textbf{tautologie} de celui-ci.
 
 \medskip
@@ -2312,8 +2357,12 @@ $\Rightarrow$Int de (1) dans (5). »
 \end{frame}
 %
 % TODO:
+% - discussion de la négation et double négation
 % - substitution des variables propositionnelles par des formules
 % - substitution d'équivalences
+% - présentation en calcul des séquents
+% - élimination des coupures
 % - Kripke
+% - inférence de type de Hindley-Milner
 %
 \end{document}
-- 
cgit v1.2.3