Pat and Chris M., (01)
We usually agree on technical details, but we often interpret
their implications differently. But the following is a very
clear technical point: (02)
JFS>> So Kripke's semantics is a *proper subset* of Dunn's semantics. (03)
PH> Wrong as stated, since Dunn's semantics has no constructions
> corresponding to Kripkean worlds. (04)
CM> It seems that one should be able to convert any Kripke model
> into a Dunn model but, off the top of my head, it's not clear to
> me that one can do so *uniquely*. (05)
There is an isomorphism from a Kripke model to a Dunn model: (06)
1. Given a Kripke model (K,R,Phi) and for each world w in K,
let M (a Hintikkastyle model set) be the set of propositions
true in w. Call M the facts of w. (07)
2. Let L be the set of propositions that are necessarily true
in w. Call L the laws of w. (08)
3. Theorem: If the accessibility relation R is true of any pair
of worlds R(w1,w2) then the laws L1 of world w1 are a subset
of the facts M2 of world w2. (09)
This is a unique mapping in which every axiom, definition, and
proof that is true in Kripke semantics is also true in Dunn's
semantics. Just identify each Kripke w with a Dunn pair (M,L).
By the way, this mapping holds for Kripke's "normal" modal logics,
and for "nonnormal" logics such as deontic logic, in which the
laws of a world w are not a subset of the facts of *the same* w. (010)
Pat claimed that Kripke's version is more "usable", but everything
that can be done with Kripke's version can be done with Dunn's
version. But if the two systems are isomorphic, the next question
is how I could claim that Dunn's version is a superset of Kripke's. (011)
CM> You don't get much more from Dunn except a very rarefied notion
> of "law". (012)
PH> And I have never seen any useful observation or insight arise
> from Dunn's work that was not already clear in the Kripke framework. (013)
My answer is that Dunn's version makes it possible to do things
that cannot be done with Kripke's: (014)
1. Unlike Kripke's "arbitrary" relation R, Dunn's version allows
R to be derived from the choice of laws and facts. (015)
2. Instead of being arbitrary, the choice can be made by principled
arguments about which statements are more "entrenched" than
others. For example, the ontology is usually considered more
fundamental than just an offhand observation or assertion. (016)
3. Pat made the claim that nobody in AI is using Dunn's semantics.
But I claim that the entire Description Logic community is using
Dunn's semantics, but they don't know it. For example, they
often say that DL's are a version of modal logic, but they don't
explain where that modal effect comes from. But with Dunn's
semantics, it's obvious: (017)
a) The TBox of definitions stated in some DL takes priority
over the ABox of simple assertions, since the ABox must
be consistent with the TBox. (018)
b) That means the TBox contains laws, and the ABox contains
the ordinary facts: a classic example of Dunn's semantics. (019)
PH> So, apply this 'insight' to temporal descriptions. Possible worlds
> are times, here, and the accessibility relation is the timeordering
> relation. What "laws" vary from time to time, and how would someone
> reconstruct the timeordering (pastpresentfuture) from how these
> "laws" change? And even if this can be done, what advantages does
> all this give over using good old, you know, *times*, things like
> [4pm on Friday 12 September 200 (020)
To answer the last question first, an explicit time coordinate is
very useful, and the choice of using it is independent of whether
you choose a Kripke or a Dunn model. (021)
Although temporal logic with the operators Always and Sometimes
is very similar to a modal logic of Necessary and Possible, the
addition of a temporal Next operator forces an another constraint
on accessibility. But in some temporal theories, everything that
has happened is considered to be necessarily true for the future.
If you choose that version, then all the facts of the past (with
their time stamps) become laws for all future times. That causes
Dunn's accessibility relation to give you the usual temporal order. (022)
But a very important application is to the semantics of a database
(or a knowledge base that includes instances as well as an ontology
of types). For the moment, consider an ordinary relational DB: (023)
1. The tuples in all the DB tables constitute the groundlevel
facts that describe a possible world. (024)
2. The DB constraints, which are checked at each update, are
the laws L. (025)
3. The deductive closure of the groundlevel facts and the
constraints constitute the complete set of facts M. (026)
4. The accessibility relation R is defined by the permissible
updates that are consistent with the constraints. (027)
If the DB constraints are fixed, then you get the modal logic S5.
But in most practical DB systems, the database administrator
often defines new tables with new constraints and add more
constraints on old tables. When the DB administrator adds a
new constraint C, it must be true for the current state of
the tables, and the DB system will ensure that it remains true
in all future updates. But it might not be possible "roll back"
the data to a previous state that could violate C. (028)
PH> Who are the 'so many of them' who use S5... (029)
It is common in many theoretical papers about agents. For example, (030)
"Nowadays, the term Dynamic Epistemic Logic... is used to refer
to formalisms that add a special class of actions  epistemic
actions  to the standard logic S5 for knowledge." (031)
From "MultiAgent systems" by W. van der Hoek & M. Wooldridge,
in _Handbook of Knowledge Representation_, Elsevier, Amsterdam,
2008, pp. 887929. (032)
In a system in which constraints can be changed (which is very
common for practical DB systems), the modal logic S5 is too strong,
and the appropriate logic is S4. (033)
JFS>> Kripke only developed his semantics for propositional modal logic. (034)
CM> Exsqueeze me?! I direct you to... (035)
I apologize. I was too hasty. (036)
PH> DunnSTYLE... rejects possible worlds as entities and
> reconceptualizes them in a metatheory of sentential relationships. (037)
Note the isomorphism above. As Chris M. said, the entities that
Kripke called worlds are arbitrary. Identifying each w with the
pair (M,L) derived above can hardly be called a "rejection".
It preserves every axiom and theorem of Kripke's, and it supports
additional options and features that Kripke doesn't support. (038)
PH> Whereas to insist on not referring to possible worlds... (039)
The phrase 'possible world' is a metaphor for arbitrary entities,
and neither Dunn nor I have any objection to it as a metaphor.
But the above examples show that the pair (M,L) corresponds to
some widely used collections of statements in AI and DB theory. (040)
PH> Its like (in fact, it is literally) saying that instead of
> using clock times we should instead refer to sets of propositions
> that are true at those times. (041)
More precisely, it is like using a temporal database that keeps
track of times *and* the data and constraints that are true at
those times. There is a profitable industry that does that. (042)
John (043)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontologforum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontologforum/
Unsubscribe: mailto:ontologforumleave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontologforum@xxxxxxxxxxxxxxxx (044)
