Exhaustividad frente a compacidad en lógica

Question

Un enfoque estándar para demostrar la compacidad de la lógica de primer orden es demostrar la completitud, de la que la compacidad es un corolario fácil. Me han dicho que este enfoque está en desuso hoy en día, ya que la compacidad se considera el resultado "más profundo".

¿Podría alguien explicar esta intuición? En particular, ¿existen sistemas lógicos que sean compactos pero no completos?

EDIT: Andreas ha planteado una cuestión excelente: el teorema de la exhaustividad es en realidad una combinación de dos resultados muy importantes pero casi sin relación entre sí. En primer lugar, el teorema de la compacidad. Segundo, la enumerabilidad recursiva de las valideces lógicas. Nótese que ninguno de estos resultados depende de los detalles del sistema sintáctico o axiomático.

¿Qué relación existe entre estos dos aspectos de la exhaustividad? ¿Existen sistemas lógicos que tengan una de estas propiedades pero no la otra?

Answer 1

La cuestión es que nos importan más los modelos que las pruebas. El teorema de la compacidad -la afirmación de que una teoría es satisfactoria si todo subconjunto finito de la misma es satisfactorio- está fundamentalmente relacionado con los modelos y la posibilidad de verdad en estos modelos. Para usarla, necesitas entender tu teoría, los modelos de tu teoría y los modelos de trozos finitos de tu teoría. Y esto es en lo que queremos pensar y lo que sabemos. En particular, cuando trabajamos con modelos, podemos utilizar todas las herramientas y construcciones matemáticas a nuestra disposición, sin necesidad de permanecer dentro de ningún lenguaje de primer orden o sistema formal (bueno, quizá tengamos la teoría de conjuntos como sistema de fondo). Somos libres de razonar sobre los modelos mediante reducciones y ultrapoderes y límites de sistemas de morfismos, etc., utilizando cualquier método matemático.

En cambio, el teorema de exhaustividad está fundamentalmente relacionado con los detalles de un sistema de deducción formal. Por eso, cuando se utiliza, se piensa en si determinadas tautologías pueden demostrarse o no, o si una determinada consecuencia formal está permitida o no en el sistema. Pero cuando estamos estudiando una determinada clase de primer orden de grupos o anillos o lo que sea, esos detalles sobre el sistema de prueba pueden parecer una distracción irrelevante.

Answer 2

Tengo dos opiniones, un tanto contradictorias, al respecto.

Desde el punto de vista de la teoría moderna de modelos, el Teorema de la compacidad es fundamental para casi todo en la teoría de modelos de la lógica de primer orden, mientras que el Teorema de la completitud es casi irrelevante. La completitud entra en juego cuando se prueba la decidibilidad de teorías axiomatizadas recursivamente completas o cuando se trata de modelos recursivamente saturados, por ejemplo, pero no son muy centrales. Incluso cuando queremos aplicar la Completitud, lo importante es que el conjunto de consecuencias lógicas de $T$ es recursivamente enumerable en $T$ --los detalles del sistema de pruebas no tienen ninguna importancia. Esto explica por qué en mi libro de teoría de modelos, aunque explico que la compacidad es una consecuencia casi trivial de la completitud, doy una prueba directa al estilo de Henkin.

No obstante, considero que el Teorema de Completitud es uno de los grandes logros intelectuales de nuestra materia. El hecho de que la noción semántica de "consecuencia lógica" pueda captarse por la noción sintáctica de "prueba" es realmente sorprendente. La primera lo es, a priori, $\Pi_1$ sobre el universo de conjuntos, mientras que el segundo es recursivamente enumerable. Esto me parece asombroso.

Answer 3

Abordaré la versión más reciente de la pregunta, que se refiere a la relación entre las dos características siguientes de una lógica $L$ pero hay que tener en cuenta que una discusión cuidadosa de este tema debería primero definir claramente lo que cuenta como lógica.

(1) Exhaustividad abstracta de $L$ : El conjunto de $L$ -sentencias es recursivamente/computablemente enumerable [en adelante: r.e.].

(2) La compacidad de $L$ : Un conjunto $S$ de frases de $L$ tiene un modelo si cada subconjunto finito de $S$ tiene un modelo.

(1) no implica (2) .

Por ejemplo $Q$ sea el cuantificador que expresa "hay incontablemente muchos", es decir, $Qx\phi(x)$ se mantiene en una estructura $\cal{M}$ con el universo $M$ si el conjunto de $m\in M$ tal que $\phi(m)$ mantiene en $\cal{M}$ es incontable. Sea $L_{FO}(Q)$ ser el resultado de aumentar la lógica de primer orden $L_{FO}$ con el nuevo cuantificador $Q$ . Vaught demostró que el conjunto de sentencias válidas de $L_{FO}(Q)$ es r.e. Más tarde [1970] en un artículo seminal, Keisler dio una axiomatización elegante de $L_{FO}(Q)$ .

Por otra parte, es fácil ver que $L_{FO}(Q)$ no satisface la compacidad, por ejemplo, para $\alpha < \aleph_1$ introducir símbolos constantes $c_{\alpha}$ y considerar el conjunto $S$ de frases compuestas por $\lnot Qx (x=x)$ [que expresa "el universo no es incontable"] más frases de la forma $c_{\alpha}\neq c_\beta$ para $\alpha < \beta < \aleph_1$ . Es fácil ver que todo subconjunto de $S$ tiene un modelo, pero S no tiene un modelo.

