But God hath revealed them unto us by his Spirit: for the Spirit searcheth all things, yea, the deep things of God.
1 Corinthians 2:10
Holy Logic: Computer Scientists 'Prove' God Exists
"When Gödel died in 1978, he left behind a tantalizing theory based on principles of modal logic -- that a higher being must exist. The details of the mathematics involved in Gödel's ontological proof are complicated, but in essence the Austrian was arguing that, by definition, God is that for which no greater can be conceived. And while God exists in the understanding of the concept, we could conceive of him as greater if he existed in reality. Therefore, he must exist.
That is where Christoph Benzmüller of Berlin's Free University and his colleague, Bruno Woltzenlogel Paleo of the Technical University in Vienna, come in. Using an ordinary MacBook computer, they have shown that Gödel's proof was correct -- at least on a mathematical level -- by way of higher modal logic.
The name Gödel may not mean much to some, but among scientists he enjoys a reputation similar to the likes of Albert Einstein -- who was a close friend.
Ultimately, the formalization of Gödel's ontological proof is unlikely to win over many atheists, nor is it likely to comfort true believers, who might argue the idea of a higher power is one that defies logic by definition. For mathematicians looking for ways to break new ground, however, the news could represent an answer to their prayers." SpiegelOnline
"Sometime between 1941 and the 1970s, Gödel wrote a brief mathematical proof that God exists----five axioms that we assume to be true:
- Any “property”, or the negation of that property, is “positive”; but it is impossible that both the property and negation are positive.
- If one positive property implies that some property necessarily exists, then the implied property is positive.
- The property of being God-like is positive.
- Positive properties are necessarily positive.
- The property of necessarily existing is positive.
- A “God-like” being has all positive properties.
- An “essence” of a being is a property that the being possesses, and that property necessarily implies any property of that being.
- The “necessary existence” of a being means that it is necessary that all the essences of that being exist (“are exemplified”).
The ancient Greek philosopher and mathematician Euclid laid the foundations of geometry in exactly the same way that Gödel constructed his proof that God exists. Euclid also provided axioms and definitions, then built theorem upon theorem by applying logic. Euclid’s results are still valid; mathematicians still use his approach.
A team of logicians and computer scientists collaborated to encode Gödel’s proof and verify it with several computer programs. These particular programs had to deal with “modal logic”, which can handle statements about “possibility” and “necessity.”
These sophisticated programs have somewhat understated names such as “Nitpick,” “Sledgehammer” and “Metis.” Apparently a MacBook computer can be powerful enough to run them.
Benzmüller and Paleo’s paper states that they used several different modal logic systems to verify Gödel’s proof. Those are different logic systems, not just different computer programs. The logic systems were:
- ‘K’, a “weak” logical system named for logician Saul Kripke;
- ‘B’ logic adds “A implies the necessity of the possibility of A” to ‘K’ logic.
- ‘S4′ and ‘S5′ logic allow some simplification of repeated “possibility” and “necessity” operations; see below.
- If A is a theorem in ‘K’, then “the necessity of A” is also a theorem in ‘K’.
- If it is necessary that “A implies B“, then “the necessity of A ” implies “B is necessary”.
- The “possibility of A” is equivalent to “it is not necessary that A is false”.
"Mathematician KURT GODEL
He turned the lens of mathematics on itself and hit upon his famous incompleteness theorem--driving a stake through the heart of formalism
"Gödel based his argument on an early argument of St. Anselm's. St. Anselm defined God as the greatest being in the universe. No greater being could be imagined. However, if God did not exist, then a greater being had to be possible to imagine - one which exists. Since it wasn't possible, by definition, to imagine a greater being than the greatest being imaginable, God had to exist.
Gödel twisted this argument a little. He used modal logic to prove his point. Modal logic distinguishes between certain different states that certain suppositions have. Some suppositions are possible in some worlds, some possible only in a certain world, and some true in all possible worlds. If they are true in all possible worlds, they are considered to be always 'necessary'.
God can either necessarily exist, or necessarily not exist. If God is an all-powerful being, and he exists, he necessarily exists in all possible worlds. If he doesn't exist, he necessarily doesn't exist in any possible worlds. It is not possible to say that God does not exist in any possible world. No matter how slim the chance is, God might exist. That means that God can't necessarily not exist. Since the choices are either God necessarily does exist, or necessarily doesn't, and we have eliminated the possibility that he necessarily doesn't, the only possibility left is that he necessarily does." WelcomeToTheFuture
"IF it is possible for a rational omniscient being to exist THEN necessarily a rational omniscient being exists.
We can write this in the symbolism of modal logic as 
g 
g b is true for material implication if it is not the case that a is true and b is false. We can also write the conclusion above as g 
g denotes weak disjunction -- equivalent to "and/or" in ordinary parlance, and ~ denotes negation. Other operators include a
b, "a is equivalent to b" and a&b, "a and b". The symbols and are called modal operators, and denote the concept of necessary (as opposed to contingent or accidental) truth, and possible truth. For example, the statement (there is a prime number between n and 2n for all positive integers n) (a tree grows in Brooklyn) t in terms of and vice versa. Thus a ~~a)& (a ~~a)