5.9: NUM y SUB son representables

En nuestra prueba del Lema de Auto-Referencia en la Sección 6.2, tendremos que poder sustituir el número Gödel de una fórmula en una fórmula. Para ello será necesario saber que un par de funciones son representables, y en esta sección describimos cómo construir\(\Delta\) -definiciones de esas funciones. Primero trabajamos con la función\(Num\).

Recordemos que\(\bar{a}\) es el numeral que representa el número\(a\). Así,\(\bar{2}\) es\(SS0\). Ya que\(SS0\) es un\(\mathcal{L}_{NT}\) término, tiene un número de Gödel, en este caso

\[\ulcorner SS0 \urcorner = \langle 11, \ulcorner S0 \urcorner \rangle = \langle 11, 2^{12} 3^{1025} \rangle = 2^{12} 3^{2^{12} 3^{1025} + 1}.\]

La función\(Num\) que busquemos mapeará 2 al número de Gödel de su\(\mathcal{L}_{NT}\) numeral,\(2^{12} 3^{1025} = 2^{12} 3^{2^{12} 3^{1025} + 1}\). Entonces\(Num \left( a \right) = \ulcorner a \urcorner\).

Para escribir una\(\Delta\) -definición\(Num \left( a, y \right)\) comenzaremos, una vez más, con una secuencia de construcción, pero esta vez construiremos el numeral\(\bar{a}\) usando un término particular secuencia de construcción. Para dar un ejemplo, considere el caso\(a = 2\). Utilizaremos la secuencia de construcción más fácil que se nos ocurra, a saber

\[\left( 0, S0, SS0 \right),\]

lo que da lugar a la secuencia de números de Gödel

\[\left( \ulcorner 0 \urcorner, \ulcorner S0 \urcorner, \ulcorner SS0 \urcorner \right) = \left( 1024, 2^{12} 3^{1025}, 2^{12} 3^{2^{12} 3^{1025} + 1} \right),\]

que está codificado por el número

\[c = 2^{\left[ 1025 \right]} 3^{\left[ 2^{12} 3^{1025} + 1 \right]} 5^{\left[ 2^{12} 3^{2^{12} 3^{1025} + 1} + 1 \right]}.\]

Observe que la longitud de la secuencia de construcción aquí es 3, y en general la secuencia de construcción tendrá longitud\(a + 1\) si buscamos codificar la construcción del número Gödel del numeral asociado al número\(a\). (Esa es una frase muy larga, pero tiene sentido si la trabajas con cuidado).

Se le pide en el Ejercicio 1 anotar la fórmula

\[NumConstructionSequence \left( c, a, y \right)\]

como una\(\Delta\) fórmula. La idea es que

\[\mathfrak{N} \models NumConstructionSequence \left( c, a, y \right)\]

si y sólo si\(c\) es el código para una secuencia de construcción de longitud\(a + 1\) con último elemento\(y = \ulcorner a \urcorner\).

Ahora nos gustaría definir la fórmula de tal\(Num \left( a, y \right)\) manera que\(Num \left( a, y \right)\) sea verdadera si y sólo si\(y\) es\(\ulcorner a \urcorner\), y como en la Sección 5.8, la fórmula no\(\left( \exists c \right) NumConstructionSequence \left( c, a, y \right)\) funciona, ya que el cuantificador es ilimitado. Entonces debemos encontrar un límite para\(c\).

Si\(\left( c, a, y \right) \in NUMCONSTRUCTIONSEQUENCE\), entonces sabemos que\(c\) codifica una secuencia de construcción de longitud\(a + 1\) y\(c\) es de la forma

\[c = 2^{\ulcorner t_1 \urcorner + 1} 3^{\ulcorner t_2 \urcorner + 1} \cdots p_{a+1}^{y+1},\]

donde cada uno\(t_i\) es un subtérmino de\(\bar{a}\). Por Lema 5.8.6 y Lema 5.8.7, lo sabemos\(\ulcorner t_i \urcorner \leq y\) y\(p_{a+1} \leq 2^{\left( a + 1 \right)^{\left( a + 1 \right)}}\), entonces

\[c \leq 2^{y + 1} 3^{y + 1} \ldots p_{a+1}^{y+1} \left( a+1 \: \text{terms} \right) \leq \left( p_{a+1} \right)^{\left( a + 1 \right)^{\left( a + 1 \right) \left( y + 1 \right)}} \leq \left( 2^{\left( a + 1 \right)^{\left( a + 1 \right)}} \right)^{\left( a + 1 \right) \left( y + 1 \right)}.\]

Esto nos da nuestro necesario atado\(c\). Ahora podemos definir

\(Num \left( a, y \right) =\)

