\documentclass[13pt,a4paper]{article} % 11pt tamaño de letra, a4paper (hoja carta), twocolumn (dos columnas)
\usepackage[utf8]{inputenc}
\usepackage{mathrsfs}
\usepackage[spanish]{babel}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{makeidx}
\usepackage{graphicx}
\usepackage[left=1cm,right=1.cm,top=2cm,bottom=2cm]{geometry}
\usepackage{makeidx}
\usepackage{listings}
\usepackage{makeidx}
\usepackage{float}
\usepackage[usenames]{color}
\usepackage{bussproofs} %prooftree
\usepackage{txfonts} %integrales dobles cerradas
\usepackage{enumerate}
\lstset{language=Matlab, breaklines=true, basicstyle=\footnotesize}
\lstset{numbers=left, numberstyle=\tiny, stepnumber=1, numbersep=-2pt}
%\numberwithin{equation}{subsection} %Numeración por sección
\usepackage[pdfstartview=FitH,pdfstartpage=1,backref=true,pagebackref=false,colorlinks=false,bookmarks=true,citebordercolor={0 1 0},linkbordercolor={0 0 1}]{hyperref}
\hyphenation{}
\usepackage{xcolor}
\usepackage{fancybox}
\lstset{language=Matlab, breaklines=true, basicstyle=\footnotesize}
\lstset{numbers=left, numberstyle=\tiny, stepnumber=1, numbersep=-2pt}
\author{\textbf{Universidad Nacional de Colombia - Sede Manizales}\\\textbf{Facultad de Ciencias Exactas y Naturales}\\Docente: Mauricio Ayala Rincón.\\ Materia: Lógica Matemática\\Diego Alejandro Londoño Patiño - 1216531 \\ Andres Felipe Morales Foronda - 1216076} % entre los {} pones los nombres
\title{\textbf{Teorema de eliminación de corte}} % entre los {} pones el nombre del trabajo
\begin{document}
\maketitle
%%
\noindent \makebox[0pt][l]{\rule[4.5pt]{19cm}{1pt}}\rule{19cm}{2.4pt}
\begin{center}
\Large \textbf{Teorema:} \textit{La regla de corte se mantiene para} \textbf{G3[mic]}+Cut
\end{center}
\noindent \makebox[0pt][l]{\rule[4.5pt]{19cm}{1pt}}\rule{19cm}{2.4pt}\\
%%Cajita
\noindent La estrategia será ir removiendo sucesivamente los cortes que estén arriba de los demás cortes con rango igual al rango de la deducción completa, es decir, los cortes mas arriba que tengan rango maximal. Procederemos por inducción principal sobre el rango de corte con una subinducción en el nivel del rango de corte en el fondo de $\mathcal{D}$. Consideraremos sólo pruebas con axiomas donde la fórmula principal sea atómica.
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$\Gamma \Rightarrow \Delta,P,D$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$P,\Gamma \Rightarrow \Delta,P,D$}
\BinaryInfC{$P,\Gamma\Rightarrow \Delta,P$}
\end{prooftree}
\noindent dónde cr$(\mathcal{D}_i)=$cr$(\mathcal{D})-1$ para $i\in\lbrace 0,1\rbrace$, por una deducción $\mathcal{D}^*$ con la misma conclusión y tal que cr$(\mathcal{D}^*)\leq |\mathcal{D}|$.
\noindent \makebox[0pt][l]{\rule[4.5pt]{19cm}{1pt}}\rule{19cm}{2.4pt}\\
\noindent {\Large\textbf{Caso 1)}} Supongamos que $\mathcal{D}_0$ o $\mathcal{D}_1$ es un axioma.\\
\noindent \textbf{Subcaso 1a)} $\mathcal{D}_0$ es una instancia del axioma y $\mathcal{D}$ no es principal en $\mathcal{D}_0$.\\
\noindent \textbf{Clásico:} $\mathcal{D}$ es de la forma:
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$P,\Gamma \Rightarrow \Delta,P,D$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$P,\Gamma,D \Rightarrow \Delta,P$}
\BinaryInfC{$P,\Gamma\Rightarrow \Delta,P$}
\end{prooftree}
\noindent La conclusión resulta ser un axioma; así que podemos tomar $\mathcal{D}^*$ como $P,\Gamma\Rightarrow\Delta P$.\\ %Similarmente, si $\mathcal{D}_0$ es una aplicación de L$\bot$.\\
\noindent \textbf{Verificación de (*):} La desigualdad $d^*\leq d_0+d_1$ se verifica ya que, para este caso, $d_0=0$, $d_1=1$ y $d^*=0$. En consecuencia $0\leq 0+1$.\\
\noindent \textbf{Intuicionista.} $\mathcal{D}$ es de la forma:
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$\bot,\Gamma \Rightarrow D$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$D,\bot,\Gamma,\Rightarrow$}
\BinaryInfC{$\bot,\Gamma\Rightarrow$}
\end{prooftree}
\noindent De la hipótesis de inducción, $\mathcal{D}^*$ es precisamente L$\bot$. Así. la prueba se disminuye y el contexto de corte es el mismo.\\
\noindent \textbf{Verificación de (*):} $d^*\leq 2(d_0+d_1)$ se verifica ya que $d_0=1$, $d_1=1$ y $d^*=0$. Así, $0\leq 2(1)$\\
\noindent \textbf{Subcaso 1b)} La premisa a la izquierda es una aplicación de $Ax$ y el sucedente principal es también una fórmula de corte\\
\noindent\textbf{Clásico: }
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$P,\Gamma \Rightarrow \Delta,P$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$P,\Gamma \Rightarrow\Delta$}
\UnaryInfC{$P,P,\Gamma \Rightarrow \Delta$}
\BinaryInfC{$P,\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent $\mathcal{D}^*$ que está dada por $P,\Gamma\Rightarrow\Delta$ fue obtenida aplicando la cerradura bajo la contracción de $\mathcal{D}_1$. Se redujo el tamaño de la prueba y no se modificó el contexto de corte\\
\noindent \textbf{Verificación de (*):} $d^*\leq d_0+d_1$ se verifica ya que $d_0=1$, $d_1=1$, $d^*=2$ y $2\leq 1+1=2$\\
\noindent \textbf{Intuicionista:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$P,\Gamma \Rightarrow P$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$P,P,\Gamma,\Rightarrow ,P$}
\BinaryInfC{$P,\Gamma\Rightarrow ,P$}
\end{prooftree}
\noindent $\mathcal{D}^*$ viene dada por $P,\Gamma\Rightarrow\Delta$, el tamaño se redujo y no cambió el contexto del corte.\\
\noindent \textbf{Verificación de (*):} $d^*\leq 2(d_0+d_1)$ se verifica ya que $d_0=1$, $d_1=1$, $d^*=2$ y $2\leq 2(2)=4$\\
\noindent \textbf{Subcaso 1c)} La premisa a la derecha es una aplicación de Ax o L$\top$ y la fórmula del antecedente principal no es una fórmula de corte.\\
\noindent \textbf{ Clásico:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$\Gamma,\bot \Rightarrow \Delta, D$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$D,\Gamma,\bot\Rightarrow\Delta$}
\BinaryInfC{$\Gamma,\bot\Rightarrow ,\Delta$}
\end{prooftree}
\noindent Por lo tanto, $\mathcal{D}^*$ está dada por $\Gamma,\bot\Rightarrow\Delta$, el tamaño de la prueba se redujo y no cambió el contexto del corte.\\
\noindent \textbf{Verificación de (*):} $d^*\leq d_0+d_1$ se verifica pues $d_0=0$, $d_1=0$, $d^*=0$ y $0\leq 0+0$\\
\noindent\textbf{Intuicionista:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$\Gamma,\bot \Rightarrow D$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$D,\Gamma,\bot\Rightarrow\Delta$}
\BinaryInfC{$\Gamma,\bot\Rightarrow \Delta$}
\end{prooftree}
\noindent Al igual que en el caso clásico $\mathcal{D}^*$ es una instancia de $L_\bot$, el tamaño de la prueba se redujo y no cambió el contexto del corte.\\
\noindent \textbf{Verificación de (*):} $d^*\leq 2(d_0+d_1)$ se verifica ya que $d_0=0$, $d_1=0$, $d^*=0$ y $0\leq 2(0+0)=0$\\
\noindent \textbf{Subcaso 1d)} La premisa en la derecha es una aplicación del axioma Ax y la fórmula de corte es también una fórmula principal del axioma.\\
\noindent\textbf{Clásico: }
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$P,\Gamma\Rightarrow \Delta,P,P$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$P,P,\Gamma\Rightarrow\Delta,P$}
\BinaryInfC{$P,\Gamma,\Rightarrow \Delta,P$}
\end{prooftree}
\noindent El tamaño de la prueba disminuyó, no cambió el contexto de corte.\\
\noindent \textbf{Verificación de (*):} $d^*\leq d_0+d_1$ se verifica ya que $d_0=0$, $d_1=0$, $d^*=0$ y $0\leq 0+0=0$\\
\noindent\textbf{Intuicionista:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$P,\Gamma\Rightarrow P$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$P,P,\Gamma\Rightarrow P$}
\BinaryInfC{$P,\Gamma,\Rightarrow P$}
\end{prooftree}
\noindent Del mismo modo, el tamaño de la prueba disminuyó y el contexto de corte siguió igual.\\
\noindent \textbf{Verificación de (*):} $d^*\leq 2(d_0+d_1)$ se verifica ya que $d_0=0$, $d_1=0$, $d^*=0$ y $0\leq 2(0+0)=0$\\
\noindent \textbf{Subcaso 1e)} La premisa en el lado derecho es una aplicación del axioma $L_\bot$ y la fórmula de corte es también una fórmula principal del axioma.
\begin{prooftree}
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$\Gamma \Rightarrow \Delta,\bot$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$\bot,\Gamma \Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent Si $\mathcal{D}_0$ termina con una regla en la cual $\bot$ es principal, $\Gamma \Rightarrow \Delta,\bot$ es de la forma $\Gamma',\bot \Rightarrow \Delta, \bot$ y así es una instancia de L$\bot$; entonces $\Gamma',\bot\Rightarrow\Delta$, el cuál es el mismo que $\Gamma\Rightarrow\Delta$, es también un axioma. Si $\mathcal{D}_0$ termina con una regla en la cual $\bot$ no es principal, digamos, dos premisas, $\mathcal{D}$ es de la forma
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma' \Rightarrow \Delta ' ,\bot$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma''\Rightarrow \Delta '',\bot$}
\RightLabel{$R$}
\BinaryInfC{$\Gamma \Rightarrow \Delta,\bot$}
\RightLabel{$Cut_{cs}$}
\AxiomC{$\bot,\Gamma \Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent Donde $R$ es cualquier regla de inferencia, vamos a analizar la expresión de la forma:
\begin{prooftree}
\AxiomC{$\Gamma'\Rightarrow \Delta',\bot$}
\AxiomC{$\Gamma''\Rightarrow \Delta'',\bot$}
\RightLabel{$R$}
\BinaryInfC{$\Gamma,\Rightarrow \Delta,\bot$}
\end{prooftree}
\noindent \textbf{i) Conjunción:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow \Delta', A,\bot$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow \Delta', B,\bot$}
\BinaryInfC{$\Gamma'\Rightarrow \Delta', A\wedge B,\bot$}
\DisplayProof
\hskip 1.5em
\AxiomC{$\Gamma',A,B\Rightarrow \Delta',\bot $}
\UnaryInfC{$\Gamma',A\wedge B\Rightarrow \Delta',\bot$}
\end{prooftree}
\noindent \textbf{ii) Disyunción:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$A,\Gamma'\Rightarrow \Delta',\bot$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$B,\Gamma\Rightarrow \Delta',\bot$}
\BinaryInfC{$A\vee B,\Gamma'\Rightarrow \Delta', \bot$}
\DisplayProof
\hskip 1.5em
\AxiomC{$\Gamma'\Rightarrow \Delta',A,B,\bot $}
\UnaryInfC{$\Gamma'\Rightarrow \Delta',A\vee B,\bot$}
\end{prooftree}
\noindent \textbf{iii) Implicación:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow \Delta', A,\bot$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$B,\Gamma'\Rightarrow \Delta',\bot$}
\BinaryInfC{$A\rightarrow B,\Gamma',\Rightarrow \Delta', \bot$}
\DisplayProof
\hskip 1.5 em
\AxiomC{$A,\Gamma'\Rightarrow \Delta',B,\bot$}
\UnaryInfC{$\Gamma'\Rightarrow \Delta',A\to B,\bot$}
\end{prooftree}
\noindent \textbf{iv) Cuantificador universal:}
\begin{prooftree}
\AxiomC{$\Gamma'[x]\Rightarrow\Delta',\bot$}
\UnaryInfC{$\forall x,\Gamma'\Rightarrow\Delta',\bot$}
\end{prooftree}
\noindent \textbf{iv) Cuantificador existencial:}
\begin{prooftree}
\AxiomC{$\Gamma'\Rightarrow\Delta[x],\bot$}
\UnaryInfC{$\Gamma'\Rightarrow\exists x,\Delta',\bot$}
\end{prooftree}
\noindent Luego, las reglas de inferencia son válidas y por lo tanto es correcto considerar a $\mathcal{D}_0$ de tal forma. Esto es transformado por una permutación y duplicación del corte arriba sobre $R$ en la izquierda:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow \Delta ',\bot$}
\AxiomC{$\bot\Gamma'\Rightarrow \Delta'$}
\LeftLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma'\Rightarrow \Delta '$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma'' \Rightarrow \Delta '' \bot$}
\AxiomC{$\bot\Gamma''\Rightarrow \Delta ''$}
\RightLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma'' \Rightarrow \Delta ''$}
\RightLabel{$R$}
\BinaryInfC{$\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent En esta deducción $\mathcal{D}'$ aplicando la hipótesis de inducción a $\mathcal{D}'_0$, $\mathcal{D}'_1$. Si $\mathcal{D}_0$ termina con una regla de premisa la transformación es similar, pero ninguna duplicación es necesaria. \\
\noindent Al final inferimos que la prueba $\mathcal{D}^*$ queda de la forma:
\begin{prooftree}
\AxiomC{$(\mathcal{D}_{00})^*$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow\Delta'$}
\AxiomC{$(\mathcal{D}_{01})^*$}
\noLine
\UnaryInfC{$\Gamma''\Rightarrow\Delta''$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent y por lo tanto la prueba fue reducida de tamaño.\\
\noindent \textbf{Verificación de (*) en el caso clásico.} Si nosotros reemplazamos, usando la hipótesis de inducción en $\mathcal{D}'$ las subdeducciones inmediatas $\mathcal{D}'_0$, $\mathcal{D}'_1$ por $(\mathcal{D}'_0)^*$, $(\mathcal{D}'_1)^*$ respectivamente, la profundidad de la deducción resultante $\mathcal{D}^*$ es:
\begin{equation*}
d^*\leq \max(d_{00}+1,d_{01}+1)
\end{equation*}
\noindent Lo cual es precisamente lo que tenemos que probar para $(*)$. \\
\noindent \textbf{Intuicionista: } Nuevamente, la premisa en el lado derecho es una aplicación del axioma $L_\bot$ y la fórmula de corte es también una fórmula principal del axioma.\\
\begin{prooftree}
\EnableBpAbbreviations
\AxiomC{$\mathcal{D}_0$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow \bot$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$\bot , \Gamma\Rightarrow \Delta$}
\BIC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent Si $\mathcal{D}_0$ termina con una regla en la cual $\bot$ es principal, $\Gamma \Rightarrow \Delta,\bot$ es de la forma $\Gamma',\bot \Rightarrow \Delta, \bot$ y así es una instancia de L$\bot$; entonces $\Gamma',\bot\Rightarrow\Delta$, el cuál es el mismo que $\Gamma\Rightarrow\Delta$, es también un axioma. Si $\mathcal{D}_0$ termina con una regla en la cual $\bot$ no es principal, digamos, dos premisas, $\mathcal{D}$ es de la forma\\
\begin{prooftree}
\EnableBpAbbreviations
\AXC{$\mathcal{D}_{00}$}
\noLine
\UIC{$\Gamma'\Rightarrow \bot$}
\AXC{$\mathcal{D}_{01}$}
\noLine
\UIC{$\Gamma''\Rightarrow \bot$}
\RightLabel{$R$}
\BIC{$\Gamma\Rightarrow\bot$}
\AXC{$\bot, \Gamma \Rightarrow \Delta$}
\RightLabel{$Cut_{cs}$}
\BIC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent Y para los demás casos tenemos los siguientes árboles.\\
\noindent \textbf{i) Conjunción:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow A$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow B$}
\BinaryInfC{$\Gamma'\Rightarrow A\wedge B,\bot$}
\DisplayProof
\hskip 1.5em
\AxiomC{$\Gamma',A,B\Rightarrow \Delta' $}
\UnaryInfC{$\Gamma',A\wedge B\Rightarrow \Delta'$}
\end{prooftree}
\noindent \textbf{ii) Disyunción:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$A,\Gamma'\Rightarrow \Delta'$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$B,\Gamma\Rightarrow \Delta'$}
\BinaryInfC{$\Gamma',A\vee B\Rightarrow \Delta'$}
\DisplayProof
\hskip 1.5em
\AxiomC{$\Gamma'\Rightarrow A $}
\UnaryInfC{$\Gamma'\Rightarrow A\vee B$}
\end{prooftree}
\noindent \textbf{iii) Implicación:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow A$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$B,\Gamma'\Rightarrow \Delta'$}
\BinaryInfC{$A\rightarrow B,\Gamma\Rightarrow \Delta'$}
\DisplayProof
\hskip 1.5 em
\AxiomC{$A,\Gamma'\Rightarrow B$}
\UnaryInfC{$\Gamma'\Rightarrow A\to B$}
\end{prooftree}
\noindent \textbf{iv) Cuantificador universal:}
\begin{prooftree}
\AxiomC{$\Gamma'[x]\Rightarrow\Delta'$}
\UnaryInfC{$\forall x,\Gamma'\Rightarrow\Delta'$}
\end{prooftree}
\noindent \textbf{iv) Cuantificador existencial:}
\begin{prooftree}
\AxiomC{$\Gamma'\Rightarrow\Delta[x]$}
\UnaryInfC{$\Gamma'\Rightarrow\exists x \Delta'$}
\end{prooftree}
\noindent Luego, las reglas de inferencia son válidas y por lo tanto es correcto considerar a $\mathcal{D}_0$ de tal forma. Esto es transformado por una permutación y duplicación del corte arriba sobre $R$ en la izquierda:
\begin{prooftree}
\EnableBpAbbreviations
\AXC{$\mathcal{D}_{00}$}
\noLine
\UIC{$\Gamma'\Rightarrow\bot$}
\AXC{$\bot,\Gamma'\Rightarrow \Delta'$}
\BIC{$\Gamma'\Rightarrow \Delta'$}
\AXC{$\mathcal{D}_{01}$}
\noLine
\UIC{$\Gamma''\Rightarrow \bot$}
\AXC{$\bot,\Gamma''\Rightarrow\Delta''$}
\BIC{$\Gamma'' \Rightarrow \Delta''$}
\RightLabel{$R$}
\BIC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent Por consiguiente la prueba queda de la siguiente forma:
\begin{prooftree}
\AxiomC{$(\mathcal{D}_{00})^*$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow\Delta'$}
\AxiomC{$(\mathcal{D}_{01})^*$}
\noLine
\UnaryInfC{$\Gamma''\Rightarrow\Delta''$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent \textbf{Verificación de (*):} Debemos ver que $d^*\leq 2\max(d_{00}+1,d_{01}+1)$. En efecto:
\begin{eqnarray*}
d^*&\leq& \max(d_{00},d_{01})\\
&=& \max(d_{00}+1,d_{01}+1)\\
&\leq& 2\max(d_{00}+1,d_{01}+1)
\end{eqnarray*}
\noindent Obteniendo así la ecuación planteada. \\
\noindent {\Large\textbf{Caso 2)}} $\mathcal{D}_0$ y $\mathcal{D}_1$ no son axiomas y la formula de corte no es principal en el sucedente. \\
\noindent\textbf{Clásico:} \\
\noindent Asumimos entonces que $\mathcal{D}$ no es principal en el sucedente y que $\mathcal{D}_0$ termina con dos premisas $R$.
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow \Delta'D$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma''\Rightarrow \Delta'',D$}
\RightLabel{R}
\BinaryInfC{$\Gamma,\Rightarrow \Delta ,D$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$D,\Gamma\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent Lo cuál puede ser transformado por una permutación del corte arriba de $R$ (izquierda)\\
\noindent Ahora, hagamos un análisis de la siguiente prueba, junto con la regla $R$:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow \Delta'D$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma''\Rightarrow \Delta'',D$}
\RightLabel{R}
\BinaryInfC{$\Gamma,\Rightarrow \Delta ,D$}
\end{prooftree}
\noindent \textbf{i) Conjunción:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow \Delta',A,D$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow \Delta',B,D$}
\BinaryInfC{$\Gamma'\Rightarrow \Delta',A\wedge B,D$}
\DisplayProof
\hskip 1.5em
\AxiomC{$\Gamma',A,B\Rightarrow \Delta',D $}
\UnaryInfC{$\Gamma',A\wedge B\Rightarrow \Delta',D$}
\end{prooftree}
\noindent \textbf{ii) Disyunción:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$A,\Gamma'\Rightarrow \Delta',D$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$B,\Gamma'\Rightarrow \Delta',D$}
\BinaryInfC{$\Gamma',A\vee B\Rightarrow \Delta',D$}
\DisplayProof
\hskip 1.5em
\AxiomC{$\Gamma'\Rightarrow A,B,\Delta',D $}
\UnaryInfC{$\Gamma'\Rightarrow A\vee B,\Delta',D$}
\end{prooftree}
\noindent \textbf{iii) Implicación:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow A,\Delta',D$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$B,\Gamma'\Rightarrow \Delta',D$}
\BinaryInfC{$A\rightarrow B,\Gamma'\Rightarrow \Delta',D$}
\DisplayProof
\hskip 1.5 em
\AxiomC{$\Gamma',A\Rightarrow \Delta',B,D$}
\UnaryInfC{$\Gamma'\Rightarrow A\to B,\Delta',D$}
\end{prooftree}
\noindent \textbf{iv) Cuantificador universal:}
\begin{prooftree}
\AxiomC{$\Gamma'[x]\Rightarrow\Delta',D$}
\UnaryInfC{$\forall x,\Gamma'\Rightarrow\Delta',D$}
\end{prooftree}
\noindent \textbf{iv) Cuantificador existencial:}
\begin{prooftree}
\AxiomC{$\Gamma'\Rightarrow\Delta[x],D$}
\UnaryInfC{$\Gamma'\Rightarrow\exists x \Delta',D$}
\end{prooftree}
\noindent Luego, las reglas del sistema clásico funcionan, y haciendo una transformación a la prueba, obtenemos:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}[\Gamma\Rightarrow \Delta]$}
\noLine
\UnaryInfC{$\Gamma,\Gamma'\Rightarrow \Delta,\Delta ',D$}
\AxiomC{$\mathcal{D}_{11}[\Gamma' \Rightarrow \Delta']$}
\noLine
\UnaryInfC{$D,\Gamma,\Gamma'\Rightarrow \Delta, \Delta'$}
\LeftLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma,\Gamma'\Rightarrow \Delta,\Delta '$}
\AxiomC{$\mathcal{D}_{01}[\Gamma\Rightarrow\Delta]$}
\noLine
\UnaryInfC{$\Gamma,\Gamma''\Rightarrow \Delta, \Delta'' D$}
\AxiomC{$\mathcal{D}_{11}[\Gamma''\Rightarrow \Delta '']$}
\noLine
\UnaryInfC{$D,\Gamma,\Gamma''\Rightarrow \Delta,\Delta ''$}
\RightLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma,\Gamma'' \Rightarrow \Delta,\Delta ''$}
\RightLabel{$R$}
\BinaryInfC{$\Gamma,\Gamma\Rightarrow \Delta,\Delta$}
\end{prooftree}
\noindent Llamamos al resultado de la deducción como $\mathcal{D}'$. Sustituyendo $\mathcal{D}'_0$, $\mathcal{D}'_1$ respectivamente por $(\mathcal{D}_0)^*$, $(\mathcal{D}_1)^*$ dada por la hipótesis de inducción produce una deducción $\Delta''$ la cuál después de usar cerraduras bajo la contracción produce $\mathcal{D}^*$. Notemos que $R$ puede en particular ser un corte con rango $\leq {|D|}$. \\
\noindent \textbf{Verificación de (*) en el caso clásico.} Notemos que $d''=d^*$. Tenemos que probar que $d^* \leq \max(d_{00},d_{01})+1+d_1$. por la hipótesis de inducción tenemos que $(d'_0)^* \leq d_{00}+d_1$ y que $(d'_1)*\leq d_{01}+d_1$ y así $d^*\leq\max(d_{00}+d_1,d_{01}+d_1)+1=\max(d_{00},d_{01})+1+d_1$.\\
\noindent\textbf{Intuicionista:} \\
\noindent De nuevo asumimos que $\mathcal{D}$ no es principal en el sucedente y que $\mathcal{D}_0$ termina con dos premisas $R$.
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow D$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma''\Rightarrow D$}
\RightLabel{R}
\BinaryInfC{$\Gamma,\Rightarrow D$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$D,\Gamma\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent Ahora analicemos cada regla en la siguiente expresión:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow D$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma''\Rightarrow D$}
\RightLabel{R}
\BinaryInfC{$\Gamma,\Rightarrow D$}
\end{prooftree}
\noindent \textbf{i) Conjunción:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow A$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow B$}
\BinaryInfC{$\Gamma'\Rightarrow A\wedge B$}
\DisplayProof
\hskip 1.5em
\AxiomC{$\Gamma',A,B\Rightarrow D $}
\UnaryInfC{$\Gamma',A\wedge B\Rightarrow D$}
\end{prooftree}
\noindent \textbf{ii) Disyunción:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$A,\Gamma'\Rightarrow D$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$B,\Gamma'\Rightarrow D$}
\BinaryInfC{$\Gamma',A\vee B\Rightarrow D$}
\DisplayProof
\hskip 1.5em
\AxiomC{$\Gamma'\Rightarrow A $}
\UnaryInfC{$\Gamma'\Rightarrow A\vee B$}
\end{prooftree}
\noindent \textbf{iii) Implicación:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma'\Rightarrow A$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$B,\Gamma'\Rightarrow D$}
\BinaryInfC{$A\rightarrow B,\Gamma'\Rightarrow D$}
\DisplayProof
\hskip 1.5 em
\AxiomC{$\Gamma',A\Rightarrow B$}
\UnaryInfC{$\Gamma'\Rightarrow A\to B$}
\end{prooftree}
\noindent \textbf{iv) Cuantificador universal:}
\begin{prooftree}
\AxiomC{$\Gamma'[x]\Rightarrow D$}
\UnaryInfC{$\forall x,\Gamma'\Rightarrow D$}
\end{prooftree}
\noindent \textbf{iv) Cuantificador existencial:}
\begin{prooftree}
\AxiomC{$\Gamma'\Rightarrow\ D[x]$}
\UnaryInfC{$\Gamma'\Rightarrow\exists x D$}
\end{prooftree}
\noindent Por lo tanto las reglas funcionan, y la prueba toma la forma:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}[\Gamma\Rightarrow ]$}
\noLine
\UnaryInfC{$\Gamma,\Gamma'\Rightarrow D$}
\AxiomC{$\mathcal{D}_{11}[\Gamma' \Rightarrow \Delta']$}
\noLine
\UnaryInfC{$D,\Gamma,\Gamma'\Rightarrow \Delta'$}
\LeftLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma,\Gamma'\Rightarrow \Delta '$}
\AxiomC{$\mathcal{D}_{01}[\Gamma\Rightarrow\Delta]$}
\noLine
\UnaryInfC{$\Gamma,\Gamma''\Rightarrow D$}
\AxiomC{$\mathcal{D}_{11}[\Gamma''\Rightarrow \Delta '']$}
\noLine
\UnaryInfC{$D,\Gamma,\Gamma''\Rightarrow \Delta ''$}
\RightLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma,\Gamma'' \Rightarrow \Delta ''$}
\RightLabel{$R$}
\BinaryInfC{$\Gamma,\Gamma'\Rightarrow \Delta$}
\end{prooftree}
\noindent Luego, aplicando hipótesis por decrecimiento estricto de nivel,
\begin{prooftree}
\AxiomC{$(\mathcal{D}_0')^*$}
\AxiomC{$(\mathcal{D}_1')^*$}
\BinaryInfC{$\Gamma,\Gamma\Rightarrow\Delta $}
\end{prooftree}
\noindent Implica:
\begin{prooftree}
\AxiomC{$D^*$}
\UnaryInfC{$\Gamma\Rightarrow\Delta $}
\end{prooftree}
\noindent \textbf{Verificación de (*) en el caso intuicionista.} Para verificar (*) debemos ver que
\[
d^*\leq 2(\max(d_{00},d_{01})+1+d_1)
\]
\noindent Entonces,
\begin{eqnarray*}
d^*&=& \max((d_0')^*,(d_1')^*)+1 \\
&=&\max(d_{00+d_1,d_{01}+d_1})+1 \\
&\leq& 2(\max(d_{00},d_{01})+d_1+1
\end{eqnarray*}
\noindent Quedando probada la desigualdad. \\
\noindent {\Large\textbf{Caso 3)}} La fórmula de corte es principal en ambos lados. Distingamos dos caso de acuerdo al operador lógico de $D$.\\
\noindent \textbf{Subcaso 3a)} Si $D\equiv D_0 \wedge D_1$ entonces
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow \Delta,D_0$}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow \Delta,D_1$}
\BinaryInfC{$\Gamma\Rightarrow \Delta,D_0\wedge D_1$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$D_0,D_1,\Gamma \Rightarrow \Delta$}
\UnaryInfC{$D_0\wedge D_1,\Gamma\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent Se convierte en lo siguiente:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{01}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow\Delta,D_1$}
\AxiomC{$\mathcal{D}_{00}[D_1\Rightarrow]$}
\noLine
\UnaryInfC{$D_1\Gamma\Rightarrow \Delta, D_0$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$D_0,D_1,\Gamma\Rightarrow \Delta$}
\BinaryInfC{$D_1,\Gamma\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent y similarmente en el caso intuicionista.\\
\noindent \textbf{Verificación de (*)} Debemos probar que $d^*\leq\max(d_{00},d_{01})+1+d_{10}+1=\max(d_{00}+1,d_{01}+1)+d_{10}+1$. De hecho, inspeccionando la construcción de $\mathcal{D}^*$, tenemos que
\begin{eqnarray*}
d^*&\leq & \max(d_{01},\max(d_{00},d_{10})+1)+1\\
&=& \max(d_{01},d_{00}+1,d_{10}+1)+1\\
&\leq & \max(d_{00}+1,d_{01}+1)+d_{10}+1
\end{eqnarray*}
\noindent \textbf{Subcaso 3b)} Si $D\equiv D_0\vee D_1$\\
\noindent \textbf{Clásico:} Supongamos que $D\equiv D_0\vee D_1$, entonces tenemos el siguiente arbol:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow D_0,D_1,\Delta$}
\UnaryInfC{$\Gamma\Rightarrow D_0\vee D_1,\Delta$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$D_0,\Gamma\Rightarrow\Delta$}
\AxiomC{$\mathcal{D}_{11}$}
\noLine
\UnaryInfC{$D_1,\Gamma\Rightarrow \Delta$}
\BinaryInfC{$\Gamma, D_0\vee D_1\Rightarrow \Delta$}
\RightLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent el cual se convierte en
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow D_0,D_1,\Delta$}
\AxiomC{$\mathcal{D}_{00}[\Rightarrow D_1]$}
\noLine
\UnaryInfC{$D_0,\Gamma\Rightarrow \Delta,D_1$}
\BinaryInfC{$\Gamma\Rightarrow D_1,\Delta$}
\AxiomC{$\mathcal{D}_{11}$}
\noLine
\UnaryInfC{$D_1,\Gamma\Rightarrow\Delta$}
\RightLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent \textbf{Verificación de (*):} Debemos ver que $d^*\leq \max(d_{10},d_{11})+1+d_{00}+1=\max(d_{10}+1,d_{11}+1)+d_{00}+1$\\
\noindent Analizando $\mathcal{D}^*$ obtenemos lo siguiente:
\begin{eqnarray*}
d^*&=&\max(d_{11},\max(d_{00},d_{01})+1)+1)\\
&=& \max(d_{11},\max(d_{00}+1,d_{01}+1))+1\\
&=& \max(d_{11},d_{00}+1,d_{10}+1)+1\\
&\leq & \max(d_{10}+1,d_{11}+1)+d_{00}+1
\end{eqnarray*}
\noindent \textbf{Intuicionista: } En este caso tenemos lo siguiente:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow D_0\vee D_1$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$D_0,\Gamma\Rightarrow\Delta$}
\AxiomC{$\mathcal{D}_{11}$}
\noLine
\UnaryInfC{$D_1,\Gamma\Rightarrow\Delta$}
\RightLabel{L$\vee$}
\BinaryInfC{$D_0\vee D_1,\Gamma\Rightarrow \Delta$}
\RightLabel{$Cut_{int}$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent Así
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow D_0$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$D_0,\Gamma\Rightarrow\Delta$}
\RightLabel{$Cut_{int}$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent \textbf{Verificación de (*):} Probemos ahora que $d^*\leq 2(\max(d_{10},d_{11})+1+d_{00}+1)=2(\max(d_{10}+1,d_{11}+1)+d_{00}+1)$. En efecto:
\begin{eqnarray*}
d^*&=&2(\max(d_{00},d_{10})+1)\\
&\leq & 2(\max(d_{10}+1,d_{11}+1)+d_{00}+1)\\
&=& 2(\max(d_{00}+1,d_{10}+1))\\
&\leq & 2(\max(d_{00},d_{11}+1)+d_{00}+1)
\end{eqnarray*}
\noindent \textbf{Subcaso 3c)} $D\equiv D_0 \to D_1$. La deducción en \textbf{G3c} tiene la siguiente forma:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma , D_0\Rightarrow D_1,\Delta$}
\UnaryInfC{$\Gamma\Rightarrow D_0\to D_1,\Delta$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\Gamma \Rightarrow D_0, \Delta$}
\AxiomC{$\mathcal{D}_{11}$}
\noLine
\UnaryInfC{$\Gamma,D_1\Rightarrow \Delta$}
\BinaryInfC{$\Gamma,D_0\to D_1\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent Árbol que se se transforma en una deducción $\mathcal{D}'$
\begin{prooftree}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow D_0,\Delta$}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma,D_0 \Rightarrow D_1, \Delta$}
\AxiomC{$\mathcal{D}_{11}[D_0\Rightarrow]$}
\noLine
\UnaryInfC{$\Gamma,D_0,D_1\Rightarrow \Delta$}
\BinaryInfC{$\Gamma,D_0\to D_1\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent El nuevo corte sobre $D_0\to D_1$ tiene un nivel menor que el original; luego, por la hipótesis de inducción podemos remover este corte.\\
\noindent \textbf{Verificación de (*)} Veamos que $d^*\leq \max(d_{10},d_{11})+1+d_{00}+1=\max(d_{10}+1,d_{11}+1)+d-{00}+1$:
\begin{eqnarray*}
d^*&=&\max(\max(d_{00},d_{11})+1,d_{00})+1\\
&=& \max(d_{00}+1,d_{11}+1,d_{10})+1\\
&\leq & \max(d_{11}+1,d_{10}+1)+d_{00}+1
\end{eqnarray*}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma , D_0\Rightarrow D_1$}
\UnaryInfC{$\Gamma\Rightarrow D_0\to D_1$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\Gamma,D_0\to D_1 \Rightarrow D_0$}
\AxiomC{$\mathcal{D}_{11}$}
\noLine
\UnaryInfC{$\Gamma,D_1\Rightarrow A$}
\BinaryInfC{$\Gamma,D_0\to D_1\Rightarrow A$}
\BinaryInfC{$\Gamma\Rightarrow A$}
\end{prooftree}
\noindent El cual es sustituido por el siguiente:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma D_0\Rightarrow D_1$}
\UnaryInfC{$\Gamma\Rightarrow D_0\to D_1$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\Gamma,D_0\to D_1 \Rightarrow D_0$}
\RightLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma\Rightarrow D_0$}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma D_0\Rightarrow D_1$}
\RightLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma \Rightarrow D_1$}
\AxiomC{$\mathcal{D}_1$}
\noLine
\UnaryInfC{$\Gamma D_1\Rightarrow A$}
\RightLabel{$Cut_{cs}$}
\BinaryInfC{$\Gamma\Rightarrow A$}
\end{prooftree}
\noindent El nuevo corte sobre $D_0\to D_1$ tiene un nivel menor y por tanto podemos remover el corte utilizando la hipótesis de inducción. Sustituimos $\mathcal{D}'_{00}$ por $(\mathcal{D}'_{00})$ y la deducción resultante es $\mathcal{D}^*$ (y $(\mathcal{D}^*_{00})=(\mathcal{D}'_{00})^*$).\\
\noindent \textbf{Verificación de (*):} En el caso intuicionista, tenemos que probar lo siguiente:
\begin{equation*}
d^*\leq 2(d_{00}+1+\max(d_{10},d_{11})+1)=\max(2d_{00}+2d_{10}+4,2d_{00}+2d_{11}+4) \qquad \dagger
\end{equation*}
\noindent La deducción $(\mathcal{D}^*)_{00}$ satisface
\begin{eqnarray*}
d^*&\leq &\max(\max(2d_{00}+2d_{100}+2,d_{00})+1,d_{11})+1\\
&=& \max(2d_{00}+2d_{10}+4,d_{00}+2,d_{11}+1)
\end{eqnarray*}
\noindent y esto es mas pequeño que el lado derecho de $\dagger$.\\
\noindent \textbf{Subcaso 3d)} Supongamos que $D\equiv \forall x D_0$, con $y\not\in FV(D_0,\Gamma,\Delta), y\not\in FV(t)$. \\
\noindent \textbf{Clásico:} \\
\noindent Transformemos el siguiente árbol:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma \Rightarrow \Delta , D_0[x/y]$}
\UnaryInfC{$\Gamma\Rightarrow \Delta,\forall x D_0$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\forall x D_0, D_0[x/t],\Gamma \Rightarrow \Delta$}
\UnaryInfC{$\forall x D_0,\Gamma\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent en
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}[y/t]$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow \Delta, D_0[x/t]$}
\AxiomC{$\mathcal{D}_{00}[D_0[x/t]\Rightarrow]$}
\noLine
\UnaryInfC{$D_0[x/t],\Gamma\Rightarrow \Delta,D_0 [x/y]$}
\UnaryInfC{$D_0[x/t],\Gamma\Rightarrow \Delta,\forall xD_0$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\forall x D_0,D_0[x/t],\Gamma\Rightarrow\Delta$}
\BinaryInfC{$D_0[x/t],\Gamma\Rightarrow\Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent La subdeducción $\mathcal{D}'$ finaliza en el corte sobre $\forall x D_0$ y es de nivel menor. Así que podemos sustituirla (por la hipótesis de inducción) por $(\mathcal{D}')^*$, lo que produce la $\mathcal{D}^*$ requerida.\\
\noindent \textbf{Verificación de (*) en el caso clásico.} Tenemos que probar que $d^*\leq d_{00}+d_{10}+2;$ para $\mathcal{D}^*$ tenemos:
\begin{equation*}
d^*\leq \max(d_{00},d_{00}+1+d_{10})+1=\max(d_{00}+d_{10}+2,d_{00}+1)=d_{00}+d_{10}+2.
\end{equation*}
\noindent Lo cual prueba lo requerido. \\
\noindent \textbf{Intuicionista:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma \Rightarrow D_0[x/y]$}
\UnaryInfC{$\Gamma\Rightarrow \forall x D_0$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\forall x D_0, D_0[x/t],\Gamma \Rightarrow \Delta$}
\UnaryInfC{$\forall x D_0,\Gamma\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent Esto se convierte en
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}[y/t]$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow D_0[x/t]$}
\AxiomC{$\mathcal{D}_{00}[D_0[x/t]\Rightarrow]$}
\noLine
\UnaryInfC{$D_0[x/t],\Gamma\Rightarrow D_0 [x/y]$}
\UnaryInfC{$D_0[x/t],\Gamma\Rightarrow \forall xD_0$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\forall x D_0,D_0[x/t],\Gamma\Rightarrow\Delta$}
\BinaryInfC{$D_0[x/t],\Gamma\Rightarrow\Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent \textbf{Verificación de (*) en el caso intuicionista.} Tenemos que probar que:
\[
d^*=2(\max(d_{00},d_{10})+1)=2(\max(d_{00}+1,d_{10}+1)=\max(d_{00}+2,d_{10}+2)
\]
\noindent Entonces,
\begin{eqnarray*}
d^*&=&\max(d_{00},\max(d_{00},d_{10})+1)+1 \\
&=& \max(d_{00},d_{00}+1,d_{10}+1)+1 \\
&=& \max(d_{00}+1,d_{10}+1)+1 \\
&=& \max(d_{00}+2,d_{10}+2) \\
&\leq& \max(2d_{00}+2,2d_{10}+2)
\end{eqnarray*}
\noindent y por lo tanto se cumple la desigualdad.\\
\noindent \textbf{Subcaso 3e)} $D\equiv \exists x D_0$. \\
\noindent \textbf{Clásico:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\Gamma \Rightarrow \Delta ,D_0[x/y]$}
\UnaryInfC{$\Gamma\Rightarrow \Delta,\exists x D_0$}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma, D_0[x/t], \Rightarrow \Delta$}
\UnaryInfC{$\Gamma,\exists x D_0,\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent Luego,
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}[\Rightarrow D_0[x/y]] $}
\noLine
\UnaryInfC{$\Gamma\Rightarrow\Delta,\exists x D_0,D_0[x/y] $}
\AxiomC{$\mathcal{D}_{10}[D_0[x/t]\Rightarrow] $}
\noLine
\UnaryInfC{$D_0[x/t],\Gamma\Rightarrow\Delta,D_0[x/y]$}
\UnaryInfC{$\exists x D_0,\Gamma\Rightarrow\Delta, D_0[x/y] $}
\BinaryInfC{$\Gamma\Rightarrow\Delta,D_0[x/y]$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$D[x/y],\Gamma\Rightarrow\Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent \textbf{Verificación de (*) en el caso clásico.} Veasmos que:
\[
d^*\leq d_{00}+1 + d_{10}+1= d_{00}+d_{10}+2
\]
\noindent Tenemos que,
\begin{eqnarray*}
d^*&=&\max(d_{10},\max(d_{00},d_{10})+1)+1 \\
&=& \max(d_{10},\max(d_{00}+1,d_{10}+1))+1 \\
&=& \max(d_{10},d_{00}+1,d_{10}+1)+1 \\
&=& \max(d_{00}+1,d_{10}+1)+1 \\
&=& \max(d_{00}+2,d_{10}+2) \\
&\leq& d_{00}+d_{10}+2
\end{eqnarray*}
\noindent \textbf{Intuicionista:}
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma \Rightarrow D_0[x/y]$}
\UnaryInfC{$\Gamma\Rightarrow \exists x D_0$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$\Gamma, D_0[x/t], \Rightarrow \Delta$}
\UnaryInfC{$\Gamma,\exists x D_0,\Rightarrow \Delta$}
\BinaryInfC{$\Gamma\Rightarrow \Delta$}
\end{prooftree}
\noindent Transformando esta expesión obtenemos:
\begin{prooftree}
\AxiomC{$\mathcal{D}_{00}$}
\noLine
\UnaryInfC{$\Gamma\Rightarrow\exists x D_0, $}
\AxiomC{$\mathcal{D}_{10}[D_0[x/t]\Rightarrow] $}
\noLine
\UnaryInfC{$D_0[x/t],\Gamma\Rightarrow D_0[x/y]$}
\UnaryInfC{$\exists x D_0,\Gamma\Rightarrow D_0[x/y] $}
\BinaryInfC{$\Gamma\Rightarrow D_0[x/y]$}
\AxiomC{$\mathcal{D}_{10}$}
\noLine
\UnaryInfC{$D[x/y],\Gamma\Rightarrow\Delta$}
\BinaryInfC{$\Gamma\Rightarrow\Delta$}
\end{prooftree}
\noindent \textbf{Verificación de (*) en el caso intuicionista.} Veamos que:
\[
d^*\leq 2(d_{00}+1+d_{10}+1)=2(d_{00}+d_{10}+2)=2d_{00}+2d_{10}+4
\]
\noindent $\mathcal{D}^*$ obtenemos:
\begin{eqnarray*}
d^*&=&\max(\max(d_{00},d_{10})+1),d_{10})+1 \\
&=& \max(d_{00}+1,d_{10}+1,d_{10})+1 \\
&=& \max(d_{00}+1,d_{10}+1)+1 \\
&=& \max(d_{00}+2,d_{10}+2) \\
&\leq& 2d_{00}+2d_{10}+4
\end{eqnarray*}
\noindent y así se cumple la desigualdad.\\\\
\noindent Con esto, completamos la demostración del teorema. $\hfill \blacksquare$
\end{document}
