Hacemos una revisión profunda cada uno de los posts en nuestra página web con el objetivo de enseñarte en todo momento información veraz y actual.
Solución:
No, no puede haber un procedimiento de decisión para la lógica de predicados intuicionista. Si lo hubiera, entonces mediante la traducción de doble negación podríamos usarlo para decidir la lógica clásica de predicados, que se sabe que es indecidible.
(Los cuadros no son un procedimiento de decisión para la lógica de predicados clásica, porque no se garantiza que terminen en presencia de cuantificadores).
Editar: La pregunta fue cambiada para hablar de intuicionista de la proposición cálculo. Eso sí que es decidible; un procedimiento de decisión es buscar una prueba libre de cortes en el cálculo secuencial intuicionista LJ. Dado que cada fórmula en una prueba sin cortes ni cuantificadores es una subfórmula de la conclusión final, solo hay un número finito de secuencias posibles que no repiten fórmulas a la izquierda del torniquete, por lo que incluso una búsqueda de prueba de fuerza bruta será Terminar.
A pesar de que ya aceptó la respuesta de Henning Makholm, esto parecía ser de alguna utilidad y era demasiado grande para un comentario, por lo que lo publicaré de todos modos.
Encontré material relacionado con su pregunta en las páginas 33 y 34 de Conferencias sobre el isomorfismo de Curry-Howard por Sorensen y Urzyczyn. En particular (teorema 2.4.8 y discusión circundante):
A [intuitionistic propositional] la fórmula de longitud $n$ es válida si es válida en todas las álgebras de cardinalidad de Heyting como máximo $2^2^n$.
Esto podría ser factible para comprobar a mano si $n<3$. Creo que por "longitud" aquí quieren decir "número de variables". Esbozan la prueba y remiten al lector a Rasiowa y Sikorski. Las Matemáticas de las Metamatemáticas (Varsovia 1963) para más detalles.
El siguiente bit es quizás más interesante:
Del teorema anterior se sigue que la lógica proposicional intuicionista es decidible. Pero el límite superior obtenido de esta manera (doble espacio exponencial) se puede mejorar hasta el espacio polinomial, con la ayuda de otros métodos, ver…
Esta vez la referencia es R. Statman. “La lógica proposicional intuicionista es un espacio polinomial completo”. Informática Teórica9:67–72, 1979.
Espero que esto sea de alguna utilidad.
Gentzen fue el primero en mostrar decidibilidad. Los artículos sobre 1990 de Jörg Hudelmaier (que dan un procedimiento de decisión en el espacio O(n log n)) y mío (Roy Dyckhoff) deben ser estudiados por cualquier persona interesada en utilizar dicho procedimiento. Estos muestran (siguiendo el trabajo anterior de Vorob’ev en 1950) cómo evitar la verificación de bucles en una búsqueda de cálculo secuencial de raíz primero. Evitar el retroceso es un problema más difícil… El cálculo apropiado G4ip está cubierto en el texto estándar, Teoría de prueba básica. La biblioteca ILTP en Potsdam (mantenida por Jens Otten) enlaza con implementaciones y clases de problemas. El uso de grandes álgebras de Heyting no es realmente la mejor manera de hacerlo…