\[\left( \exists c < \left( \bar{2}^{\left( a + \bar{1} \right)^{\left( a + \bar{1} \right)}} \right)^{\left( a + \bar{1} \right) \cdot \left( y + \bar{1} \right)} \right) NumConstructionSequence \left( c, a, y \right).\]

Las siguientes fórmulas que necesitamos discutir tratarán de la sustitución. Vamos a definir dos\(\Delta\) -fórmulas:

1. \(TermSub \left( u, x, t, y \right)\)representará la sustitución de un término por una variable en un término\(\left( u_t^x \right)\).
2. \(Sub \left( f, x, t, y \right)\)representará la sustitución de un término por una variable en una fórmula\(\left( \phi_t^x \right)\).

Específicamente, vamos a mostrar que\(\mathfrak{N} \models TermSub \left( \ulcorner u \urcorner, \ulcorner x \urcorner, \ulcorner t \urcorner, y \right)\) si y sólo si\(y\) es el número de Gödel de\(u_t^x\), donde se asume que\(u\) y\(t\) son términos y\(x\) es una variable. De igual manera,\(Sub \left( \ulcorner \phi \urcorner, \ulcorner x \urcorner, \ulcorner t \urcorner, y \right)\) será cierto si y sólo si\(\phi\) es una fórmula y\(y = \ulcorner \phi_t^x \urcorner\).

Vamos a desarrollar\(TermSub\) cuidadosamente y delinear la construcción de\(Sub\), dejando los detalles al lector.

Primero, veamos un ejemplo. Supongamos que ese\(u\) es el término\(+ \cdot 0S0x\). Entonces una secuencia de construcción para\(u\) podría parecerse

\[\left( 0, x, S0, \cdot 0S0, + \cdot 0S0x \right).\]

Si\(t\) es el término\(SS0\), entonces\(u_t^x\) es\(+ \cdot 0S0SS0\), y encontraremos una secuencia de construcción para este término por etapas.

Lo primero que haremos es mirar la secuencia (ya no una secuencia de construcción) que obtenemos reemplazando todas las secuencias de construcción\(x\)\(u\)'s in por\(t\)'s:

\[\left( 0, SS0, S0, \cdot 0S0, + \cdot 0S0SS0 \right).\]

Esto no logra ser una secuencia de construcción, ya que el segundo término de la secuencia es ilegal. Sin embargo, si precedemos a todo esto con la secuencia de construcción para\(t\), todo estará bien (recordemos que se nos permite repetir elementos en una secuencia de construcción):

\[\left( 0, S0, SS0, 0, SS0, S0, \cdot 0S0, + \cdot 0S0SS0 \right).\]

Entonces, para que todo esto funcione, tenemos que hacer tres cosas:

1. Debemos mostrar cómo cambiar la secuencia\(u\) de construcción reemplazando las ocurrencias de\(x\) con\(t\).
2. Debemos mostrar cómo poner una secuencia de construcción frente a otra.
3. Debemos asegurarnos de que todos nuestros cuantificadores estén acotados a lo largo, para que nuestra fórmula final\(TermSub\) sea una\(\Delta\) fórmula.

Entonces, primero definimos una fórmula\(TermReplace \left( c, u, d, x, t \right)\) tal que si\(c\) es el código para una secuencia de construcción de un término con número de Gödel\(u\), entonces\(d\) es el código de la secuencia (probablemente no una secuencia de construcción) que resulta de reemplazar cada ocurrencia de la variable con el número de Gödel \(x\)por el término con número de Gödel\(t\). En la siguiente definición, la idea es que\(e_i\) y\(a_i\) son las entradas en posición\(i\) de la secuencia codificadas por\(c\) y\(d\), respectivamente, y si la miramos línea por línea vemos:\(c\) codifica una secuencia de construcción para el término codificado por\(u\), \(d\)codifica una secuencia; las longitudes de las dos secuencias son las mismas; si\(e_i\) y\(a_i\) son las\(i^\text{th}\) entradas en secuencia\(c\) y\(d\), respectivamente, entonces\(e_i\) codifica 0 si y solo si\(a_i\) también codifica 0;\(e_i\) codifica el sucesor de un anterior \(e_j\)si y sólo si\(a_i\) codifica al sucesor del correspondiente\(a_j\); y así sucesivamente.

\(TermReplace \left( c, u, d, x, t \right) =\)

