# A Computationally-Discovered Simplification of the Ontological Argument

@article{Oppenheimer2011ACS, title={A Computationally-Discovered Simplification of the Ontological Argument}, author={Paul E. Oppenheimer and Edward N. Zalta}, journal={Australasian Journal of Philosophy}, year={2011}, volume={89}, pages={333 - 349} }

The authors investigated the ontological argument computationally. The premises and conclusion of the argument are represented in the syntax understood by the automated reasoning engine PROVER9. Using the logic of definite descriptions, the authors developed a valid representation of the argument that required three non-logical premises. PROVER9, however, discovered a simpler valid argument for God's existence from a single non-logical premise. Reducing the argument to one non-logical premise… Expand

#### 34 Citations

On the PROVER9 Ontological Argument

- Philosophy
- 2015

Oppenheimer & Zalta have re-formulated their non-modal version of the ontological argument, with the help of PROVER9, an automated reasoning engine. The authors end up rejecting the new argument;… Expand

The Ontological Argument in PVS

- Mathematics
- 2013

The Ontological Argument, an 11th Century proof of the existence of God, is a good candidate for Fun With Formal Methods as nearly everyone finds the topic interesting. We formalize the Argument in… Expand

Variants of Gödel’s Ontological Proof in a Natural Deduction Calculus

- Mathematics, Computer Science
- Stud Logica
- 2017

The first formal proof closely follows the hints in Scott's manuscript about Gödel’s argument and fills in the gaps, thus verifying its correctness, and the second formal proof improves the first, by relying on the weaker modal logic KB instead of S5 and by avoiding the equality relation. Expand

A Computationally Assisted Reconstruction of an Ontological Argument in Spinoza’s The Ethics

- Philosophy
- Open Philosophy
- 2019

Abstract The comments accompanying Proposition (Prop.) 11 (“God ... necessarily exists”) in Part I of Spinoza’s The Ethics contain sketches of what appear to be at least three more or less distinct… Expand

An Object-Logic Explanation for the Inconsistency in Gödel's Ontological Theory (Extended Abstract, Sister Conferences)

- Philosophy
- 2016

This paper discusses the inconsistency in Gödel’s ontological argument. Despite the popularity of Gödel’s argument, this inconsistency remained unnoticed until 2013, when it was detected… Expand

The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics

- Computer Science
- IJCAI
- 2016

The discovery of the inconsistency in Godel's ontological argument as a success story for artificial intelligence and the development of an improved syntactical hiding for the utilized logic embedding technique allows the refutation to be presented in a human-friendly way, suitable for non-experts in the technicalities of higher-order theorem proving. Expand

Can Computers Help to Sharpen our Understanding of Ontological Arguments

- Computer Science
- 2018

It is claimed that interreligious understanding may be fostered by means of formal argumentation and, in particular, formal logical analysis supported by modern interactive and automated theorem proving technology. Expand

Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers

- Computer Science
- ECAI
- 2014

The background theory of the work presented here offers a novel perspective towards a computational theoretical philosophy in Kurt Godel's ontological argument for God's existence. Expand

A Case Study On Computational Hermeneutics: E. J. Lowe's Modal Ontological Argument

- Computer Science, Philosophy
- FLAP
- 2018

This claim is defended by showcasing the application of a new, computer-assisted interpretive method to an exemplary natural-language argument with strong ties to metaphysics and religion: E. Lowe's modern variant of St. Anselm’s ontological argument for the existence of God. Expand

Mechanized analysis of Anselm’s modal ontological argument

- Philosophy
- 2020

We use a mechanized verification system, PVS, to examine the argument from Anselm’s Proslogion Chapter III, the so-called “Modal Ontological Argument.” We consider several published formalizations… Expand

#### References

SHOWING 1-10 OF 21 REFERENCES

REFLECTIONS ON THE LOGIC OF THE ONTOLOGICAL ARRGUMENT

- Mathematics
- 2007

Our 1991 paper on the logic of the ontological argument contained an analysis of the structure of Anselm’s argument for the existence of God. We showed that there is a valid argument for God’s… Expand

ON THE LOGIC OF THE ONTOLOGICAL ARGUMENT

- Philosophy
- 1991

Saint Anselm of Canterbury offered several arguments for the existence of God. We examine the famous ontological argument in Proslogium II. Many recent authors have interpreted this argument as a… Expand

Steps Toward a Computational Metaphysics

- Computer Science
- J. Philos. Log.
- 2007

This paper describes what is discovered when the theory of abstract objects is implemented in prover9 (a first-order automated reasoning system which is the successor to otter), and how prover 9 then finds proofs of interesting theorems of metaphysics, such as that every possible world is maximal. Expand

Mace4 Reference Manual and Guide

- Computer Science, Mathematics
- ArXiv
- 2003

Mace4 is a program that searches for finite models of first-order formulas and performs better on equational problems than did the previous model-searching program Mace2. Expand

OTTER 3.3 Reference Manual

- Computer Science, Mathematics
- ArXiv
- 2003

OTTER is a resolution-style theorem-proving program for first-order logic with equality. OTTER includes the inference rules binary resolution, hyperresolution, UR-resolution, and binary… Expand

Prover9 Manual, URL = <http://www.cs.unm.edu/ ̃mccune/mace4/manual/2009-11A/>

- 2009

Reflections on the Logic of the Ontological Argument: A Journal of Analytic Scholasticism

- Philosophy
- 2007

Steps Towards a Computational Metaphysics

- Journal of Philosophical Logic
- 2007

2003b, Mace4 Reference Manual and Guide (Tech

- Memo ANL/MCS-TM-264, Mathematics and Computer Science Division),
- 2003