diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 84 |
1 files changed, 84 insertions, 0 deletions
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$. @@ -2635,6 +2636,89 @@ 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: % - présentation en calcul des séquents % - élimination des coupures |