¿es la lógica de primer orden con constantes igual de expresiva que la lógica de primer orden sin constantes?

Question

Defino una lógica como un conjunto de fórmulas $\mathcal{L}$ (formulado en alguna firma dada) con una relación de consecuencia $\vDash$ . Digamos que una lógica $L_1$ es al menos tan expresivo como $L_2$ si existe una traducción conservadora de $L_1$ a $L_2$ es decir, ~hay $t: \mathcal{L}_1\rightarrow\mathcal{L_2}$ tal que $\Gamma\vDash_1\varphi$ si $t(\Gamma)\vDash_2t(\varphi)$ . Considere $\mathcal{L}_{con}$ el lenguaje de la lógica de primer orden con un número denumerable de constantes, y $\mathcal{L}$ el lenguaje de la lógica de primer orden sin constantes. Sospecho que estos dos lenguajes son igualmente expresivos. En particular, podemos traducir cualquier fórmula con constantes en $\mathcal{L}_{con}$ a una fórmula con sólo variables en $\mathcal{L}$ con la restricción de que diferentes constantes se asignan a diferentes variables. Así, por ejemplo, $F(c_1,c_2)\mapsto F(x_1,x_2)$ . ¿Es correcto?

Supongo que una cuestión más fundamental es que no tengo muy claro cómo demostrar propiedades de las traslaciones. Supongo que, dada la solidez y completitud de la lógica de primer orden, se podría inducir sobre la complejidad de las pruebas. Pero esto parece bastante tedioso y no se extiende a las lógicas que se sabe que son incompletas. ¿Existe una forma canónica de demostrar la igualdad de expresividad (o, equivalentemente, la existencia de una traducción conservativa) entre dos lógicas cualesquiera?

Answer 1

Traducir símbolos constantes a variables no funciona bien, porque en la mayoría de las lógicas en las que se contemplan fórmulas con variables libres, la semántica pretendida es la de su cierre universal. En esos sistemas tenemos, por ejemplo $$ p(x) \vDash p(y) \qquad\text{but not}\qquad p(c_0) \vDash p(c_1) $$ porque los modelos que satisfacen $p(x)$ son exactamente aquellas en las que $p$ se cumple para cada individuo, que son los mismos modelos que satisfacen $p(y)$ .

---

Sin embargo, puede simular constantes utilizando nuevos símbolos de función y predicado. Construya un nuevo lenguaje añadiendo una nueva letra de variable $0$ un nuevo símbolo de predicado unario $Z$ y un número contable de nuevas funciones simbólicas $f_n$ y luego traducir

• cada constante $c_n$ como $f_n(0)$ ;
• todas las demás partes de términos permanecen sin cambios;
• cada fórmula atómica $p(t_1, \ldots, t_n)$ como $$ \neg \exists 0\Bigl (Z(0) \land \forall x(Z(x)\to x=0) \land \neg p(t[t_1],\ldots,t[t_n]\Bigr); $$
• y todas las conectivas y cuantificadores siguen siendo ellos mismos

Espero que esto se ajuste a su concepto de traducción. $\mathcal L_1\to\mathcal L_2$ . Si quiere ser completamente rígido al respecto, podría "hacer sitio" para el nuevo $\{0,Z,f_n\}$ símbolos seleccionando existente símbolos para ellos y el desplazamiento de los símbolos existentes fuera del camino con el mapa de Hilbert-hotel como parte de la traducción, pero no voy a complicar mi notación por hacer que explícita.

Supongamos que para algunos $\Gamma$ , $\varphi$ tenemos que $t(\Gamma) \vDash_2 t(\varphi)$ y para algún modelo $\mathfrak M$ tenemos $\mathfrak M\vDash_1 \Gamma$ . Entonces podemos construir un nuevo $\mathfrak M_2$ seleccionando uno de $\mathfrak M$ para que los elementos de $Z$ propiedad y alquiler $(f_n)^{\mathfrak M_2}$ asignar todo a $(c_n)^{\mathfrak M}$ para cada $n$ .

Entonces $\mathfrak M_2\vDash_2 t(\psi)$ exactamente si $\mathfrak M\vDash_1 \psi$ . Ahora bien $\mathfrak M\vDash_1 \Gamma$ tenemos $\mathfrak M_2\vDash_2 t(\Gamma)$ y entonces por suposición $\mathfrak M_2 \vDash_2 t(\varphi)$ y luego $\mathfrak M\vDash_1 \varphi$ .

Por el contrario, supongamos $\Gamma \vDash_1 \varphi$ y tenemos algunos $\mathfrak M \vDash_2 t(\Gamma)$ . Entonces,

• o bien existe un único $m_0\in\mathfrak M$ que satisfaga $Z(m_0)$ y en ese caso podemos construir un $\mathfrak M_1$ mediante el procedimiento inverso, es decir, que $(c_n)^{\mathfrak M_1}$ sea $f^{\mathfrak M}(m_0)$ -- tal que $\mathfrak M_1\vDash_1 \psi$ si $\mathfrak M\vDash_2 t(\psi)$ .
• o no existe tal elemento, en cuyo caso la traducción de cada fórmula atómica es verdadero en $\mathfrak M$ para todos los valores de las variables. En ese caso $\mathfrak M_0$ sea el modelo con un único elemento en el que todos los predicados son verdaderos; entonces $\mathfrak M_0\vDash_1 \psi$ si $\mathfrak M\vDash_2 t(\psi)$ .

(Las negaciones en la traducción de fórmulas atómicas están ahí para permitir $\mathfrak M_0$ trabajar cuando $p$ es el predicado de igualdad $=$ que no podemos hacer que sea "siempre falsa" al construir un modelo. puede hacerla "siempre verdadera" seleccionando un modelo con un solo elemento).