[Numerarius]

Bueno, sin querer desalentar la utilización del computador en estos temas...Bueno, el caso es que en estos temas de teoría de la computación aparecen razonamientos sobre conjuntos infinitos (los cuales, obviamente no se pueden implementar en un computador).

Por ejemplo, el problema de la parada de la máquina de Turing, o la demostración de que el conjunto de las funciones recursivas totales no es recursivamente enumerable. Éstas son demostraciones que utilizan el método diagonal de Cantor. Creo que este tipo de demostraciones no las aceptaría un intuicionista. No son demostraciones constructivas ni finitistas.

Un saludo cordial. 

[argentinator]

De acuerdo, pero hay cosas que sí son finitistas, y las voy a programar.
Quiero entender dónde está la frontera de lo computable y lo no computable.
Además, las demostraciones de teoremas matemáticos supuestamente son computables.
Toda la matemática debiera ser computable.
Podría demostrar al menos algunos teoremitas sencillos con la computadora.

En realidad todos los teoremas matemáticos se pueden demostrar con reglas y axiomas finitistas,
o sea que se puede diseñar un programa que sea capaz de llevar a cabo cualquier demostración si uno se la pide.
Es decir, si existe la demostración de un teorema, la máquina puede llevarla a cabo, y en número finito de pasos, si es que estoy entendiendo bien todas estas cosas.

Los teoremas de Turing y sus equivalentes no son matemáticos, sino metamatemáticos.
Así que no me preocupa que no pueda probarse usando una computadora.

Aún en el terreno de las demostraciones hechas por una computadora, soy conciente de ciertas limitaciones prácticas.
Por ejemplo, aunque una demostración sea perfectamente realizable por una máquina, es posible que sea tan complicada que lleve millones de años de procesamiento. Eso podría pasar por ejemplo con una proposición lógica muy rebuscada, como las que dan la cota superior en el calculo de complejidad del problema de Satisfabilidad de orden \( k  \geq  3 \) (Un típ¡co problema de la clase NP).
Así que no voy a intentar hacer un programa que demuestre cualquier teorema, aún sabiendo de antemano si es demostrable, porque en ese caso, además de realizar un algoritmo correcto, debe ser eficiente, lo cual lleva otro tipo de trabajo.

Lo que estoy diseñando es una especie de calculadora metalógica, con la que uno puede jugar un poco, y hacer experimentos.
Acá en casa me estoy divirtiendo con el programita.
Y aquello que no sea finitista en el teorema de Godel... ya veremos qué pasa.

[LauLuna]

Vaya, parece que se me pasó algún mensaje de advertencia de que había nuevas participaciones en el hilo y rinconmatematico ha dejado de enviarme mensajes de aviso. Ingenuamente creí que Gustavo había iniciado sus vacaciones de verano (!) y se había tomado un respiro. Así que me incorporo ahora con retraso.

Es impresionante la demostración que Gustavo está desarrollando. No he visto nunca nada parecido en cuanto al detalle y la claridad. Está haciendon algo muy parecido a la exposición original de Gödel pero con demostraciones mucho más detalladas. La idea de la expresión de los códigos en números binarios con 1 y 2 es genial; hace diáfanas las demostraciones.

Merece la pena seguir con detalle esta exposición. Intentaré ponerme al día.

Un saludo.

[LauLuna]

Ahora queremos que el lenguaje nos permita escribir: "El código de este mismo enunciado es el código de una fórmula demostrable", o, más brevemente, "Yo soy demostrable".

El objetivo, en última instancia es, mediante la negación de la última afirmación del párrafo anterior, llegar a un enunciado que diga: "Yo no soy demostrable".

Gustavo, se entiende perfectamente lo que quieres decir ahí: que si 'el código de este mismo enunciado es el código de una fórmula demostrable' es expresable, entonces 'el código de este mismo enunciado no es el código de una fórmula demostrable' es también expresable utilizando los mismos recursos expresivos que en la anterior más la negación. Pero conviene advertir que la segunda expresión no es la negación de la primera, porque el enunciado al que se refiere cada una no es el mismo.

Sabes que la expresión que dice de sí misma que es demostrable es la llamada 'sentencia de Henkin', de la que Loeb (o Löb) demostró en los cincuenta que es demostrable (y, por tanto, verdadera); la expresión que dice de sí misma que no es demostrable es la sentencia de Gödel, que, aunque no es demostrable, es también verdadera (siempre en la interpretación estándar). Por tanto, no es la negación de la anterior.

Sucede lo que en las oraciones:

'esta oración contiene exactamente seis palabras'

y

'esta oración no contiene exactamente seis palabras'

Ambas son verdaderas.

Un saludo.

[LauLuna]

Quiero entender dónde está la frontera de lo computable y lo no computable.

Está exactamente ahí.

Además, las demostraciones de teoremas matemáticos supuestamente son computables.

Sí, para todo teorema (para el que tengas una demostración, valga la redundancia) puedes diseñar un sistema del que sea un teorema y, por tanto, un programa que lo demuestre.
 

Toda la matemática debiera ser computable.

Eso no. Hay problemas (que siempre involucran un número infinito de casos, "mass problems" en inglés) que ningún algoritmo puede resolver: podemos definir clases de naturales tales que ningún programa es capaz de decidir para todo natural n si n pertenece a la clase en cuestión; por ejemplo, el conjunto de los códigos de máquinas de Turing que paran cuando se les da su propio código como input (el "halting set").

Date cuenta de que esto y lo anterior son dos cuestiones diferentes: aunque para todo teorema hay un programa que lo demuestra, no todos los problemas matemáticos son computables.

Los teoremas de Turing y sus equivalentes no son matemáticos, sino metamatemáticos.
Así que no me preocupa que no pueda probarse usando una computadora.

Yo no diría eso: los teoremas metamatemáticos son teoremas matemáticos, la metamatemática es una parte de la matemática; es decir, la matemática sin la metamatemática es la matemática en un sentido especial y restringido. Además, el teorema de Turing es demostrable mediante un programa igual que cualquier otro teorema matemático, tal como señalabas. Basta explicitar los axiomas y las reglas de inferencia que uno ha usado en la demostración, y eso permite crear un programa que la realiza.

Esto, sin embargo, no implica que exista un programa capaz de demostrar toda verdad matemática (lo que contradiría los resultados de Gödel, Church, Turing, Matijasevich, etc.). Ni siquiera implica que exista un programa capaz de demostrar todo cuanto la razón humana pueda eventualmente demostrar. Es la diferencia (en el orden de los cuantificadores) entre el enunciado:

'para todo teorema eventualmente demostrable existe un programa que lo demuestra'

que parece a todas luces verdadero, y el enunciado más fuerte:

'existe un programa que demuestra todo teorema eventualmente demostrable'

que es muy discutible.
 

Así que no voy a intentar hacer un programa que demuestre cualquier teorema

Muy sensato 

[argentinator]

Toda la matemática debiera ser computable.

Eso no. Hay problemas (que siempre involucran un número infinito de casos, "mass problems" en inglés) que ningún algoritmo puede resolver: podemos definir clases de naturales tales que ningún programa es capaz de decidir para todo natural n si n pertenece a la clase en cuestión; por ejemplo, el conjunto de los códigos de máquinas de Turing que paran cuando se les da su propio código como input (el "halting set").

Date cuenta de que esto y lo anterior son dos cuestiones diferentes: aunque para todo teorema hay un programa que lo demuestra, no todos los problemas matemáticos son computables.

Bueno, esto lo entiendo, sólo que me expresé mal.
En lo que estaba pensando era algo como "todos los teoremas que en matemática forman una demostración son demostrables con computadora", y a esa totalidad lo llamé "matemática"... Pero:

Los teoremas de Turing y sus equivalentes no son matemáticos, sino metamatemáticos.
Así que no me preocupa que no pueda probarse usando una computadora.

