Algunos detalles de definición en la teoría de modelos: igualdad y QE

¿Requerimos que cada idioma (al menos en el contexto de la teoría de modelos) debe contener un símbolo de igualdad? ¿Y este símbolo de igualdad debe interpretarse como la igualdad "real" (la igualdad en el metalenguaje)?

Si y si. Por defecto, la sintaxis de la lógica de primer orden contiene un símbolo primitivo$=$, y la semántica de la lógica de primer orden trata este símbolo como una referencia a la verdadera igualdad en los modelos. La lógica sin igualdad primitiva se denomina "lógica de primer orden sin igualdad". Advertencia: en mi experiencia, este es el uso moderno estándar de la terminología. Pero hay que tener un poco de cuidado, especialmente al leer fuentes antiguas, ya que no siempre ha sido una convención universal que la lógica de primer orden incluya la igualdad primitiva.

Para que nuestra teoría del modelo sea más general, definitivamente no queremos imponer ninguna suposición adicional.

Pero la lógica de primer orden sin igualdad se encuentra dentro de la lógica de primer orden con igualdad, por lo que no pierde ninguna generalidad. Si desea hacer lógica de primer orden sin igualdad, puede concentrarse en oraciones y fórmulas que no usan el símbolo de igualdad. Y si desea un símbolo de igualdad que no necesariamente se interprete como verdadera igualdad, puede introducir un nuevo símbolo de relación binaria$\hat{=}$.

Por otro lado, si requerimos que todos los lenguajes tengan igualdad, entonces, ¿qué pasa con la teoría de conjuntos en sí misma, que usa$\in$como la única relación primitiva y considera$=$como una especie de relación derivada?

Eso no es lo que hace la teoría de conjuntos (estándar). ZFC es una teoría en lógica de primer orden con igualdad. El axioma de extensionalidad$\forall x\forall y(\forall z(z\in x\leftrightarrow z\in y)\leftrightarrow (x=y))$incluye el símbolo de igualdad, y cuando hablamos de modelos de ZFC, este símbolo de igualdad se interpreta como verdadera igualdad.

Además, necesitamos reformular cuidadosamente teoremas como el teorema de completitud, ya que fórmulas como "$\forall x\ (x = x)$" fue (implícitamente) satisfecha por cada estructura, pero no es una tautología desde el punto de vista sintáctico (y por lo tanto no puede derivarse de un axioma vacío).

No,$\forall x\ (x = x)$ es una tautología sintáctica y no se puede derivar de ninguna hipótesis en ningún sistema de prueba estándar para la lógica de primer orden. Por supuesto, esta oración no se puede derivar en un sistema de prueba para la lógica de primer orden sin igualdad, ya que tal sistema de prueba no tiene ninguna regla que mencione el símbolo$=$! Pero el punto es que un sistema de prueba para la lógica de primer orden sin igualdad no está completo para la lógica de primer orden (con igualdad).

En la definición de eliminación de cuantificadores (QE), ¿requerimos que la fórmula eliminada tenga las mismas variables libres que la fórmula original?

Sí.

¿Existe una teoría?$T$, sin símbolo constante y no completo, pero tiene QE?

Bueno, algunas formulaciones de la lógica de primer orden también permiten$0$-símbolos de relación aria ("símbolos proposicionales"). Un símbolo proposicional$P$es una oración en sí misma. Así por ejemplo en el lenguaje$L = \{P\}$dónde$P$es un símbolo proposicional, la teoría$T = \{(\exists x\top)\land \forall x\forall y(x = y)\}$tiene QE pero no es completa, ya que no decide el valor de verdad de$P$.

Pero por otro lado, tenemos:

Proposición Si$L$es un idioma sin$0$símbolos -arios (sin constantes o símbolos proposicionales), entonces cada$L$-teoría$T$con qe es completo.

Prueba: Deja$\varphi$frijol$L$-oración. Entonces hay un cuantificador libre$L$-oración$\psi$tal que$T\models \varphi\leftrightarrow \psi$. Pero el único cuantificador libre$L$-las oraciones son$\top$y$\bot$. De este modo$T\models \varphi$o$T\models \lnot \varphi$, entonces$T$Esta completo.$\square$

Incluso para lenguajes con símbolos constantes, probar QE es una estrategia común para probar que una teoría está completa. Si una teoría$T$tiene QE, entonces es completo si y solo si decide la verdad de todas las oraciones libres de cuantificadores, lo que se reduce a decir que$T$determina el tipo de isomorfismo de la "estructura generada por las constantes". Más precisamente, dado cualquier modelo$M\models T$,$M$tiene una subestructura más pequeña$M_\emptyset$, la subestructura de$M$generada por las constantes. Si$T$tiene QE, entonces$T$es completo si y solo si para todos$M\models T$y$N\models T$, las estructuras$M_\emptyset$y$N_\emptyset$son isomorfos. En el caso cuando$T$no tiene constantes,$M_\emptyset$es siempre la estructura vacía, y cuando$T$tampoco tiene símbolos proposicionales, dos estructuras vacías cualesquiera son isomorfas.