Recordatorio de lo triste que es que uno malgaste su potencial por pura y simple pereza...

Indecidibilidad general de la lógica cuantificacional poliádica.

Discusión en el grupo de Usenet es.humanidades.filosofia entre junio y julio de 1999. Comentarios de Jean Mallart sobre la respuesta de Josman a una solicitud de Blume sobre el Teorema de Church.

Dramatis personae: BLUME, estudiante de filosofía. JOSMAN, licenciado en Filosofía. XAVIER, licenciado en filosofía. JEAN MALLART, ex-estudiante de filosofía.

Introducción:

Lo que determina la decidibilidad de un sistema formal es la existencia de un procedimiento decisorio (de aquí el nombre) que permita determinar de una manera mecánica si una fórmula cualquiera del mismo es o no deducible. La lógica de enunciados es decidible. En cambio, por lo que respecta a la lógica de predicados, el problema de la decisión no tiene solución general satisfactoria, como demostró Alonzo Church en 1936. Según el Teorema de Church, la lógica cuantificacional de primer orden, considerada como un todo, es indecidible. ¿Qué significa esto? Que no se puede hallar un algoritmo que permita determinar en un número finito de pasos si una fórmula cualquiera de la lógica cuantificacional de primer orden es deducible o no dentro de ella, es decir: si esa fórmula es o no un teorema del sistema.

(Comienza la discusión.)

Blume (pregunta): ¿Hay alguien tan amable como para decirme qué afirma el teorema de Church?

Josman (responde a Blume): Me gustaría, antes de decir qué dice el teorema, enmarcarlo un poco. Tenemos de partida el teorema de incompletud de Gödel. Ese teorema indica que dada una teoría formal T que abarca la teoría de los números enteros si es consistente, entonces es incompleta.

Jean Mallart (comenta la respuesta de Josman a Blume): Supongo que te refieres a la prueba de Gödel de 1931 que demostró que no era posible axiomatizar completamente la matemática. Dado un sistema axiomático, éste es esencialmente incompleto, ya que en él aparece por lo menos un teorema indecidible. Se puede construir un sistema lógico dentro del cual ese teorema resulte decidible, pero siempre se podrá encontrar en el nuevo sistema otro teorema indecidible. Para resolverlo, se puede construir otro aún, pero nuevamente encontraríamos en éste un teorema indecidible. Como dice Ferrater Mora, “Por más sistemas lógicos que se construyeran, no se haría sino hacer retroceder indefinidamente el hallazgo de un supuesto cálculo completo y consistente capaz de alojar en su seno la matemática. Todo sistema lógico de tal especie debe poseer reglas de inferencia más ricas que el cálculo sobre el cual se pronuncia, y en el interior del sistema vuelve a aparecer la dificultad apuntada. En suma, si el sistema es completo, no es consistente; si es consistente, no es completo.”

»El teorema de completud de Gödel dice: “Para toda fórmula A de la lógica cuantificacional de primer orden, si A es lógicamente verdadera, entonces A es deducible.” No es lo mismo.

»El teorema de Church viene a decir que, si bien la lógica cuantificacional de primer orden es, como demostró Gödel, completa, no es, sin embargo, decidible en su totalidad.

Josman (continúa la respuesta a Blume): Este teorema, en su enunciación habla de la matemática; ahora bien como el aparato lógico que Gödel utiliza es la lógica de predicados de segundo orden su resultado se amplía a esta; es más es que es por ésta por lo que se da el resultado anterior en la matemática.

»Por tanto tenemos que la lógica de predicados es incompleta. Que sea incompleta viene a significar que hay proposiciones indecidibles, es decir que hay proposiciones que sabemos que no podemos deducir ni su afirmación ni su negación. Sin embargo no todas las proposiciones de la lógica de predicados son así. El mismo Gödel demuestra en 1930 que la lógica de predicados de primer orden es consistente y completa, por eso donde se va a poner el acento es en el problema de la decisión.

Jean Mallart (comenta la respuesta de Josman a Blume): Creo que aquí has confundido algunas cosas. Según el teorema de completud de Gödel, la lógica cuantificacional de primer orden es completa. Como has dicho, la decidibilidad viene determinada por la existencia de un procedimiento que permita decidir de un modo mecánico si una fórmula es o no deducible en el sistema. Según tú, sabemos que una proposición es indecidible cuando no podemos deducir su afirmación ni su negación; esto es inexacto. La decidibilidad no es (cuando es) una propiedad de la fórmula únicamente, sino del sistema, es decir: la decidibilidad de la fórmula depende de la existencia de un algoritmo que demuestre que es deducible o que no lo es, mientras que Church se refiere a la decidibilidad del sistema en general. Por otra parte, la posibilidad de deducir una fórmula determina si es lógicamente verdadera; si no es deducible, no lo es (partiendo del teorema de completud de Gödel, si es universalmente válida, es deducible). Después de dar la definición de decidibilidad, continúas:

