Autor Tema: Duda sobre consecuencias del principio de reflexión

0 Usuarios y 1 Visitante están viendo este tema.

22 Enero, 2024, 08:15 pm
Respuesta #10

Eparoh

  • $$\Large \color{#c88359}\pi\,\pi\,\pi\,\pi$$
  • Mensajes: 897
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola.

Es verdad lo que dices, pero, fallar, fallar, realmente no falla nada. Lo único que pasa es que en la definición 3.28 de mi libro de lógica puse que \( x\in M \) tiene a \( x \) como única variable libre porque no necesitaba otro caso allí, pero si admites que  \( x\in M \) tenga otras variables libres y prohíbes que estén en cualquier fórmula que relativices, todo funciona igual. Concretamente, las pruebas de los teoremas 3.29 y 3.30 (que es lo único que necesitas) funcionan exactamente igual, sin cambio alguno.

Vale, ya veo. En un vistazo rápido efectivamente no parece que vaya a fallar nada con lo que sugieres, pero recuerdo que justo para probar esos teoremas con todo detalle las cuentas salieron larguísimas... De momento me lo creo sin reparos, pero en algún momento revisaré las cuentas que en su día hicimos y si algo "fallara" ya te diría :P

Cuando pueda añadiré un comentario al respecto en mi libro de teoría de conjuntos sobre que admitir variables libres en \( x\in M \) no supone ningún problema. Si algo no te convence, dilo.

Cuando lo añadas, si puedes, avísame, que me gustaría ver los enunciados concretos con esta variante para asegurarme que no se me está escapando nada de momento.

Un saludo.

22 Enero, 2024, 08:46 pm
Respuesta #11

manooooh

  • $$\Large \color{#9c57a6}\pi\,\pi\,\pi\,\pi\,\pi\,\pi$$
  • Mensajes: 4,391
  • País: ar
  • Karma: +1/-0
  • Sexo: Masculino
Hola

Cuando pueda añadiré un comentario al respecto en mi libro de teoría de conjuntos sobre que admitir variables libres en \( x\in M \) no supone ningún problema. Si algo no te convence, dilo.

Cuando lo añadas, si puedes, avísame, que me gustaría ver los enunciados concretos con esta variante para asegurarme que no se me está escapando nada de momento.

Perdón la intromisión, no sigo mucho de lo que hablan, pero parece que pretendes que Carlos escriba una alternativa a algunos teoremas de su libro. Creo que lo que él quiso decir es que solamente pondrá una aclaración, no añadir teoremas que funcionan con su variante, aunque la tuya funcione igual de bien.

Saludos

22 Enero, 2024, 08:54 pm
Respuesta #12

Eparoh

  • $$\Large \color{#c88359}\pi\,\pi\,\pi\,\pi$$
  • Mensajes: 897
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola.

Perdón la intromisión, no sigo mucho de lo que hablan, pero parece que pretendes que Carlos escriba una alternativa a algunos teoremas de su libro. Creo que lo que él quiso decir es que solamente pondrá una aclaración, no añadir teoremas que funcionan con su variante, aunque la tuya funcione igual de bien.

No es escribir una alternativa, es simplemente que quiero ver como escribe la aclaración para indicar que los teoremas también funcionan en algo más de generalidad en el contexto de su libro que es donde aparecen dichos teoremas.

Un saludo.

22 Enero, 2024, 10:51 pm
Respuesta #13

Carlos Ivorra

  • Administrador
  • Mensajes: 11,114
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
Cuando lo añadas, si puedes, avísame, que me gustaría ver los enunciados concretos con esta variante para asegurarme que no se me está escapando nada de momento.

Ahora mismo no es buen momento para hacer cambios en mi libro de lógica, porque estoy escribiendo otro sobre la formalización de la metamatemática, empezando en la Aritmética Recursiva Primitiva y usando teorías más potentes según va siendo necesario hasta llegar a teorías aritméticas de segundo orden cuya consistencia es "controlable" en cierto sentido (es equivalente a la de la Aritmética de Peano o más débil, en casi todas ellas).

Luego, mi idea es eliminar de mi libro de lógica los resultados que no son realmente necesarios para profundizar en la teoría de conjuntos, remitiendo al nuevo libro para los de interés puramente lógico.

Así, una posibilidad es demostrar los teoremas necesarios sobre relativización de fórmulas en el caso particular de la teoría de conjuntos en el libro de Lógica en lugar de remitir al teorema general sobre interpretaciones, que pasaría al nuevo, aunque no sé si será eso lo que decida finalmente.

De todos modos, creo que hay una forma muy sencilla de trabajar en una situación totalmente general:

En la definición 3.28 de mi libro de Lógica se exige que una interpretación de una teoría \( S \) sobre un lenguaje \( \mathcal L_S \) en otra teoría \( T \) sobre un lenguaje \( \mathcal L_T \) asigne a cada variable \( x \) de \( \mathcal L_S \) una variable \( \bar x \) de \( \mathcal L_T \).

Luego, al introducir la fórmula \( x\in M \) de \( \mathcal L_T \), basta exigir que no tenga variables libres de la forma \( \bar y \), para ninguna variable \( y \) de \( \mathcal L_S \) (que la variable \( x \) sea o no de la forma \( \bar y \) es irrelevante, porque luego sólo vamos a usar fórmulas de la forma \( \bar x\in M \), es decir, cambiando la variable \( x \) por imágenes de variables de \( \mathcal L_S \), pero las demás variables posibles de \( x\in M \) nunca se van a sustituir por otras.) Actualmente, lo que se pide es que no haya más variables libres, que es un caso particular de pedir que no haya más variables libres asociadas a variables de \( \mathcal L_S \).

Lo mismo con los demás apartados de la definición: si \( c \) es una constante de \( \mathcal L_S \), no hace falta que \( c \) sea un designador de \( \mathcal L_T \). Basta con que sea un término cuyas variables libres no sean de la forma \( \bar y \). Si \( f \) es un funtor \( n \)-ádico, el término \( \bar f(x_1,\ldots, x_n) \) puede tener más variables libres a condición de que no sean de la forma \( \bar y \), etc.

Con esta definición, no hay que cambiar nada ni añadir ninguna hipótesis a los teoremas 3.29 y 3.30, y las demostraciones valen sin cambio alguno.

Para cada expresión \( \theta(x_1, \ldots, x_n) \), la traducción \( \bar \theta(\bar x_1, \ldots, \bar x_n) \) es otra expresión que, si tiene otras variables libres, no serán de la forma \( \bar y \), para ninguna variable \( y \) de \( \mathcal L_S \), y eso basta para que funcionen todos los argumentos sin cambio alguno. Simplemente, las posibles variables adicionales "no molestan", "no interfieren". De hecho, como no se hace nada con ellas, se tratan siempre como si fueran constantes y, si lo fueran, estaríamos en el caso en el que no hay más variables libres.

22 Enero, 2024, 11:32 pm
Respuesta #14

Carlos Ivorra

  • Administrador
  • Mensajes: 11,114
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
He revisado la sección correspondiente a la interpretación de teorías en el libro que estoy escribiendo y he añadido esta nota, que me parece suficiente:

Citar
Nota La definición de interpretación que hemos dado en es suficiente en nuestro contexto, pero conviene observar que puede generalizarse ligeramente para que los teoremas siguientes sean aplicables al contexto de los modelos internos de teorías de conjuntos.

Se trata simplemente de permitir que las expresiones \( x\in M, \bar c, \bar f(x_1, \ldots, x_n) \) o \( \bar R(x_1, \ldots, x_n) \) que se consideran en la definición puedan tener otras variables libres aparte de las indicadas, a condición de que éstas no sean de la forma \( \bar x \), para ninguna variable \( x \) de \( \mathcal L_S \).

Por ejemplo, si tomamos como \( \mathcal L_S \) el lenguaje \( \mathcal L_{\rm tc} \) de la teoría de conjuntos y como \( \mathcal L_T \) este mismo lenguaje pero con dos variables adicionales \( M, R \), podemos tomar como fórmula \( x\in M \) la fórmula \( x\in M\cup\{\emptyset\} \), (con lo que garantizamos que \( (u|u = u)\in M\cup\{\emptyset\} \), si tomamos al conjunto vacío como descripción impropia) y \( x\,\bar\in\, y\equiv (x, y)\in R \), y así tenemos una interpretación en este sentido más general, para el cual siguen siendo válidos los teoremas siguientes de esta sección.

Los teoremas siguientes son los correspondientes a 3.29 y 3.30.

En la nota estoy considerando la posibilidad de interpretar la relación de pertenencia como una relación arbitraria. En el contexto en el que tú trabajas, puedes omitir la \( R \) y tomar \( x\,\bar\in\, y\equiv x\in y \).

23 Enero, 2024, 07:33 pm
Respuesta #15

Eparoh

  • $$\Large \color{#c88359}\pi\,\pi\,\pi\,\pi$$
  • Mensajes: 897
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola Carlos.

Ahora mismo no es buen momento para hacer cambios en mi libro de lógica, porque estoy escribiendo otro sobre la formalización de la metamatemática, empezando en la Aritmética Recursiva Primitiva y usando teorías más potentes según va siendo necesario hasta llegar a teorías aritméticas de segundo orden cuya consistencia es "controlable" en cierto sentido (es equivalente a la de la Aritmética de Peano o más débil, en casi todas ellas).

Luego, mi idea es eliminar de mi libro de lógica los resultados que no son realmente necesarios para profundizar en la teoría de conjuntos, remitiendo al nuevo libro para los de interés puramente lógico.

Así, una posibilidad es demostrar los teoremas necesarios sobre relativización de fórmulas en el caso particular de la teoría de conjuntos en el libro de Lógica en lugar de remitir al teorema general sobre interpretaciones, que pasaría al nuevo, aunque no sé si será eso lo que decida finalmente.

Entiendo. Solo por curiosidad, si en tu libro de lógica solo dejaras los resultados necesarios para profundizar en la teoría de conjuntos, ¿qué partes son las que trasladarías al nuevo libro?

De todos modos, creo que hay una forma muy sencilla de trabajar en una situación totalmente general:

En la definición 3.28 de mi libro de Lógica se exige que una interpretación de una teoría \( S \) sobre un lenguaje \( \mathcal L_S \) en otra teoría \( T \) sobre un lenguaje \( \mathcal L_T \) asigne a cada variable \( x \) de \( \mathcal L_S \) una variable \( \bar x \) de \( \mathcal L_T \).

Luego, al introducir la fórmula \( x\in M \) de \( \mathcal L_T \), basta exigir que no tenga variables libres de la forma \( \bar y \), para ninguna variable \( y \) de \( \mathcal L_S \) (que la variable \( x \) sea o no de la forma \( \bar y \) es irrelevante, porque luego sólo vamos a usar fórmulas de la forma \( \bar x\in M \), es decir, cambiando la variable \( x \) por imágenes de variables de \( \mathcal L_S \), pero las demás variables posibles de \( x\in M \) nunca se van a sustituir por otras.) Actualmente, lo que se pide es que no haya más variables libres, que es un caso particular de pedir que no haya más variables libres asociadas a variables de \( \mathcal L_S \).

Lo mismo con los demás apartados de la definición: si \( c \) es una constante de \( \mathcal L_S \), no hace falta que \( c \) sea un designador de \( \mathcal L_T \). Basta con que sea un término cuyas variables libres no sean de la forma \( \bar y \). Si \( f \) es un funtor \( n \)-ádico, el término \( \bar f(x_1,\ldots, x_n) \) puede tener más variables libres a condición de que no sean de la forma \( \bar y \), etc.

Con esta definición, no hay que cambiar nada ni añadir ninguna hipótesis a los teoremas 3.29 y 3.30, y las demostraciones valen sin cambio alguno.

Para cada expresión \( \theta(x_1, \ldots, x_n) \), la traducción \( \bar \theta(\bar x_1, \ldots, \bar x_n) \) es otra expresión que, si tiene otras variables libres, no serán de la forma \( \bar y \), para ninguna variable \( y \) de \( \mathcal L_S \), y eso basta para que funcionen todos los argumentos sin cambio alguno. Simplemente, las posibles variables adicionales "no molestan", "no interfieren". De hecho, como no se hace nada con ellas, se tratan siempre como si fueran constantes y, si lo fueran, estaríamos en el caso en el que no hay más variables libres.

Entiendo la idea. Parece mucho más elegante sí. Pero entonces, cuando se hacen interpretaciones entre dos teorías sobre un mismo lenguaje, a la hora de interpretar las variables no podría usarla la aplicación identidad porque habría que "esquivar" las variables libres adicionales de \( x \in M \), ¿no?

Quiero decir, por ejemplo, para la demostración del ya famoso Lema 9 no debería tomar la identidad como identificación de las variables, sino algo así como tomar \( X \) como una variable de índice mayor que cualquiera de las que aparecen en \( \alpha_1, \cdots, \alpha_n, \alpha \) y definir

\( I(x_i)=\begin{cases}{x_i}&\text{si}& i < \text{Indice}(X)\\ x_{i+1} & \text{si}& i \geq \text{Indice}(X)\end{cases} \)

Entonces, se cumpliría lo que has propuesto pues no habría en \( X \) ninguna variable de la forma \( I(x) \) y, como al definirla así la asignación de variables si se cumple que, efectivamente, la traducción de \( \alpha_1, \cdots, \alpha_n, \alpha \) es justo su relativización, todo lo demás funciona igualmente.

He revisado la sección correspondiente a la interpretación de teorías en el libro que estoy escribiendo y he añadido esta nota, que me parece suficiente:

Citar
Nota La definición de interpretación que hemos dado en es suficiente en nuestro contexto, pero conviene observar que puede generalizarse ligeramente para que los teoremas siguientes sean aplicables al contexto de los modelos internos de teorías de conjuntos.

Se trata simplemente de permitir que las expresiones \( x\in M, \bar c, \bar f(x_1, \ldots, x_n) \) o \( \bar R(x_1, \ldots, x_n) \) que se consideran en la definición puedan tener otras variables libres aparte de las indicadas, a condición de que éstas no sean de la forma \( \bar x \), para ninguna variable \( x \) de \( \mathcal L_S \).

Por ejemplo, si tomamos como \( \mathcal L_S \) el lenguaje \( \mathcal L_{\rm tc} \) de la teoría de conjuntos y como \( \mathcal L_T \) este mismo lenguaje pero con dos variables adicionales \( M, R \), podemos tomar como fórmula \( x\in M \) la fórmula \( x\in M\cup\{\emptyset\} \), (con lo que garantizamos que \( (u|u = u)\in M\cup\{\emptyset\} \), si tomamos al conjunto vacío como descripción impropia) y \( x\,\bar\in\, y\equiv (x, y)\in R \), y así tenemos una interpretación en este sentido más general, para el cual siguen siendo válidos los teoremas siguientes de esta sección.

Los teoremas siguientes son los correspondientes a 3.29 y 3.30.

En la nota estoy considerando la posibilidad de interpretar la relación de pertenencia como una relación arbitraria. En el contexto en el que tú trabajas, puedes omitir la \( R \) y tomar \( x\,\bar\in\, y\equiv x\in y \).

Vale, después de escribir lo anterior acabo de leer esto, con el ejemplo que propones y veo que otra opción es simplemente ampliar el lenguaje de llegada con nuevas variables y, como la teoría axiomática que pusieras por encima será exactamente la misma, de esta forma queda mucho más elegante  ::)

Un saludo.

23 Enero, 2024, 09:40 pm
Respuesta #16

Carlos Ivorra

  • Administrador
  • Mensajes: 11,114
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
Entiendo. Solo por curiosidad, si en tu libro de lógica solo dejaras los resultados necesarios para profundizar en la teoría de conjuntos, ¿qué partes son las que trasladarías al nuevo libro?

Pues eso es algo que tendré que meditar detenidamente, pero, por poner un ejemplo: podríamos prescindir del hecho de que los teoremas conjuntistas demostrables en I\( \Sigma_1 \) son exactamente los teoremas de la teoría de Kripke-Platek más la negación del axioma de infinitud, y que los teoremas aritméticos de esta teoría son exactamente los de I\( \Sigma_1 \).

También podemos prescindir de que la Aritmética de Peano permite probar la consistencia de cualquier conjunto finito de sus axiomas (el teorema de reflexión aritmético).

También se puede eliminar todo lo tocante a lógica de segundo orden.

También se puede profundizar menos en la formalización de partes de la matemática en teorías aritméticas, limitándose a lo necesario para probar los teoremas de incompletitud...

En suma, aligerar resultados muy técnicos (aunque sean interesantes), pero que son prescindibles. Incluso se podría valorar no dar los detalles sobre cómo se prueba el segundo teorema de incompletitud formalizando algunos resultados lógicos en cualquier teoría aritmética, pero eso tendría que pensármelo. De todos modos, no estoy hablando de suprimir nada, sino de redistribuir la información entre dos libros para que cada cual pueda elegir lo que le interese.

Entiendo la idea. Parece mucho más elegante sí. Pero entonces, cuando se hacen interpretaciones entre dos teorías sobre un mismo lenguaje, a la hora de interpretar las variables no podría usarla la aplicación identidad porque habría que "esquivar" las variables libres adicionales de \( x \in M \), ¿no?

Sí, pero no tienes ninguna necesidad de interpretar una teoría en otra sobre el mismo lenguaje. Siempre puedes considerar que el lenguaje de la otra tiene unas variables adicionales, lo cual no cambia nada, y considerar que cada variable se traduce a ella misma.

Quiero decir, por ejemplo, para la demostración del ya famoso Lema 9 no debería tomar la identidad como identificación de las variables, sino algo así como tomar \( X \) como una variable de índice mayor que cualquiera de las que aparecen en \( \alpha_1, \cdots, \alpha_n, \alpha \) y definir

\( I(x_i)=\begin{cases}{x_i}&\text{si}& i < \text{Indice}(X)\\ x_{i+1} & \text{si}& i \geq \text{Indice}(X)\end{cases} \)

Entonces, se cumpliría lo que has propuesto pues no habría en \( X \) ninguna variable de la forma \( I(x) \) y, como al definirla así la asignación de variables si se cumple que, efectivamente, la traducción de \( \alpha_1, \cdots, \alpha_n, \alpha \) es justo su relativización, todo lo demás funciona igualmente.

Pero no necesitas hacerlo así. En el Lema 9, partes de una deducción, tomas una variable X que no aparezca en ella, y enuncias que si X es un conjunto tal que son teoremas de ZFC(+) las fórmulas ... etc., y luego usas que la deducción dada puede verse también como una deducción en el lenguaje formal de la teoría de conjuntos \( \mathcal L'_{\rm tc} \) cuyas variables son todas las de \( \mathcal L_{\rm tc} \) menos X, y usas que \( K_{\mathcal L'_{\rm tc}} \) está representado en \( K_{\mathcal L_{\rm tc}} \) mediante la fórmula \( x\in X \).

Vale, después de escribir lo anterior acabo de leer esto, con el ejemplo que propones y veo que otra opción es simplemente ampliar el lenguaje de llegada con nuevas variables y, como la teoría axiomática que pusieras por encima será exactamente la misma, de esta forma queda mucho más elegante  ::)

Sí, es otra forma de verlo. En el párrafo precedente, en lugar de ampliar, lo que hacía era quitar una variable, pero es lo mismo visto en sentido contrario.

25 Enero, 2024, 03:46 pm
Respuesta #17

Eparoh

  • $$\Large \color{#c88359}\pi\,\pi\,\pi\,\pi$$
  • Mensajes: 897
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola Carlos.

Pues eso es algo que tendré que meditar detenidamente, pero, por poner un ejemplo: podríamos prescindir del hecho de que los teoremas conjuntistas demostrables en I\( \Sigma_1 \) son exactamente los teoremas de la teoría de Kripke-Platek más la negación del axioma de infinitud, y que los teoremas aritméticos de esta teoría son exactamente los de I\( \Sigma_1 \).

También podemos prescindir de que la Aritmética de Peano permite probar la consistencia de cualquier conjunto finito de sus axiomas (el teorema de reflexión aritmético).

También se puede eliminar todo lo tocante a lógica de segundo orden.

También se puede profundizar menos en la formalización de partes de la matemática en teorías aritméticas, limitándose a lo necesario para probar los teoremas de incompletitud...

En suma, aligerar resultados muy técnicos (aunque sean interesantes), pero que son prescindibles. Incluso se podría valorar no dar los detalles sobre cómo se prueba el segundo teorema de incompletitud formalizando algunos resultados lógicos en cualquier teoría aritmética, pero eso tendría que pensármelo. De todos modos, no estoy hablando de suprimir nada, sino de redistribuir la información entre dos libros para que cada cual pueda elegir lo que le interese.

Entiendo. Y ya, por más curiosidad, ¿qué aparecerá en el nuevo libro que no esté en los que ya tienes actualmente? :P

Porque parte de lo que comentaste en el mensaje anterior, por ejemplo, sobre ARP, ya aparece en tu libro sobre el calculo secuencial de Gentzen, ¿no?

Respecto a las interpretaciones, todo claro ya, muchas gracias 8^)

Un saludo.

25 Enero, 2024, 04:11 pm
Respuesta #18

Eparoh

  • $$\Large \color{#c88359}\pi\,\pi\,\pi\,\pi$$
  • Mensajes: 897
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Hola de nuevo.

Una cosa que no me di cuenta antes.

Pero no necesitas hacerlo así. En el Lema 9, partes de una deducción, tomas una variable X que no aparezca en ella, y enuncias que si X es un conjunto tal que son teoremas de ZFC(+) las fórmulas ... etc., y luego usas que la deducción dada puede verse también como una deducción en el lenguaje formal de la teoría de conjuntos \( \mathcal L'_{\rm tc} \) cuyas variables son todas las de \( \mathcal L_{\rm tc} \) menos X, y usas que \( K_{\mathcal L'_{\rm tc}} \) está representado en \( K_{\mathcal L_{\rm tc}} \) mediante la fórmula \( x\in X \).

¿Por qué hace falta lo que comentas al final de que \( K_{\mathcal L'_{\rm tc}} \) está representado en \( K_{\mathcal L_{\rm tc}} \)? Quiero decir, si simplemente defino la teoría \( S \) sobre \( \mathcal L'_{\rm tc} \) cuyos axiomas no lógicos son \( \alpha_1, \cdots, \alpha_n \), ¿no puedo simplemente definir la interpretación de esta teoría sobre \( ZFC \) "normal" mediante la fórmula \( x\in X \)? Y, como en esta fórmula no aparece ninguna variable libre del lenguaje de \( S \) (salvo tal vez \( x \)), por lo que comentaste se puede aplicar el teorema 3.30 sin problemas igualemnte, ¿no?

EDITO: Me explico mejor. Primero se ve que \( S \) se interpreta en \( ZFC \) mediante \( x \in X \). Después se observa que, como en la deducción de \( \alpha \) a partir de \( \alpha_1, \cdots, \alpha_n \) no aparece \( X \), entonces es claro que dicha deducción será también una deducción en \( K_{\mathcal L'_{\rm tc}} \). Así, se tiene que \( \underset{S}{\vdash} \alpha \) y ya se puede aplicar sin problemas el Teorema 3.30.

Un saludo.

25 Enero, 2024, 04:33 pm
Respuesta #19

Carlos Ivorra

  • Administrador
  • Mensajes: 11,114
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
Entiendo. Y ya, por más curiosidad, ¿qué aparecerá en el nuevo libro que no esté en los que ya tienes actualmente? :P

Pues, por una parte, tenemos un cambio completo de enfoque: en mi libro de lógica actual incido mucho en la relación entre la metamatemática informal y la matemática formal, mientras que en el nuevo, una vez introducida informalmente la ARP y habiendo probado algunos resultados elementales sobre la interpretación de las fórmulas aritméticas en el modelo natural (para que quede claro que todo razonamiento formal nos proporciona un argumento informal, con un significado preciso) toda la metamatemática se introduce formalizada tomando la metateoría más débil posible (bueno, dentro de lo razonable, sin ánimo de apurar a lo mínimo, mínimo posible).

De este modo conseguimos una determinación precisa de qué hechos informales estamos usando cuando probamos informalmente cada teorema. Los argumentos puramente sintácticos son estrictamente finitistas y son formalizables en ARP, mientras que los resultados semánticos sobre modelos requieren trabajar con conjuntos no recursivos, y ello nos lleva a teorías un poco más fuertes.

Esto lleva a profundizar mucho más en las teorías aritméticas de segundo orden. Demuestro (y esto es "nuevo" —respecto de mis libros—) que la teoría conocida como RCA\( _0 \) (la aritmética de segundo orden con el axioma de comprensión recursiva) es una extensión conservativa de la ARP (o de I\( \Sigma_1) \), al igual que WKL\( _0 \) (la teoría de tomar como axioma el Lema de König Débil).

Para hacerte una idea genera que qué son estas teorías puedes mirar este artículo de la wikipedia.

Así, por ejemplo, WKL\( _0 \) es una teoría de segundo orden equiconsistente con la ARP y en la cual se puede demostrar formalmente el teorema de completitud semántica de Gödel. Esto es muy interesante, porque la prueba del teorema de completitud no es ni puede ser constructiva (prueba la existencia de conjuntos no recursivos), pero puede demostrarse en una teoría equiconsistente con ARP.

El hecho de que es una extensión conservativa de ARP (y por lo tanto equiconsistente) tenía fama de "duro de probar", pero he encontrado una demostración reciente relativamente sencilla de unos portugueses. Me refiero a una prueba puramente sintáctica, que no involucre modelos, lo cual me interesaba para no volver circular la demostración formal del teorema de completitud.

Sin embargo, en WKL\( _0 \) no es posible demostrar que a partir de un modelo en el sentido usual (de un conjunto con unas relaciones y funciones) es posible definir una relación \( M\vDash \alpha[v] \)) pues entonces podríamos definir el modelo natural de la aritmética de Peano y probar su consistencia, cuando WKL\( _0 \) es mucho más débil que AP.

Por ello, ahora tocaría estudiar la teoría ATR\( _0 \), donde ya es posible definir la relación  \( M\vDash \alpha[v] \) para cualquier modelo y probar la consistencia de AP, y me gustaría relacionarla con el concepto de "predicativismo", pues se puede probar que ATR\( _0 \) es una extensión conservativa de una teoría (de varias, de hecho) que pueden "justificarse predicativamente", es decir, que puede considerarse que hablan de hablan de conjuntos de números naturales "bien definidos" en el sentido de que se pueden definir por etapas: primero los definibles a partir de los números naturales con fórmulas aritméticas (sin cuantificar sobre conjuntos), luego los definidos a partir de estos conjuntos, etc., donde el "etc." no es nada trivial.

Pero en esto no he entrado y no sé si no será materia para otro libro, porque llevo ya 483 páginas sin contar todos los resultados necesarios sobre cálculo secuencial, que los dejaré en un libro aparte.