Algunas preguntas acerca de Smullyan ' s prueba del teorema de compacidad para lógica proposicional

Question

Según Jeremy Avigad la descripción de Gödel original del argumento (http://www.andrew.cmu.edu/user/avigad/Papers/goedel.pdf) el segundo paso en la prueba de establecer el siguiente resultado :

Si un conjunto $S$ de fórmulas proposicionales no es rebatible, tiene la satisfacción de la verdad asignación.

Vamos $S$ = {$\phi_0, \phi_1, \phi_2$, . . .}. Construir un finitely ramificación de los árboles donde los nodos en el nivel uno son todos la verdad de las asignaciones a las variables de $\phi_0$ que hacen de $\phi_0$ true; los nodos en el nivel dos son toda la verdad de las asignaciones las variables de $\phi_0 \land \phi_1$ que hacen que la fórmula de la verdad; y así sucesivamente. (Los descendientes de un nodo son todos la verdad de las asignaciones que se extienden.) Si, en algún nivel,$k$, no hay ninguna que cumpla la asignación a $\phi_0 \land \phi_1 \land . . . \land \phi_{k−1}$, $S$ es rebatible. De lo contrario, por Konig el lema, hay un camino a través del árbol, que corresponde a la satisfacción de la verdad asignación de $S$.

Creo que este es el básico de la construcción se utiliza en R. Smullyan, la Lógica de Primer Orden (1968 - Dover reimpresión) para la prueba del Teorema de Compacidad para la lógica proposicional (pag.30).

Pregunta 1) ¿tengo razón ?

En la pag.34 Smullyan da el siguiente argumento :

"queremos señalar que a pesar de que utiliza [...] Konig del lexema en nuestra prueba del teorema de compacidad, [no es] realmente esencial."

Después de la construcción (pag.36), se discute el resultado :

"La anterior prueba en ningún lugar se utiliza Konig del lexema [...]. La anterior construcción en efecto genera la izquierda infinito rama de la completa de tableau para $S$."

Pregunta 2) ¿En qué sentido se puede prescindir de Konig del lema ?

Mi última preocupación es con tableaux método como un procedimiento a prueba (para la lógica proposicional).

Suponga que $A$ es una tautología (o, si $S$ es un finito conjunto de fórmulas, vamos a $A$ su conjunto, por lo que no hay realmente una limitación en la consideración de una única fórmula).

La aplicación del método, se puede construir, en un finito número de pasos, un tableau cerrado $\mathcal{T}$ ($A$ es una tautología).

Debido al hecho de que estamos tratando con una sola fórmula (o un finito conjunto de ellos) que explotan la propiedad de que estamos construyendo un árbol de $\mathcal{T}$, en la que cada rama es finito.

Pregunta 3) Si no es necesario Konig del lema para la prueba de este hecho, puedo decir que este es un constructiva prueba procedimiento para la lógica proposicional ?

Answer 1

Como Benedicto Eastaugh, dice en un comentario, el teorema de compacidad no puede ser probado sin alguna forma de Konig del lexema o de otros "no constructiva" de los principios.

En el contexto de las teorías contables, que puede ser estudiado con la Inversa de las Matemáticas, el teorema de compacidad es equivalente a la debilidad de Konig del lema sobre la base de sistema de $\mathsf{RCA}_0$. Débil Konig del lema dice que cada árbol infinito de 0s y 1s tiene una infinita rama.

En el contexto de la teoría de conjuntos, el teorema de compacidad de teorías arbitrarias es equivalente a la Booleano Primer Ideal Teorema, llamado también el Ultrafilter Lema. Ver esta respuesta en las matemáticas.SE.

Es difícil de decir de las citas breves exactamente lo Smullyan está tratando de decir. Sin embargo, puedo decir que el principio de "cada árbol infinito de 0s y 1s tiene una izquierda infinito rama", que él parece haber llamado la atención, es que en realidad más fuerte que "cada árbol infinito de 0s y 1s tiene una infinita rama" (que es débil Konig del lema). Trivialmente, el primero es al menos tan fuerte como el último. Pero, por ejemplo, en el Reverso de las Matemáticas, el primero es equivalente a $\mathsf{ACA}_0$ que es bastante más que el segundo (débil Konig del lema) sobre la base estándar del sistema. El hecho de que la rama de la izquierda puede ser construido "hands-on" es engañosa, en un sentido, porque la construcción nos obliga a veces a responder las preguntas que pueden ser respondidas de manera constructiva (es decir, "es este subárbol infinito?").

Tal vez lo que Smullyan significa es que él es capaz de evitar la invocación de Konig del lexema mediante la incorporación de su prueba en la prueba de su resultado. Que es ciertamente posible.

Y, para la tercera pregunta, tanto el tableau método y la tabla de verdad del método constructivo a prueba de procedimientos para el clásico de la lógica proposicional.