Debo señalar que $L_{FO}(Q)$ tiene una forma limitada de compacidad conocida como compacidad contable : si $S$ es un contable conjunto de frases de $L_{FO}(Q)$ entonces S tiene un modelo si cada subconjunto finito de $S$ tiene un modelo [Vaught, ibid].

Todas estas características de $L_{FO}(Q)$ [abstractamente completo, contablemente pero no totalmente compacto] son compartidos por otros cuantificadores generalizados, incluido el cuantificador cuantificador estacionario [introducido a finales de los 70 y estudiado intensamente en los 80]. Sin embargo, como muestra Shelah, hay otros cuantificadores generalizados que generan lógicas totalmente compactas que también son abstractamente completas

(2) no implica (1) tampoco.

Consideremos, por ejemplo, la "lógica" cuyos símbolos no lógicos son los aritméticos, y cuyos axiomas son los axiomas habituales de la lógica de primer orden más todos los axiomas de aritmética verdadera es decir, sentencias aritméticas que se cumplen en $\Bbb{N}$ . La semántica de la lógica es la misma que la de la lógica de primer orden, por lo que la compacidad sigue siendo válida; pero la completitud abstracta falla claramente por Teorema de la indefinibilidad de la verdad de Tarski que dice que $Th(\Bbb{N})$ no es aritmética, y mucho menos r.e.

PS Una "lógica natural" que también sirve para demostrar que (2) no implica (1) es el fragmento existencial de la lógica de segundo orden su compacidad se deduce de las pruebas habituales de compacidad de la lógica de primer orden [incluida la prueba del ultraproducto], pero se sabe que su conjunto de sentencias válidas es co-r.e., pero no r.e..

Answer 4

¿De verdad se considera que la compacidad es el resultado más profundo? Tengo que decir que a mí también me interesan más los modelos que las fórmulas y los sistemas de deducción, y por eso me gusta enseñar a los alumnos pruebas del teorema de la compacidad que no utilicen el teorema de la completitud. completitud. Normalmente demuestro la compacidad utilizando ultraproductos.

Por otro lado, sigo creyendo que el teorema de completitud para la lógica de primer orden es el teorema más importante de la lógica matemática.
El teorema dice que, en principio, existen pruebas verificables por ordenador de todos los teoremas "verdaderos". "verdaderos". Sé que a muchos matemáticos no les preocupa mucho tener una base sólida para el concepto de "demostración" (la reconoces cuando la ves). Pero tener este concepto formal de prueba en el fondo ayuda enormemente cuando cuando quieres enfrentarte a gente que presenta sus $n$ -ésima prueba de la incoherencia de PA o ZFC, o que no hay conjuntos infinitos o que CH se cumple. Además, el teorema de completitud explica por qué podemos hacer matemáticas como las hacemos. Aunque en realidad nadie escribe pruebas formales de nada, nunca, a menos que la corrección de las pruebas se cuestione seriamente (véase el proyecto FLYSPECK en http://code.google.com/p/flyspeck/ ).

Además, creo que la demostración del teorema de completitud es más profunda que la de la compacidad compacidad. En cierto sentido, la demostración del teorema de la completitud (me refiero a la demostración en la que se construye un modelo canónico de una teoría de Henkin maximalmente consistente) es más sencilla que, por ejemplo, la demostración del teorema de la compacidad mediante un ultraproducto, pero es más complicada en los detalles y ciertamente menos accesible a la corriente principal de las matemáticas que, por ejemplo, la prueba del teorema de la compacidad por ultraproducto.

Answer 5

Este es un comentario al margen. Hay varias respuestas que explican por qué la compacidad es tan importante en la teoría de modelos, y estoy de acuerdo con lo que dicen. Pero quiero señalar que la parte "en la teoría de modelos" es clave aquí. En el estudio general de la lógica, no restringido a la teoría de modelos, tanto la compacidad como la completitud son importantes, y cada una de ellas tiene áreas de la lógica que la favorecen. La teoría de modelos, al ser un campo semántico, naturalmente se identifica más con las nociones semánticas.

En matemáticas fuera de la lógica, creo que hay más uso implícito de la completitud que de la compacidad. Cada vez que demuestro que una identidad es derivable de los axiomas de un grupo trabajando semánticamente y mostrando que la identidad se cumple en todos los grupos, estoy utilizando implícitamente el teorema de completitud. Es fácil pasar esto por alto o darlo por sentado, porque el teorema de completitud es muy conocido.

Hay sistemas que no tienen sistemas completos de deducción; un ejemplo es la lógica de segundo orden con semántica completa de segundo orden. En este sistema es perfectamente posible que algo sea cierto en cada modelo sin que sea demostrable en nuestro sistema de demostración habitual. Por lo tanto, cuando estudiamos este sistema en lógica, tenemos que vigilar de cerca si hemos demostrado que algo es demostrable, o sólo hemos demostrado que es lógicamente válido.

Imaginemos las dificultades de un mundo alternativo en el que los matemáticos tuvieran que distinguir entre "cierto en todos los grupos" y "demostrable a partir de los axiomas de un grupo". El teorema de completitud es lo que nos permite ignorar esto. En comparación, es más difícil ver reflejos del teorema de la compacidad en las matemáticas cotidianas.