Sketch of proof of cut elimination, and applications thereof.

1 files changed, 91 insertions, 6 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 64f597f..cd3857a 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2939,8 +2939,8 @@ dans $\Gamma\vdash P$ et à gauche dans $\Gamma,P\vdash Q$
 \label{cut-elimination-boring-cases}
 \frametitle{Exemples d'étape d'élimination des coupures (1)}
 
-\itempoint Cas « inintéressants » : la dernière règle d'une des
-branches de la coupure n'opère pas sur la formule coupée : on fait
+\itempoint Cas « déplaçants » : la dernière règle d'une des branches
+de la coupure n'opère pas sur la formule coupée : on fait
 \alert{remonter} la coupure sur cette branche (quitte à choisir).
 
 \begin{center}
@@ -2988,8 +2988,8 @@ $\mpdotsabove{\Gamma\vdash Q}$
 \label{cut-elimination-interesting-cases}
 \frametitle{Exemples d'étape d'élimination des coupures (2)}
 
-\itempoint Cas « intéressants » : la dernière règle de chaque branche
-de la coupure concerne le connecteur logique de la formule coupée : la
+\itempoint Cas « principaux » : la dernière règle de chaque branche de
+la coupure concerne le connecteur logique de la formule coupée : la
 coupure ne remonte pas et peut même se multiplier, mais le « degré »
 de complexité de la formule coupée diminue :
 
@@ -3031,9 +3031,94 @@ $\inferrule*[left={\color{purple}Cut}]{
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Élimination des coupures : récurrence}
+
+\itempoint Le \textbf{degré} $\deg P$ d'une formule propositionnelle
+est : $0$ pour une variable propositionnelle ou $\top$, $\bot$, et
+$\max(\deg P_1, \deg P_2) + 1$ si $P = P_1 \circ P_2$ pour un
+connecteur $\circ \in \{\Rightarrow, \land, \lor\}$.  C'est donc la
+profondeur de l'arbre de cette formule.
+
+\smallskip
+
+{\footnotesize P.ex., $\deg(((A\Rightarrow B)\Rightarrow A)\Rightarrow
+  A) = 3$.\par}
+
+\medskip
+
+\itempoint Le degré d'une coupure est le degré de la formule coupée.
+Le \textbf{degré de coupure} d'une démonstration en calcul des
+séquents est le plus grand degré d'une coupure (ou $-1$ s'il n'y en a
+pas).  Une \textbf{coupure critique} est une coupure de degré
+maximal.
+
+\medskip
+
+\itempoint La preuve de l'élimination des coupures se fait par une
+\alert{double récurrence} :
+\begin{itemize}
+\item récurrence principale sur le degré de coupure de la
+  démonstration,
+\item récurrence secondaire, à degré donné, sur la somme des hauteurs
+  des deux branches de la coupure à éliminer.
+\end{itemize}
+
+\medskip
+
+\itempoint La démonstration est constructive (algorithmique) ;
+l'algorithme esquissé est p.r. (même « élémentaire »).  Il n'est pas
+déterministe {\footnotesize (ni même confluent)}.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Élimination des coupures : conséquences}
+
+{\footnotesize\textcolor{blue}{Quel intérêt de pouvoir éliminer les
+    coupures ?}  Les preuves sans coupure ne peuvent pas faire
+  apparaître de formule inattendue.\par}
+
+\medskip
+
+\itempoint\textbf{Propriété de la disjonction :} si $\vdash Q_1\lor
+Q_2$ (\alert{sans hypothèse !}) alors $\vdash Q_1$ ou bien $\vdash
+Q_2$.  {\footnotesize (\underline{Preuve :} une démonstration sans
+  coupure de $\vdash Q_1\lor Q_2$ doit finir par la règle $\lor$R$_1$
+  ou $\lor$R$_2$. \qedsymbol)}
+
+\medskip
+
+\itempoint\textbf{Corollaire :} $\vdash A\lor\neg A$ n'est pas
+prouvable en logique intuitionniste.
+
+\medskip
+
+\itempoint\textbf{Propriété de la sous-formule :} si $P_1,\ldots,P_r
+\vdash Q$ alors une preuve sans coupure ne fait intervenir que des
+formules qui sont des \alert{sous-formules} de $P_1,\ldots,P_r$ ou
+$Q$.  {\footnotesize (\underline{Preuve :} c'est clair sur chacune des
+  règles. \qedsymbol)}
+
+\medskip
+
+\itempoint\textbf{Corollaire :} on peut \alert{décider
+  algorithmiquement} si $P_1,\ldots,P_r \vdash Q$.
+
+\smallskip
+
+{\footnotesize\underline{Algorithme :} construire l'ensemble $\Phi$ de
+  toutes les sous-formules d'une de $P_1,\ldots,P_r$ ou $Q$, et
+  l'ensemble de tous les séquents possibles $\Gamma\vdash R$ avec
+  $\Gamma\subseteq\Phi$ et $R\in\Phi$.  Marquer comme « valables »
+  ceux qui découlent de séquents déjà marqués comme valables par
+  application d'une des règles du calcul des séquents (autre que la
+  coupure), et répéter jusqu'à ce que le séquent recherché ait été
+  marqué ou que plus aucun séquent ne soit marqué.\qed\par}
+
+\end{frame}
+%
 % TODO:
-% - présentation en calcul des séquents
-% - élimination des coupures
 % - Kripke
 % - fragment négatif
 % - call/cc