5.11: La colección de axiomas es representable
- Page ID
- 113531
En esta sección expondremos dos\(\Delta\) -fórmulas que están diseñadas para escoger los axiomas de nuestro sistema deductivo.
La colección de números de Gödel de los axiomas de\(N\) es representable.
La fórmula\(AxiomOfN\) es fácil de describir. Como solo hay un número finito de\(N\) -axiomas, un número natural\(a\) está en el conjunto\(AXIOMOFN\) si y solo si es uno de un número finito de números de Gödel. Así
\(AxiomOfN \left( a \right) =\)
\[a = \overline{\ulcorner \left( \forall x \right) \neg Sx = 0 \urcorner} \lor \\ a = \overline{\ulcorner \left( \forall x \right) \left( \forall y \right) \left[ Sx = Sy \rightarrow x = y \right] \urcorner} \lor \\ \vdots \\ \lor a = \overline{ \ulcorner \left( \forall x \right) \left( \forall y \right) \left[ \left( x < y \right) \lor \left( x = y \right) \lor \left( y < x \right) \right] \urcorner}.\]
(Para ser más de lo habitual quisquilloso, necesitamos cambiar los\(x\) “s” y “"\(y\) s "\(v_1\)” y\(v_2\) “" s "”, pero puedes hacerlo).”
La colección de números de Gödel de los axiomas lógicos es representable.
La fórmula que reconoce los axiomas lógicos es más complicada que la fórmula\(AxiomOfN\) por dos razones. El primero es que hay infinitamente muchos axiomas lógicos, así que no podemos limitarnos a enumerarlos todos. La segunda razón por la que este grupo de axiomas es más complicado es que los axiomas cuantificadores dependen de la noción de sustituibilidad, por lo que tendremos que utilizar nuestros resultados de la Sección 5.10.
Muy probablemente estés en un punto en el que podrías recurrir a la Sección 2.3.3 y escribir una\(\Delta\) -definición del conjunto\(LOGICALAXIOM\). Hacerlo sería un ejercicio que valía la pena. Pero si te sientes perezoso, aquí tienes un intento:
\(LogicalAxiom \left( a \right) =\)
\[\left( \exists x < a \right) \left( Variable \left( x \right) \land a = \bar{2}^\bar{8} \bar{3}^{Sx} \bar{5}^{Sx} \right) \lor \\ \left( \exists x, y < a \right) \left( Variable \left( x \right) \land Variable \left( y \right) \land \\ a = \bar{2}^\bar{4} \bar{3}^{\left( \bar{2}^\bar{2} \bar{3}^{\left( \bar{2}^\bar{8} \bar{3}^{Sx} \bar{5}^{Sy} + 1 \right)} + 1 \right)} \bar{5}^{\left( \bar{2}^\bar{8} \bar{3}^{\bar{2}^\bar{12} \bar{3}^{Sx} + 1} \bar{5}^{\bar{2}^\bar{12} \bar{3}^{Sy} + 1} + 1 \right)} \right) \lor \\ \left( \left( \exists x_1, x_2, y_1, y_2 < a \right) \left( Variable \left( x_1 \right) \land \cdots \land Variable \left( y_2 \right) \land \\ a = \: \text{Ugly Mess saying} \: \left[ \left( x_1 = y_1 \right) \land \left( x_2 = y_2 \right) \right] \rightarrow \\ \left( x_1 + x_2 = y_1 + y_2 \right) \right) \right) \lor \\ \vdots \\ \text{(Similar clauses coding up (E2) and (E3) for} \: \cdot, E, =, \: \text{and} \: < \text{)} \\ \vdots \\ \lor \left( \exists f , x, t, y < a \right) \left( Formula \left( f \right) \land Variable \left( x \right) \land Term \left( t \right) \land \\ Substitutable \left( t, x, f \right) \land Sub \left( f, x, t, y \right) \land \\ a = \bar{2}^\bar{4} \bar{3}^{\left( \bar{2}^\bar{2} \bar{3}^{\left( \bar{2}^\bar{6} \bar{3}^{Sx} \bar{5}^{Sf} + 1 \right)} + 1 \right)} \bar{5}^{Sy} \right) \lor \\ \text{(Similar clause for Axiom (Q2))}.\]
Para ver esto con un poco más de detalle, se supone que la primera cláusula de la fórmula corresponde al axioma (E1):\(x = x\) para cada variable\(x\). Así\(a\) es el número Gödel de un axioma de esta forma si hay alguna\(x\) que sea el número Gödel de una variable [que es lo que\(Variable \left( x \right)\) dice] tal que\(a\) es el número de Gödel de una fórmula que parece
variable con número Gödel\(x =\) variable con número Gödel\(x\).
Pero el número de Gödel para esta fórmula es justo\(2^8 3^{Sx} 5^{Sx}\), así que eso es lo que exigimos ese\(a\) igual.
La segunda cláusula abarca los axiomas de la forma (E2), cuando la función\(f\) es la función\(S\). Exigimos que\(a\) sea el código para la fórmula
\[\left( v_i = v_j \right) \rightarrow Sv_i = Sv_j,\]
dónde\(x = \ulcorner v_i \urcorner\) y\(y = \ulcorner v_j \urcorner\). Después de alboroto con la codificación, sales con la expresión que se muestra. Las demás cláusulas de tipo (E2) y (E3) son similares.
La última cláusula que se escribe es para los axiomas cuantificadores (Q1). Después de exigir que el término codificado por\(t\) sea sustitutable por la variable codificada por\(x\) en la fórmula codificada por\(f\) y que\(y\) sea el código para el resultado de sustituir de esa manera, la ecuación para no\(a\) es más que el análogo de\(\left( \forall x \phi \right) \rightarrow \phi_t^x\).
Ejercicios
- Completar la definición de la fórmula\(LogicalAxiom\).