Autor Tema: Sobre la demostración formalizada

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

12 Agosto, 2017, 08:58 pm
Leído 3510 veces

alexpglez

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 166
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
¿Es cierto que:
[texx]\vdash_{I \Sigma_1} (\vdash_{I\Sigma_1} \alpha) \rightarrow \alpha [/texx]?

Si es cierto que existe una deducción de alpha formalizada, los siguientes pasos en la demostración de alpha, sería asignar al número de Gödel de la deducción, su sucesión de fórmulas correspondientes e incorporarla para deducir alpha.

No estoy seguro de si esto es legítimo o no. Porque formal no lo encuentro, es decir, no encuentro una demostración verdadera siguiendo los axiomas de la teoría sin basarse en la decodificación de Gödel.

12 Agosto, 2017, 09:09 pm
Respuesta #1

Carlos Ivorra

  • Administrador
  • Mensajes: 11,112
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
No, no es cierto. Aplícalo a \( \alpha\equiv 0\neq 0 \). Si fuera cierto, en \( I\Sigma_1 \) podrías demostrar que \(  (\vdash_{I\Sigma_1} 0\neq 0) \rightarrow 0\neq 0 \) y, como también puedes demostrar que \( 0=0 \), negando la implicación habrías probado en \( I\Sigma_1 \) que  \( \lnot (\vdash_{I\Sigma_1} 0\neq 0) \), pero eso es justo lo que el segundo teorema de incompletitud dice que no se puede hacer. Esta fórmula afirma precisamente que \( I\Sigma_1 \) es consistente.

13 Agosto, 2017, 02:50 am
Respuesta #2

alexpglez

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 166
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Gracias, entiendo.

Sigo teniendo una duda relativo a esto. En el teorema de incompletitud de Gödel, se usa que si T es una teoría semirrecursiva. Entonces:
[texx] \vdash_T G [/texx]  implica [texx] \vdash_Q \vdash_T G [/texx]


Sin embargo, si una teoría axiomática T la podemos formalizar en [texx] I\Sigma_1 [/texx], entonces toda demostración en T se puede "calcar" en la teoría formalizada. Es decir, que encuentro que:
[texx] \vdash_T G [/texx] si y sólo si [texx] \vdash_{I\Sigma_1} \vdash_T G [/texx]

Sin embargo esto es erróneo, ya que entonces se podría eliminar la hipótesis de teoría semirrecursiva del teorema de Gödel (y cambiar por que T interprete a ISigma1)

Por otra parte, ¿qué implicaciones se dan si T fuese semirrecursiva, recursiva o demostrablemente recursiva?

Creo que me estoy perdiendo bastante con tantos conceptos...

13 Agosto, 2017, 12:17 pm
Respuesta #3

Carlos Ivorra

  • Administrador
  • Mensajes: 11,112
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
Sigo teniendo una duda relativo a esto. En el teorema de incompletitud de Gödel, se usa que si T es una teoría semirrecursiva. Entonces:
[texx] \vdash_T G [/texx]  implica [texx] \vdash_Q \vdash_T G [/texx]

Correcto.

Sin embargo, si una teoría axiomática T la podemos formalizar en [texx] I\Sigma_1 [/texx], entonces toda demostración en T se puede "calcar" en la teoría formalizada. Es decir, que encuentro que:
[texx] \vdash_T G [/texx] si y sólo si [texx] \vdash_{I\Sigma_1} \vdash_T G [/texx]

Sin embargo esto es erróneo,

Si \( \vdash_{I\Sigma_1} \vdash_T G  \), entonces \( \mathbb N\vDash \vdash_T G \), luego existe un número natural que es una demostración de \( G \) en \( T \), luego \(  \vdash_T G  \).

Ahora, si \(  \vdash_T G  \), existe un número natural que demuestra \( G \), luego \( \vdash_{I\Sigma_1} \vdash_T G  \).

Ahora bien, ambas implicaciones suponen que en \( I\Sigma_1 \) tienes definida una fórmula \( x\in Ax(T) \) con la propiedad de que \( \vdash_{I\Sigma_1} 0^{(n)}\in Ax(T) \) si y sólo si \( n \) es un axioma de \( T \). Esto se cumple si \( T \) es semirrecursiva, y de hecho es un si y sólo si, pues si un conjunto de axiomas puede representarse así en \( I\Sigma_1 \), entonces la relación "\( n \) es un axioma" equivale a "existe un número natural \( m \) que demuestra \( 0^{(n)}\in Ax(T) \) en \( I\Sigma_1 \)", y esta relación (sin el primer "existe") es recursiva, luego con el "existe" es semirrecursiva.

