5.12: Deducciones de codificación

Probablemente sea difícil de recordar en este punto de nuestro viaje, pero nuestro objetivo es probar el Teorema de Incompletitud, y para ello necesitamos escribir una\(\mathcal{L}_{NT}\) -oración que sea cierta en\(\mathfrak{N}\), la estructura estándar, pero no demostrable desde los axiomas de\(N\). Nuestra frase,\(\theta\), va a “decir” que no\(\theta\) es demostrable a partir de\(N\), y para “decir” eso, necesitaremos una fórmula que identifique los (números de Gödel del) fórmulas que son probables a partir de\(N\). Para ello tendremos que poder codificar deducciones de\(N\), lo que hace necesario codificar secuencias de\(\mathcal{L}_{NT}\) -fórmulas.

Hemos sido bastante cuidadosos con nuestra codificación hasta este punto. Si verifica, cada número de Gödel que hemos utilizado ha sido par, con la excepción de 3, que es el caso de basura en la Definición 5.7.1. Ahora usaremos números con el factor primo más pequeño 5 para codificar secuencias de fórmulas.

Supongamos que tenemos la secuencia de fórmulas

\[D = \left( \phi_1, \phi_2, \ldots, \phi_k \right).\]

Vamos a definir el código de secuencia\(D\) de ser el número

\[\ulcorner D \urcorner = 5^{\ulcorner \phi_1 \urcorner} 7^{\ulcorner \phi_2 \urcorner} \cdots p_{k+2}^{\ulcorner \phi_k \urcorner}.\]

Entonces, el exponente en el\(\left( i + 2 \right)^\text{nd}\) primo es el número Gödel del\(i^\text{th}\) elemento de la secuencia. Se le pide en los Ejercicios producir varias\(\mathcal{L}_{NT}\) fórmulas útiles relacionadas con los códigos de secuencia.

Estaremos interesados en usar códigos de secuencia para codificar deducciones de\(N\). Si miras hacia atrás a la definición de una deducción (Definición 2.2.1), verás que para verificar si una secuencia es una deducción, solo necesitamos verificar que cada entrada sea un axioma o siga de líneas anteriores de la deducción vía una regla de inferencia. Por lo que decir que\(c\) codifica una deducción de\(N\), queremos poder decir, para cada entrada\(e\) en posición\(i\) de la deducción codificada por\(c\),

\[AxiomOfN \left( e \right) \lor LogicalAxiom \left( e \right) \lor RuleOfInference \left( c, e, i \right).\]

Los dos primeros de estos ya los hemos desarrollado. El último gran objetivo de esta sección (y de este capítulo) es dar a conocer los detalles de una\(\Delta\) -definición de una fórmula que reconozca cuando una entrada en una deducción se justifica por una de nuestras reglas de inferencia.

Como recuerda de la Sección 2.4, existen dos tipos de reglas de inferencia: la consecuencia proposicional y las reglas del cuantificador. Este último de estos es más fácil de\(\Delta\) -definir, por lo que nos ocupamos primero de ello.

La regla de inferencia (QR) es la Definición 2.4.6, que dice que si no\(x\) es libre en\(\psi\), entonces las siguientes son reglas de inferencia:

\[\left( \{ \psi \rightarrow \phi \}, \psi \rightarrow \left( \forall x \phi \right) \right) \\ \left( \{ \phi \rightarrow \psi \}, \left( \exists x \phi \right) \rightarrow \psi \right).\]

Si miramos el primero de estos, vemos que si\(e\) es una entrada en un código para una deducción, y\(e = \ulcorner \psi \rightarrow \left( \forall x \phi \right) \urcorner\), entonces\(e\) se justifica siempre y cuando haya una entrada anterior en la deducción que codifique la fórmula\(\psi \rightarrow \phi\), asumiendo que no\(x\) es libre en\(\psi\). Entonces todo lo que tenemos que hacer es encontrar nuestra forma de decir esto.

Escribiremos la fórmula\(QRRule1 \left( c, e, i \right)\), donde\(c\) está el código de la deducción, y\(e\) es la entrada en posición\(i\) que está siendo justificada por la primera regla del cuantificador. En lo siguiente,\(f\) está desempeñando el papel de\(\ulcorner \psi \urcorner\), mientras que\(g\) se supone que es\(\ulcorner \phi \urcorner\):

\(QRRule1 \left( c, e, i \right) =\)

