Básicamente, sí. Una vieja resultado de Kleene [1], reforzada posteriormente por Craig y Vaught [2], muestra que cada recursivamente axiomatizable de la teoría de la lógica de primer orden, sin identidad, y cada recursivamente axiomatizable de la teoría de la lógica de primer orden con identidad que sólo tiene infinitos modelos, tiene un finitely axiomatized conservador de extensión. Véase también Mihály Makkai la revisión, Richard Zach del resumen, y un artículo relacionado por Pakhomov y Visser [3].
Permítanme subrayar que los resultados anteriores se aplican a la definición literal de conservador de extensión, es decir, extender el lenguaje de la $T$ adicional en el predicado o función de símbolos, y exigimos que cualquier frase en el idioma original, es comprobable en la extensión de la fib es comprobable en $T$. Si soltamos la definición de modo de permitir adicional tipo o extensión por medio de un pariente de la interpretación, entonces cada recursivamente axiomatizable de primer orden de la teoría tiene una finitely axiomatized conservador de extensión.
Pero volvamos a la definición estándar. Estoy asumiendo la lógica de la identidad a partir de ahora. Lo que sucede, por teorías, que también pueden tener finito de modelos? En primer lugar, [2] dar el siguiente caracterización (que ellos llaman la condición 1 "f.a.${}^+$", y la condición 2".f.a.${}^+$"):
Teorema. Para cualquier teoría de la $T$ en un lenguaje finito, los siguientes son equivalentes:
- $T$ tiene un finitely axiomatized conservador de extensión.
- Existe una finitely axiomatized extensión de $T'\supseteq T$ de tal forma que cada modelo de $T$ se expande a un modelo de $T'$.
- $T$ es equivalente a un $\Sigma^1_1$ de segundo orden de la frase.
Siguiente Dmytro Taranovsky comentarios, se tiene la siguiente condición necesaria (que es en realidad también se menciona en [2], refiriéndose a Scholz la noción de espectro en lugar de NP, que sólo fue definido más de una década después):
Teorema. Para cualquier teoría de la $T$ en un lenguaje finito, 1 implica 2:
- $T$ tiene un finitely axiomatized conservador de extensión.
- $T$ es recursivamente axiomatizable, y el conjunto de sus modelos finitos es reconocible en NP.
En efecto, la verdad de un fijo $\Sigma^1_1$ sentencia en lo finito de los modelos se puede comprobar en NP.
No se sabe si esta es una caracterización completa: si $T$ es r.e. teoría cuya finito modelos son NP, a continuación, $T$ es equivalente a un $\Sigma^1_1$ frase en infinitos modelos [1,2], y $T$ es equivalente a un $\Sigma^1_1$ frase en finitos modelos de Fagin del teorema, pero no está claro cómo combinar los dos a una sola $\Sigma^1_1$ frase que funciona para todos los modelos. Esto se menciona como un problema abierto en la reciente artículo [3].
Referencias:
[1] Stephen Cole Kleene: Finito axiomatizability de teorías en el predicado de cálculo adicionales utilizando símbolos de predicado, en: Dos artículos sobre el predicado de cálculo. Memorias de la Sociedad Matemática Americana, no. 10, Providencia, 1952 (reimpreso 1967), pp 27-68.
[2] William Craig y Robert L. Vaught: Finito axiomatizability el uso de predicados adicionales, Revista de la Lógica Simbólica 23 (1958), no. 3, pp 289-308.
[3] Fedor Pakhomov y Albert Visser, En una cuestión de Krajewski del, Revista de la Lógica Simbólica 84 (2019), no. 1, pp 343-358. arXiv: 1712.01713 [matemáticas.LO]