¿A qué te refieres cuando dices "si una teoría axiomática T la podemos formalizar en \(  I\Sigma_1  \)"? Si te refieres a que \( I\Sigma_1 \) interprete a \( T \), eso no te dice nada al respecto.

ya que entonces se podría eliminar la hipótesis de teoría semirrecursiva del teorema de Gödel (y cambiar por que T interprete a ISigma1)

Aquí me pierdo, ¿querías decir que \( I\Sigma_1 \) interprete a \( T \) y no al revés? Si es así, es lo que te he dicho antes, que eso sólo te dice que las fórmulas de T son traducibles a fórmulas de \( I\Sigma_1 \) de modo que los axiomas se traducen a teoremas, pero eso no tiene nada que ver con definir una fórmula aritmética en \( I\Sigma_1 \) que la cumplan exactamente los axiomas de T vistos como números naturales.

Por otra parte, ¿qué implicaciones se dan si T fuese semirrecursiva, recursiva o demostrablemente recursiva?

Aquí no sé a qué te refieres. ¿Qué implicaciones entre qué? Si te refieres a qué implicaciones se dan entre ser semirrecursiva, recursiva o demostrablemente recursiva, la respuesta es que toda teoría demostrablemente recursiva es recursiva y toda teoría recursiva es semirrecursiva, pero luego se da una "casi" implicación en el sentido de que toda teoría semirrecursiva tiene los mismos teoremas que una teoría demostrablemente recursiva, es decir, que entre sus teoremas puedes encontrar un conjunto demostrablemente recursivo (es decir un conjunto de axiomas alternativos que cumplan la definición 8.17) de modo que dichos teoremas tomados como axiomas implican todos los demás axiomas de la teoría, luego todos sus teoremas.

13 Agosto, 2017, 04:37 pm
Respuesta #4

alexpglez

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 166
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Ahora bien, ambas implicaciones suponen que en \( I\Sigma_1 \) tienes definida una fórmula \( x\in Ax(T) \) con la propiedad de que \( \vdash_{I\Sigma_1} 0^{(n)}\in Ax(T) \) si y sólo si \( n \) es un axioma de \( T \). Esto se cumple si \( T \) es semirrecursiva, y de hecho es un si y sólo si, pues si un conjunto de axiomas puede representarse así en \( I\Sigma_1 \), entonces la relación "\( n \) es un axioma" equivale a "existe un número natural \( m \) que demuestra \( 0^{(n)}\in Ax(T) \) en \( I\Sigma_1 \)", y esta relación (sin el primer "existe") es recursiva, luego con el "existe" es semirrecursiva.
Es decir que siempre:
[texx]\vdash_{I\Sigma_1} \vdash_T G [/texx] implica que [texx]  \vdash_T G [/texx]
Y si la teoría T es semirrecursiva es un si y sólo si.

El resto de mis preguntas iban dirigidas a la hipótesis de si fuese un "si y sólo si" aunque la teoría no fuese semirrecursiva.

Creo que ya entiendo por qué no entendía las teorías no recursivas. Aunque exista una demostración para un cierto teorema, no implica que sea demostrable (en [texx] I\Sigma_1 [/texx] en este caso) que sea una demostración. En una teoría no recursiva, falla que se pueda demostrar que una fórmula sea un axioma.

Sin embargo, si uno quiero ser persistente en la idea, ¿podría tratar de demostrar que cierta fórmula usada en una demostración es un axioma si no se deduce de fórmulas anteriores de la sucesión por MP o IG y tampoco es un esquema de KL?
(Así demostrar que aunque la teoría no sea recursiva, si lo es el conjunto de sus teoremas)

Añado:

Es decir, sea [texx] \Gamma [/texx] el conjunto de axiomas de T.
[texx] \vdash_T \alpha [/texx] implica [texx] \mathbb N \models \exists d \Gamma \vdash^d \alpha [/texx]
Que, si llamamos [texx] \Gamma' \equiv \{x \in Rd | \exists i <l (d) ( x=d_i \wedge d_i \not \in Axl(L) \wedge \forall jk <i (d_k \not = d_l \rightarrow d_i ) \wedge \forall k<i \forall x \in Rd_i (d_i\not = \forall x d_k))\}[/texx]
Entonces:
[texx] \mathbb N \models \exists d   \Gamma' \vdash^d \alpha [/texx]
Que es [texx] \Sigma_1 [/texx]... pero creo haberme equivocado en algo

 