\[SequenceCode \left( c \right) \land IthSequenceElement \left( e, i, c \right) \land \\ \left( \exists x, f, g < c \right) \left[ Formula \left( f \right) \land Formula \left( g \right) \land Variable \left( x \right) \land \\ \neg Free \left( x, f \right) \land \\ e = \bar{2}^\bar{4} \bar{3}^{\bar{2}^\bar{2} \bar{3}^{Sf} + 1} \bar{5}^{\bar{2}^\bar{6} \bar{3}^{Sx} \bar{5}^{Sy} + 1} \land \\ \left( \exists j < i \right) \left( \exists e_j < c \right) \left( IthSequenceElement \left( e_j, j, c \right) \land \\ e_j = \bar{2}^\bar{4} \bar{3}^{\bar{2}^\bar{2} \bar{3}^{Sf} + 1} \bar{5}^{Sg} \right) \right].\]

Después de escribir\(QRRule2\) en los Ejercicios, es obvio definir

\(QRRule \left( c, e, i \right) =\)

\[QRRule1 \left( c, e, i \right) \lor QRRule2 \left( c, e, i \right).\]

Ahora tenemos que abordar la consecuencia proposicional. Esto implicará alguna codificación bastante complicada, así que manténgase firme mientras revisamos la lógica proposicional.

Supongamos que\(D\) es nuestra deducción, y\(D\) es la secuencia de fórmulas

\[\left( \alpha_1, \alpha_2, \alpha_3, \ldots, \alpha_k \right).\]

Observe que el ingreso\(\alpha_i\) de una deducción se justifica como consecuencia proposicional si y solo si la fórmula

\[\beta = \left( \alpha_1 \land \alpha_2 \land \cdots \land \alpha_{i-1} \right) \rightarrow \alpha_i\]

es una tautología.

Ahora, como discutimos en la Sección 2.4, para decidir si una fórmula de primer orden\(\beta\) es una tautología, debemos tomar\(\beta\) y encontrar la fórmula proposicional\(\beta_P\). Entonces si\(\beta_P\) es

\[\left[ \left( \alpha_1 \right)_P \land \left( \alpha_2 \right)_P \land \cdots \land \left( \alpha_{i-i} \right)_P \right] \rightarrow \left( \alpha_i \right)_P,\]

debemos mostrar cualquier asignación de verdad que haga\(\left( \alpha_1 \right)_P\) a través de la\(\left( \alpha_{i-1} \right)_P\) verdad también debe hacer\(\left( \alpha_i \right)_P\) realidad.

Como se describe en la Sección 2.4, para crear una versión proposicional de una fórmula, primero debemos encontrar los componentes primos de esa fórmula, donde un componente primo es una subfórmula que es universal y no está contenida en ninguna otra subfórmula universal, o atómica y no contenida en ninguna fórmula universal. En lugar de escribir explícitamente una\(\Delta\) fórmula -que identifique a los pares\(\left( u, v \right)\) tal que\(u\) sea el número Gödel de un componente primo de la fórmula con el número de Gödel\(v\), escribamos una definición recursiva de este conjunto de fórmulas, y dejaremos que el lector encuentre la modificación menor del Teorema 5.10.2, que garantizará que este conjunto de números de Gödel sea representable.

Definición 5.12.1.

Si\(\beta\) y\(\gamma\) son\(\mathcal{L}_{NT}\) -formulas,\(\gamma\) se dice que es un componente primo de\(\beta\) if:

1. \(\beta\)es atómico y\(\gamma = \beta\), o
2. \(\beta\)es universal y\(\gamma = \beta\), o
3. \(\beta\)es\(\neg \alpha\) y\(\gamma\) es un componente principal de\(\alpha\), o
4. \(\beta\)es\(\alpha_1 \lor \alpha_2\) y\(\gamma\) es un componente principal de cualquiera\(\alpha_1\) o\(\alpha_2\).

proposición 5.12.2.

El conjunto

\(PRIMECOMPONENT =\)

\[\{ \left( u, f \right) | u = \ulcorner \gamma \urcorner \: \text{and} \: f = \ulcorner \beta \urcorner \: \text{and} \: \gamma \: \text{is a prime component of} \: \beta \: \text{for some} \: \mathcal{L}_{NT} \text{-formulas} \: \gamma \: \text{and} \: \beta \}\]

es representable y tiene\(\Delta\) -definición\(PrimeComponent \left( u, f \right)\).

prueba

Teorema 5.10.2.

