1.9: Sustituciones y sustituibilidad

Supongamos que sabía que la oración\(\forall x \phi \left( x \right)\) era cierta en una estructura particular\(\mathfrak{A}\). Entonces, si\(c\) es un símbolo constante en el idioma, sin duda esperarías\(\phi \left( c \right)\) ser cierto en\(\mathfrak{A}\) también. Lo que hemos hecho es sustituir el símbolo constante\(c\) por la variable\(x\). Esto parece perfectamente razonable, aunque hay momentos en los que sí hay que tener cuidado.

Supongamos que\(\mathfrak{A} \models \forall x \exists y \neg \left( x = y \right)\). Esta frase es, de hecho, cierta en cualquier estructura\(\mathfrak{A}\) tal que\(A\) tenga al menos dos elementos. Si luego procedemos a reemplazar la variable\(x\) por la variable\(u\), obtenemos la sentencia\(\exists y \neg \left( u = y \right)\), que seguirá siendo verdadera en\(\mathfrak{A}\), no importa qué valor le demos a la variable\(u\). Si, sin embargo, tomamos nuestra fórmula original y la reemplazamos\(x\) por\(y\), entonces nos encontramos mirando\(\exists y \neg \left( y = y \right)\), lo que será falso en cualquier estructura. Entonces, por una mala elección de la variable sustitutiva, hemos cambiado el valor de verdad de nuestra fórmula. Las reglas de sustituibilidad que discutiremos en esta sección están diseñadas para ayudarnos a evitar este problema, el problema de intentar sustituir un término dentro de un cuantificador que vincula una variable involucrada en el término.

Comenzamos definiendo exactamente lo que queremos decir cuando sustituimos un término\(t\) por una variable ya sea\(x\) en un término\(u\) o en una fórmula\(\phi\).

