modal Logic

in statement P(x), P is called predicate, while x is called term

First-Order Logic (FOL, which is studied in universities) allows to apply quantifiers ∃ and ∀ for terms, but not for predicates. it is also not allowed to apply predicates to other predicates

Higher-Order Logic (HOL) differs from FOL - it relaxes this requirement, so we may write statements like that: ∀P.∃x.P(x)

now the interesting part: Modal Logic says that some of the statements can be NECESSARILY True or False, and some of the statements are POSSIBLY True or False. there are three possibilities here:

Modal Logic has a number of axioms:

M1: ¬◆P ↔ ⋄¬P
if it is not True that something is True in each universe, then there may exist a universe where it is False

M2: ◆P → P
if something is necessarily True, then it is True in all universes

M3: ◆(P → T) → (◆P → ◆T)
if in all universes T follows from P, and if in all universes P is True then in all universes T is True

M4:
if P can be proven (which includes the case when P is an axiom), then ◆P

M5: ⋄◆P → ◆P
if ⋄◆P is True, then it means that there exists some universe where it is known that ◆P. if we could transfer ourselves to that universe, we would know that P is necessarily True. so we conclude that ◆P

application of implication contrapositive rule to M5 gives us formula ⋄¬P → ◆⋄¬P
denoting ¬P by T we get an equivalent statement of the same axiom:

M5: ⋄T → ◆⋄T

Modal Logic has other axioms, but we wouldnt need them

following Hartshorne

and now we are ready to prove the existence of God

lets denote statement "god exists" by g and assume two axioms:

HA1: ⋄g

assuming that even atheists can imagine the existence of god

HA2: ⋄¬g → ¬g

from the fact that it is possible that god doesnt exist in some other universe, we immediately conclude that it doesnt exist in our own universe

let us start the proof:

H1: lets substitute ¬g to M5 axiom: ⋄¬g → ◆⋄¬g

H2: substitute ◆g to the law of excluded middle and use M1: (◆g) ∨ (⋄¬g)

H3: applying implication H1 to H2 we are getting ◆g ∨ ◆⋄¬g

H4: since we assume HA2 as an axiom, we can apply rule M4 to get ◆(⋄¬g → ¬g)

H5: by M3: ◆⋄¬g → ◆¬g

H6: H5 and H3 together gives us ◆g ∨ ◆¬g

this eliminates the possibility of accidental god existence: either god exists in all possible worlds or it cannot exist in any of them

H7: axiom M1 is equivalent to ¬¬⋄g (two negations cancel each other), to which we can apply M1 to get ¬◆¬g

H8: from H7 we know that term ◆¬g in H6 cannot be True. so the only possibility for H6 to be True (and we know that it is True because we proved it) is that ◆g is True. this shows that god necessarily exists which completes the proof

does this really prove that god exists?

it depends if you agree with Hartshornes axioms and axioms of Modal Logic. in fact, this proof doesnt even say what god is. it can be applied for any statement which matches the same set of axioms. for example, substitute "god doesnt exist" for g and the same reasoning would apply for the proof that god doesnt exist

it is interesting to note that axiom HA2 is equivalent to statement g → ◆g (using implication contra-positive and M1) which reads as "if god exists in our world, it must exist in any possible world". this statement looks much stronger than the original axiom and seems to be less probable to be True, even though these two formulations are totally equivalent!

can this proof be considered mathematical? it depends on what you call mathematics. the only bit of mathematics here is the usage of formulas and a strict agreement on axioms and what logical derivations we consider as acceptable. but this is what mathematics is actually is: it is just an agreement on rules which we use and a convenient language which helps our reasoning