Las pruebas son las mismas y sólo cambia la terminología.
La longitud de una fórmula ( peso en [NvP2001]) corresponde al número de conectivas que tiene ( grado en [T1987]). Esto se debe a que todas las conectivas son binarias (la negación puede traducirse en implicación a falsedad, $\neg A\equiv A\to\bot$ ).
Así que la inducción externa es la misma en ambas pruebas. Entonces, para cada $n$ de la inducción externa, ambas pruebas utilizan una inducción interna sobre la alto / rango de la derivación de la fórmula con longitud o peso $n$ .
Alto de una derivación es el número máximo de reglas sucesivas, es decir, el recorrido máximo del árbol de pruebas de la derivación. Así, teniendo una fórmula de longitud $n$ fijado a partir de la inducción exterior, digamos $Q$ es el secuente que concluye esa fórmula. Entonces, [NvP2001] hace la inducción interna sobre el mayor recorrido de las derivaciones de las premisas de $Q$ es decir, el camino más largo del subárbol que $Q$ define.
Rango de una derivación es el número máximo de secuentes consecutivos que empiezan a contar a partir de un secuente $J$ . Pero si pones $J=Q$ entonces se ve que la altura de las derivaciones de las premisas de $Q$ es exactamente igual que el rango de la prueba entera $P$ con respecto a $Q$ . Es decir, en la demostración de [T1987], después de haber fijado una fórmula de grado $n$ hace la inducción interna en el rango de toda la prueba $P$ donde $J$ es el secuente que concluye la fórmula que se fija a partir de la inducción externa (que es $Q$ ). Entonces, el rango de $P$ con respecto a $J$ es el camino máximo del subárbol que $J$ define. Esto es exactamente lo mismo que la altura de las derivaciones de las dos premisas de $J$ donde $J=Q$ .
Cuando se realizan dos inducciones, se puede definir una inducción doble, es decir un inducción en un variable que tiene paridad dos y sobre la que se hace la inducción total. Entonces, Takeuti dice que la variable, $v$ de la inducción total (interna y externa juntas) es $v(g,r)=\omega\cdot g+r$ . Atención que $\omega\cdot g+r$ es un nuevo variable definidos en los dos anteriores. Lo que ha declarado ser $\omega\times\omega$ es el espacio de la que $v$ toma valores. En realidad, la expresión $\omega\cdot g+r$ define una jerarquía en las dos inducciones. En este caso, significa que la inducción sobre $r$ es una subinducción de la inducción sobre $g$ . Esto se debe a que $v(g,r)=\omega g +r=g+r=\max\{g,r\}$ ( $\omega g$ es la intersección de $\omega$ y $g$ que es, por supuesto $g$ y $g+r$ es la unión de $g$ y $r$ que es su máximo). Por lo tanto, tiene variable $v$ definido como: $$v(g,r)= \begin{cases} g,~\text{ if } g\geq r\\ r,~\text{ if } g< r \end{cases}$$
Pero esto es lo mismo que hacer una inducción externa en $g$ y luego hacer una inducción interna sobre $r$ para $r\leq g$ . Porque si la inducción exterior está en $g$ esto significa que $v(g,r)=g\Rightarrow r\leq g$ . Por lo tanto, a continuación, hacer su inducción interna en $r$ .
