Tendencias Científicas
Kurt Gödel a los 19 años. Fuente: Wikipedia.
“Investigadores prueban la existencia de Dios con un programa de ordenador”, han publicado en las últimas semanas diversos medios, como el alemán Die Welt.
En realidad, lo que han conseguido los investigadores Christoph Benzmüller, de la Universidad Libre de Berlín en Alemania, y Bruno Woltzenlogel Paleo de la Universidad Técnica de Viena en Austria, es validar informáticamente un teorema del renombrado matemático austríaco Kurt Gödel que señalaba que, desde el punto de vista de la lógica, el argumento de la existencia de Dios es válido.
Como explicaba a SINC recientemente el matemático Jorge López Abad, del ICMAT: “Lo que han hecho estos autores es formalizar el resultado de Gödel en lenguajes informáticos apropiados y luego utilizar paquetes de demostración automatizados para que una máquina demuestre ese resultado”.
Así lo confirmaban Benzmüller y Woltzenlogel en un artículo sobre su trabajo aparecido en el repositorio científico arXiv : el teorema ontológico de Gödel ha sido analizado por vez primera con un nivel de detalle sin precedentes usando herramientas informáticas de interpretación de la sintaxis, de verificación automática de la consistencia de sus axiomas y definiciones; y de demostración automática del teorema, entre otras.
Y lo curioso es que todo se ha hecho con dos MacBooks ordinarios, unos ordenadores portátiles de Apple, desarrollados para el uso en el hogar y en pequeñas empresas. En general, el uso de computadoras para reducir el trabajo de los matemáticos no es nuevo. En concreto, la demostración automática de teoremas (ATP, por Automated theorem proving) o Deducción automatizada, es actualmente el subcampo más desarrollado del razonamiento automatizado.
En realidad, lo que han conseguido los investigadores Christoph Benzmüller, de la Universidad Libre de Berlín en Alemania, y Bruno Woltzenlogel Paleo de la Universidad Técnica de Viena en Austria, es validar informáticamente un teorema del renombrado matemático austríaco Kurt Gödel que señalaba que, desde el punto de vista de la lógica, el argumento de la existencia de Dios es válido.
Como explicaba a SINC recientemente el matemático Jorge López Abad, del ICMAT: “Lo que han hecho estos autores es formalizar el resultado de Gödel en lenguajes informáticos apropiados y luego utilizar paquetes de demostración automatizados para que una máquina demuestre ese resultado”.
Así lo confirmaban Benzmüller y Woltzenlogel en un artículo sobre su trabajo aparecido en el repositorio científico arXiv : el teorema ontológico de Gödel ha sido analizado por vez primera con un nivel de detalle sin precedentes usando herramientas informáticas de interpretación de la sintaxis, de verificación automática de la consistencia de sus axiomas y definiciones; y de demostración automática del teorema, entre otras.
Y lo curioso es que todo se ha hecho con dos MacBooks ordinarios, unos ordenadores portátiles de Apple, desarrollados para el uso en el hogar y en pequeñas empresas. En general, el uso de computadoras para reducir el trabajo de los matemáticos no es nuevo. En concreto, la demostración automática de teoremas (ATP, por Automated theorem proving) o Deducción automatizada, es actualmente el subcampo más desarrollado del razonamiento automatizado.
El presente trabajo ayudará a impulsar la filosofía teórica asistida por ordenador, esperan sus autores. Imagen: MacBook. Fuente: Apple.
Benzmüller y Woltzenlogel Paleo han explicado a Tendencias21 en la siguiente entrevista los detalles de su investigación:
¿En qué consiste exactamente el sistema que han utilizado para probar el teorema de Gödel?
Hemos verificado el teorema de Gödel en sistemas computacionales estándar, con herramientas de software específicas, denominadas probadores de teoremas y model finders. Para ello, usamos un MacBookPro 2GHz Intel Core i7 8GB y un MacBook 2.4GHz Intel Core 2 Duo y 2 GB.
En nuestros experimentos también hemos hecho consultas remotas a probadores de teoremas instalados y mantenidos por la iniciativa SystemOnTPTP de Geoff Sutcliffe. Estas consultas remotas son muy útiles, pues permiten evitar la localidad de las instalaciones de los probadores de teoremas. La especificación de los ordenadores de SystemOnTPTP en Miami es: i686 Intel(R) Xeon(R) CPU 5140 @ 2.33GHz, NumberOfCPUs: 4, RAMPerCPU: 1006.25MB, OS: Linux 2.6.32.26.
¿Cuál sería la diferencia entre estos sistemas y otros de razonamiento automatizado?
Las herramientas de razonamiento que usamos en este caso son capaces de razonar con una lógica clásica de orden superior con gran capacidad expresiva. Eso resultó esencial en la formalización, la verificación y la automatización de la prueba de Gödel sobre la existencia de Dios.
La mayoría de otros sistemas de razonamiento automatizado, por el contrario, se centran en partes de la lógica de predicados de primer orden (por ejemplo, en la lógica proposicional), lo cual resulta menos expresivo, aunque sea más sencillo de gestionar.
¿Por qué escogieron el teorema de Gödel para su investigación?
En realidad por varias razones. Por un lado, el teorema de Gödel es un estándar de comparación para probar los límites de nuestras propias herramientas de razonamiento automatizado. Su formalización requiere de una lógica modal de orden superior para distinguir entre una verdad “posible” y una verdad “necesaria”. Con nuestro trabajo queríamos demostrar que el razonamiento en una lógica modal de primer orden puede ser reducido elegante y efectivamente a un razonamiento lógico de primer orden clásico.
Por otra parte, el teorema de Gödel es muy interesante desde el punto de vista filosófico y es objeto de continuas investigaciones.
¿Qué opinan de las implicaciones filosóficas y religiosas que algunos medios de comunicación han resaltado de su trabajo? ¿Realmente demuestra éste la existencia de Dios?
El teorema de Gödel depende de axiomas y de definiciones. En concreto, Gödel definió a Dios como un ser que posee todas las propiedades positivas. Propuso cinco axiomas que describen lo que son las propiedades positivas, y señaló que la necesaria existencia de Dios podía inferirse a partir de esos axiomas. En nuestro trabajo hemos verificado esa afirmación de forma automatizada.
Eso simplemente demostró que el teorema de Gödel (la necesaria existencia de Dios) debe ser cierto en nuestro mundo, si los cinco axiomas también son verdaderos. Sin embargo, la veracidad de dichos axiomas es cuestionable y no empíricamente comprobable.
¿Por qué usaron el MacBook para sus análisis?
Cualquier otro portátil con una configuración de hardware similar y un sistema operativo moderno habría bastado. Simplemente, somos usuarios de Mac.
Sin embargo, a los medios parece haberles gustado este hecho, y han provocado una reacción en cadena que lo ha convertido en titular. Nos ha divertido mucho este mecanismo de propagación mediática.
Entonces, para conseguir una mejora del sistema utilizado, ¿se requerirían ordenadores más avanzados?
Un hardware más potente permitiría a nuestros sistemas de software operar más rápidamente y manejar espacios de búsqueda más amplios (la prueba de un teorema es un proceso de búsqueda).
En consecuencia, existe una pequeña posibilidad de que con un sistema más avanzado se pudieran comprobar algunos teoremas que no pueden demostrarse con un PC estándar. Sin embargo, la experiencia nos dice que sería más inteligente invertir en mejorar las herramientas de software y su teoría subyacente que en ordenadores más rápidos.
¿Qué teoremas podrían analizarse con esos otros sistemas? ¿Planean aplicarlos a teoremas más complejos?
La lógica modal de primer orden tiene muchas aplicaciones potenciales, por ejemplo, en inteligencia artificial, lingüística computacional o verificación formal de sistemas de hardware y software. Pero la técnica que hemos aplicado propicia la automatización de otras lógicas desafiantes (y de sus combinaciones), para las cuales no existen actualmente probadores. Queremos explorar esta variedad de posibilidades en el futuro.
A corto plazo, tenemos intención de centrarnos en pruebas ontológicas y queremos analizar las críticas y las adaptaciones de la prueba de Gödel con nuestra tecnología. A partir de este trabajo, nos gustaría contribuir a una metodología y a una infraestructura que apoye lo que nosotros llamamos una “filosofía teórica asistida por ordenador”.
¿Qué ventajas científicas pueden obtenerse de este avance?
Las herramientas para probar teoremas que empleamos garantizan una mayor precisión. Este nivel de precisión no se encuentra normalmente en pruebas humanas, ni siquiera en las de los presupuestos de Gödel.
Por ejemplo, en nuestro trabajo los parámetros de la lógica modal de primer orden que hemos empleado son conocidos con exactitud, algo que a menudo no sucede con los documentos filosóficos.
Además, algunas tareas de razonamiento, como llenar lagunas en bocetos de prueba o encontrar contra-modelos para conjeturas erróneas, pueden apoyarse ahora eficazmente con computadoras. Esperamos que en un futuro próximo los filósofos sean preparados para utilizar nuestras herramientas, y así mejorar su precisión y su eficiencia.
¿En qué consiste exactamente el sistema que han utilizado para probar el teorema de Gödel?
Hemos verificado el teorema de Gödel en sistemas computacionales estándar, con herramientas de software específicas, denominadas probadores de teoremas y model finders. Para ello, usamos un MacBookPro 2GHz Intel Core i7 8GB y un MacBook 2.4GHz Intel Core 2 Duo y 2 GB.
En nuestros experimentos también hemos hecho consultas remotas a probadores de teoremas instalados y mantenidos por la iniciativa SystemOnTPTP de Geoff Sutcliffe. Estas consultas remotas son muy útiles, pues permiten evitar la localidad de las instalaciones de los probadores de teoremas. La especificación de los ordenadores de SystemOnTPTP en Miami es: i686 Intel(R) Xeon(R) CPU 5140 @ 2.33GHz, NumberOfCPUs: 4, RAMPerCPU: 1006.25MB, OS: Linux 2.6.32.26.
¿Cuál sería la diferencia entre estos sistemas y otros de razonamiento automatizado?
Las herramientas de razonamiento que usamos en este caso son capaces de razonar con una lógica clásica de orden superior con gran capacidad expresiva. Eso resultó esencial en la formalización, la verificación y la automatización de la prueba de Gödel sobre la existencia de Dios.
La mayoría de otros sistemas de razonamiento automatizado, por el contrario, se centran en partes de la lógica de predicados de primer orden (por ejemplo, en la lógica proposicional), lo cual resulta menos expresivo, aunque sea más sencillo de gestionar.
¿Por qué escogieron el teorema de Gödel para su investigación?
En realidad por varias razones. Por un lado, el teorema de Gödel es un estándar de comparación para probar los límites de nuestras propias herramientas de razonamiento automatizado. Su formalización requiere de una lógica modal de orden superior para distinguir entre una verdad “posible” y una verdad “necesaria”. Con nuestro trabajo queríamos demostrar que el razonamiento en una lógica modal de primer orden puede ser reducido elegante y efectivamente a un razonamiento lógico de primer orden clásico.
Por otra parte, el teorema de Gödel es muy interesante desde el punto de vista filosófico y es objeto de continuas investigaciones.
¿Qué opinan de las implicaciones filosóficas y religiosas que algunos medios de comunicación han resaltado de su trabajo? ¿Realmente demuestra éste la existencia de Dios?
El teorema de Gödel depende de axiomas y de definiciones. En concreto, Gödel definió a Dios como un ser que posee todas las propiedades positivas. Propuso cinco axiomas que describen lo que son las propiedades positivas, y señaló que la necesaria existencia de Dios podía inferirse a partir de esos axiomas. En nuestro trabajo hemos verificado esa afirmación de forma automatizada.
Eso simplemente demostró que el teorema de Gödel (la necesaria existencia de Dios) debe ser cierto en nuestro mundo, si los cinco axiomas también son verdaderos. Sin embargo, la veracidad de dichos axiomas es cuestionable y no empíricamente comprobable.
¿Por qué usaron el MacBook para sus análisis?
Cualquier otro portátil con una configuración de hardware similar y un sistema operativo moderno habría bastado. Simplemente, somos usuarios de Mac.
Sin embargo, a los medios parece haberles gustado este hecho, y han provocado una reacción en cadena que lo ha convertido en titular. Nos ha divertido mucho este mecanismo de propagación mediática.
Entonces, para conseguir una mejora del sistema utilizado, ¿se requerirían ordenadores más avanzados?
Un hardware más potente permitiría a nuestros sistemas de software operar más rápidamente y manejar espacios de búsqueda más amplios (la prueba de un teorema es un proceso de búsqueda).
En consecuencia, existe una pequeña posibilidad de que con un sistema más avanzado se pudieran comprobar algunos teoremas que no pueden demostrarse con un PC estándar. Sin embargo, la experiencia nos dice que sería más inteligente invertir en mejorar las herramientas de software y su teoría subyacente que en ordenadores más rápidos.
¿Qué teoremas podrían analizarse con esos otros sistemas? ¿Planean aplicarlos a teoremas más complejos?
La lógica modal de primer orden tiene muchas aplicaciones potenciales, por ejemplo, en inteligencia artificial, lingüística computacional o verificación formal de sistemas de hardware y software. Pero la técnica que hemos aplicado propicia la automatización de otras lógicas desafiantes (y de sus combinaciones), para las cuales no existen actualmente probadores. Queremos explorar esta variedad de posibilidades en el futuro.
A corto plazo, tenemos intención de centrarnos en pruebas ontológicas y queremos analizar las críticas y las adaptaciones de la prueba de Gödel con nuestra tecnología. A partir de este trabajo, nos gustaría contribuir a una metodología y a una infraestructura que apoye lo que nosotros llamamos una “filosofía teórica asistida por ordenador”.
¿Qué ventajas científicas pueden obtenerse de este avance?
Las herramientas para probar teoremas que empleamos garantizan una mayor precisión. Este nivel de precisión no se encuentra normalmente en pruebas humanas, ni siquiera en las de los presupuestos de Gödel.
Por ejemplo, en nuestro trabajo los parámetros de la lógica modal de primer orden que hemos empleado son conocidos con exactitud, algo que a menudo no sucede con los documentos filosóficos.
Además, algunas tareas de razonamiento, como llenar lagunas en bocetos de prueba o encontrar contra-modelos para conjeturas erróneas, pueden apoyarse ahora eficazmente con computadoras. Esperamos que en un futuro próximo los filósofos sean preparados para utilizar nuestras herramientas, y así mejorar su precisión y su eficiencia.
Referencia bibliográfica:
Christoph Benzmüller, Bruno Woltzenlogel Paleo. Formalization, Mechanization and Automation of Gödel's Proof of God's Existence. arXiv:1308.4526 (2013).
Christoph Benzmüller, Bruno Woltzenlogel Paleo. Formalization, Mechanization and Automation of Gödel's Proof of God's Existence. arXiv:1308.4526 (2013).
Inicio
Enviar a un amigo
Versión para imprimir
Compartir
Javier Cacho: La Antártida es una ventana abierta a la esperanza
CIENCIA ON LINE