Then you’re simply bending definitions. If you eliminate ‘doesn’t have to’ then your “can” = “has to” = “must”.
Zwaldd
It isn’t eliminated. Eris gave you the building blocks with which to build any modal statement. You just have to think a bit. “Doesn’t have to”, for example, is rendered by ~.
That’s ridiculous. Everything about this proof has been defined to a fare-thee-well forty ways from Sunday with links to everything from logic primers to advanced essays, and by supporters and critics alike.
Exactly… which, of course, is equivalent to <>~
Of course. 
~ = ~~<>~ = <>~
In response to this from me
You wrote.
In the earlier part of this thread you claimed that you “worship” G. If G is NOT Christ you have become an idolater in the Christian view if I am not mistaken. And If G and Christ/Jehovah have nothing to do with each other then this whole exercise is pointless.
What I said was this:
“That’s about the gist of it. Personally, I don’t worship God just because He is ontologically perfect (which is what G means). I worship Him because He is morally perfect. Were this the only convincing evidence of His existence, I would hate Him.”
The MOP is about nothing but God’s ontological nature, which I’ve said many times as well. Certainly, Christ is ontologically perfect, but that does not mean that this proof is NECESSARILY about Christ. A cow, after all, is a bovine, but a bovine is not necessarily a cow.
I believe that Christ is God, but not because of this proof.
And honestly, if the proof was exlcuding <>~G, we’d be assuming:
~<>~G == G
which, of course, is not the assumption of the proof. <>G is.
My point above was that you cannot just abstract out god’s ontological nature and form an argument about that, calling it “G”, and then come back at the end and decide that this “G” is, in fact, the OM3I god of Christianity. Your subject, start to end, must be the same thing.
So Christ is simply one of a class of ontologically perfect beings? What about Allah? Shiva? Buddha? The Great Spirit of the plains indians? Do they make the cut? And if so we have some pretty unorthodox theology here.
But ~ is not a quality assigned to G (correct me if I’m wrong), so it doesn’t apply here.
The premise seems to change every few posts (at least in my mind), so let’s address them both at once:
If <>~G is not excluded, then G is not the greatest possible existence because there are already existences for which a greater existence, ~<>~, holds true.
If <>~G is excluded, then G has to be something we already know exists, which of course rules out anything supernatural, which is fine I suppose since we’re only concerned with existence (right Lib?).
The subject start to end of the proof IS the same thing. It’s the ontological nature of the supreme being. I can talk about a room in my house in terms of its dimensions, for example. I can make a blueprint of it and talk about it in terms of what’s in the blueprint. That doesn’t mean that in some other context, I can’t talk about it in terms of, say, how it’s furnished, how its colors are coordinated, how it makes me feel, how it was conceived, and so on. God’s existence is not His only property, but it is the only property that is appropriate for an ontological argument to adress.
Well, this is way off-topic, but my belief is that Christ is love. God is love. And in general, all who love are God. I define goodness as the aesthetic most valued by God. I define sin as the obstruction of goodness. Love is the means by which goodness is shared. Sin is the opposite of love. Truth is the lens through which goodness is seen.
Apply to what?
The premises have never changed. They are:
~~G (which is the same as <>G)
G -> G
G -> G
I don’t know what you mean about exclusions. There is an infinite number of premises that are excluded. But that is true of every proof of anything.
Is <>~G true or false a priori?
I don’t buy it. G is “something which necessarily exists”. It is not an “ontological nature” but an entity itself. That entity is god. In my first post in the original thread I made clear that I do not think OM3I is a coherent concept. If you talk about a room in your house you are discussing something which is a coherent concept. If we later find out that the room in your house is something that you imagine to have contradictoy properties, say we find that you believe that the room exists (simultaneously) entirely in a parallel universe as well as this one, we are justified in questioning whether the “room” in the original discussion is that same as what you now call a “room”.
I don’t think it’s off topic at all. You want to use the MOA to prove your view of God then I am justified in asking what the MOA actually applies to and what the criteria are for applying the MOA to a specific supernatural entity or entities.
Well, the truth of propositions in modal logic is already at a world, so I think you can drop “in the actual world” and let G be “the greatest possible being exists”. That’s fine, but the only way you can compel adoption of (G -> G) is by defining “greatest possible” as “existing in all possible worlds”. And then we’re left with
G = “there is a being that exists in all possible worlds”
Right?
I never said anything was being circumvented. I said: “your proof is not valid”. That is:
(G -> G) -> <>G -> G
is not a theorem of S5. It isn’t, and I’ve proven it. I’ve given you the proof over and over again, for almost two years now. Here it is again:
Two worlds, world 0 and world 1. G is false in world 0 and true in world 1.
Now, is G -> G true in world 0? Yes, because G is false. Is <>G true in world 0? Yes, because G is true in world 1. Is G true in world 0? No, because G is not true in world 0.
I’m trying to help you by pointing out why and how your proof is not valid. You might reasonably ask which step in the proof is invalid. Your application of modal modus tollens is not valid, unless you change G -> G to (G -> G). It’s not even a big step; in fact, when you write prose, I hear you saying (G -> G), but you just don’t render it into symbols correctly.
(G -> G) -> <>G -> G
is a theorem of S5.
By the way, I don’t know what you mean “All modal rules of inference and formulas are based on the implication of the RN”. First, I think you must mean rules of inference and axioms. But they aren’t “based on” RN, they can be the subject of an application of RN. And you can’t apply RN here anyway, because G -> G is one of your premises.
Even your insults are illogical 
Here’s a countermodel: I have just now (in the past month, I guess) stumbled (whell, I didn’t stumble, but who cares?) upon a particular paper that was submitted for publication in February 2004. However, it is not the case that I have just now started studying computer science or modal logic.
I have been studying computer science and logic for over 10 years, my Ph.D. in CS with a minor in logic is ABD, and I am professionally employed with the job title of “Research Scientist” and am currently the principal investigator of three U.S. Government sponsored research projects in computer science. I’m not trying to argue from authority; merely convince you that you don’t need to tutor me in logic.
I know how to make an implication into a strict implication; I’m telling you that you have to do it to G -> G. If you don’t want to write (G -> G), we can introduce a new connective and write G => G. But you need to do that to make the argument valid.
See, that’s what I don’t understand. “If Al Gore had been elected, then he would have necessarily been impeached due to a sex scandal in his first year in office”. That statement is certainly true in this world (Gore was not elected). However, if we determined that there was no possible world where Gore had been impeached due to a sex scandal, we would not be justified in concluding that he had not possibly been elected.
I should only get credit for bringing it to your attention, not for the idea.
Pfenning et. al. don’t include negation in their system, but it can be added. The computational interpretation of negation is interesting. We make use of the definition of negation in terms of implication and falsum to define:
~A == A -> 0
Where 0 is the empty type (a type with no values, not a type with a single value. This is not C’s void type, it is the return type of a function that never returns, like exit() in C). Replacing the <>G with <>~G allows me to build a term with type:
(G -> G) -> <>(G -> 0) -> (G -> 0)
What it does is takes mobile code for a function that turns a G into mobile code for a G, and a reference to a remote function taking a G and never returning, and produces a function taking a G and never returning.
I’m too tired now to write down the implementation, but you can imagine how it works. The resulting function of type G -> 0 is implemented by taking an argument of type G, turning it into mobile code, sending it to the site of the remote G -> 0 function, and then invoking it.
You can also make use of <>~G = ~G to write a term with a simpler implementation of type
(G -> G) -> (G -> 0) -> (G -> 0)
And what it does is take that same first mobile code to turn a G into mobile code for a G, and a function taking mobile code for G and never returning. It produces a function of type G -> 0 that takes it’s argument, turns it into mobile code, and then passes it to the G -> 0 function.
Actually, you don’t need G -> G. You don’t even need a reflexive accessibility relation. The proof is valid with the following three premises:
(G -> G)
<>G
a symmetric accessibility relation
If you want to reject the conclusion, you should reject at least one of these premises.
Now, Newton, you know or should know that I meant no insult. I greatly respect not just your intellectual prowess and credentials, but your eminently civil manner in expressing them. Sometimes, I have a lot of time to spend and sometimes I don’t. Much civility is often lost in writing pithily. Nor do I resent you stating your credentials since I have, from time to time, stated those of Plantinga, Godel, Hartshorne, Suber, Tisthammer, et al. In this matter, expertise is an important consideration and appeal to it is not a rhetorical vice.
From the very first time you raised your objection to G -> G, I’ve searched the literature for a similar argument and have never found it. I don’t mean to pit a dozen PhDs against one, but given how modal logic was developed in the first place along with the nearly fifty years of this controversy, you must give me that the absence of your particular criticism is conspicuous. Naturally, that doesn’t mean that you’re wrong (in fact, you’re right). But it certainly calls into question why even a critic so severe as Suber has never pointed out what you’re pointing out here. And the reason is that it simply is not relevant. (Please, hear me out.)
Your criticism would apply were the proof in S4. But the whole point of drawing the tableau in S5 is that <>A -> <>A and A -> <>A. In other words, for any string of modal symbols, the last symbol is equivalent to the whole string. So, if A is possibly necessary, then A is necessary. That gives us the Euclidean frame whose accessibility relation both you and I have already described. Although the M axiom, A -> A, is necessary for any system 4 and above, consider that you could form S5 without the 5 axiom simply by adding Brower to 4. As you know, that’s A -> <>A. Invoking 5 invokes both 4 and B.
Note that criticizing the premise, G -> G, because it is not an axiom in S5 is irrelevant. The premise is drawn, not from the rules of modality, but from the coherent definition of G. (It is not an axiom of S5, but merely an axiom of the proof. Just like ~~G.) If G exists in actuality, then it must be the case that G, existing necessarily if at all, exists necessarily. This premise would not apply to any other ontological commitment. That’s the important consideration. There is no other way to define G such that G -> G. Therefore, (G -> G) is not, well, necessary. There is no need whatsoever to make an epistemic commitment on G.
If that’s the case Libertarian, then the proof is simply a miserable tautology as Kant puts it. But I can’t see how you can allow <>~G (even if you say that <>G is more reasonable) if this is how you define the proof. It’s a bit disingenuous, IMO. If you allow <>~G, there can be no compelling reason to prefer <>G over <>~G or vice versa. Your reason that <>~G is a denial of a positive ontological proposition is not true.