From 663e73acd329df0ed327d94845730e77f3c59e09 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 9 Dec 2023 11:37:43 +0100
Subject: 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.)
---
 transp-inf110-02-typage.tex | 17 +++++++----------
 1 file 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}
-- 
cgit v1.2.3