Ahora vamos a codificar una secuencia canónica de todos los componentes principales de\(\alpha_1\) through\(\alpha_i\). Diremos los\(r\) códigos PrimeList para las primeras\(i\) entradas de la deducción codificada por\(c\) si cada elemento codificado por\(r\) es un componente primo de una de las primeras\(i\) entradas de la deducción codificada por\(c\),\(r\)'s elementos son distintos, cada componente primo de cada una de las primeras\(i\) entradas de la deducción codificada por\(c\) se encuentra entre las entradas en\(r\), y si\(s\) es un número de código menor,\(s\) le falta uno de estos componentes primos:

\(PrimeList \left( c, i, r \right) =\)

\[SequenceCode \left( c \right) \land CodeNumber \left( r \right) \land \\ \left( \exists l < r \right) \left[ Length \left( r, l \right) \land \\ \left( \forall m, n \leq l \right) \left( \forall e_m, e_n < r \right) \\ \left( IthElement \left( e_m, m, r \right) \land IthElement \left( e_n, n, r \right) \right) \rightarrow \\ \left( \left( \exists k \leq i \right) \left( \exists f_k \leq c \right) IthSequenceElement \left( f_k, k, c \right) \land \\ PrimeComponent \left( e_m, f_k \right) \land \\ \left[ \left( m \neq n \right) \rightarrow \left( e_m \neq e_n \right) \right] \right) \land \\ \left[ \left( \forall k \leq i \right) \left( \forall f_k \leq c \right) \left( \forall u \leq f_k \right) \left( IthSequenceElement \left( f_k, k, c \right) \land \\ PrimeComponent \left( u, f_k \right) \rightarrow \\ \left( \exists m < l \right) IthElement \left( u, m, r \right) \right) \right] \right] \land \\ \left( \forall s < r \right) \left( CodeNumber \left( s \right) \rightarrow \\ \left( \exists k \leq i \right) \left( \exists f_k \leq c \right) \left( \exists u \leq f_k \right) \left[ IthSequenceElement \left( f_k, k, c \right) \land \\ PrimeComponent \left( u, f_k \right) \land \\ \left( \forall m < s \right) \left( \neg IthElement \left( u, m, s \right) \right) \right] \right)\]

Para decidir si\(\beta\) es una tautología, necesitamos asignar todos los valores de verdad posibles a todos los componentes principales de nuestra lista, y luego evaluar la verdad de cada uno\(\alpha_i\) bajo una asignación de verdad dada. Entonces, lo siguiente que tenemos que hacer es encontrar una manera de codificar una asignación de valores de verdad a todos los componentes primos de todos los\(\alpha_i\) 's. diremos que\(v\) codifica una asignación de verdad si\(v\) es el número de código de una secuencia de la longitud correcta y todos los elementos codificados por\(v\) son 0 (para false) o 1 (para true).

\(TruthAssignment \left( c, i, r, v \right) =\)

\[PrimeList \left( c, i, r \right) \land CodeNumber \left( v \right) \land \\ \left( \exists l < r \right) \left( Length \left( r, l \right) \land Length \left( v, l \right) \land \\ \left( \forall i \leq l \right) \left( \forall e < v \right) \left( IthElement \left( e, i, v \right) \rightarrow \\ \left[ e = \bar{0} \lor e = \bar{1} \right] \right) \right).\]

Ahora, dada una asignación de verdad para los componentes principales de\(\alpha_1\) through\(\alpha_i\), codificados en\(v\), necesitamos ser capaces de evaluar la verdad de cada fórmula\(\alpha_n\) bajo esa asignación. Para ello tendremos que poder evaluar el valor de verdad de una sola fórmula.

Supongamos que primero miramos un ejemplo. Aquí hay una secuencia de construcción de fórmulas que termina con alguna fórmula\(\alpha\):

\[\left( 0 < x, x< y, \left( 0 < x \lor x < y \right), \neg \left( 0 < x \right), \left( \forall x \right) \left( 0 < x \lor x < y \right), \left[ \left( \forall x \right) \left( 0 < x \lor x < y \right) \lor \left( \neg 0 < x \right) \right] \left( \alpha \right) \right).\]

Supongamos que el PrimeList con el que estamos trabajando es

\[\left( \left( \forall x \right) \left( 0 < x \lor x < y \right), 0 < x \right)\]

y la asignación de verdad elegida para nuestro PrimeList es

\[\left( 0.1 \right).\]

Para asignar el valor de verdad\(\alpha\), seguimos a lo largo de la secuencia de construcción. Cuando vemos una entrada que está en PrimeList, asignamos a esa entrada el valor de verdad correspondiente de nuestra asignación de verdad. Si la entrada en la secuencia de construcción no es un componente primo, una de tres cosas podría ser cierta:

