"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."
Bruno Woltzenlogel Paleo y Christoph Benzmüller
"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.
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 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."
Bruno Woltzenlogel Paleo y Christoph Benzmüller
"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”."
Bruno Woltzenlogel Paleo y Christoph Benzmüller
"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."
Bruno Woltzenlogel Paleo y Christoph Benzmüller
No hay comentarios:
Publicar un comentario