From 4ff71fa17d9611851c8fae2673912a93894ad565 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Mon, 11 Dec 2023 13:55:47 +0100 Subject: Equivalence of sequent calculus with natural deduction. --- transp-inf110-02-typage.tex | 55 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) 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 @@ -2834,6 +2834,61 @@ 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} +% +\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: -- cgit v1.2.3