Josman (en cita de Jean Mallart; continúa la respuesta de aquel a Blume): Es decir, si sabemos que hay fórmulas en el sistema que no son deducibles, convendría saber si, para cualquier fórmula con la que nos hallemos, disponemos de un procedimiento efectivo con el que decidir si esa proposición es en concreto indecidible o no lo es.

Jean Mallart (comenta la respuesta de Josman de Blume): Es lo mismo de antes. El sistema es indecidible si no disponemos de un procedimiento con el que saber si una fórmula es deducible. No podemos saber si hay fórmulas en el sistema que no son deducibles sin saber si éste es decidible (y para saber lo primero, tiene que serlo). Creo que esto es lo que querías decir.

Josman (continúa la respuesta a Blume): Pues bien, y ya llego al Teorema de Church, la noción de un tal procedimiento efectivo fue definida por Church mediante el concepto de función recursiva o computable. Church mostró que, en general, no es posible un procedimiento de decisión. Es decir dada una proposición concreta del sistema no siempre se puede mostrar un algoritmo para determinar si es demostrable o indecidible.

Jean Mallart (comenta la respuesta de Josman a Blume): Bien, pero de nuevo hay que aclarar un detalle: “Un sistema es indecidible cuando, dada una proposición concreta del sistema no siempre se puede mostrar un algoritmo para determinar si es demostrable.”

Josman (continúa la respuesta a Blume): Es decir, no podemos saber de cualquier proposición concreta si es o no indecidible.

Jean Mallart (comenta la respuesta de Josman a Blume): De nuevo, no se trata de la decidibilidad de una proposición concreta, sino del sistema, en general. Aquí tendrías que haberte referido a la deducibilidad de la proposición.

Xavier (responde a Blume): Imagino que te refieres a la tesis de Church. Si ese es el caso, la tesis de Church dice que toda función computable en un sentido intuitivo de esta palabra, es computable en el sentido formal, es decir, computable por una máquina de Turing.

Jean Mallart (comenta la respuesta de Xavier a Blume citando a Manuel Garrido): Exacto: “Church demostró en su artículo de 1936 que los conceptos matemáticamente precisos de ‘función lambda-definible’ y ‘función recursiva general’ son equivalentes. Y Turing demostró en el suyo que los conceptos matemáticamente precisos de ‘función Turing-computable’ y ‘función recursiva general’ son asimismo equivalentes. La prueba de que estas diversas caracterizaciones matemáticas del concepto intuitivo de función calculable son equivalentes refuerza, aunque sin poder demostrarlas, ambas conjeturas, la de Church y la de Turing, a las que es usual reunir, por su semejanza, en una sola denominación como la ‘tesis de Church-Turing’.» (Manuel Garrido, “Lógica simbólica”.)

Xavier (más tarde, a Blume): De todas, maneras, hay un teorema de Church que tiene que ver con la decidibilidad de la aritmética de Peano... si es esto a lo que te referías, ¿puedes indicarlo?

Blume (respondiendo a la solicitud de Xavier): Pues, en efecto, me refería al teorema, no al “principio de Church”. La duda me vino porque según unas notas que tomé hace tiempo venía a decir lo que tan pacientemente ha comentado Josman y lo que tú indicas, a saber, que existen proposiciones para las que no existen algoritmos de decisión. En su día me sonó muy gödeliano. Y hace unos días leí (en Dennet, "La actitud intencional", Gedisa, p. 71) una enunciación de la tesis de Church en los términos de que “todo procedimiento efectivo en matemáticas es recursivo, es decir, computable por la Turing”. Entonces me asaltó la duda de si había tomado mal las notas sobre el teorema, pues me parecía que éste y la tesis de Church “no casaban”. Si hay proposiciones no decidibles mediante algoritmo ¿cómo es que todas las funciones de la matemática son computables por la máquina de Turing? En fin, debo de estar confundiendo algo.

