Turin y Gödel

Jim Jubak
La Máquina Pensante. El cerebro humano y la inteligencia artificial.
Ediciones B. Documentos.
Barcelona, febrero 1993

Pag.55:
Pero el trabajo de Kurt Gödel, complementado por informes de Alan Turing, Emil Post y Alonzo Church, demostraba que la búsqueda de una conclusión completamente formal estaba condenada. En 1931, Gödel, entonces con veinticinco años de dad, probó, en su teorema de la incompletitud y su corolario sobre consistencia, que cualquier sistema formal equivalente al de Whitehead y Rusell tenía, por necesidad, que ser incompleto. Gödel demostró que tenían que existir proposiciones no decidibles en un sistema semejante, proposiciones que no podían ser probadas o refutadas utilizando cualquiera de las reglas del sistema. Su corolario afirmaba que la consistencia misma es una de esas proposiciones no decidibles.

El trabajo de Turing confirmó el teorema de Gödel. Pero Turing demostró también que, a pesar de que un sistema completamente formal era imposible, sistemas formales específicos podían ser notablemente potentes y expresivos. Turing, Post y Church desarrollaron de manera independiente sistemas formales específicos que eran completos en el sentido de que, si bien no podían probar o refutar todas las proposiciones, podían generar formalmente todos los teoremas demostrables de la lógica. La estructura formal de Turing llamda Universal Turing Machine (Máquina Universal de Turing) podía simular cualquier teorema lógico en este sistema. La máquina de Turing manipulaba los símbolos de la lógica, sus pruebas y teoremas, en forma de unos y ceros sobre una cinta de papel. Con esos unos y ceros y bastante cinta la máquina de Turing podía expresar cualquier teorema comprobable producido en cualquier sistema lógico.