Pregunta sobre los resultados de inexpresividad sobre modelos finitos utilizando la compacidad y el teorema de Löwenheim-Skolem

Question

En el libro Elements of finite model theory de Leonid Libkin, muestran que la consulta de paridad para estructuras sobre un vocabulario vacío no es definible en primer orden.

Para ello, construyen dos modelos infinitos contables $\mathcal{A}$ et $\mathcal{B}$ utilizando el teorema de la compacidad y el teorema de Löwenheim-Skolem. Como ambos modelos son infinitos contables, son isomorfos y, por tanto, todas las sentencias de primer orden coinciden en ambos modelos. Sin embargo, el teorema de la compacidad implica que la consulta de paridad no coincide en esas dos estructuras. Por lo tanto, la consulta de paridad no es definible en primer orden.

Ahora mi pregunta: dicen que esto también implica que la consulta de paridad no es definible en primer orden sobre modelos finitos. Creo que esto se debe a que la consulta de paridad sólo tiene sentido sobre modelos finitos. ¿Es esto correcto?

Entonces demuestran el siguiente lema: Para toda estructura finita $\mathcal{A}$ hay una frase $\psi_\mathcal{A}$ tal que $\mathcal{B} \models \psi_\mathcal{A}$ si y sólo si $\mathcal{B} \cong \mathcal{A}$ .

Y afirman que esto implica que la técnica utilizada para demostrar que la consulta de paridad no es definible en primer orden no puede extenderse para demostrar más resultados de inexpresabilidad sobre modelos finitos.

Sé que no siempre basta con considerar sólo dos estructuras, ya que algunas consultas no definibles en primer orden son expresables para todas las estructuras de conjuntos finitos, por ejemplo, la conectividad de los grafos. Sin embargo, no veo que ese lema implique lo que ellos afirman.

P.D. Si es necesario, puedo incluir ambas pruebas.

Answer 1

Nótese que Libkin dice lo siguiente (pp.25-26):

Como introducción a estas herramientas, revisemos la prueba de la Proposición 3.3 [ $\mathsf{even}$ no es definible por FO sobre una firma vacía] . En la prueba, construimos dos modelos, $\mathfrak{A}_1$ et $\mathfrak{A}_2$ que están de acuerdo en todo FO (ya que son isomorfas), y sin embargo la compacidad nos dice que no están de acuerdo en $\Phi$ que asumimos para definir $\mathsf{even}$ - por lo tanto $\mathsf{even}$ no es de primer orden.

¿Podemos extender esta técnica para demostrar resultados de inexpresividad sobre modelos finitos? El intento más sencillo de hacerlo fracasa debido a lo siguiente.

Lema 3.4. Para toda estructura finita $\mathfrak{A}$ hay una frase $\Phi_\mathfrak{A}$ tal que $\mathfrak{B} \models \Phi_\mathfrak{A}$ si $\mathfrak{B} \cong \mathfrak{A}$ .

...

En particular, cada dos estructuras finitas que coinciden en todas las sentencias FO son isomorfas, y por lo tanto coinciden en cualquier consulta booleana (ya que las consultas booleanas son cerradas bajo isomorfismo).

Desde el técnica que quiere ampliar parece ser la de construir equivalente elemental que dan respuestas diferentes a la consulta dada, el lema 3.4 dice que una extensión directa de esta técnica no puede funcionar en el dominio de los modelos finitos, ya que dos modelos finitos elementales equivalentes son isomorfos (y por lo tanto darán la misma respuesta a cualquier consulta booleana).

En el caso de una consulta booleana como $\mathsf{even}$ esto queda claro: si $\mathfrak{A}, \mathfrak{B}$ eran modelos finitos tales que $\mathfrak{A} \models \mathsf{even}$ et $\mathfrak{B} \models \neg \mathsf{even}$ entonces $\mathfrak{A} \not\cong \mathfrak{B}$ y, por tanto, por el lema 3.4 $\mathfrak{A} \not\equiv \mathfrak{B}$ y a priori no hay ninguna razón para que una sentencia $\Phi$ tal que $\mathfrak{A} \models \Phi$ et $\mathfrak{B} \models \neg \Phi$ no puede ser una fórmula definitoria de $\mathsf{even}$ sobre modelos finitos.

Nótese que esto es similar al intento fallido de demostrar que $\mathsf{even}$ no es definible por FO sobre estructuras ordenadas. Aunque la compacidad de Löwenheim-Skolem resultó en dos modelos (ordenados) contablemente infinitos $\mathfrak{A}_1, \mathfrak{A}_2$ satisfaciendo $\mathsf{even}$ et $\neg \mathsf{even}$ respectivamente, ya que no había forma de garantizar que $\mathfrak{A}_1$ et $\mathfrak{A}_2$ son elementalmente equivalentes no podríamos lograr la tan deseada contradicción.