To all readers: This is going to be a long post. The middle section is a lengthy explanation of the semantics of modal logic, designed for consumption by anyone who wants a better understanding of it, even if you have no background in modal logic at all. But if you don’t care about the semantics of modal logic, you should just skip to the last section instead.
Ok, here comes the post.
[QUOTE=Liberal]
I see. Thanks for explaining that. I’m sorry for my social density.
[/QUOTE]
Hey, no problem. Occasional misinterpretation is just a fact of life.
[QUOTE=Liberal]
As I understand it, S5 is constructed with three axioms (and Barcan may be added): (1) K, (x -> y) -> (x -> y); (2) T, x -> x; and (3) 5, <>x -> <>x. I was not aware that any other form of S5 could be constructed. It’s true that this construct can be derived different ways. But all roads must come to the same place. If I’m misinformed, I’m open to instruction.
[/QUOTE]
Well, in short, all roads come to the same place for sentences without quantifiers (“for all” or “there exists”).
Specifically, if we restrict our attention to propositional logic (no “for all” or “there exists” quantifiers), then there is a unique system S5 and it is axiomatized as you say. However, once we start looking at first-order modal formulas (sentences that contain quantifiers as well as modal operators), there is more than one way to set it up and still be considered an S5 system. Some of these will prove the Barcan formula, etc., and some of these won’t. It may not matter so much for your MOP, since you seem to phrase it in such a way as that you don’t make any use of “for all” or “there exists” quantifiers (though, if you choose to adopt the approach I outlined before for making G = G definitionally true and thus not needing to take it as a premise, you will be bringing in those quantifiers, and the correctness of the approach will begin to depend on what particular way you handle them). It definitely matters for your argument concerning the validity of the necessary existence principle, which of course has to make use of existential quantification.
(Here starts the lengthy middle section)
It all basically comes down to this, much of which you already know, but but to spell it out in full will hopefully be useful for just explaining modal logic to everyone: a Kripke frame is a collection of what are known as possible worlds, along with some accessibility relation, saying which worlds can “see” which other worlds. At each world, some primitive facts are true, and some primitive facts are false, and the truth of more complex facts (e.g., A AND B) can be determined in the obvious way. A primitive fact can be true in one possible world and yet false in another. The particular rules of interest are the modal ones, dealing with A (which says A is necessarily true) and <>A (which says A is possibly true). The rules dealing with these are that A is true at the world W iff A is true at every world W can see, and that <>A is true at the world W iff A is true at some world that W can see. After we set this all up, the logically valid statements and acceptable rules of inference will be those which are guaranteed to work out at every world, no matter how the Kripke frame is set up.
(All of this I’m sure you already know, Liberal, but I’m hoping to educate the other posters about modal logic at the same time, so that they will better be able to take part in the discussion, and am also leading up to the points which you yourself seem unclear on; please don’t take any offense at my giving this explanation).
If we put different restrictions on how sight works, we get different systems of modal logic. With no restrictions, the system is called K. If we demand that every world be able to see itself (i.e., that accessibility is reflexive), the system is called T. If we further demand that W seeing X and X seeing Y implies that W sees Y (i.e., that accessibility is also transitive), we get the system S4. Finally, if we demand that W seeing X implies that X sees W (that accessibility is also symmetric), we get the system S5. We actually get the same collection of validities if we just demand that every world be able to see every other world, and basically do away with the accessibility relation altogether.
That hopefully brought everyone up to speed a bit, and was just a refresher for you, Liberal. Now, for the part that I think you may be unclear on.
The above was the end-all, be-all for the propositional aspect of modal logic, but it left unclear how to deal with the quantifiers. The basic idea for dealing with them is to add to the Kripke frame some “individuals” (things like God, the Eiffel Tower, my left hand, etc.), and have primitive facts at a possible world include relations between and properties of individuals (like “George Washington is Martha Washington’s husband” and “The Eiffel Tower is tall”). But there’s one major bit of trickiness here: how do we accommodate the intuition that some possible worlds don’t even have an Eiffel Tower, and thus shouldn’t be forced to assign a truth value to the primitive fact of its tallness, while other worlds would have to?
There are many different ways of dealing with this, and all of them are still considered S5 systems, as long as their “sight” rules are still just the S5 sight rules.
One way of dealing with this is to say that every world has to decide every primitive fact, no exceptions, and that the statement Ex(P(x)) is true at world W iff there is some individual z at all such that P(z) is true at world W. If we go with this set-up, the Barcan formula becomes logically valid, as does the necessary existence principle, and, basically, any individual that can be said to exist in one world will be said to exist in all worlds. This seemed to be the logic you were using, Liberal, with which my whole quibble started. It is particularly easy to give rules of inference for this logic, because not much care must be taken in terms of the quantifier rules, but it seems very unsuitable as a description of “the real world”, and what intuitively the modal operators and first-order quantifiers mean.
Another way of dealing with this, then, as outlined in the SEP article, is to say that each world still has to decide every primitive fact, no exceptions, but also associate with each world some particular subset of the individuals which are considered to exist in that world. A world still has to decide primitive facts about individuals who don’t exist in it, though. We will say that the statement Ex(P(x)) is true at world W iff there is some individual z such that P(z) is true at world W, AND such that z is part of the set associated with W. Now, the necessary existence principle is no longer logically valid (an individual can be associated with some worlds and not others, and thus exist in a world without having necessary existence across all worlds), nor is the Barcan formula, nor various other controversial propositions. This is Kripke’s quantified modal logic, and takes some more care to axiomatize, but is much more appealing as a description of reality.
There are many more ways of dealing with this, as well, some of which don’t require worlds to decide primitive facts about individuals not associated with them, and which thus require much more care to properly axiomatize, but seem even more appealing as descriptions of reality.
(Here ends the lengthy middle section)
Anyway… all that just arose from my taking exception to (what I perceived to be) your glibly considering the necessary existence principle an indisputable logical fact. But hopefully just spelling it all out was of some use.
[QUOTE=Liberal]
That’s fine. It is your prerogative to reject any premise, and I must respect your choice as I do The PC Apeman’s. I disagree, of course, and if you don’t mind a question now that our issues are settled, what do you think of G -> G when the definition is substituted for the term? We get G -> G, which is the base axiom for S4. Do you think it is unfair to make the substitution? If not, do you have a problem with the S4 axiom?
[/QUOTE]
I have truly no problem with S4, and am fully ready to accept G -> G, as S4 says I must. Furthermore, in fact, in the context of S4 alone, understanding the modal operators in an S4 sense, I would even be willing to grant both G -> G and <>G. But without the additional symmetry condition from S5, this would not be enough to derive G. And if I were told to understand the modal operators in an S5 sense, I would not be willing to grant both G -> G and <>G simultaneously (I might grant one or the other depending on what I was told to interpret G as).