From 078a1662d0ebeb28c217eb60eac5600e4652c418 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 4 Dec 2023 22:08:41 +0100
Subject: The rules of sequent calculus.

---
 transp-inf110-02-typage.tex | 84 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index c0aeb08..cae26b4 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1374,6 +1374,7 @@ En français, et un peu informellement :
 \end{frame}
 %
 \begin{frame}
+\label{natural-deduction-rules}
 \frametitle{Le calcul propositionnel intuitionniste : règles}
 
 Axiomes : si $Q \in \{P_1,\ldots,P_r\}$ alors $P_1,\ldots,P_r \vdash Q$.
@@ -2633,6 +2634,89 @@ P.ex., on peut remplacer $Q_1\land Q_2$ par $Q_2\land Q_1$ ou
 $(Q_1\land Q_2)\land Q_3$ par $Q_1\land (Q_2\land Q_3)$ n'importe où
 dans une formule et on obtient ainsi une formule équivalente.
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Calcul des séquents}
+
+\itempoint Le \textbf{calcul des séquents} est une autre présentation
+de la (même) logique propositionnelle intuitionniste (mêmes
+tautologies, mêmes séquents).
+
+\medskip
+
+\itempoint Cette présentation est peut-être moins « naturelle », mais
+elle est plus symétrique, et a divers intérêts théoriques.
+
+\medskip
+
+\itempoint La différence principale porte sur les \alert{règles
+  d'élimination} (transp. suivant) : au lieu d'une règle
+d'introduction et d'une règle d'élimination, on a une \textbf{règle
+  droite} (= introduction) et une \textbf{règle gauche}
+($\leftrightarrow$ élimination), qui introduisent le connecteur à
+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 :
+\begin{center}
+\begin{tabular}{c|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}$
+\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}
+\frametitle{Calcul des séquents : les règles (intuitionnistes)}
+
+{\footnotesize
+
+La colonne de droite est la même que la colonne de gauche (intro) du
+transp. \ref{natural-deduction-rules}.  C'est la colonne de gauche qui
+est « nouvelle » :
+
+\par}
+
+\bigskip
+
+\begin{tabular}{c|c|c}
+&Gauche&Droite\\\hline
+$\Rightarrow$
+&$\inferrule{\Gamma\vdash M\\\Gamma,P\vdash R}{\Gamma,M\Rightarrow P\vdash R}$
+&$\inferrule{\Gamma,P\vdash Q}{\Gamma\vdash P\Rightarrow Q}$
+\\\hline
+$\land$
+&$\inferrule{\Gamma,P_1\vdash R}{\Gamma,P_1\land P_2\vdash R}$
+\quad$\inferrule{\Gamma,P_2\vdash R}{\Gamma,P_1\land P_2\vdash R}$
+&$\inferrule{\Gamma\vdash Q_1\\\Gamma\vdash Q_2}{\Gamma\vdash Q_1\land Q_2}$
+\\\hline
+$\lor$
+&$\inferrule{\Gamma,P_1\vdash R\\\Gamma,P_2\vdash R}{\Gamma,P_1\lor P_2\vdash R}$
+&$\inferrule{\Gamma\vdash Q_1}{\Gamma\vdash Q_1\lor Q_2}$
+\quad$\inferrule{\Gamma\vdash Q_2}{\Gamma\vdash Q_1\lor Q_2}$
+\\\hline
+$\top$
+&(néant)
+&$\inferrule{\strut}{\Gamma\vdash \top}$
+\\\hline
+$\bot$
+&$\inferrule{\strut}{\Gamma,\bot\vdash R}$
+&(néant)
+\\
+\end{tabular}
+
 \end{frame}
 %
 % TODO:
-- 
cgit v1.2.3