Fix a mistake: contraction rule cannot be dispensed with.

(See discussion in example 3.1.3 in Troelstra & Schwichtenberg: the
system I presented is essentially their G2i, and the contraction rule
is necessary.)

1 files changed, 7 insertions, 10 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index f3e8b1d..35425f0 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2675,22 +2675,19 @@ droite \alert{ou à gauche} du symbole « $\vdash$ ».
 \medskip
 
 \itempoint On garde la règle $\inferrule*[left=Ax]{ }{\Gamma,Q \vdash
-  Q}$, qu'on peut choisir de séparer en :
+  Q}$, ou on peut en séparer une règle d'qffaibilissement ; et on va
+reparler des règles de « contraction » et « coupure » :
+
 \begin{center}
-\begin{tabular}{c|c|c}
+\begin{tabular}{c|c}
 $\inferrule*[left=Ax]{ }{Q \vdash Q}$
 &$\inferrule*[left=Weak]{\Gamma \vdash Q}{\Gamma,P\vdash Q}$
-&$\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}$
+\\\hline
+$\inferrule*[left=Contr]{\Gamma,P,P \vdash Q}{\Gamma,P\vdash Q}$
+&$\inferrule*[left=Cut]{\Gamma \vdash P\\\Gamma,P\vdash Q}{\Gamma\vdash Q}$
 \end{tabular}
 \end{center}
 
-\medskip
-
-\itempoint On va reparler de la règle de « coupure » :
-\[
-\inferrule*[left=Cut]{\Gamma \vdash P\\\Gamma,P\vdash Q}{\Gamma\vdash Q}
-\]
-
 \end{frame}
 %
 \begin{frame}