More discussion of the logical connectors.

1 files changed, 53 insertions, 4 deletions

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
@@ -1342,6 +1342,38 @@ 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}
 \frametitle{Le calcul propositionnel intuitionniste : règles}
 
 Axiomes : si $Q \in \{P_1,\ldots,P_r\}$ alors $P_1,\ldots,P_r \vdash Q$.
@@ -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}