13 Agosto, 2017, 06:09 pm
Respuesta #5

Carlos Ivorra

  • Administrador
  • Mensajes: 11,112
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
Es decir que siempre:
[texx]\vdash_{I\Sigma_1} \vdash_T G [/texx] implica que [texx]  \vdash_T G [/texx]
Y si la teoría T es semirrecursiva es un si y sólo si.

Si supones que \( \vdash_{I\Sigma_1} \vdash_T G  \), entonces, interpretando en \( \mathbb N \), tienes que existe un número natural \( n \) que demuestra \( G \), en el sentido de que hay una sucesión de fórmulas que termina en \( G \), en la que cada una se deduce de las anteriores por una regla lógica, o es un axioma lógico, o bien cumple \( \mathbb N\vDash 0^{(m)}\in Ax(T) \).

Para concluir necesitas que los números \( m \) que cumplen esto sean justamente los axiomas de T. Para ello no hace falta que T sea semirrecursiva, pero no vale cualquier teoría. Necesitas que sus axiomas puedan caracterizarse como los que cumplen una determinada fórmula aritmética. No necesitas que en \( I\Sigma_1 \) pueda probarse esta fórmula, cuando \( m \) es un axioma de T, pero sí al menos que exista una fórmula que sea verdadera justo cuando \( m \) es un axioma de T.

Los conjuntos de números naturales definibles por fórmulas aritméticas se llaman aritméticos, y son más que los recursivos o los semirrecursivos, pero hay conjuntos no aritméticos.

El resto de mis preguntas iban dirigidas a la hipótesis de si fuese un "si y sólo si" aunque la teoría no fuese semirrecursiva.

Creo que ya entiendo por qué no entendía las teorías no recursivas. Aunque exista una demostración para un cierto teorema, no implica que sea demostrable (en [texx] I\Sigma_1 [/texx] en este caso) que sea una demostración. En una teoría no recursiva, falla que se pueda demostrar que una fórmula sea un axioma.

Correcto.

Sin embargo, si uno quiero ser persistente en la idea, ¿podría tratar de demostrar que cierta fórmula usada en una demostración es un axioma si no se deduce de fórmulas anteriores de la sucesión por MP o IG y tampoco es un esquema de KL?
(Así demostrar que aunque la teoría no sea recursiva, si lo es el conjunto de sus teoremas)

Añado:

Es decir, sea [texx] \Gamma [/texx] el conjunto de axiomas de T.
[texx] \vdash_T \alpha [/texx] implica [texx] \mathbb N \models \exists d \Gamma \vdash^d \alpha [/texx]
Que, si llamamos [texx] \Gamma' \equiv \{x \in Rd | \exists i <l (d) ( x=d_i \wedge d_i \not \in Axl(L) \wedge \forall jk <i (d_k \not = d_l \rightarrow d_i ) \wedge \forall k<i \forall x \in Rd_i (d_i\not = \forall x d_k))\}[/texx]
Entonces:
[texx] \mathbb N \models \exists d   \Gamma' \vdash^d \alpha [/texx]
Que es [texx] \Sigma_1 [/texx]... pero creo haberme equivocado en algo

¿Qué significa \( Rd \)?

