Hace un finitas de primer orden de la teoría que tiene un modelo siempre tiene un modelo finito?

Question

Tengo la curiosidad de si esto es cierto o no:

Sea T un finito, de primer orden de la teoría. Si T tiene un modelo, entonces T tiene un modelo finito.

Supongo que la respuesta es 'sí', pero quería asegurarme de que no me perdí de algo que es obvio. La razón creo que este sea el caso es que, según mi comprensión de la Lowenheim-Skolem teorema, la única manera de que una contables de primer orden de la teoría se puede 'fuerza' a un tamaño en su potencial modelos es la inclusión de una contables serie de constantes que el modelo debe tener representaciones. Por lo tanto, si la teoría es finito, entonces el número de constantes que pueden ser 'fuerza' a existir también debe ser finito, asegurando de esta manera la existencia de un modelo finito (suponiendo que cualquier modelo puede existir en absoluto). Nada malo con mi razonamiento (aparte de su relativa informalidad)?

Answer 1

Noé y Brian han dado uno de los ejemplos canónicos de un finitely axiomatizable teoría con ningún modelo finito (los ejemplos son esencialmente el mismo). Te voy a dar el otro - muestra que este comportamiento es posible, incluso en un lenguaje relacional sin funciones ajustables por el, así que al pensar en constante símbolos y términos es un arenque rojo (a menos que usted piense acerca de Skolemization, como Noé, dice).

Deje $L$ ser el lenguaje que consiste en un único binario relación símbolo $\leq$, y deje $T$ ser la teoría que afirme que el $\leq$ es un no-vacía orden lineal sin mayor elemento. Es decir, $T$ contiene el orden lineal de tres axiomas, junto con las oraciones $\forall x\, \exists y\, (x\leq y\land \lnot (x = y))$ $\exists x\, x = x$ (para descartar la estructura vacía, si su semántica para la lógica de primer orden permite).

---

Así que no es cierto que cada finitely axiomatizable teoría tiene un modelo finito. De hecho, el problema de determinar si una teoría tiene un modelo finito es indecidible en general. Esto se conoce como Trakhtenbrot del teorema.

Tiempo para una tangente: Si su suposición era correcta, y cada finitely axiomatizable de primer orden de la teoría había un modelo finito, entonces, en el hecho de que el problema de decisión para la lógica de primer orden sería decidable. Que es, se podría escribir un programa de computadora que toma como entrada un primer orden de la frase $\varphi$ y salidas "sí" o "no" de acuerdo a si $\varphi$ tiene un modelo. Este programa iba a iniciar la enumeración de lo finito $L$-estructuras y comprobar si son modelos de $\varphi$, mientras que, simultáneamente, la búsqueda de pruebas de la $\lnot \varphi$. Si $\varphi$ no tiene modelo, una prueba de $\lnot\varphi$ eventualmente encontrarse (por el teorema de completitud), mientras que si $\varphi$ tiene un modelo, un modelo finito finalmente será encontrado.

Por supuesto, el problema de decisión para la lógica de primer orden es bien conocido por ser indecidible. Pero hay clases de primer orden de las frases (por ejemplo, en una relacional del lenguaje universal de las sentencias $\forall \overline{x}\, \varphi(\overline{x})$ $\varphi$ cuantificador-libre) que ¿ tiene el modelo finito de la propiedad (si es que tiene un modelo, entonces ellos tienen un modelo finito) y, por tanto, estas clases son decidable por el argumento anterior.

Answer 2

No, esto es incorrecto. En el lenguaje consta de una sola unario símbolo de función $f$, considere las siguientes afirmaciones acerca de $f$:

• $f$ es inyectiva.

• $f$ no es surjective.

Es un buen ejercicio para demostrar que estas pueden ser escritas como de primer orden de la pena; pero cualquier modelo de la conjunción de estas frases tiene que ser infinita.

---

El punto es que las "constantes" que usted menciona no son sólo cosas nombrado por la constante de símbolos, sino también de los términos (en realidad, incluso más amplio - constante de símbolos en el más grande, "Skolemized del lenguaje" - pero por ahora es suficiente como para considerar los términos). Incluso un lenguaje finito puede tener un número infinito de términos.

Answer 3

Tome una teoría con una única función de símbolo $f$, uno de los constantes símbolo $a$, y los axiomas

$$\begin{align*} &\forall x\Big(\big(\exists y\big(f(y)=x\big)\leftrightarrow x\ne a\Big)\;,\text{ and}\\ &\forall x\,\forall y\big(f(x)=f(y)\to x=y\big)\;. \end{align*}$$

Para la intuición, para pensar $\Bbb N$, $0$, y la función sucesor.

Answer 4

Deje que el lenguaje contiene un único binario símbolo de predicado, debe interpretarse como "menor que".

Considerar la teoría de la $T$ con los siguientes axiomas:

1) Hay al menos dos objetos.

2) La relación $L$ es un estricto orden total.

3) Para cualquier $x$ $y$ tal que $L(x,y)$, existe un $t$ tal que $L(x,t)$$L(t,y)$.

A continuación, todos los modelos de $T$ son infinitas. Esta es la teoría de la densa orden lineal. Tiene buen modelo teórico de propiedades. Cantor demostró que cualquier contables densamente conjunto ordenado con el primero y el último elemento es el fin-isomorfo a los racionales bajo el orden habitual. Del mismo modo, un contable densamente conjunto ordenado con el primer elemento y el último es isomorfo a los racionales en $[0,1)$, con resultados similares para las otras dos posibilidades.

Answer 5

Todos los ejemplos hasta ahora hacer uso de la igualdad símbolo $=$. En algunas zonas de la lógica (generalizado), a menudo se considera de primer orden idiomas sin el símbolo de la igualdad que siempre se interpreta como la verdadera igualdad. Pero uno puede construir un número finito de la teoría de la $T_0$ que no se menciona la igualdad tal que $T_0$ no tiene un modelo finito.

Tomar como $T$ como uno de el otro ejemplo. A continuación, vamos a $T_0$ ser la teoría obtenidos por:

1. la sustitución de cada una de las $=$$\equiv$, un nuevo símbolo
2. la adición de las frases que dice $\equiv$ es un equivalente de la relación y
3. el uno para el otro símbolo que ocurren en $T$ (hay un número finito de ellos), la adición de la frase que dice que el símbolo es compatible con (la relación de equivalencia) $\equiv$.

Supongamos $T_0$ tenía un modelo finito $M$. A continuación, el cociente $M/\equiv^M$ $M$ por la interpretación de $\equiv$ es un modelo de la teoría original de $T$. Pero $M/\equiv^M$ es también finito, una contradicción.