1. La entrada podría ser universal, en cuyo caso le asignamos valor de verdad 2 (para undefined).
2. La entrada podría ser una fórmula atómica que termina dentro del alcance de un cuantificador en\(\alpha\). Nuevamente, utilizamos el valor de la verdad 2.
3. La entrada podría ser la negación o disyunción de entradas anteriores en la secuencia de construcción. En este caso podemos averiguar su valor de verdad, siempre usando 2 si alguna de las partes tiene valor de verdad 2.

Entonces, para continuar nuestro ejemplo desde arriba, la secuencia de valores de la verdad sería

\[\left( 1, 2, 2, 0, 0, 0 \right).\]

El ejercicio 7 le pide que escriba una\(\Delta\) fórmula\(Evaluate \left( e, r, v, y \right)\), donde debe asumir que\(e\) es el número de Gödel para una fórmula\(\alpha\),\(r\) es un código para una lista que incluye todos los componentes primos de\(\alpha\),\(v\) es una TruthAssignation para\(r\), y\(y\) es el valor de verdad para\(\alpha\), dada la asignación de verdad\(v\). El ejercicio 8 también se refiere a esta fórmula.

Ahora, sabiendo evaluar la verdad de una sola fórmula\(\alpha\), podremos decidir si\(\alpha_i\), el\(i^\text{th}\) elemento de la supuesta deducción que está codificado por\(c\), puede justificarse por la regla de las consecuencias proposicionales. Recordemos que solo necesitamos verificar si

\[\left( \alpha_1 \land \alpha_2 \land \cdots \land \alpha_{i-1} \right) \rightarrow \alpha_i\]

es una tautología. Para ello, sólo necesitamos ver si alguna asignación de verdad que haga\(\alpha_1\) a través de la\(\alpha_{i-1}\) verdad también la hace\(\alpha_i\) realidad. Aquí está la\(\Delta\) -fórmula que dice esto, donde\(c\) codifica la supuesta deducción, y\(e\) se supone que es el código para el\(i^\text{th}\) ingreso en la deducción, la entrada que se va a justificar mediante un recurso a la regla PC:

\(PCRule \left( c, e, i \right) =\)

\[IthSequenceElement \left( e, i, c \right) \land \\ \left( \exists r < \left[ \bar{2}^{\left( c^\bar{2} \right)^{\left( c^\bar{2} \right)}} \right]^{c^\bar{3}} \right) \\ \left( \forall v < \left( \left[ \bar{2}^{\left( c^\bar{2} \right)^{\left( c^\bar{2} \right)}} \right]^{\overline{\ulcorner \bar{1} \urcorner}} \right)^{c^\bar{2}} \right) \\ \left( \left[ PrimeList \left( c, i, r \right) \land TruthAssignment \left( c, i, r, v \right) \right] \rightarrow \\ \left[ \left( \left( \forall j < i \right) \left( \exists e_j < c \right) \\ \left( IthSequenceElement \left( e_j, j, c \right) \land Evaluate \left( e_j, r, v, \bar{1} \right) \right) \right) \\ Evaluate \left( e, r, v, \bar{1} \right) \right] \right).\]

Ahora bien, para saber que esto funciona, debemos justificar los límites que hemos dado para\(r\) y\(v\). \(r\)Se supone que el número codifica la lista de componentes primos entre los primeros\(i\) elementos de la deducción\(c\). Así\(r\) es de la forma\(5^{\ulcorner \gamma_1 \urcorner} 7^{\ulcorner \gamma_2 \urcorner} \cdots p_{k+2}^{\ulcorner \gamma_k \urcorner}\), donde los componentes principales son\(\gamma_1\) a través\(\gamma_k\). Primero, necesitamos manejar el número de componentes primos que hay. Ya que\(c\) es el código para la deducción, hay menos que\(c\) fórmulas en la deducción, y cada una de esas fórmulas tiene un número de Gödel que es menor o igual a\(c\). Entonces cada fórmula en la deducción tiene menos que\(c\) símbolos en ella, y por lo tanto menos que componentes\(c\) primos. Entonces no tenemos más que\(c\) fórmulas, cada una con no más que componentes\(c\) primos, por lo que no hay más que componentes\(c^2\) primos totales en la deducción codificada por\(c\). Si nos fijamos en el número\(r\), vemos que

