Decidibilidad de la completitud en lógica proposicional

Question

La lógica proposicional puede presentarse como en el libro de Mendelson, con la única regla de inferencia del modus ponens, y con los tres axiomas siguientes: $$B \Rightarrow (C \Rightarrow B)$$ $$(B \Rightarrow (C \Rightarrow D)) \Rightarrow ((B \Rightarrow C) \Rightarrow (B \Rightarrow D))$$ $$((\neg C) \Rightarrow (\neg B)) \Rightarrow (((\neg C) \Rightarrow B) \Rightarrow C)$$ Se trata de una teoría sólida y completa, al igual que otras teorías de la lógica proposicional.

Tengo preguntas sobre teorías similares para la lógica proposicional:

1. Dado un conjunto completo de conectivas lógicas y un conjunto finito de axiomas y reglas de inferencia sólidos, ¿podemos determinar algorítmicamente si la teoría resultante es completa?

2. Dado un conjunto finito de axiomas y reglas de inferencia $X$ (no necesariamente sólida) y una fórmula $\alpha$ en el lenguaje subyacente de las conectivas proposicionales, ¿podemos determinar algorítmicamente si $\alpha$ puede derivarse de $X$ ?

Answer 1

Es indecidible, porque incluso es indecidible reconocer si un conjunto finito de axiomas junto con la regla del modus ponens axiomatiza exactamente la lógica proposicional clásica por el teorema de Post-Linial. Esto fue demostrado en 1948 por Linial y Post, véase su anuncio (p. 50) pero la primera publicada prueba es de Yntema. Hay muchos resultados similares para otras lógicas proposicionales.