Jean Mallart (responde a la aclaración de Blume sobre sus dudas volviendo a citar a Garrido): Para aclararte me parece conveniente transcribir parte de uno de los apartados del libro “Lógica simbólica”, de Manuel Garrido, que lo explica muy bien (más que nada, por ahorrarme trabajo, je je). Hago notar que el texto entre apóstrofos está en cursiva en el original. (Corregido en esta versión de la discusión).

(Sigue el texto de Manuel Garrido.)

«Alonzo Church demostró en 1936 la imposibilidad de hallar un procedimiento decisorio adecuado para la lógica elemental (incluyendo, por supuesto, la lógica cuantificacional poliádica).

»El resultado obtenido por Church es, como el famoso resultado de Gödel de 1931, uno de los “teoremas de limitación”, que pusieron en crisis en los años treinta la ilimitada fe que hasta entonces se había venido depositando en los métodos axiomáticos y dieron lugar, al mismo tiempo, a una de las corrientes más fecundas de la investigación lógico-matemática de los últimos cuarenta años: la teoría de la computabilidad.

»Desde principios de siglo David Hilbert había defendido el punto de vista (históricamente sostenido por Ramón Llull en la Edad Media y Leibniz en la Edad Moderna) de que todo problema lógico y matemático podría ser resuelto por procedimientos mecánicos. De ahí la importancia que adquirió hacia los años veinte el llamado Entscheidungsproblem (problema de la decisión). De hecho, el problema de la decisión para el cálculo elemental de cuantores era, en el sentir de Hilbert, el problema fundamental de la lógica matemática.

»Sorprendentemente, los hallazgos más interesantes en la investigación del problema de la decisión fueron hallazgos negativos que establecieron la existencia de problemas insolubles y las fatales limitaciones de sistemas axiomáticos de interés fundamental. En 1931 Kurt Gödel demostró que todo sistema axiomático que pretenda formalizar la aritmética elemental es incompleto. Y en 1936 Church probó primero la indecidibilidad de la aritmética, y luego, con ayuda de este resultado, la indecidibilidad de la lógica elemental (teorema de Church).

»(...) En su contribución An unsolvable problem of number theory (1936) Church propuso definir el concepto intuitivo y más bien vago de “función efectivamente calculable” mediante el concepto matemáticamente preciso y riguroso de “recursividad”. Tal es el fin que persigue la llamada TESIS DE CHURCH (1936): Toda función efectivamente calculable es una función recursiva.

»Esta tesis no es susceptible de demostración rigurosa, como puede serlo un teorema, sino que ha de tener más bien, forzosamente, el carácter de una conjetura. La razón de ello es que la cópula “es” tiene aquí el sentido de una equivalencia por la que se equipara el concepto de “función calculable”, que es vago e intuitivo, con el concepto de “función recursiva”, que es preciso y riguroso. Pero nunca será posible demostrar satisfactoriamente una equivalencia entre dos conceptos cuando uno de ellos es intrínsecamente vago e intuitivo.

»Con ayuda de su tesis probó Church que no es posible hallar una solución general para el problema de la decisión en teoría elemental de números, es decir, que el sistema formal de la aritmética es indecidible.

»En su contribución A note on the Entscheidungsproblem (1936) Church mostró que el sistema formal de teoría elemental de números podía ser reducido al sistema formal de lógica elemental mediante una serie de transformaciones tendentes a eliminar los símbolos aritméticos; y a continuación hizo ver, como consecuencia de tal reducción, que si hubiera un procedimiento decisorio para toda la lógica elemental, lo habría para la teoría elemental de números. Pero teniendo en cuenta el anterior resultado de Church acerca de la indecidibilidad de la teoría elemental de números, queda establecida la indecidibilidad de la lógica elemental.

»El curso de la argumentación puede detallarse mejor con ayuda de letras metalingüísticas. Convengamos en designar por:

»L El sistema formal de la lógica elemental.

»N El sistema formal de la teoría elemental de números.

»L' La reducción del sistema N al sistema L por virtud de las transformaciones eliminatorias de símbolos aritméticos.

»T La conjunción de los axiomas de N, pero después de haber eliminado en ellos, por virtud de tales transformaciones, los símbolos aritméticos.

»A Una fórmula cualquiera de N.

»A' El resultado de eliminar, por esas transformaciones, los símbolos aritméticos en A.

»Obviamente, puede afirmarse que A es deducible de N si y sólo si la implicación T -> A' es deducible en L:

»(...)

»Pero esto es tanto como decir que N es decidible si y sólo si L es decidible. De este modo, la decidibilidad en aritmética y la decidibilidad en lógica resultan ser equivalentes. Una solución del caso general del problema de la decisión para N equivale a una solución del caso general del problema de la decisión para L. Ahora bien, el caso general del problema de la decisión para N es insoluble (primer resultado de Church, con base en la tesis de recursividad). Por tanto:

»TEOREMA DE CHURCH: El caso general del problema de la decisión para L es insoluble. Esto es: la lógica elemental de la cuantificación es indecidible.

»El teorema de Church posee relevancia filosófica. Desde el punto de vista de la filosofía, el interés principal de este aserto está en que por él se establece, o se pretende establecer, la no mecanicidad de la lógica formal. Pues si bien es cierto que existen algoritmos que permiten resolver de modo mecánico grandes grupos de problemas de la lógica elemental, según el teorema de Church no existe ni puede existir un algoritmo que los resuelva mecánicamente todos. La operación deductiva de la razón no es totalmente mecanizable.

»Un fenómeno en cierto modo coincidente con el teorema de Church es la existencia de tablas semánticas infinitas (...). En su contribución de 1956, Beth consideró la idea de construir una máquina lógica que tramitase la confección de tablas semánticas. Dado que el proceso de confección de una tabla semántica desemboca fatalmente en uno de estos tres resultados: 1) clausura total de la tabla; 2) hallazgo de contraejemplos en un número finito de pasos, o 3) derivación al infinito; una máquina que pudiera realizar ese proceso debería estar capacitada para afrontar con éxito las tres posibilidades, lo cual podria materializarse, por ejemplo, en el sistema de comunicación de la máquina con el mundo exterior mediante una luz roja que avisase del primer caso, una luz amarilla que avisase del segundo y una verde del tercero. A juicio de Beth, es factible una máquina que cumpla las dos primeras funciones, pero no la tercera, porque nunca es posible decidir mecánicamente si una búsqueda de contraejemplo que se abre al infinito alcanzará o no alcanzará éxito, aunque, de hecho, la mente humana puede muchas veces resolver por modo no mecánico esa cuestión. En palabras de Beth: “La máquina lógica provista de una luz roja y una luz amarilla realiza una función muy análoga a la facultad de razonar de la mente humana, y, de hecho, es capaz de realizar un gran número de sus operaciones con un grado superior de eficiencia y precisión. Sin embargo, la mente humana está equipada con operaciones adicionales que van más allá del poder de una tal máquina...; podemos, pues, suponer que nuestra mente está equipada con una especie de luz verde. Pero no podemos suponer que opere con una luz verde de una manera sistemática y perfectamente controlable; porque ello implicaría que la mente humana incorporase, por así decirlo, una máquina lógica con una luz roja, una amarilla y una verde, y sabemos que una máquina semejante no puede existir.”»

Jean Mallart (continúa con la pertinente referencia bibliográfica) Manuel Garrido, “Lógica simbólica”, Tecnos, Madrid, 1995 (3ª ed.), pp. 368-372. ISBN: 84-309-2604-6.

Jean Mallart (aclara sus citas): Post data: He tirado de libros para intentar contestarme yo mismo, pues lo cierto es que todo este asunto excede mis conocimientos reales de lógica, materia que, aunque me gusta e interesa mucho, tengo bastante olvidada. No intento “hacerme” el erudito. Probablemente haya en mis comentarios un fallo fundamental que no alcanzo a detectar, y agradeceré mucho que se me aclaren los puntos donde ese fallo se evidencie.

Josman (responde a las críticas de Jean Mallart sobre la respuesta de aquel a Blume): Hola, Jean. A mí me ha parecido que quizá estés tomando dos teoremas distintos, debidos al mismo Gödel, como si fueran uno solo.

»Por un lado está el teorema que demuestra que la lógica de predicados de primer orden, es decir aquella que no cuantifica letras predicativas, es completa.

»Por el otro se encuentra el que demuestra que cualquier sistema que incorpore la lógica de predicados de segundo orden, como es el caso de la aritmética, es incompleto.

»Que un sistema formal sea completo significa que para toda fórmula bien formada del sistema podemos deducir su afirmación o su negación; es decir podemos deducir o A o su negación: ¬A.

»Pues bien, una vez que sabemos que un sistema formal es incompleto lo que sabemos es que en él hay fórmulas bien formadas (FBF) que son indecidibles, es decir que no podemos deducir ni su afirmación ni su negación. pero no significa que no podamos deducir en él ninguna fórmula, sólo que sabemos que no todas son decidibles.

