# Gods, phylosophy and computers


by @ulaulaman http://t.co/Q3AODpvKAs #Godel #ontologicalproof #god #computer

The [ontological arguments](http://plato.stanford.edu/entries/ontological-arguments/) for the existence of God was introduced for the first time by **St. Anselm** in 1078:

> God, by definition, is that for which no greater can be conceived. God exists in the understanding. If God exists in the understanding, we could imagine Him to be greater by existing in reality. Therefore, God must exist.

There are a lot of phylosophies, mathematics and logicians that proposed their ontological argument, for example Descartes, Leibniz, Frege, and also **Kurt Gödel**, that proposed the most formal [ontological proof](http://en.wikipedia.org/wiki/G%F6del's_ontological_proof):

![](https://cdn.hashnode.com/res/hashnode/image/upload/v1743071183395/bb5022b1-1ccd-42a3-bc18-ae4235f3986c.jpeg)

The [proof](http://sas.uwaterloo.ca/~cgsmall/ontology.html) was published in 1987 (Godel died in 1978), and a lot of logicians discussed around it. One of the last papers published about the argument is an [arXiv](http://arxiv.org/abs/1308.4526) that suggested to **Anna Limind** to write that [_European Mathematicians ‘Prove’ the Existence of God_](http://www.learning-mind.com/european-mathematicians-prove-the-existence-of-god/), but the aim of the paper is to control the consistence of the proof and not the reality of the theorem (I think that the theorem is, simply, undecidable), and also to start a new discipline: the _computer-phylosophy_.  
Indeed **Benzmüller** and **Paleo** developed an algorothm in order to use a computer to control the ontological proof. So the work:

> (...) opens new perspectives for a computerassisted theoretical philosophy. The critical discussion of the underlying concepts, definitions and axioms remains a human responsibility, but the computer can assist in building and checking rigorously correct logical arguments. In case of logico-philosophical disputes, the computer can check the disputing arguments and partially fulfill Leibniz' dictum: _Calculemus_

* * *

**Read also**: [Spiegel Online International](http://www.spiegel.de/international/germany/scientists-use-computer-to-mathematically-prove-goedel-god-theorem-a-928668.html)

* * *

Christoph Benzmüller & Bruno Woltzenlogel Paleo (2013). Formalization, Mechanization and Automation of Gödel's Proof of God's Existence, arXiv: [1308.4526v4](http://arxiv.org/abs/1308.4526v4)