\[\begin{align} r &= 5^{\ulcorner \gamma_1 \urcorner} 7^{\ulcorner \gamma_2 \urcorner} \cdots p_{k+2}^{\ulcorner \gamma_k \urcorner} \\ &\leq 5^c 7^c \cdots p_{k+2}^c \\ &\leq 5^c 7^c \cdots p_{c^2}^c \\ &\leq \left[ 2^{\left( c^2 \right)^{\left( c^2 \right)}} \right]^{c^3}, \end{align}\]

donde la última línea depende de nuestro límite habitual para el tamaño de la\ (\ left (c^2\ right) th prime.

En cuanto a\(v\),\(v\) es un número de código que nos da los valores de verdad de los diversos componentes primos codificados en\(r\). Así\(v\) es de la forma\(2^{i_1} 3^{i_2} \cdots p_k^{i_k}\), donde hay componentes\(k\) primos, y cada uno\(i_j\) es\(\ulcorner \bar{0} \urcorner\) o bien\(\left( \ulcorner \bar{1} \urcorner \right)\). Por el argumento anterior, sabemos que no hay más que componentes\(c^2\) primos, entonces

\[\begin{align} v &= 2^{i_1} 3^{i_2} \cdots p_k^{i_k} \\ &\leq 2^{\ulcorner \bar{1} \urcorner} 3^{\ulcorner \bar{1} \urcorner} \cdots p_{c^2}^{\ulcorner \bar{1} \urcorner} \\ &\leq \left( \left[ 2^{\left( c^2 \right)^{\left( c^2 \right)}} \right]^{\ulcorner \bar{1} \urcorner} \right)^{c^2}. \end{align}\]

Así hemos justificado los límites dados para\(r\) y\(v\) en la definición de\(PCRule \left( c, e, i \right)\). Así tenemos una\(Delta\) -definición, y el conjunto\(PCRULE\) es representable.

Ahora tenemos que recordar dónde estábamos después de definimos\(QRRule\). Estamos pensando en codificar una supuesta deducción de\(N\), y necesitamos verificar todas las entradas de\(c\) para ver si son legales.\(c\) Ya hemos escrito\(\Delta\) -fórmulas\(LogicalAxiom\) y\(AxiomOfN\), y estamos trabajando en las reglas de inferencia. Las reglas del cuantificador fueron relativamente fáciles, por lo que luego escribimos una\(\Delta\) -fórmula\(PCRule \left( c, e, i \right)\) que es verdadera si y sólo si\(e\) es la\(i^\text{th}\) entrada de la deducción\(c\) y puede ser justificada por la regla PC.

Por fin, podemos decidir si\(c\) es el código para una deducción\(N\) de una fórmula con número Gödel\(f\):

\(Deduction \left( c, f \right) =\)

\[SequenceCode \left( c \right) \land Formula \left( f \right) \land \\ \left( \exists l < c \right) \left( SequenceLength \left( c, l \right) \land IthSequenceElement \left( f, l, c \right) \land \\ \left( \forall i \leq l \right) \left( \forall e < c \right) \left[ IthSequenceElement \left( e, i, c \right) \rightarrow \\ \left( LogicalAxiom \left( e \right) \lor AxiomOfN \left( e \right) \lor \\ QRRule \left( c, e, i \right) \lor PCRule \left( c, e, i \right) \right) \right] \right).\]

Esta fórmula representa el conjunto\(DEDUCTIONS \subseteq \mathbb{N}^2\) y muestra que\(DEDUCTION\) es un conjunto representable. Dada la Tesis de Iglesia, esto hace formales las ideas del Capítulo 2, donde se sugirió que deberíamos poder programar una computadora para decidir si una supuesta deducción es, de hecho, una deducción. Dijimos antes que si una computadora pudiera decidir si un supuesto axioma era un axioma, es decir, si la colección de axiomas era representable, y si un uso de una regla de inferencia era legítimo, entonces podría verificar si una supuesta deducción estaba bien. Esto nos lleva a un punto ligeramente pegajoso.

Notarás que hemos estado usando cuidadosamente la cuantificación acotada y que la fórmula\(Deduction \left( c, f \right)\) anterior es una\(\Delta\) fórmula. Pero eso depende de que la colección de axiomas\(N\) tenga una\(\Delta\) -definición, que es más restrictiva que simplemente decir que la colección de axiomas es un conjunto representable. Entonces tal vez, si\(A\) es un conjunto representable de axiomas que no tiene una\(\Delta\) -definición, tenemos un problema. Afortunadamente, este no es el caso.

Supongamos que\(A\) es un conjunto representable de axiomas. Sabemos, a través de los Ejercicios 13 y 14 de la Sección 5.3, que\(A\) tiene una definición determinada numéricamente\(AxiomOfA \left( e \right)\). Además, si definimos la fórmula\(Deduction_A\) como arriba, reemplazando\(AxiomOfN\) con\(AxiomOfA\), entonces\(Deduction_A\) es una fórmula determinada numéricamente que define el conjunto\(DEDUCTION_A\), y así el conjunto de códigos de deducciones de nuestro conjunto representable de axiomas\(A\) es en sí mismo representable y nuestro computadora puede, de hecho, verificar si una supuesta deducción de\(A\) es, de hecho, una deducción de A.

Si mantienes en tu cabeza la equivalencia entre “decidible por computadora” y representable, diremos más sobre esto en los Capítulos 6 y 7.

Ejercicios

1. Escribe una\(\Delta\) fórmula\(SequenceCode \left( c \right)\) -que sea verdadera en\(\mathfrak{N}\) si y sólo si\(c\) es el código de una secuencia de\(\mathcal{L}_{NT}\) -fórmulas.
2. Escribe una\(\Delta\) fórmula\(SequenceLength \left( c, l \right)\) -que sea verdadera en\(\mathfrak{N}\) si y solo si\(c\) es un código de secuencia de una secuencia de longitud\(l\).
3. Escribe una\(\Delta\) fórmula\(IthSequenceElement \left( e, i, c \right)\) -que sea verdadera en\(\mathfrak{N}\) si y solo si\(c\) es un código de secuencia y el\(i^\text{th}\) elemento de la secuencia codificada por\(c\) tiene número de Gödel\(e\).
4. Escribe una\(\Delta\) fórmula\(QRRule2 \left( c, e, i \right)\) -que sea verdadera en\(\mathfrak{N}\) si\(e\) es la\(i^\text{th}\) entrada en la secuencia codificada por\(c\) y está justificada por la segunda regla del cuantificador.
5. Aquí está tu promedio, tautología ordinaria:
   \[\phi \left( x, y \right) \: \text{is} \: \left[ \left[ \forall x P \left( x \right) \right] \rightarrow \left( Q \left( x, y \right) \rightarrow \left[ \forall x P \left( x \right) \right] \right) \right].\]
   Encuentra una secuencia de construcción para\(\phi\). Haga una lista de los componentes principales de\(\phi\). Fingiendo que su lista de componentes principales es la lista principal para\(\phi\), encuentre todas las asignaciones de verdad posibles\(\phi\) y use las asignaciones de verdad para evaluar la verdad de\(\phi\) debajo de sus asignaciones. Si todo va bien, cada vez que evalúes la verdad de\(\phi\), obtendrás: Cierto.
6. Repita el Ejercicio 5 con las siguientes fórmulas, que no están (necesariamente) garantizadas para ser tautologías:
   a)\(\left( \forall x \right) \left( x < y \right) \rightarrow \left( \forall x \right) \left( x < y \right)\)
   b)\(\left( A \left( x \right) \lor B \left( y \right) \right) \lor \neg B \left( x \right)\)
   c) d\(\left( A \left( x \right) \lor B \left( y \right) \right) \rightarrow \left[ \left( \forall x \right) \left( \forall y \right) \left( A \left( x \right) \lor B \left( y \right) \right) \right]\)
   ) e)\(\left( \forall x \right) \left( x < y \rightarrow x < y \right)\)
   \(\left[ \left( \forall x \right) \left( \forall y \right) \left( A \left( x \right) \lor B \left( y \right) \right) \right] \rightarrow \left( A \left( x \right) \lor B \left( y \right) \right)\)
7. Escriba la\(\Delta\) fórmula\(Evaluate \left( e, r, v, y \right)\) -como se indica en el texto. Tendrás que pensar en las secuencias de construcción de fórmulas, como hiciste en el Ejercicio 6 en la Sección 5.8.
8. Mostrar por inducción en la más larga de las dos secuencias de construcción que si\(d_1\) y\(d_2\) son códigos para dos secuencias de construcción de\(\alpha\), y si\(Evaluate \left( d_1, r, v, y_1 \right)\) y\(Evaluate \left( d_2, r, v, y_2 \right)\) son ambas verdaderas, entonces\(y_1\) y\(y_2\) son iguales. Así, la verdad asignada\(\alpha\) no depende de la secuencia constructiva elegida para evaluar la verdad.