\[TermConstructionSequence \left( c, u \right) \land Codenumber \left( d \right) \land \\ \left( \exists l < c \right) \left[ Length \left( c, l \right) \land Length \left( d, l \right) \land \\ \left( \forall i \leq l \right) \left( \forall e_i < c \right) \left( \forall a_i < d \right) \\ \left( \left( IthElement \left( e_i, i, c \right) \land IthElement \left( a_i, i, d \right) \right) \rightarrow \\ \left[ \left( \left[ \left( Variable \left( e_i \right) \land e_i = x \right) \leftrightarrow a_i = t \right] \land \\ \left( Variable \left( e_i \right) \land e_i \neq x \right) \leftrightarrow \left( Variable \left( a_i \right) \land a_i = e_i \right) \right) \land \\ \left( e_i = \bar{2}^{\bar{10}} \leftrightarrow a_i = \bar{2}^{\bar{10}} \right) \land \\ \left( \forall j < i \right) \left[ \left( \left( \exists e_j < c \right) IthElement \left( e_j, j, c \right) \land e_i = \bar{2}^{\bar{12}} \cdot \bar{3}^{e_j} \right) \rightarrow \\ \left( \left( \exists a_j < d \right) IthElement \left( a_j, j, d \right) \land a_i = \bar{2}^{\bar{12}} \cdot \bar{3}^{a_j} \right) \right] \land \\ \vdots \\ \left( \text{Similar clauses for} \: +, \cdot, \: \text{and} \: E. \right) \\ \vdots \\ \right] \right) \right].\]

Ahora que sabemos destruir una secuencia de construcción para\(u\) reemplazando todas las ocurrencias de\(x\) con\(t\), tenemos que poder poner un término secuencia de construcciones para delante de nuestra secuencia para convertirla nuevamente\(t\) en una secuencia de construcción. Entonces supongamos que\(d\) es el código para la secuencia que se obtiene reemplazando\(x\) por\(t\), y ese\(b\) es el código para el término secuencia de construcción para\(t\). Esencialmente, queremos\(a\) codificar\(d\) anexado a\(b\). Entonces la longitud de\(a\) es la suma de las longitudes de\(b\) y\(d\), y los primeros\(l\) elementos de la\(a\) secuencia deben ser los mismos que la\(b\) secuencia, donde está la longitud de la\(b\) secuencia\(l\), y el resto de la\(a\) secuencia debe coincidir, entrada por entrada, la\(d\) secuencia:

\(Append \left( b, d, a \right) =\)

\[Codenumber \left( b \right) \land Codenumber \left( d \right) \land Codenumber \left( a \right) \land \\ \left( \exists l < b \right) \left( \exists m < d \right) \left( Length \left( l, b \right) \land \\ Length \left( m, d \right) \land Length \left( l + m, a \right) \land \\ \left( \forall e < a \right) \left( \forall i \leq l \right) \left[ IthElement \left( e, i, a \right) \leftrightarrow IthElement \left( e, i, b \right) \right] \land \\ \left( \forall e < a \right) \left( \forall j \leq m \right) \left[ 0 < j \rightarrow \\ \left( IthElement \left( e, l+ j, a \right) \leftrightarrow IthElement \left( e, j, d \right) \right) \right] \right).\]

Ahora estamos listos para definir la fórmula\(TermSub \left( u, x, t, y \right)\) que se supone que es verdadera si y solo si\(y\) es el (número de Gödel del) término que resulta cuando se toma el término (con el número de Gödel)\(u\) y se reemplaza (la variable con el número de Gödel)\(x\) por (el término con el número de Gödel)\(t\). Un primer intento de definición podría ser

\[\left( \exists a \right) \left( \exists b \right) \left( \exists d \right) \left( \exists c \right) \left[ TermConstructionSequence \left( c, u \right) \land \\ TermConstructionSequence \left( b, t \right) \land \\ TermReplace \left( c, u, d, x, t \right) \land Append \left( b, d, a \right) \land \\ TermConstructionSequence \left( a, y \right) \right].\]

Esto es agradable, pero necesitamos encuadernar todos los cuantificadores. Limitar\(b\) y\(d\) es fácil: Son más pequeños que\(a\). En cuanto a\(c\), mostramos cuando definimos la fórmula\(Term \left( a \right)\) que el término codificado por\(u\) debe tener una secuencia de construcción codificada por un número menor que\(\left( 2^{u^u} \right)^{u^2 + u}\). Entonces todo lo que queda es encontrar un atado\(a\). Observe que podemos suponer que\(b\) codifica una secuencia de longitud menor o igual a\(t\), la última entrada de\(b\), y de manera similar,\(c\) codifica una secuencia menor o igual a\(u\). Dado que la secuencia codificada por\(d\) tiene la misma longitud que la secuencia codificada por\(c\), y como secuencia de\(a\) códigos\(b\) seguida\(d\) de's, la longitud de la secuencia codificada por\(a\) es menor o igual a\(u + t\). Entonces

\[a \leq 2^{e_1} 3^{e_2} \cdots p_{t+u}^y.\]

