Логическое доказательство существования Бога: аргумент Гёделя

Logical argument for the existence of God
Gödel's ontological proof is a formal argument by the mathematician Kurt Gödel (1906–1978) for the existence of God. The argument is in a line of development that goes back to Anselm of Canterbury (1033–1109). St. Anselm's ontological argument, in its most succinct form, is as follows: "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." A more elaborate version was given by Gottfried Leibniz (1646–1716); this is the version that Gödel studied and attempted to clarify with his ontological argument. Gödel left a fourteen point outline of his philosophical beliefs in his papers. Points relevant to the ontological proof include:
4. There are other worlds and rational beings of a different and higher kind. 5. The world in which we live is not the only one in which we shall live or have lived. 13. There is a scientific (exact) philosophy and theology, which deals with concepts of the highest abstractness; and this is also most highly fruitful for science. 14. Religions are, for the most part, bad—but religion is not.

The first version of the ontological proof in Gödel's papers is dated "around 1941". Gödel is not known to have told anyone about his work on the proof until 1970, when he thought he was dying. In February, he allowed Dana Scott to copy out a version of the proof, which circulated privately. In August 1970, Gödel told Oskar Morgenstern that he was "satisfied" with the proof, but Morgenstern recorded in his diary entry for 29 August 1970, that Gödel would not publish because he was afraid that others might think "that he actually believes in God, whereas he is only engaged in a logical investigation (that is, in showing that such a proof with classical assumptions (completeness, etc.) correspondingly axiomatized, is possible)." Gödel died January 14, 1978. Another version, slightly different from Scott's, was found in his papers. It was finally published, together with Scott's version, in 1987. In letters to his mother, who was not a churchgoer and had raised Kurt and his brother as freethinkers, Gödel argued at length for a belief in an afterlife. He did the same in an interview with a skeptical Hao Wang, who said: "I expressed my doubts as G spoke [ ] Gödel smiled as he replied to my questions, obviously aware that his answers were not convincing me." Wang reports that Gödel's wife, Adele, two days after Gödel's death, told Wang that "Gödel, although he did not go to church, was religious and read the Bible in bed every Sunday morning." In an unmailed answer to a questionnaire, Gödel described his religion as "baptized Lutheran (but not member of any religious congregation). My belief is theistic, not pantheistic, following Leibniz rather than Spinoza."

Most criticism of Gödel's proof is aimed at its axioms: as with any proof in any logical system, if the axioms the proof depends on are doubted, then the conclusions can be doubted. It is particularly applicable to Gödel's proof – because it rests on five axioms, some of which are considered questionable. A proof does not necessitate that the conclusion be correct, but rather that by accepting the axioms, the conclusion follows logically. Many philosophers have called the axioms into question. The first layer of criticism is simply that there are no arguments presented that give reasons why the axioms are true. A second layer is that these particular axioms lead to unwelcome conclusions. This line of thought was argued by Jordan Howard Sobel, showing that if the axioms are accepted, they lead to a "modal collapse" where every statement that is true is necessarily true, i. e. the sets of necessary, of contingent, and of possible truths all coincide (provided there are accessible worlds at all). According to Robert Koons,

There are suggested amendments to the proof, presented by C. Anthony Anderson, but argued to be refutable by Anderson and Michael Gettings. Sobel's proof of modal collapse has been questioned by Koons, but a counter defence by Sobel has been given. Gödel's proof has also been questioned by Graham Oppy, asking whether many other almost gods would also be "proven" through Gödel's axioms. This counter argument has been questioned by Gettings, who agrees that the axioms might be questioned, but disagrees that Oppy's particular counter example can be shown from Gödel's axioms. Religious scholar Fr. Robert J. Spitzer accepted Gödel's proof, calling it "an improvement over the Anselmian Ontological Argument (which does not work)." There are, however, many more criticisms, most of them focusing on the question of whether these axioms must be rejected to avoid odd conclusions. The broader criticism is that even if the axioms cannot be shown to be false, that does not mean that they are true. Hilbert's famous remark about interchangeability of the primitives' names applies to those in Gödel's ontological axioms ("positive", "god like", "essence") as well as to those in Hilbert's geometry axioms ("point", "line", "plane"). According to André Fuhrmann (2005) it remains to show that the dazzling notion prescribed by traditions and often believed to be essentially mysterious satisfies Gödel's axioms. This is not a mathematical, but a theological task. It is this task which decides which religion's god has been proven to exist.

Christoph Benzmüller and Bruno Woltzenlogel Paleo formalized Gödel's proof to a level that is suitable for automated theorem proving or at least computational verification via proof assistants. The effort made headlines in German newspapers. According to the authors of this effort, they were inspired by Melvin Fitting's book. In 2014, they computationally verified Gödel's proof (in the above version). They also proved that this version's axioms are consistent, but imply modal collapse, thus confirming Sobel's 1987 argument. In the same paper, they suspected Gödel's original version of the axioms to be inconsistent, as they failed to prove their consistency. In 2016, they gave an automated proof that the original version implies , i. e., is inconsistent in every modal logic with a reflexive or symmetric accessibility relation. Moreover, they gave an argument that this version is inconsistent in every logic at all, but failed to duplicate it by automated provers. However, they were able to verify Melvin Fitting's reformulation of the argument and guarantee its consistency.

A humorous variant of Gödel's ontological proof is mentioned in Quentin Canterel's novel The Jolly Coroner. The proof is also mentioned in the TV series Hand of God. Jeffrey Kegler's 2007 novel The God Proof depicts the (fictional) rediscovery of Gödel's lost notebook about the ontological proof.