¿Cómo se demuestra la decidibilidad de la lógica proposicional intuicionista, dada la propiedad de la subfórmula si una fórmula $A \rightarrow B$ es una subfórmula de sí misma?
Dos de los textos que estoy leyendo dicen que esta prueba es inmediata, pero qué impide que uno aplique repetidamente una regla como:
$\Gamma \vdash A \rightarrow B \\ ----- \\ \Gamma \vdash A \rightarrow B$
¿Es que la decidibilidad no es realmente inmediata a partir de la sola propiedad de la subfórmula y estos autores están apelando implícitamente a las reglas específicas de la lógica en cuestión, o me estoy perdiendo algo?
En otras palabras, ¿la decidibilidad sólo se desprende de una propiedad ligeramente más fuerte como la propiedad de la subfórmula adecuada, o de algún otro orden estrictamente decreciente en los secuentes?
Estoy mirando específicamente a Girard Pruebas y tipos en el que dice que la decidibilidad es un "corolario inmediato" del teorema de normalización débil de la página 24.
