Sesión especial del Seminario (2-11-2010): Ed Zalta

Fecha / Date: 2-11-2010.

Hora / Time: 17:00 h.

Lugar / Location: Seminario de Lógica del Dpto. de Filosofía y Lógica y Filosofía de la Ciencia - Universidad de Sevilla.

Ponente / Lecturer: Ed Zalta, Stanford University, EE.UU. (website)

Título / Tittle: New results in Computational Methaphysics.

Resumen / Abstract:
Se presentan nuevos resultados de investigación que siguen las líneas descritas en "Steps Toward Computational Metaphysics'' (coautores: Branden Fitelson y Edward N. Zalta), publicada en el Journal of Philosophical Logic, 36/2 (Abril 2007, p.227-247). En esta investigación implementamos una metafísica axiomatizada en el sistema de razonamiento automático PROVER9. Hay dos áreas en las cuáles se han obtenido nuevos resultados: (1) el argumento ontológico de Anselmo y (2) el cálculo de conceptos de Leibniz.
En (1), mostramos que la versión formal del argumento ontológico, desarrollado por Oppenheimer y Zalta en el artículo "The Logic of Ontological Argument" (Philosophical Perspectives, 5, 1991, p.509-529), puede ser simplificado. El motor del razonador automático PROVER9 descubrió que el argumento descrito por los autores no necesita apelar a una de las premisas no lógicas presentadas en el artículo. Se explicará como el razonador automático descubrió dicha simplificación.
En (2), se presentan los nuevos resultados donde el razonador automático E-PROVER derivó los teoremas y axiomas fundamentales del cálculo de conceptos de Leibniz (de su publicación de 1689) desde la teoría axiomática de los objetos abstractos. Asimismo, revisamos los principios básicos de dicha teoría.
/
In this presentation, I present new results from the research that was described in the paper ''Steps Toward Computational Metaphysics'' (coauthors: Branden Fitelson and Edward N. Zalta), published in J. Philosophical Logic, 36/2 (April 2007): 227--247). In this research, we implement an axiomatic metaphysics in the automated reasoning program PROVER9. There are two areas in which new results have been developed: (1) Anselm's ontological argument and (2) Leibniz's calculus of concepts.
In (1), we show that the formal version of Anselm's ontological argument,developed by Oppenheimer and Zalta in their paper "The Logic of Ontological Argument" (Philosophical Perspectives, 5, 1991, 509-529), can be simplified. The automated reasoning engine PROVER9 discovered that the argument described by the authors need not appeal to one of the non-logical premises described in the paper. So we explain how the automated reasoning engine discovered a simplification overlooked by the authors.
In (2), we describe the new results we've obtained in which an automated reasoning engine (E-prover) derived the fundamental axioms and theorems of Leibniz's calculus of concepts (in his paper of 1689) from the axiomatic theory of abstract objects. We review the basic principles of axiomatic theory of abstract objects.