On the verification of a proof of ‘God’s existence’

Der Spiegel online offered an eye-cathcing headline last week: ‘Computer Scientists “Prove”  God Exists’ (article here). The article referred to a pre-publication report of a paper submitted to arxiv.org last month, entitled ‘Formalization, Mechanization and Automation of Gödel’s Proof of God’s Existence’ (here). Essentially, the paper claims – it is more of an abstract and statement of results – that (a form of) Kurt Gödel’s modal ontological argument had been successfully coded, and that its validity had been demonstrated using – the detail I rather liked – programs running on a MacBook. As my colleague Alan Torrance pointed out on FB, this is not surprising; there has been a fairly general acceptance of Gödel’s logic for a while now. And as Der Spiegel pointed out, the point of the research was not to prove God’s existence but to demonstrate the possibility of computerised verification of logical arguments, using an argument of some fame, and of acknowledged complexity, as a test case. That said, the statement that a proof of God’s existence has been shown to be valid is not uninteresting – and that it is a version of the (in)famous ontological argument is very pleasing to those, like me, who see a restless fascination with the ontological argument as the infallible mark of a truly philosophical mind…

Attentive readers will have noted some variation in use of scare quotes in the various headlines: the original piece used none; the newspaper article suggested ‘proof’ was being used wrongly; my title suggests the issue lies with ‘God’s existence’. Obviously, I think my usage is correct, but these differences highlight what is at stake. In defence of the original authors, they were referring to ‘Gödel’s proof of God’s existence’ in the same way they might have referenced ‘Fermat’s last theorem’: it is a well-known logical conundrum of interest to logicians because it appears correct but seeming has proved difficult to demonstrate completely. Der Spiegel‘s headline (at least in translation; I could not find an easy way to navigate to a German original of the article) suggested that the ‘proof’ was dubious; this is precisely wrong; assuming the correctness of the results reported, the heart of the research findings is the fact that the proof is certain, and demonstrated to be so.

But what has been proved? Deductive logic always proves the same thing: that, given a certain set of axioms and definitions, a certain set of conclusions follows from a certain set of premises. (In modal logic there is an added complication of which modal logic is in play; if you are interested in the technical details of modal logics, go and get a life the paper claims that KB is sufficient for the proof to work; S5 is not needed.) In serious logic, the axioms and definitions are necessarily seriously abstruse and formal (here, Definition 3 asserts ‘Necessary existence of an individual is the necessary exemplification of all its essences’). The precise proof is that, given five axioms and accepting three definitions, it can be shown that a ‘God-like being’ necessarily exists, where ‘God-like’ means ‘possessing all positive properties’ (this is essentially a formalisation of perfect being theology).

So what hesitations might we have before claiming ‘scientists have proved that God exists?’ Two, one more (theologically) significant than the other.

First, and less significant, the proof is uninteresting (except as a neat bit of demonstrated logic) if any of the axioms or definitions are dubious. The three required definitions and five stated axioms are as follows (you can look up the symbolic logic in the paper above if you are interested):

  • D1 A ‘God-like’ being possesses all positive properties.
  • D2 An ‘essence’ of an individual is a property possessed by it and necessarily implying any of its properties.
  • D3 ‘Necessary existence’ of an individual is the necessary exemplification of all its essences.
  • A1 Either a property or its negation is positive, but not both.
  • A2 A property necessarily implied by a positive property is positive.
  • A3 The property of being ‘God-like’ is positive.
  • A4 Positive properties are necessarily positive.
  • A5 Necessary existence is a positive property.

Now, anyone at all familiar with debate over the ontological argument in its various forms will fairly quickly spot the first point of attack here: is the concept of ‘necessary existence’ coherent/meaningful? (And, concomitantly, is the claim that it is a positive property if coherent justified?) As the authors say in their concluding paragraph, ‘[t]he critical discussion of the underlying concepts, definitions and axioms remains a human responsibility…’ (In reading the proof, I am also struck by the unspecified value-judgement implied in the word ‘positive’; A3, A5, and probably D1 seem to me to smuggle in a set of ethical assumptions that need to be uncovered and tested at the very least – I suspect that this has been worked through in philosophical literature I have not read, however.)

