Investigating Logical Arguments with somerby.net/mack/logic

I created a web application that evaluates logical arguments.  To provide an example of how it might be used, I'm going to use it to help me do a brief investigation of two modal arguments about the existence of God.  The first is Alvin Plantinga's modal argument for the existence of God.  The second is Juan Manuel Correa's counter-argument against the existence of God (or at least against the soundness of Plantinga's argument).  Statements of both arguments can be found on Wikipedia at http://en.wikipedia.org/wiki/Ontological_argument#Alvin_Plantinga.

First off, I'm going to strip the arguments down to what I think is the essential logic that makes both arguments work.  I don't suppose this will be agreeable to everyone, at least not without some persuasion, but I'll just go with it for now and try to defend myself later if I have to.  So, for Plantinga's argument I will use:

<>G->[]G
<>G
->
G

Which is saying,

• If God exists in some possible world, God exists in every possible world.
• There is a possible world in which God exists.
• Therefore, God exists.

For Correa's counterargument, I will use:

<>G->[]G
<>~G
->
~G

Which is saying,

• If God exists in some possible world, God exists in every possible world.
• There is a possible world in which God does not exist.
• Therefore, God does not exist.

 The web application, which, in this post, I will call "the decider", decides that both arguments are valid.  So what's going on?  There are three premises between the two arguments, and each seems plausible.  I suspect the fact that both arguments are valid in spite of their contradictory conclusions means that the three premises are logically inconsistent with each other.  So I try them out in the decider:

<>G->[]G
<>G
<>~G

It tells me they are impossible, i.e. logically inconsistent with each other.  So we can't believe all of them at once.  Which one should I doubt?

Before I try to answer that question, I want to check that neither argument is trivially valid.  I mean, I want to be sure that neither conclusion follows from its premises simply because those premises contain a contradiction and anything follows from a contradiction.  So I test the premises by themselves in the decider.

<>G->[]G
<>G

Then

<>G->[]G
<>~G

The decider says both pairs are contingent.  So no problem there.   What about the two differing premises?  The decider says

<>G & <>~G

is possible, which it just what I expect, so I could believe both.  Which is what I'm inclined to do.  I can imagine a world with God, and I can imagine a world without God.  Of course, just because I can imagine them doesn't mean that there is not some contradiction hiding in either conception.  But I'm still most inclined to drop Premise #1.  It's obvious that []G and <>~G are incompatible, and it's not clear to me that there ever could be such a thing as a necessary being.  Some logics entail that at least one being must exist; See Proposition 24.52 in Principia Mathematica for one.  Even so, just because you can prove that at least one object exists doesn't mean you can prove that it has any nontrivial properties, like divinity.  And I'm not enamoured of the idea that God has every possible perfection; necessary being being one of those perfections.  Clearly, if a being has every possible perfection, it must smell like freshly-baked chocolate chip cookies at least some of the time.  And play a face-melting guitar solo every time it picks up a guitar.  Unless someone is taking a nap within earshot.  But I'm a Christian, and I'm sure both of these perfections are irrelevant to the Gospel, so I don't care.

So, to conclude, I will assert 1. that God exists in some possible world.  2. There is a possible world where God doesn't exist.  Therefore, Premise #1 is false.  

To summarize my reasoning in symbolic form:

<>G
<>~G
[]( (<>G&P) ->  C )
[]( (<>~G&P) -> ~C )
->
~P

Where  P is premise #1, C is the conclusion of  Plantinga's argument, and G is as defined above.

The decider confirms that this argument is valid.

One more thing I'd like to point out: when considering modal arguments for the existence of God, one should be careful about the statement "It is possible that God exists."  It might be interpreted two different ways.  First, as "there is a possible world in which God exists".  The second, as "I don't know anything that precludes the existence of God."  The first is easy to represent in terms of modal logic, but the second is the more natural interpretation.  In my analysis, I assumed the first.  If I were to choose the second interpretation, my analysis of these two arguments would have to be different.