Definición 1.8.1. Supongamos que\(u\) es un término,\(x\) es una variable, y\(t\) es un término. Definimos el término\(u_t^x\) (léase "\(u\)con\(x\) reemplazado por\(t\) “) de la siguiente manera:

1. Si\(u\) es una variable no igual a\(x\), entonces\(u_t^x\) es\(u\).
2. Si\(u\) es\(x\), entonces lo\(u_t^x\) es\(t\).
3. Si\(u\) es un símbolo constante, entonces\(u_t^x\) es\(u\).
4. Si\(u : \equiv f u_1 u_2 \ldots u_n\), donde\(f\) es un símbolo de función\(n\) -aria y los términos\(u_i\) son, entonces\(u_t^x\) es\(f \left( u_1 \right)_t^x \left( u_2 \right)_t^x \ldots \left( u_n \right)_t^x.\)

Chafia: En la cuarta cláusula de la definición anterior y en las dos primeras cláusulas de la siguiente definición, los paréntesis no están realmente ahí. No obstante, creemos que nadie puede mirar\(u_1 \:_t^x\) y averiguar lo que se supone que significa. Por lo que se han agregado los paréntesis en aras de la legibilidad.

Por ejemplo, si dejamos\(t\) ser\(g \left( c \right)\) y dejamos\(u\) ser\(f \left( x, y \right) + h \left( z, x, g \left( x \right) \right)\), entonces\(u_t^x\) es

\[f \left( g \left( c \right), y \right) + h \left( z, g \left( c \right) , g \left( g \left( c \right) \right) \right).\]

La definición de sustitución en una fórmula también es por recursión:

Definición 1.8.2. Supongamos que\(\phi\) es una\(\mathcal{L}\) fórmula,\(t\) es un término, y\(x\) es una variable. Definimos la fórmula\(\phi_t^x\) (léase "\(\phi\)con\(x\) reemplazado por\(t\) “) de la siguiente manera:

1. Si\(\phi : \equiv = u_1 u_2\), entonces lo\(\phi_t^x\) es\(= \left( u_1 \right)_t^x \left( u_2 \right)_t^x\).
2. Si\(\phi : \equiv R u_1 u_2 \ldots u_n\), entonces lo\(\phi_t^x\) es\(R \left( u_1 \right)_t^x \left( u_2 \right)_t^x \ldots \left( u_n \right)_t^x\).
3. Si\(\phi : \equiv \neg \left( \alpha \right)\), entonces lo\(\phi_t^x\) es\(\neg \left( \alpha_t^x \right)\).
4. Si\(\phi : \equiv \left( \alpha \lor \beta \right)\), entonces lo\(\phi_t^x\) es\(\left( \alpha_t^x \lor \beta_t^x \right)\).
5. Si\(\phi : \equiv \left( \forall y \right) \left( \alpha \right)\), entonces
   \[\phi_t^x = \begin{cases} \phi \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \: \text{if} \: x \: \text{is} \: y \\ \left( \forall y \right) \left( \alpha_t^x \right) \: \: \: \text{otherwise} \end{cases}\]

Como ejemplo, supongamos que esa\(\phi\) es la fórmula

\[P \left( x, y \right) \rightarrow \left[ \left( \forall x \right) Q \left( g \left( x \right), z \right) \right) \lor \left( \forall y \right) \left( R \left( x, h \left( x \right) \right) \right].\]

Entonces, si\(t\) es el término\(g \left( c \right)\), obtenemos

\[\phi_t^x \: \text{is} P \left( g \left( c \right), y \right) \rightarrow \left[ \left( \forall x \right) \left( Q \left( g \left( x \right), z \right) \right) \right) \lor \left( \forall y \right) \left( R \left( g \left( c \right), h \left( g \left( c \right) \right) \right) \right].\]

Habiendo definido lo que queremos decir cuando sustituimos un término por una variable, ahora definiremos lo que significa que un término sea sustitutable por una variable en una fórmula. La idea es que si\(t\) es sustitutable por una variable en una fórmula. La idea es que si\(t\) es sustitutable por\(x\) in\(\phi\), no nos toparemos con los problemas discutidos al inicio de esta sección -no vamos a sustituir un término de tal manera que una variable contenida en ese término quede vinculada inadvertidamente por un cuantificador.

Definición 1.8.3. Supongamos que\(\phi\) es una\(\mathcal{L}\) fórmula,\(t\) es un término, y\(x\) es una variable. Nosotros manera que \(t\)es sustituibles\(x\) en\(\phi\) si

1. \(\phi\)es atómico, o
2. \(\phi : \equiv \neg \left( \alpha \right)\)y\(t\) se puede sustituir\(x\) en\(\alpha\), o
3. \(\phi : \equiv \left( \alpha \lor \beta \right)\)y\(t\) se puede sustituir\(x\) en ambos\(\alpha\) y\(\beta\), o
4. \(\phi : \equiv \left( \forall y \right) \left( \alpha \right)\)y o bien
   (a) no\(x\) está libre en\(\phi\), o
   (b)\(y\) no ocurre en\(t\) y\(t\) es sustituibles\(x\) en\(\alpha\)

Aviso que\(\phi_t^x\) se define si\(t\) es o no sustituibles\(x\) en\(\phi\). Por lo general no vamos a querer hacer una sustitución a menos que verifiquemos la sustituibilidad, pero tenemos la capacidad de sustituir si es o no una buena idea. En el siguiente capítulo, sin embargo, a menudo verás que ciertas operaciones están permitidas solo si\(t\) es sustituibles por\(x\) in\(\phi\). Esa restricción está ahí por una buena razón, ya que nos ocuparemos de preservar la verdad de las fórmulas después de realizar sustituciones.

Ejercicios

1. Para cada una de las siguientes, escribir\(u_t^x\):
   (a)\(u : \equiv \cos x\),\(t\) es\(\sin y\).
   b)\(u : \equiv y\),\(t\) es\(Sy\).
   (c)\(u : \equiv \sharp \left( x, y , z \right)\),\(t\) es\(423 - w\).
2. Para cada una de las siguientes, primero escribe\(\phi_t^x\), luego decide si\(t\) es sustitutable por\(x\) in\(\phi\), y luego (si aún no lo has hecho) usa la definición de sustituibilidad para justificar tus conclusiones.
   (a)\(\phi : \equiv \forall x \left( x = y \rightarrow Sx = Sy \right)\),\(t\) es\(S0\).
   b)\(\phi : \equiv \forall y \left( x = y \rightarrow Sx = Sy \right)\),\(t\) es\(Sy\).
   (c)\(\phi : \equiv x = y \rightarrow \left( \forall x \right) \left( Sx = Sy \right)\),\(t\) es\(Sy\).
3. Demuestre que si\(t\) está libre de variables, entonces siempre\(t\) es sustituibles por\(x\) in\(\phi\).
4. Demostrar que siempre\(x\) es sustituibles\(x\) en\(\phi\).
5. Demostrar que si no\(x\) es libre en\(\psi\), entonces\(\psi_t^x\) es\(\psi\).
6. Podrías pensar que eso\(\left( \phi_y^x \right)_x^y\) es\(\phi\), pero el pensamiento de un momento te dará un ejemplo para demostrar que esto no siempre funciona. (¿Y si\(y\) está libre en\(\phi\)?) Encuentra un ejemplo que demuestre que aunque no\(y\) sea libre en\(\phi\), todavía podemos tener\(\left( \phi_y^x \right)_x^y\) diferente de\(\phi\). ¿Bajo qué condiciones sabemos que\(\left( \phi_y^x \right)_x^y\) es eso\(\phi\)?
7. Escribe un programa de computadora (en tu idioma favorito, o en pseudo-código) que acepte como entrada una fórmula\(\phi\), una variable\(x\) y un término\(t\) y dé salida “yes” o “no” dependiendo de si\(t\) es o no sustituibles por\(x\) in\(\phi\).