Wei Dai wrote:
>According to possible world semantics, "it's necessary that P" means that
>P is true in all worlds accessible from this one. Different modal logics
>correspond to different restrictions on the accessibility relation. Before
>the invention of possible world semantics, people argued about which modal
>logic is the correct one, but now philosophers realize that different
>notions of accessibility (and the corresponding notions of modality) are
>useful at different times, so there is no single correct modal logic.
>That's my one paragraph summary of possible world semantics. Please
>correct me if I'm wrong, or read these articles if you're not familiar
>with this topic:
>My questions is, why not just quantify over the possible worlds and refer
>to the accessibility relation directly? This way you can talk about
>multiple accessibility relations simultaneously, and you don't have to
>introduce new logical symbols (i.e. the box and the diamond). Is
>modality just a syntactic shorthand now?
Each time you can reduce a theory in another you can considered it
as a syntactic shorthand. In fact you could just as well throw all
math in the basket keeping numbers, right at the start.
It reminds me early programmers saying that FORTRAN was just a toy
language for those stupid guy unable to manage binary code.
Of course your question is not *that* stupid, for sure, :-)
The first answer I would give is that Kripke Possible world semantics
just works for a portion of the possible modal logics. (Sometimes
called the classical normal modal logics). So, if modal logician
would have defined the modal logic by the accessibility relations,
they would have missed the whole forest.
Just in my thesis, among G, G*, S4Grz, Z, X, Z*, X*, Z1, Z1*, X1, X1*,
only G and S4Grz have Kripke semantics. (Z, X, Z1, X1 have Scott-
Montague semantics, the others ... are more difficult...).
Note that in first order logic, the quantifier "For all" and "it exists"
are sort of modal connector and are used in your sense: the variable "x"
denoting a sort of abtract "world").
But even for modal logic with possible world semantics, it is
important (for a logician) to distinguish 0-order and first-order
complexity, and this in a a priori, non semantical way.
Also first order modal logic, would be syntactically awkward if
everything was done by quantifying on the worlds.
Last answer: if you take a simple modal logic like S4, that is:
AXIOMS: (p -> q) -> (p -> q)
p -> p
p -> p
RULES: p p->q p
You can define the accessibility relation in a first order formula.
The accessibility relation, indeed, is just a transtive and reflexive
relation, making the frame of world a partially ordered set (the
model of intutionnistic propositional calculus).
But take the famous G "Lob formula": (p->p)->p, there is *no*
semantics for it describable by a first order formula. The frame is
an "inverse" of a well founded set. This means that to continue your
semantical use of modal logic in a synctatical well defined way, you should
use second order logic. Here, the fact that there is a simple modal
formula making all the heavy work for you is *very* nice. It really
simplify things a lot.
To sum up, my main answer is that
Kripke semantics has been invented to handle
better some--not all--modalities (invented by Aristotle!).
Modalities has not been invented for shortand description of Kripke
worlds. It is the other way round. In the real life (like in comp!)
Kripke semantics can only be used exceptionally.