Cálculo de la altura/profundidad de un corte en Sequent Calculus

Question

Me cuesta entender el cálculo de una idea, que se llama "altura de corte" en la obra de Negri y von Plato Teoría de la prueba estructural (SPT), y la "profundidad de un corte" en Troelstra y Schwichtenberg Teoría básica de la prueba (BPT).

La altura de corte, según SPT, es la siguiente:

Y la profundidad de un corte como se define en BPT:

Por lo que tengo entendido, "altura" en SPT significa lo mismo que "profundidad" en BPT. Si comparamos la formulación de la altura de corte con la propiedad (*), también parecen decir lo mismo.

---

Pero mirando el ejemplo de abajo de BPT, habría esperado que para el corte en el 2º cálculo secuencial de abajo tuviera una altura/profundidad de corte de $d_{01}+(d_{00}+d_{10})+1$ . Pero BPT lo pone como $\max(d_{00},d_{01})+1+d_{10}+1$ .

Entonces, ¿por qué el $\max(d_{00},d_{01})$ ? (¿Y qué es toda la transformación que está haciendo allí?) ¿Me equivoco al pensar que tanto SPT como BPT están hablando de lo mismo?

---

EDIT: Añadiendo la definición de profundidad de BPT a continuación

Answer 1

La definición de altura de corte en SPT (p. 35) es la misma que la definición de nivel de un corte en BPT (p. 93).

Nótese que la noción de altura de corte en SPT se refiere al tamaño de una ocurrencia la regla de corte en una derivación; mientras que, en BPT, la noción de profundidad se refiere al tamaño de un todo derivación. Su definición en BPT se da en general como la profundidad de un árbol, ver p. 9. Como las derivaciones son casos especiales de árboles (cuyos nodos son secuencias), esto proporciona también una definición de profundidad de una derivación $\mathcal{D}$ : es el mayor número de aplicaciones sucesivas de no $0$ -reglas de la vida en un rama de $\mathcal{D}$ (por lo que coincide con la definición de altura de $\mathcal{D}$ en SPT, p. 30).

Incluso en el caso de la demostración del Teorema 4.1.5 en BPT (lo que te interesa), las nociones de profundidad de una derivación y altura de corte de un corte no coinciden, incluso si estás considerando sólo derivaciones cuya última regla es un corte y comparas la profundidad de tales derivaciones con la altura de corte de tal (último) corte. En efecto, la altura de corte de un corte $c$ es (en la terminología de BPT) el suma de las profundidades de las dos derivaciones que son premisas $c$ no su máximo (o su máximo más $1$ ).

Concretamente, respecto a su caso 3a en la demostración del Teorema 4.1.5 en BPT, si $\mathcal{D}^*$ es la derivación \begin{align} \dfrac{\overset{\mathcal{D}_{01}}{\Gamma \Rightarrow \Delta, D_1} \qquad \dfrac{\overset{\mathcal{D}_{00}[D_1 \Rightarrow]}{\Gamma \Rightarrow \Delta, D_0} \qquad \overset{\mathcal{D}_{10}}{D_0, D_1, \Gamma \Rightarrow \Delta}} {D_1, \Gamma \Rightarrow \Delta}\text{cut}_\text{cs} }{\Gamma \Rightarrow \Delta}\text{cut}_\text{cs} \end{align} entonces la profundidad de $\mathcal{D}^*$ es $d^* = \max ({d_{01}}, \max (d_{00}, d_{10}) + 1) + 1$ como se indica correctamente en la p. 97.