Re: modal logic and possible worlds

From: Wei Dai <weidai.domain.name.hidden>
Date: Tue, 13 Aug 2002 10:29:52 -0700

On Tue, Aug 13, 2002 at 03:27:49PM +0200, Bruno Marchal wrote:
> 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.

Agreed. Thanks for the reminder. :)

> 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...).

Ok, got it.

> 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").

I guess, but I'm not sure what would be the point of thinking about first
order logic that way in general.

> 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.

Ok. I'd be interested in seeing an example of this syntactic awkwardness
if you have time.

> 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
> --------, ---
> 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).

Does it mean anything that S4 and intuitionistic propositional calculus (=
0-order intutionistic logic, right?) have the same kind of models, or is
it just a coincidence? I guess Tim is saying that it does mean something,
but I don't understand what.

Anything you can say using the language of S4, you can say in first order
classical logic by quantifying over possible worlds. Does that mean
anything you can say in the language of intuitionistic propositional
calculus, you can also say in first order classical logic?

> 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.

Thanks for your answers. They are very helpful.
Received on Tue Aug 13 2002 - 10:40:25 PDT