¿Integridad lógica Infinitary?

Question

He oído un rumor de que hay una prueba de sistema para ciertas infinitary lógicas, dado por Carol Karp (?) en su tesis, pero no puedo encontrar una copia. El resultado que me han dicho que existe es la siguiente:

• Una frase $\phi$,$L_{\omega_1\omega}$, tiene un modelo si y sólo si es coherente; es decir, no hay ninguna prueba (en el anterior sentido) de $\phi$ de una falsa frase (por ejemplo,$\exists x (x\not=x)$)
• Esto no es cierto para general $L_{\infty\omega}$ frases; es decir, hay una frase con ningún modelo. (De lo contrario debería ser trivial; cualquier frase con un modelo debe ser coherente)

Lo que realmente me gusta es una descripción de este sistema a prueba. Pensé que podría "adivinar" por mi cuenta, pero supongo que no puedo. Sospecho que, una vez dado, que las pruebas de los anteriores teoremas son relativamente fáciles. De hecho, tengo la sentencia, lo cual es consistente con ningún modelo, a pesar de que claramente no tengo una precisa argumento de la coherencia sin la prueba del sistema.

Soy consciente de algunos modelos de teoremas de existencia (por ejemplo, Makkai), que son probablemente equivalente a la anterior. Pero de verdad que estoy a la caza de la prueba del sistema.

Answer 1

Así que yo no sé acerca de Karp del trabajo en este ámbito (y google no parece saber tanto), pero sí sé que López-Escobar desarrollado un sistema a prueba de $L_{\omega_1\omega}$. Creo que este fue originalmente hecho en su Tel. D. tesis, "Infinitamente larga fórmulas contables cuantificador grados," que no tengo acceso. Sin embargo, su papel http://matwbn.icm.edu.pl/ksiazki/fm/fm57/fm57119.pdf describe y muestra que cumple con un corte de eliminación del teorema. A simple vista, parece fácil generalizar que la prueba del sistema (pero no la metatheorems de curso) a $L_{\infty\omega}$, por lo que este puede ser lo que estás buscando.

Nota al margen: por una barra mejorado mucho en esto, por el desarrollo de los sistemas de prueba de fragmentos de $L_{\omega_1\omega}$: dada la admisión de un conjunto de $A$, vamos a $L_A=L_{\omega_1\omega}\cap A$. A continuación, Barwise define una colección de $P$ de la prueba-los objetos que $P\cap A$ $\Delta_1$ $A$ y completa para $L_A$; vea la página 14 de la "Barwise: infinitary lógica y admisible conjuntos" por Keisler y Caballero. Creo que por una barra' a prueba de sistema(s) se discuten en Keisler del "Modelo de la teoría de infinitary lógica" y Barwise' "Admisible conjuntos y estructuras", pero en realidad nunca he usado. Yo sé que él tiene una reputación de ser tedioso para trabajar directamente, aunque la metatheorems uno recibe son bastante útiles. (E. g., el Barwise Teorema de Compacidad puede ser demostrado mediante este sistema, si recuerdo correctamente).