My friend sent me this argument to "prove the existence of god". I am not smart on Logic and I know people here are. The argument is explained in detail on Pruss's blog. Below is the formalization (G stands for "God exists"):
Like all variations on this argument, several modal principles are accepted as true from the start which are not at all obvious (to put it mildly). In this case, each of the first four statements involves such a hypothesis: 1, 2, and 4 literally are such hypotheses, and 3 invokes one (namely K).
So what the argument actually shows is that the existence of god would follow if certain ontological hypotheses actually hold. This is, to put it mildly, far from a proof of the existence of god.
That said, in principle of course there's nothing wrong with that - conditional results are (or at least can be) perfectly interesting. But the conditional nature of the argument has to be acknowledged at the outset. Note that this would all be much clearer, if one is unfamiliar with modal logic, if the argument were stated in clear natural language instead of symbolically; whether intentionally or not, unnecessary use of formalism does often (in my experience anyways) pose a "barrier to objection" for audiences unfamiliar with it.
Here's a basic way of interpreting the semantic meaning of modal logic symbols. Say we have a set of propositions about the world that can be true or false, and a set of possible worlds that are each defined in terms of which of the propositions they label true and which they label false. Also assume that when we just assert a proposition without the modal symbols □ or ◇, that proposition is being asserted in one specific member of the set of worlds which we consider to be "our world". For example, the proposition U = "Unicorns exist" would be false in our world, but it could be true in other possible worlds. Then if we put ◇ in front of a proposition P we are asserting that there's at least one possible world where P is true, and if we put □ in front or a proposition P we are asserting that P is true in every possible world including ours.
So, let G = "God exists". Then asserting the proposition G would just be asserting that "God exists" is true in our world, while asserting □G would be asserting that "God exists" is true in every possible world. So G → □G would be asserting something like "if God exists in our world, then God exists in every possible world".
This translation might be a little misleading since the "→" symbol is the material conditional which differs in some ways from if-then statements in ordinary language, or what philosophers call the indicative conditional. In logic the assertion "P → Q" is totally equivalent "¬P ∨ Q", i.e the statement "either P is false OR Q is true". So it might make things a little clearer conceptually to turn "G → □G" into the equivalent statement "¬G ∨ □G", i.e. "Either God does not exist in our world, OR God exists in every possible world". And then proposition 1, □(G → □G), can likewise be turned into the equivalent statement □(¬G ∨ □G), which is just saying that "¬G ∨ □G" would be true if asserted in any possible world. In other words, "In every possible world, it's either true that God does not exist in that world, OR it's true that God exists in every possible world".
I think an advocate of the ontological argument would say this follows from the very notion of what "God" means (or at least their notion of what it means), which conceptually is supposed to include the notion of existing necessarily rather than contingently. I'd be inclined to say "sure, if necessary existence is inherent to your concept of God, then I'll accept that "□(G → □G)" is true even though I don't think there is any such necessary being".
The problem, then, would be with the combination of proposition 1) and proposition 2), where 2) states that a God satisfying 1) "possibly exists". Keep in mind that the notion of "possible world" being assumed here doesn't just refer to epistemological possibility (where we aren't sure whether something is true or not, so it's subjectively 'possible' to us), but to some notion of logical or metaphysical possibility. To illustrate the difference, consider some mathematical conjecture that hasn't been proven yet, like the Golbach conjecture. Since we haven't found any counter-examples to the conjecture yet, in the subjective epistemological sense it might be true, but it also might be true that we will someday find a counter-example and therefore prove that it's false. And if that happens, we would say in retrospect that it's false in every possible world, since mathematical claims are supposed to be a matter of necessity that don't vary from one possible world to another. So if C="The Goldbach conjecture is true", we wouldn't be justified in asserting ◇C.
So I think there's the same issue with asserting ◇G, where we have already defined G to be a necessary being. It's not quite as straightforward since the notion of "necessity" here doesn't seem to be just logical or mathematical necessity, but something more like "metaphysical necessity". For another example of this concept, in the recent PhilPapers survey of philosophers, the final question asks about p-zombies--beings that are identical to ordinary human beings in both behavior and physical structure, but that are internally lacking in subjective experience--and a plurality of philosophers said that they think p-zombies are "conceivable" (unlike things that are logically self-contradictory in terms of the collection of properties they're defined to have, like square circles), but "not metaphysically possible". So probably most would believe that there are some metaphysical truths about the connection between behavior/structure and subjective experience which aren't derivable from logic alone, but are nevertheless a matter of necessity. In other words, if Z="there exists a p-zombie", then most of these philosophers would probably say that ◇Z is false, even though they think Z is conceivably true and isn't self-contradictory in the logical or mathematical sense.
With this sort of notion of metaphysical possibility/necessity in mind, it seems to me that if we weren't confident that G="God exists" was true as a matter of metaphysical necessity before seeing this proof, we shouldn't have reason to accept as sound the combination of premises 1) and 2). Premise 1) asserts that God is defined to be a necessary being (so if an entity satisfying the definition of God exists in any possible world, that entity must exist in every possible world), and premise 2) asserts that God does exist in at least one possible world. The existence of such a being may be conceptually possible, just as the truth of Goldbach's conjecture is conceptually possible, but that is no reason to accept the definite claim that there is a logically and metaphysically possible world where this is true.
In Anselm's original ontological argument, Gaunilo also raised the objection that an argument with the same structure could be used to try to prove the existence of anything with the property of "perfection", not just a "perfect being"--Gaunilo used the example of a "perfect island" as a reductio ad absurdum. The same type of issue would seem to apply to Adam's version of the ontological argument--the structure of the argument doesn't depend on any aspect of the semantic meaning of "God" other than the idea that necessary existence is part of the definition. So we could have I="there is a necessarily-existing perfect island", then □(I → □I) would seem to follow directly from the definition, and then if we asserted that such an island does exist in at least one logically/metaphysically possible world, we could use the combination of these two claims to logically prove that such an island exists in every possible world including our own. So if a theist thinks that Adams' argument is convincing, you should ask them why they wouldn't accept Gaunilo's parody, in particular why they wouldn't accept ◇I given the above definition of I. (This paper discusses the responses that theists have given to Gaunilo's island parody, but the author argues that even if the responses are an adequate basis to rule out the island parody as unsound, they may not give a basis for ruling out another parody called the 'devil corollary' which posits a worst possible being).
Kant has a famous criticism against such ontological argument according to reference here
Immanuel Kant put forward an influential criticism of the ontological argument in his Critique of Pure Reason... Kant then proposes that the statement "God exists" must be analytic or synthetic—the predicate must be inside or outside of the subject, respectively. If the proposition is analytic, as the ontological argument takes it to be, then the statement would be true only because of the meaning given to the words. Kant claims that this is merely a tautology and cannot say anything about reality. However, if the statement is synthetic, the ontological argument does not work, as the existence of God is not contained within the definition of God (and, as such, evidence for God would need to be found).
So your friend's proof above is only analytic a priori tautology at best, it has nothing to do with God's existence in the actual world which needs synthetic a posteriori statements. Your friend's created simple deductive system does depend on your first 2 assumptions (1st is your definition of what you want to prove its existence and 2nd is an assumed true proposition not everyone will agree perhaps) in addition to the usual normal modal system (K+B), and the result is correct following K's inference rules. But keep in mind that your friend's conclusion is just a logical entailment of those 2 assumptions in addition to system (K+B).
By the way, the above definition 1 seems reasonable, it does capture some essential aspect of our ideal concept of god following Leibniz's famous definition of universal necessary truths. But the 2nd assumed proposition sounds much weaker and unconvincing since in alethic modal logic we all agree □G → ◇G in D (serial system), then you don't even need all later convoluted steps including Brouwer's axiom, you only need principle of sufficient reason you can quickly arrive at □G which your referenced blog also claims to be able to arrive at after further derivation. Intuitively, if a thing is so necessarily demanded to exist by definition, then any possible positive verification or confirmation of its existence unsurprisingly abductively hints that it must necessarily exist first. In a word, we simply circularly defined an eagerly demanded concept at every possible world...
Finally please note even in minimal system K we have □G → □(G' → G) as a true proposition which can be proved (* see below), so by the blog author's conclusion even we arrive at □G by adding Reflexivity axiom M, then there implies another G' causing G in every PW, meaning such defined and existence-proved G still falls short of the common expectation of first cause...
*: below is a simple derivation of the claimed proposition in simple system K for those interested:
