Equivalence of sequent calculus with natural deduction.

1 files changed, 55 insertions, 0 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 9c88889..b31d1cb 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2836,6 +2836,61 @@ d'hypothèse en remontant.
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Calcul des séquents : équivalence avec la déduction naturelle}
+
+L'équivalence générale entre déduction naturelle et calcul des
+séquents n'est pas difficile si on utilise librement la règle de
+coupure.
+
+\medskip
+
+Montrons l'exemple de la conversion entre $\Rightarrow$Élim et
+$\Rightarrow$Left :
+
+\medskip
+
+\itempoint Dans le sens déduction naturelle $\to$ calcul des
+séquents :
+\vskip-3ex\leavevmode
+\begin{center}
+\scalebox{0.8}{%
+\begin{tabular}{c|c}
+Déduction naturelle&Calcul des séquents\\\hline
+$\inferrule*[left=$\Rightarrow$Élim]{\Gamma\vdash P\Rightarrow Q\\\Gamma\vdash P}{\Gamma\vdash Q}$
+&
+$\inferrule*[left=Cut]{\Gamma\vdash P\Rightarrow Q
+\\
+\inferrule*[left=$\Rightarrow$L]{\Gamma\vdash P\\
+\inferrule*[left=Ax]{ }{\Gamma,Q\vdash Q}
+}{\Gamma,P\Rightarrow Q\vdash Q}
+}{\Gamma\vdash Q}$
+\end{tabular}
+}
+\end{center}
+
+\itempoint Dans le sens calcul des séquents $\to$ déduction
+naturelle :
+\vskip-6ex\leavevmode
+\begin{center}
+\scalebox{0.8}{%
+\begin{tabular}{c|c}
+Calcul des séquents&Déduction naturelle\\\hline
+$\inferrule*[left=$\Rightarrow$L]{\Gamma\vdash M\\\Gamma,P\vdash R}{\Gamma,M\Rightarrow P\vdash R}$
+&
+$\inferrule*[left=$\Rightarrow$Élim]{
+\inferrule*[left=\llap{$\Rightarrow$Intro}]{\Gamma,P\vdash R}{\Gamma\vdash P\Rightarrow R}
+\\
+\inferrule*[left=$\Rightarrow$Élim]{
+\inferrule*[left=\llap{Ax}]{ }{\Gamma,M\Rightarrow P\vdash M\Rightarrow P}
+\\\Gamma\vdash M}{\Gamma,M\Rightarrow P\vdash P}
+}{\Gamma,M\Rightarrow P\vdash R}$
+\end{tabular}
+}
+\end{center}
+
+\end{frame}
+%
 % TODO:
 % - présentation en calcul des séquents
 % - élimination des coupures