Yo no diría eso: los teoremas metamatemáticos son teoremas matemáticos, la metamatemática es una parte de la matemática; es decir, la matemática sin la metamatemática es la matemática en un sentido especial y restringido. Además, el teorema de Turing es demostrable mediante un programa igual que cualquier otro teorema matemático, tal como señalabas. Basta explicitar los axiomas y las reglas de inferencia que uno ha usado en la demostración, y eso permite crear un programa que la realiza.

Bueno, esto último que dijiste no lo tengo muy claro.
Creo que no estoy entendiendo cuáles son los límites de la matemática, a qué se considera matemática.
¿O es que esos límites no están claros?
Aunque por otro lado me olvidé de que Godel relaciona directamente la metamatemática con un sistema aritmético, y entonces ambas cosas son parte de un mismo tema de estudio...

Pero bueno. Si a la metamatemática le ponemos axiomas y reglas de inferencia, ¿seguimos hablando de lo mismo?
Hasta ahora lo que vengo entendiendo es que la metamatemática acepta una versión intuicionista de número natural, o de finitud, y unas reglas de inferencia bastante estrictas, que involucran el manejo de símbolos de un cierto lenguaje, y nada más.
Pero todo eso me parece que está como ''en el aire''.

Si yo formalizo la metamatemática en un sistema de símbolos, para estudiarla deberé recurrir a una meta-meta-matemátca, ¿o no? No creo que sea sano proceder de ese modo, porque así nunca le encuentra uno la punta al ovillo.
Después a alguno se le ocurre aceptar que le pongamos un sistema formal a la meta-meta-matemátca, y entonces para demostrar hechos sobre ella tendríamos que hacerlo con una meta-meta-meta-matemátca, y así sigue la historia.

¿O cómo es esto?

[Gustavo Piñeiro]

Gustavo, se entiende perfectamente lo que quieres decir ahí: que si 'el código de este mismo enunciado es el código de una fórmula demostrable' es expresable, entonces 'el código de este mismo enunciado no es el código de una fórmula demostrable' es también expresable utilizando los mismos recursos expresivos que en la anterior más la negación. Pero conviene advertir que la segunda expresión no es la negación de la primera, porque el enunciado al que se refiere cada una no es el mismo.

Sucede lo que en las oraciones:

'esta oración contiene exactamente seis palabras'

y

'esta oración no contiene exactamente seis palabras'

Ambas son verdaderas.

Tu aclaración es perfecta.

Saludos!

[LauLuna]

Argentinator, yo diría que los límites de la matemática no están claros.

Hace ya unos años hubo un hilo en el foro general (creo) en el que se planteaba qué es la matemática. Yo propuse lo único que vislumbro, a saber, que matemáticas es todo aquello para lo que podemos demostrar teoremas. Según esto la lógica y la metamatemática serían también matemáticas.

Cuando propuse esa misma idea en sci.logic, Aatu Koskensilta me preguntó si, en el caso de que alguien demostrara como un teorema la existencia de Dios, yo consideraría que está haciendo matemáticas; y le dije que sí; y que además en ese caso aparecería en poco tiempo una multitud de matemáticos con demostraciones alternativas, más sencillas, involucrando otros axiomas, etc. Y se crearía toda una disciplina, a saber, la Teología Matemática.

A veces utilizo otra definición más personal de la matemática: aquello cuyo estudio que me provoca sudores.  

En cuanto a la meta-meta-meta-...-matemática, me temo que eso es como tú te temes: la metateoría (o parte de ella) de un sistema puede formalizarse en otro sistema (con frecuencia, pero no necesariamente, estrictamente más potente) y así indefinidamente; a veces parte de la metamateoría de un sistema puede formalizarse en ese mismo sistema (es lo que Gustavo nos viene mostrando), pero nunca toda (es lo que el teorema de Gödel demuestra).

En concreto, ningún sistema consistente que contenga la aritmética de Peano puede demostrar su propia consistencia; Gustavo nos adelantó este resultado, que suele llamarse el segundo teorema de Gödel. Así que puedes partir de un sistema como el que Gustavo ha descrito (llámalo PA), que es sin duda consistente, y añadirle un axioma afirmando la consistencia de PA; tienes entonces el sistema PA*, más potente que PA pero que tampoco demuestra su propia consistencia; eso te permite construir PA**, etc.

