From b2f4e549cbee31cc1ee486030dff14b0a3762149 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 11 Dec 2023 11:54:26 +0100
Subject: Sequent calculus: better discuss structural rules.
---
transp-inf110-02-typage.tex | 38 ++++++++++++++++++++++++++++++++++++++
1 file changed, 38 insertions(+)
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 07e2999..9c88889 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1420,6 +1420,9 @@ $\bot$
\\
\end{tabular}
+{\footnotesize Dans tout ça, $\Gamma$ désigne un jeu (\alert{non
+ ordonné}, mais avec multiplicités) d'hypothèses.\par}
+
{\footnotesize Les hypothèses en \textcolor{mydarkgreen}{vert} sont
« déchargées », c'est-à-dire qu'elles disparaissent.\par}
@@ -2796,6 +2799,41 @@ Et que dans le transp. \ref{example-proposition-proof-with-implication} :
\]
\par}
+\end{frame}
+%
+\begin{frame}
+\label{sequent-calculus-structural-rules}
+\frametitle{Calcul des séquents : règles « structurales »}
+
+\itempoint On peut choisir de séparer la règle $\inferrule*[left=Ax]{
+}{\Gamma,Q \vdash Q}$ en deux, une règle d'axiome strict et une règle
+d'« affaiblissement » :
+
+\begin{center}
+\begin{tabular}{c|c}
+$\inferrule*[left=Ax]{ }{Q \vdash Q}$
+&$\inferrule*[left=Weak]{\Gamma \vdash Q}{\Gamma,P\vdash Q}$
+\end{tabular}
+\end{center}
+
+\medskip
+
+\itempoint Comme en déduction naturelle, les hypothèses n'ont pas
+d'ordre.
+
+\medskip
+
+\itempoint Si elles ont des multiplicités, la règle de contraction est
+nécessaire (sans elle, on ne peut pas prouver $(A\Rightarrow B) \land A
+\vdash B$) :
+\[
+\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}
+\]
+On peut s'en dispenser en décidant que les hypothèses n'ont pas de
+multiplicité (forment un ensemble, pas un multi-ensemble), ou en
+modifiant les règles $\Rightarrow$L et $\land$L pour ne pas perdre
+d'hypothèse en remontant.
+
\end{frame}
%
% TODO:
--
cgit v1.2.3