All of this is to say that the ‘proof’ relies on the acceptance of some foundations which are not beyond question, as any proof does. As I say, this is hardly very interesting, but it does need saying.

Second, and more significant: even if we grant the axioms and proofs, what is proved is the (necessary) existence of a ‘God-like’ being, where (D1 above) ‘God-like’ means ‘possessing all positive properties’. What – if any – is the relation of this being to the One who spoke to Moses from the bush, the One who Jesus called Father, the One who sent Mohammed as His messenger, or indeed the Flying Spaghetti Monster of contemporary parody? (Other putative deities are available…) In the classic treatment of proving God’s existence in the Christian tradition, the ‘Five Ways’ of St Thomas, this problem is acknowledged carefully, but (unfortunately…) quietly enough that it has often been missed. Having proved the existence of a first mover, or first efficient cause, or… Thomas carefully says ‘and this everyone understands to be God’ (hoc omnes intelligunt Deum) or ‘which everyone names “God”‘ (quam omnes Deum nominant) or ‘which everyone speaks of as “God”‘ (quod omnes dicunt Deum) or ‘this we speak of as “God”.’ (hoc dicimus Deum – used twice in ST Ia q2 art3 resp.) Thomas knew that there is a conceptual distance between what is proved by  various arguments – including those bearing the imprimatur of Apple hardware – and what is implied in Christian theology by the name ‘God’. He seemingly bridged this distance by an appeal to nothing more than universal custom: ‘we speak of …’; ‘everybody calls …’

That said, St Thomas claimed to be proving the existence of God; he introduces the Five Ways with the (remarkably laconic…) comment ‘I answer that the existence of God can be proved in five ways…’ (Respondeo dicendum quod Deum esse quinque viis probari potest). Thomas was a brilliant logician; how do we make sense of this gap? I think the answer is in noticing that the Five Ways, and the discussion of the possibility of knowing God’s existence that they are a part of, occur in question 2 of the prima pars, and so follow on from question 1 (I know; they pay me to have these brilliant insights…). The name ‘God’ has already been given, by implication, rich content; Scripture has been introduced as a necessary source for theological knowledge (the very first response of the work reads: Respondeo dicendum quod necessarium fuit ad humanam salutem, esse doctrinam quandam secundum revelationem divinam, praeter philosophicas disciplinas, quae ratione humana investigantur!)

Thomas argues for the existence of various primal beings: the unmoved mover; the first cause; the being that is sufficient reason for its own existence; the highest good; and the final end – to this list our mathematicians have added ‘a being possessing all positive properties’. He then asserts on the basis of revelation (in ST) that these primal realities are in fact one and the same, and identified with the triune God. It may be that there is a good logical argument for at least some of this unity (I offer no formal argument, but the identity of the unmoved mover and the first cause feels like a proposition that might well be susceptible to some future work with an iMac…), but Thomas relies on an unnarrated account of revelation, not a careful chain of argument, to link the primal beings proved by his logic with the name of Jesus.

1 Comment

  1. Tyler Wittman
    Oct 29, 2013

    I always love to see sane commentary on Thomas! Two thoughts:

    1. Thomas would still object to the iProof just as he did Anselm’s ontological proof, no? God’s existence is self-evident per se, but not quoad nos.

    2. I’m not sure where I come down on the Five Ways just yet, but I do see some plausibility in the view that Thomas was actually trying to demonstrate the existence of a rather formal ‘deity’, i.e. ‘quod habet providentiam universalem de rebus’ (Ia.13.8), defined at least initially apart from the material content of faith.

    Yet even if that’s the case, what strikes me as more saliently theological in the Five Ways is the assumption about material reality being an effect. Naturally, this is more striking to a Westerner in the 21st century, but still: the atheist simply believes selfish genes ‘habet providentiam universalem de rebus’. What the atheist doesn’t believe is that life, the universe, and everything is an effect of something other than itself. I’m more inclined to locate Thomas’ ‘cheating’, as it were, there in the doctrine of creation.

Leave a Reply to Tyler Wittman Cancel reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.

get facebook like button