Ahora reflejamos la definición de\(TermConstructionSequence\). Como cada entrada de se\(a\) puede suponer que es menor o igual a\(y\), obtenemos

\[\begin{align} a &\leq 2^y 3^y \ldots p_{t+u}^y \\ &\leq \left[ \left( p_{t+u} \right)^y \right]^{t+u} \\ &\leq \left( \left[ 2^{t+u^{t+u}} \right]^y \right)^{t+u}. \end{align}\]

Entonces nuestra\(\Delta\) -definición de\(TERMSUB\) es

\(TermSub \left( u, x, t, y \right) =\)

\[\left( \exists a < \left( \left[ \bar{2}^{t+u^{t+u}} \right]^y \right)^{t+u} \right) \left( \exists b < a \right) \left( \exists d < a \right) \left( \exists c < \left( \bar{2}^{u^u} \right)^{u^{\bar{2}} + u} \right) \\ \left[ TermConstructionSequence \left( c, u \right) \land \\ TermConstructionSequence \left( b, t \right) \land TermReplace \left( c, u, d, x, t \right) \land Append \left( b, d, a \right) \land \\ TermConstructionSequence \left( a, y \right) \right].\]

Basura: Casos de basura. Qué molestia. Nuestra afirmación en el párrafo anterior a la definición de\(TermSub\) que cada entrada de\(a\) será menor o igual a\(y\) podría no ser correcta si\(y = u_t^x = u\), por lo que la sustitución es vacua. La razón de esto es que las entradas de\(a\) incluirían una secuencia de construcción para\(t\), que podría ser enorme, mientras que\(y\) podría ser relativamente pequeña. Por ejemplo, podríamos tener\(u = 0\) y\(t = v_{123456789}\) y\(x = v_1\). En el Ejercicio 3 se le invita a averiguar la ligera adición a la definición de\(TermSub\) que se encarga de esto.

Ahora esbozamos la construcción de la fórmula\(Sub \left( f, x, t, y \right)\), que es para ser verdad si\(f\) es el número de Gödel de una fórmula\(\phi\) y\(y\) es\(\ulcorner \phi_t^x \urcorner\). La idea es tomar una secuencia de construcción de fórmulas\(\phi\) y seguirla por una copia de la misma secuencia de construcción donde reemplazamos sistemáticamente las ocurrencias de\(x\)\(t\) con's, aunque hay que tener un poco de cuidado en sus reemplazos. Si comparas Definiciones 1.8.1 y 1.8.2, puedes ver que las reglas para reemplazar variables por términos son un poco más complicadas en el caso de la fórmula que en el caso del término, particularmente cuando estás sustituyendo en una fórmula cuantificada. Pero las dificultades no son tan malas.

Entonces, si\(b\) codifica la secuencia de construcción para\(\phi\), si\(d\) codifica la secuencia que obtiene después de reemplazar los\(x\)'s\(t\) by's, y si se\(Append \left( b, d, a \right)\) mantiene, entonces\(a\) codificará una secuencia de construcción para\(\phi_t^x\). Después de lidiar con los límites, tendrás una\(\Delta\) fórmula en la línea de

\(Sub \left( f, x, t, y \right) =\)

\[\left( \exists a < \: \text{Bound} \right) \left( \exists b < a \right) \left( \exists d < a \right) \\ FormulaConstructionSequence \left( b, f \right) \land \\ FormulaReplace \left( b, f, d, x, t \right) \land Append \left( b, d, a \right) \land \\ FormulaConstructionSequence \left( a, y \right).\]

Ejercicios

1. Escribe la fórmula\(NumConstructionSequence \left( c, a, y \right)\). Asegúrate de que tu fórmula sea una\(\Delta\) fórmula con las variables\(c\),\(a\), y\(y\) libre. [Sugerencia: Es posible que desee modelar su respuesta sobre la construcción de\ (TermConstructionSequence).]
2. Escriba las “Cláusulas Similares” en la definición de\(TermReplace\).
3. Cambiar la definición de\(TermSub\) para atender el problema mencionado en la Chaffa siguiendo la definición. [Sugerencia: El problema ocurre sólo si la sustitución es vacua. Entonces hay dos casos. O bien\(u\) y\(y\) son diferentes, en cuyo caso nuestra definición está bien, o\(u\) y\(y\) son iguales. ¿Qué necesitas hacer entonces? Entonces te sugerimos que tu respuesta sea una disyunción, algo así como
   \(MyTermSub \left( u, x, t, y \right) =\)
   \[\left[ \left( u \neq y \right) \land TermSub \left( u, x, t, y \right) \right] \lor \left[ \left( u = y \right) \land \left( \text{Something Brilliant} \right) \right].\]
4. Escribe los detalles de la fórmula\(Sub\).