»Es por eso por lo que entra en juego el problema de la decisión. Se trata de saber si tenemos un procedimiento general para conocer si una fórmula bien formada en concreto es indecidible o no lo es. Es en ese contexto en el que se enmarca el teorema de Church.

»Lo que el teorema de Church dice es que no disponemos tampoco de un procedimiento efectivo para saber si para cualquier fórmula bien formada del sistema ella es deducible, en el sistema, o no lo es.

»Y por tanto, una cosa es demostrar, por el teorema de incompletud de Gödel, que un sistema formal axiomático que incluya la lógica de predicados de segundo orden es incompleto, y que en él hay proposiciones indecidibles, y otra cosa distinta es demostrar, a través de teorema de Church, que no hay una manera de saber, para cualquier FBF que podamos construir en ese sistema formal, si esa misma fórmula es indecidible o si sí es decidible aunque quizá aún no hayamos encontrado el procedimiento para deducirla.

»Yo no sé si he atinado con el asunto que planteabas. En cualquiera de los casos, si no estamos aún de acuerdo en la cuestión, o si algo de lo dicho por mi sigue siendo oscuro, señálamelo y lo comentamos.

Jean Mallart (responde a Josman): Hola, Josman. (Cita su último comentario:) Decías: “A mí me ha parecido que quizá estés tomando dos teoremas distintos, debidos al mismo Gödel, como si fueran uno solo.”

»Es curioso, porque yo pensaba que eras tú quien los confundía. :-) Lo que ocurre es que ignoro el nombre de la prueba de Gödel de 1931 (que demuestra la incompletud de los sistemas axiomáticos), así que me limité a describirla someramente. A continuación, me refiero a su teorema de completud, que afirma que la lógica de predicados de primer orden es completa, añadiendo: "No es lo mismo". Como ves, no los confundí. Y ya veo que tú tampoco. :-)

«En tu respuesta a Blume, diste inicio a tu explicación sobre el teorema de Church diciendo: “Tenemos de partida el teorema de incompletud de Gödel. Ese teorema indica que dada una teoría formal T que abarca la teoría de los números enteros si es consistente, entonces es incompleta.” Así que, en efecto, te referías a la prueba de 1931 que demuestra la incompletud de los sistemas axiomáticos.

»Mis "críticas" iban dirigidas al uso que das a la palabra "indecidibilidad".

»Vuelves a afirmar: “(…) una vez que sabemos que un sistema formal es incompleto lo que sabemos es que en él hay fórmulas bien formadas (FBF) que son indecidibles, es decir que no podemos deducir ni su afirmación ni su negación.”

»Afirmas que de una fórmula indecidible no es posible deducir ni su afirmación ni su negación. Tengo que comprobarlo. :-) Pero creo que debemos precisar que la indecidibilidad de una fórmula no depende de si ésta es deducible, sino de si existe un medio (un algoritmo) para saber si es deducible. Puede parecer lo mismo, pero hay una sutil diferencia. Un sistema formal completo puede ser indecidible, como demostró, precisamente, Church.

»En definitiva, venía a decirte que creo que a veces confundes decidibilidad con deducibilidad (Jean Mallart cita a Josman): “(...) una cosa es demostrar, por el teorema de incompletud de Gödel, que un sistema formal axiomático que incluya la lógica de predicados de segundo orden es incompleto, y que en él hay proposiciones indecidibles, y otra cosa distinta es demostrar, a través del teorema de Church, que no hay una manera de saber, para cualquier FBF que podamos construir en ese sistema formal, si esa misma fórmula es indecidible (...)”.

»Demostrar (corrige Jean Mallart), mediante el teorema de Church, que no hay una manera de saber si una FBF de un sistema es deducible es demostrar la indecidibilidad de la fórmula y, por extensión, del sistema. A eso me refería.

»Saludos cordiales (estoy disfrutando mucho este intercambio; gracias, Josman). :-)

Josman (responde a las aclaraciones de Jean Mallart): En respuesta al mensaje de Jean. Hola de nuevo. Ahora sí que he entendido tu mensaje y su sentido.

»En éste dices: “En definitiva, venía a decirte que creo que a veces confundes decidibilidad con deducibilidad.”

»Es verdad, lo estaba haciendo y eso podía estar liando la explicación. Estaba utilizando indistintamente ambas palabras en la idea de que su diferente significado no afectaba a la cuestión. Y sin embargo ahora veo que sí que la puede afectar y que incluso el mismo teorema de Church es un intento de distinguir esos dos significados.

»Lo que lamento es quedarme sin discusión... :-)

(Fin de la discusión.)