Cálculo proposicional: ¿La compacidad implica la completitud?

Question

¿Existe una forma rápida de demostrar el teorema de completitud (toda teoría consistente tiene un modelo) a partir del teorema de compacidad (una teoría tiene un modelo si toda subteoría finita de la misma tiene un modelo)? Normalmente el teorema de la compacidad es un resultado muy fácil del teorema de la completitud, pero también se puede demostrar de otras maneras (por ejemplo, utilizando el teorema de Tychonoff) y me pregunto si esto proporciona un "atajo" al teorema de la completitud.

Sólo pregunto por el cálculo proposicional, pero si lo mismo vale para la lógica de primer orden también me alegraré de oírlo.

Answer 1

Está claro que el teorema de compacidad reduce el teorema de completitud a su caso finito: "si una teoría finita es consistente entonces tiene un modelo".

En el caso de la lógica proposicional, dependiendo del sistema de prueba que se elija, esa forma finita puede ser relativamente sencilla de probar, porque un conjunto finito $F$ de fórmulas proposicionales sólo menciona un número finito de variables, por lo que realmente sólo hay $2^n$ casos a considerar en los que $n$ es el número de variables. Así, por ejemplo, en un sistema de tablas el árbol para un conjunto finito de fórmulas proposicionales será finito. En otros sistemas de prueba, se puede utilizar una regla deductiva como $(A \to \phi) \to (\lnot A \to \phi) \to \phi$ , aplicado $n$ veces, una por cada variable $A$ mencionado por las fórmulas, dejando $\phi$ sea $(\bigwedge F) \to \bot$ . La cuestión es hacer la deducción esencialmente una prueba por casos que considere todos $2^n$ filas de una tabla de verdad para $F$ .

Este método no funciona tan bien para la lógica de primer orden porque, aunque una teoría sólo tenga un número finito de fórmulas, suele haber infinitos términos de los que preocuparse. Por ejemplo, en el entorno de las tablas, el árbol puede ser infinito aunque la teoría sea finita.

Answer 2

Este es un boceto de una prueba que puede encontrar en R. "Una introducción a la teoría de la prueba" de Buss . Lo interesante es que es directo, en el sentido de que no crea un modelo para una teoría consistente sino que demuestra que la consecuencia lógica implica la demostrabilidad.

Quiere demostrar que $\Gamma\models\phi$ puis $\Gamma\vdash\phi$ . Supongamos que $\Gamma\models\phi$ . Utilizando la compacidad esto implica que un subconjunto finito de $\Gamma$ , $\{\psi_1,\ldots\psi_n\}\models\phi$ o, por el contrario $\models\psi_1\to(\psi_2\to\ldots(\psi_n\to\phi)\ldots)$ . Por lo tanto, sólo necesitas que las tautologías sean demostrables.

Para demostrarlo, primero hay que probar que dado $\phi$ y $p_0,\ldots,p_n$ los átomos de $\phi$ , si $f:n+1\to 2$ puis $$(\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\phi\textrm{ or } (\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\lnot\phi$$ (donde $(\lnot)^1=\lnot$ y $(\lnot)^0$ no es nada). Se puede hacer esto por inducción en la complejidad de $\phi$ , dadas algunas afirmaciones sencillas demostrables sobre las conectivas.

Ahora observe que si $\Gamma,\sigma\vdash\chi$ y $\Gamma,\lnot\sigma\vdash\chi$ puis $\Gamma\vdash\chi$ . Dada una tautología $\phi$ por la solidez se tiene que por cada $f:n+1\to2$ es el caso que $(\lnot)^{f(0)}p_0,\ldots,(\lnot)^{f(n)}p_n\vdash\phi$ . A continuación, utilizando lo anterior eliminar los átomos proposicionales uno por uno para llegar a que $\vdash\phi$ .