Generalmente se considera que estos sistemas recurrentes se extienden a través de los ordinales conjuntistas hasta un cierto ordinal transfinito que definieron Church y Kleene. La idea de estas iteraciones parte de un artículo de Turing de 1939 y fue retomada por Feferman en los sesenta (creo); Franzén da una visión general en su 'Inexhaustibility. A Non-Exhaustive Treatment'.

Pero sí: dado un sistema consistente S, hay siempre otro sistema consistente S* que formaliza una parte mayor de la metateoría de S que S mismo.

¡Qué le vamos a hacer!

[argentinator]

En cuanto a la meta-meta-meta-...-matemática, me temo que eso es como tú te temes:

[...]

Generalmente se considera que estos sistemas recurrentes se extienden a través de los ordinales conjuntistas hasta un cierto ordinal transfinito que definieron Church y Kleene. La idea de estas iteraciones parte de un artículo de Turing de 1939 y fue retomada por Feferman en los sesenta (creo); Franzén da una visión general en su 'Inexhaustibility. A Non-Exhaustive Treatment'.

Bueno, pero entonces ¿hay algún ordinal donde toda esta recurrencia se termina?
Eso me daría algo de alivio por ahora.
 

[Numerarius]

Quiero entender dónde está la frontera de lo computable y lo no computable.

Está exactamente ahí.

Además, las demostraciones de teoremas matemáticos supuestamente son computables.

Sí, para todo teorema (para el que tengas una demostración, valga la redundancia) puedes diseñar un sistema del que sea un teorema y, por tanto, un programa que lo demuestre.
 

Toda la matemática debiera ser computable.

Eso no. Hay problemas (que siempre involucran un número infinito de casos, "mass problems" en inglés) que ningún algoritmo puede resolver: podemos definir clases de naturales tales que ningún programa es capaz de decidir para todo natural n si n pertenece a la clase en cuestión; por ejemplo, el conjunto de los códigos de máquinas de Turing que paran cuando se les da su propio código como input (el "halting set").

Date cuenta de que esto y lo anterior son dos cuestiones diferentes: aunque para todo teorema hay un programa que lo demuestra, no todos los problemas matemáticos son computables.

Los teoremas de Turing y sus equivalentes no son matemáticos, sino metamatemáticos.
Así que no me preocupa que no pueda probarse usando una computadora.

Yo no diría eso: los teoremas metamatemáticos son teoremas matemáticos, la metamatemática es una parte de la matemática; es decir, la matemática sin la metamatemática es la matemática en un sentido especial y restringido. Además, el teorema de Turing es demostrable mediante un programa igual que cualquier otro teorema matemático, tal como señalabas. Basta explicitar los axiomas y las reglas de inferencia que uno ha usado en la demostración, y eso permite crear un programa que la realiza.

Esto, sin embargo, no implica que exista un programa capaz de demostrar toda verdad matemática (lo que contradiría los resultados de Gödel, Church, Turing, Matijasevich, etc.). Ni siquiera implica que exista un programa capaz de demostrar todo cuanto la razón humana pueda eventualmente demostrar. Es la diferencia (en el orden de los cuantificadores) entre el enunciado:

'para todo teorema eventualmente demostrable existe un programa que lo demuestra'

que parece a todas luces verdadero, y el enunciado más fuerte:

'existe un programa que demuestra todo teorema eventualmente demostrable'

que es muy discutible.
 

Así que no voy a intentar hacer un programa que demuestre cualquier teorema

Muy sensato 

Vaya. Es cierto que, por la tesis de Church-Turing, cualquier teorema que se demuestra en matemáticas debería ser calculable  por una función recursiva.

Ahora bien, teniendo en cuenta que el conjunto de las máquinas de Turing es infinito-numerable, entonces ¿cómo se demuestra mediante una función recursiva, un teorema acerca de las máquinas de Turing (por ejemplo el "Halting Problem"?

Un saludo cordial.