[Top] [All Lists]

Re: [ontolog-forum] Is modal logic first-order?

To: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Mon, 26 Feb 2007 10:19:03 -0500
Message-id: <45E2FA67.1000707@xxxxxxxxxxx>
Chris, Michael, and Till,    (01)

I was trying to make several independent points, which I
might not have distinguished with sufficient clarity:    (02)

  1. Dunn's semantics and Kripke's semantics are isomorphic.
     The basic difference is the choice of primitives:  the
     accessibility relation or the sets of laws and facts.
     Therefore, every axiomatization and model that has been
     used with Kripke's semantics can be adapted to Dunn's
     semantics in a logically equivalent way.  (See below.)    (03)

  2. But by combining Dunn's semantics with a hierarchy of
     first-oder metalevels, it is possible to formalize a
     version of modal logic that treats modality as a kind
     of metalevel reasoning about the choice of laws and
     facts -- or to use different terminology -- the choice
     of levels of entrenchment.    (04)

  3. I grant that this approach to modality is different
     from the kinds of modal systems that have been explored
     in terms of Kripke semantics.  But it is significant
     for both theoretical and practical reasons, especially
     for multimodal reasoning.  (See my papers.)    (05)

  4. The connection with levels of entrenchment also makes
     it possible to combine techniques of belief revision
     with multimodal reasoning.  This combination is very
     important for reasoning with and about distributed
     agents.  Dunn's semantics combined with metalevels
     can support it, but Kripke's semantics cannot (at
     least not without some major readjustments).    (06)

  5. As I said in another thread, probabilistic reasoning
     and nonmonotonic reasoning have important connections
     with a partial ordering of propositions by levels of
     entrenchment.  That is another field with significant
     applications.  No study of this field has been done
     with Kripke's semantics, but it's possible with Dunn's.    (07)

MG> Furthermore, this modal logic [G] is not first-order
 > definable (since the additional axiom requires that the
 > accessibility is well-founded).    (08)

That's fine, if you're concerned about non-well-founded
sets.  I'm concerned about the fact that Kripke semantics
has been around for over 40 years, and there is no decent
system for reasoning with and about multiple interacting
agents.  People are still publishing papers that only
permit one agent to act at a time because their formalisms
can't handle more than one actor at any step.    (09)

CM> I am quite certain that your claim about the number
 > of papers published about S5 is not even close to true,
 > given vast literature on provability logics, temporal
 > logics, logics of belief, and many other applications
 > of modal logic where S5 is inappropriate.    (010)

Yes, I was reacting to the significant number of papers
that try to apply S5 to databases and ontologies.   The
database field, in particular, has practitioners who
have inflicted many short-sighted disasters on us and
theoreticians who publish papers that are irrelevant
to anything that could ever be used in practice.    (011)

CM> Yes, of course, because S5 is meant to reflect a
 > context where "law" means something like "logical
 > necessity".  It's perfectly appropriate for laws in
 > that sense to be constant across all possible worlds.    (012)

Unfortunately, S5 has been applied in fields where the
"laws" are domain-dependent constraints -- and that
makes the applications impossible to generalize.    (013)

CM> Which, if true, simply goes to show that S5 is not
 > the right modal logic for modeling DBs.    (014)

Or knowledge bases, or ontologies, or....  What
applications can S5 support other than publishing
papers in the Journal of Tenure and Promotion?    (015)

_________________________________________________________    (016)

Demonstration that Dunn's semantics is isomorphic to Kripke's:    (017)

  1. Starting with a Kripke model structure (W,R,Phi),
     define a pair (Mi,Li) for each world wi in W such that    (018)

        Mi = {p | p is a true proposition in wi}    (019)

        Li = {p | p is a necessary proposition in wi}    (020)

     Call Mi the _facts_ and Li the _laws_ of world wi.    (021)

  2. Starting with a Dunn structure of pairs,    (022)

        Define each world wi to be the pair (Mi,Li).    (023)

        Define the accessibility relation R by    (024)

           R(wi,wj) = Li is a subset of Mj    (025)

           (i.e., the laws of wi remain true in wj).    (026)

        Define Phi(p,wi) = True iff p is in Mi.    (027)

These definitions demonstrate a one-to-one mapping
between that preserves the accessibility relation
(and all the modal axioms systems that have been used).
In effect, each of Kripke's worlds is an undefined
element, and the accessibility relation is an undefined
primitive.  But Dunn's worlds are descriptions, and the
accessibility relation is derived from those descriptions.    (028)

For every database or knowledge-based system, programmers
are implementing sets of statements, not possible worlds.
In effect, they use Dunn's method, but pay lip service
to Kripke.    (029)

Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (030)

<Prev in Thread] Current Thread [Next in Thread>