Los investigadores informáticos europeos, Christoph Benzmüller de la Universidad Libre de Berlín (Alemania) y Bruno Woltzenlogel de la Universidad Técnica de Viena (Austria), han formalizado el argumento ontológico sobre la existencia de Dios del matemático Kurt Gödel, el cual ha sido analizado por primera vez 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.
Los argumentos ontológicos sobre la existencia de Dios son razonamientos que pretenden probar la existencia de este ser superior empleando solo la razón. Inspirado por las propuestas medievales de San Anselmo de Canterbury, Gödel planteó en los años 70 una versión lógico-modal (deducciones a partir de expresiones como “es necesario que” y “es posible que” para calificar la verdad de los juicios) con sus correspondientes axiomas, definiciones, corolarios y teoremas.
Cuando Gödel murió en 1978, dejó tras de sí una teoría tentadora basada en los principios de la lógica modal que sugería que un ser superior debe existir. Este razonamiento matemático no tenía como intención convencer de la existencia de Dios, sino demostrar que el llamado “argumento ontológico” de la existencia de Dios es válido.
Gödel definió a Dios como un ser que posee todas las propiedades ‘positivas’, y no entró en profundidad a explicar cuáles son pero indicó unos axiomas razonables (aunque discutibles) que deben satisfacer. Estos son los que ahora han confirmado los científicos informáticos Benzmüller y Woltzenlogel.
Sistema y herramientas de software
Se ha 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, se usaron un MacBookPro 2GHz Intel Core i7 8GB y un MacBook 2.4GHz Intel Core 2 Duo y 2 GB.
Se hicieron 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.
Sistemas de razonamiento automatizado
Las herramientas de razonamiento usadas en la investigación son capaces de razonar con una lógica clásica de orden superior con gran capacidad expresiva. Eso es 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, 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.
Imagen: Kurt Gödel (Izquierda) y Albert Einstein (Derecha). Kurt Friedrich Gödel es reconocido como uno de los más importantes lógicos de todos los tiempos, su trabajo ha tenido un impacto inmenso en el pensamiento científico y filosófico del siglo XX. Llegó a ser un gran amigo de Einstein, y trabajaron juntos los aspectos filosóficos y matemáticos de la Teoría de la Relatividad.
Razones para investigar el teorema de Gödel
El teorema de Gödel es un estándar de comparación para probar los límites de las propias herramientas de razonamiento automatizado en la investigación. Su formalización requiere de una lógica modal de orden superior para distinguir entre una verdad “posible” y una verdad “necesaria”. Para 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.
Además el teorema de Gödel es muy interesante desde un punto de vista filosófico y es objeto de continuas investigaciones.
¿Realmente se demuestra 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. La investigación ha verificado esa afirmación de forma automatizada.
Simplemente se ha demostrado 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.
Se utilizó una computadora portátil
Usando una computadora portátil los científicos Benzmüller y Woltzenlogel han mostrado que la prueba ontológica de Gödel era correcta, al menos a nivel matemático. La investigación se ha publicado en un artículo llamado “Formalización Mecanización y Automatización de la Prueba de la Existencia de Dios de Gödel”.
Benzmüller afirmó que el hecho de que las computadoras puedan resolver teoremas tan complejos abre una nueva gama de posibilidades. Es increíble que el argumento de Gödel pueda ser demostrado de manera automática en tan solo unos segundos o menos en un ordenador portátil estándar, sostuvo. Asimismo, espero que el ejemplo provisto a través de la comprobación de este teorema pueda atraer la atención hacia el método.
Los argumentos ontológicos sobre la existencia de Dios son razonamientos que pretenden probar la existencia de este ser superior empleando solo la razón. Inspirado por las propuestas medievales de San Anselmo de Canterbury, Gödel planteó en los años 70 una versión lógico-modal (deducciones a partir de expresiones como “es necesario que” y “es posible que” para calificar la verdad de los juicios) con sus correspondientes axiomas, definiciones, corolarios y teoremas.
Cuando Gödel murió en 1978, dejó tras de sí una teoría tentadora basada en los principios de la lógica modal que sugería que un ser superior debe existir. Este razonamiento matemático no tenía como intención convencer de la existencia de Dios, sino demostrar que el llamado “argumento ontológico” de la existencia de Dios es válido.
Gödel definió a Dios como un ser que posee todas las propiedades ‘positivas’, y no entró en profundidad a explicar cuáles son pero indicó unos axiomas razonables (aunque discutibles) que deben satisfacer. Estos son los que ahora han confirmado los científicos informáticos Benzmüller y Woltzenlogel.
Sistema y herramientas de software
Se ha 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, se usaron un MacBookPro 2GHz Intel Core i7 8GB y un MacBook 2.4GHz Intel Core 2 Duo y 2 GB.
Se hicieron 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.
Sistemas de razonamiento automatizado
Las herramientas de razonamiento usadas en la investigación son capaces de razonar con una lógica clásica de orden superior con gran capacidad expresiva. Eso es 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, 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.
Imagen: Kurt Gödel (Izquierda) y Albert Einstein (Derecha). Kurt Friedrich Gödel es reconocido como uno de los más importantes lógicos de todos los tiempos, su trabajo ha tenido un impacto inmenso en el pensamiento científico y filosófico del siglo XX. Llegó a ser un gran amigo de Einstein, y trabajaron juntos los aspectos filosóficos y matemáticos de la Teoría de la Relatividad.
Razones para investigar el teorema de Gödel
El teorema de Gödel es un estándar de comparación para probar los límites de las propias herramientas de razonamiento automatizado en la investigación. Su formalización requiere de una lógica modal de orden superior para distinguir entre una verdad “posible” y una verdad “necesaria”. Para 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.
Además el teorema de Gödel es muy interesante desde un punto de vista filosófico y es objeto de continuas investigaciones.
¿Realmente se demuestra 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. La investigación ha verificado esa afirmación de forma automatizada.
Simplemente se ha demostrado 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.
Se utilizó una computadora portátil
Usando una computadora portátil los científicos Benzmüller y Woltzenlogel han mostrado que la prueba ontológica de Gödel era correcta, al menos a nivel matemático. La investigación se ha publicado en un artículo llamado “Formalización Mecanización y Automatización de la Prueba de la Existencia de Dios de Gödel”.
Benzmüller afirmó que el hecho de que las computadoras puedan resolver teoremas tan complejos abre una nueva gama de posibilidades. Es increíble que el argumento de Gödel pueda ser demostrado de manera automática en tan solo unos segundos o menos en un ordenador portátil estándar, sostuvo. Asimismo, espero que el ejemplo provisto a través de la comprobación de este teorema pueda atraer la atención hacia el método.