Salvo que por no entender esa notación me esté confundiendo, entiendo que lo que planteas es partir de una demostración \( d \) y definir un conjunto \( \Gamma' \) que depende de \( d \) ¿no? y concluyes que de \( \Gamma' \) se deduce \( \alpha \). Aunque no lo llegas a escribir, supongo que quieres llegar a que además, eso se puede demostrar en \( I\Sigma_1 \), lo cual es cierto, pues \( \Gamma' \) es finito, luego recursivo y todo lo que quieras. Pero no veo por qué dices que tienes una teoría \( \Sigma_1 \). Lo que tienes es una teoría recursiva distinta para cada teorema de la teoría original.

Tampoco veo qué tiene que ver esto con lo primero que planteas. Aquí no estás demostrando que nada es un axioma. Estás tomando como axiomas todo lo que no puede ser otra cosa para que la demostración sea realmente una demostración.

Tampoco sé qué quieres probar exactamente. ¿Que el conjunto de teoremas de cualquier teoría no recursiva es recursivo? Desde luego, si la teoría es contradictoria es cierto. Pero si no, es imposible. El conjunto de teoremas de una teoría aritmética consistente nunca es recursivo (teorema 9.5).

13 Agosto, 2017, 11:18 pm
Respuesta #6

alexpglez

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 166
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
Respecto a la primera observación. ¿De poder definir la fórmula [texx] x \in Ax (T) [/texx] para una cierta teoría T, no quiere decir el conjunto de axiomas que ya es aritmético?. Es decir, si la relación "[texx] x [/texx] es un axioma" no fuese aritmético, entonces creo que no podemos definir su teoría formalizada en [texx] I\Sigma_1 [/texx].
Entendiendo la teoría T formalizada aquella que:
[texx] \alpha [/texx] es un axioma de T syss [texx] \mathbb N \models \alpha \in Ax (T) [/texx]
Donde la fórmula de la derecha es una teoría axiomática en [texx] I \Sigma_1 [/texx] (en los términos que escribes en el primer apartado del capítulo sobre la formalización de la lógica).

No sé si me explico, pero entiendo lo que me quieres decir. Hasta ahora no había caído en que hay teorías axiomáticas cuyo conjunto de axiomas no sea aritmético (por ejemplo si consideramos el conjunto de las sentencias verdaderas en N, que no puede ser una relación aritmética por el teorema de Tarski), y que no se pueden formalizar en los términos anteriores.

Respecto a lo segundo, no lo he detallado del todo porque me parecía evidente.
Quiero demostrar que en cualquier teoría en la que la relación "ser un axioma" es aritmética, el conjunto de sus teoremas es semirrecursivo.
Ya me has dicho que es falso, pero quiero ver el fallo del argumento que expuse.

Rd es el recorrido de d. El argumento anterior, detallando el final como dices:
[texx] \mathbb N \models (\vdash_T \alpha ) \leftrightarrow (\exists d \Gamma' \vdash \alpha) [/texx]
Y la equivalencia también se demuestra en [texx] I \Sigma_1 [/texx]. Entonces como la fórmula de la derecha es [texx] \Sigma_1 [/texx], utilizando esto y la completitud de Q para estas fórmulas:
[texx] \vdash_T \alpha [/texx] syss [texx] \vdash_{I \Sigma_1} \vdash_T \alpha [/texx]

¿Cuál fallo hay?


13 Agosto, 2017, 11:37 pm
Respuesta #7

Carlos Ivorra

  • Administrador
  • Mensajes: 11,112
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
Respecto a la primera observación. ¿De poder definir la fórmula [texx] x \in Ax (T) [/texx] para una cierta teoría T, no quiere decir el conjunto de axiomas que ya es aritmético?.

Sí, en efecto.

Es decir, si la relación "[texx] x [/texx] es un axioma" no fuese aritmético, entonces creo que no podemos definir su teoría formalizada en [texx] I\Sigma_1 [/texx].
Entendiendo la teoría T formalizada aquella que:
[texx] \alpha [/texx] es un axioma de T syss [texx] \mathbb N \models \alpha \in Ax (T) [/texx]
Donde la fórmula de la derecha es una teoría axiomática en [texx] I \Sigma_1 [/texx] (en los términos que escribes en el primer apartado del capítulo sobre la formalización de la lógica).

No sé si me explico, pero entiendo lo que me quieres decir. Hasta ahora no había caído en que hay teorías axiomáticas cuyo conjunto de axiomas no sea aritmético (por ejemplo si consideramos el conjunto de las sentencias verdaderas en N, que no puede ser una fórmula por el teorema de Tarski), y que no se pueden formalizar en los términos anteriores.

Sí, sí. Todo lo que dices es correcto. Simplemente me pareció oportuno señalarte precisamente eso en lo que dices que no habías caído.

Respecto a lo segundo, no lo he detallado del todo porque me parecía evidente.
Quiero demostrar que en cualquier teoría en la que la relación "ser un axioma" es aritmética, el conjunto de sus teoremas es semirrecursivo.
Ya me has dicho que es falso, pero quiero ver el fallo del argumento que expuse.

Bueno, antes habías dicho recursivo, no semirrecursivo (o eso había entendido yo). Y lo que te he dicho que es falso es que el conjunto de teoremas pueda ser recursivo. Cuando los axiomas son recursivos, el conjunto de teoremas siempre es semirrecursivo. Si los axiomas no son recursivos, entonces el conjunto de los teoremas puede ser semirrecursivo y puede no serlo.

Por ejemplo, si tomas como axiomas los axiomas de Peano más un conjunto de axiomas de la forma \( 0^{(n)}+0^{(1)}=0^{(n+1)} \), donde \( n \) recorre un conjunto no recursivo de números naturales, entonces el conjunto de los axiomas no es recursivo (y si coges un conjunto no semirrecursivo, los axiomas tampoco son semirrecursivos), pero el de los teoremas es semirrecursivo, porque es el mismo que el conjunto de los teoremas de la aritmética de Peano.

Por otra parte, si tomas como axiomas todas las afirmaciones verdaderas en el modelo natural, el conjunto de los teoremas es el mismo, y no es semirrecursivo. De hecho, ni siquiera es aritmético.

Rd es el recorrido de d. El argumento anterior, detallando el final como dices:
[texx] \mathbb N \models (\vdash_T \alpha ) \leftrightarrow (\exists d \Gamma' \vdash \alpha) [/texx]
Y la equivalencia también se demuestra en [texx] I \Sigma_1 [/texx]. Entonces como la fórmula de la derecha es [texx] \Sigma_1 [/texx], utilizando esto y la completitud de Q para estas fórmulas:
[texx] \vdash_T \alpha [/texx] syss [texx] \vdash_{I \Sigma_1} \vdash_T \alpha [/texx]

¿Cuál fallo hay?

No entiendo el argumento. \( \Gamma' \) es un conjunto finito que depende de \( d \) y, desde luego, no es \( T \). ¿Cómo relacionas el hecho de que de \( \Gamma' \) se deduzca \( \alpha \) con que de \( T \) se deduzca \( \alpha \)?

14 Agosto, 2017, 12:07 am
Respuesta #8

alexpglez

  • $$\Large \color{#5e8d56}\pi\,\pi\,\pi$$
  • Mensajes: 166
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
No entiendo el argumento. \( \Gamma' \) es un conjunto finito que depende de \( d \) y, desde luego, no es \( T \). ¿Cómo relacionas el hecho de que de \( \Gamma' \) se deduzca \( \alpha \) con que de \( T \) se deduzca \( \alpha \)?
Creo que me explicaré mejor sólo con palabras.
Si una fórmula A es un teorema de T, entonces existe una demostración D. Si cogemos de T sólo los axiomas necesarios para demostrar A, entonces la relación "D es una demostración de A, utilizando tales axiomas" es recursiva (puesto que es un número finito de axiomas). Luego "D es una demostración de A en T" es casi recursiva, puesto que es equivalente a lo anterior salvo fijar los axiomas necesarios para la demostración, pero si existe una forma de fijar esos axiomas tal que la fórmula sea recursiva, entonces "D es una demostración de A en T" es recursiva.
Ahora, fijándonos en la demostración D, nos fijamos en las fórmulas que no se deducen por IG o MP de fórmulas anteriores de la sucesión, ni sea un axioma lógica. Si podemos concluir la búsqueda de los axiomas, "ser un axioma de la demostración" es recursiva. Luego finalmente "D es una demostración de A en T" es recursiva.

14 Agosto, 2017, 12:22 am
Respuesta #9

Carlos Ivorra

  • Administrador
  • Mensajes: 11,112
  • País: es
  • Karma: +0/-0
  • Sexo: Masculino
    • Página web personal
Decir que "D es una demostración de A en T" es recursiva equivale a decir que si yo te doy una D, tú puedes saber si es o no una demostración de A en T.

Pues bien, yo te doy una D. Tú la miras y extraes de ella el conjunto \( \Gamma \) de fórmulas que no se deducen de las anteriores ni son axiomas lógicos, y con ello puedes concluir que D es una demostración de A a partir de \( \Gamma \), pero no sabes si es una demostración de A en T porque no tienes ni idea de si las fórmulas de \( \Gamma \) son o no axiomas de T.

Tú estás partiendo del supuesto de que las fórmulas con las que no sabes que hacer serán axiomas de T, y eso es verdad si realmente te he dado una demostración en T, pero ¿y si lo que te he dado no es una demostración en T?

Por eso te preguntaba que cómo relacionas el hecho de que A se deduzca de \( \Gamma \) con el hecho de que se deduzca de T.

Dicho de otro modo, tú presupones que D es una demostración en T, pero tienes que partir de una D arbitraria, que no sabes si es o si no es una demostración en T.

Un caso más simple: yo te doy simplemente la fórmula A, de modo que puede ser que sea una demostración en T porque A sea un axioma, o puede ser que te esté intentando colar algo que no es realmente una demostración en T.

El caso es que te doy A y tú concluyes que \( \Gamma = \{A\} \). ¿Y ahora qué? ¿A es o no es un teorema de T? Si me dices que sí, entonces tendrás que decirme que sí te dé la fórmula que te dé, y si me dices que no ¿por qué no?