Re: Proposed definition of "possible world"
Chris,
We are talking past one another because we haven't spelled out
the correspondences between the words I'm using and the words
you're using. Let me spell out the details:
1. The question of how "proof theory" gets into the semantics
can be interpreted in several ways. Instead of looking
at Dunn's semantics, you can look at Hintikka's models
for modality, which illustrate the same issues, but in a
simpler way. Instead of the undefined notion of "possible
world", Hintikka uses the notion of "model set", which is
a maximally consistent set of sentences. Once you have
that set, proof theory is not involved in any further
steps of the semantics. But proof theory does creep
into the specification of "maximally consistent".
2. If all your sentences are limited to pure FOL, you can
use the principles of soundness & completeness to relate
any specification in proof theoretic terms to an equivalent
one in model theoretic terms. Therefore, you could, in
principle, replace the term "maximally consistent" with
the model-theoretic term "maximally satisfiable".
3. Dunn's innovation is to add a new feature L to Hintikka's
model set M. Each possible world w has two parts (M,L).
M is a maximally consistent set (a Hintikka model set) of
sentences in FOL, and L is a subset of M, whose elements
are called "laws". For the purpose of the formalism, the
word "law" is just a synonym for "sentence in L". The
word "fact" can be used as a synonym for "sentence in M".
Any informal meanings of "law" or "fact" are irrelevant
to the formalism.
4. To define Kripke's accessibility relation R(w1,w2),
let world w1 be defined as (M1,L1) and w2 as (M2,L2).
Then R is defined by the following equivalence:
R(w1,w2) iff L1 is a subset of M2.
5. Given these equivalences, any Kripke model structure can be
mapped to a structure with every w replaced by a pair (M,L).
Everything that can be done with a Kripke model can be done
in exactly the same way after each w is replaced by a pair.
No "proof theoretic" notions enter into the formalism.
6. After this equivalence has been established, we can ask
new questions about the pair (M,L) that could not be
discussed in terms of a single node w. Some of these
questions are informal (talky-talky kind of stuff a la
David Lewis) and others are formal (some model theoretic,
some proof theoretic, some computational, and some
miscellaneous -- human factors, teaching aids, etc.).
7. Some theorems that can be proved from the formalism are
that necessarily p in a world (M,L) is equivalent to
provability from L, and that possibly p is equivalent to
consistency with L. These are metalevel theorems that
result from the model theory. They provide an additional
way of characterizing modality that is not available in
a model theory that can talk only about a single node w
for each possible world.
8. Informally, the pair (M,L) allows us to translate a
statement that some property p is "essential" iff it is
true in all possible worlds into a more explicit form:
A property p is essential to an entity x of type t in
a world (M,L) iff the laws L imply that every entity
of type t have property p. We can then go further and
ask for the minimal subset of L that implies property p.
9. Computationally, we can relate the pair (M,L) to various
sets of statements in databases and knowledge bases.
For a relational DB, L corresponds to the set of DB
constraints, and M corresponds to the deductive closure
of L and the contents of the current DB. Similar
equivalences are possible with various implemented KBs.
Some comments on your comments:
>... Also, John, surely you are aware that the
>textbook definition of "tautology" is *semantic*: a tautology is a
>sentence of propositional logic that is true under any assignment of
>truth values to its constituent sentence letters.
That is one definition. But the word "tautology" is much
older than model theory. Since I use a version of proof theory
whose only axiom is the empty set, I prefer to define a
tautology as anything that is provable from the empty set.
For FOL, the two definitions are equivalent.
>... Most notably, intuitively once again, necessity doesn't
>have a thing to do with formal languages or systems. You are proposing
>to connect them intimately. Far be it from me to claim that this won't
>be useful in certain circumstances. But it would be shortsighted, to
>say the least, to pretend that it will always provide an appropriate
>understanding of necessity and possibility.
If you say "intuitively", we are on very shaky grounds
because "chacun a son gout". That is why I was proposing
to replace one formal notion (possible world) with another
formal notion (pair of propositions) which can be given a
much clearer informal interpretation. I don't pretend to
capture anybody's full intuitions (certainly not David L's,
Nicola's, or yours) with the pair (M,L). What I claim,
however, is that replacing w with (M,L) gives us a better
way of defining the little box []p. And I support "better"
with lots of examples -- formal, informal, and computational.
>> And what elements of the object language are you talking about
>> that lack any "notion of interpretation"?
>
>Constants and predicates, for example, at least as far as I could see.
Take your pick. Dunn's version applies to exactly the same
constants and predicates as Kripke's or Hintikka's, namely
whatever you want to specify.
>Well, you could formalize his "definition" by formalizing the more basic
>notions of a spatio-temporal relation and his underlying mereology. As
>I recall, a world w is just an object such that any object that bears
>any spatio-temporal relation to w is part of w. Not that I think this
>is a happy notion of a world.
That is precisely my point. Every formalization that goes
into any detail at all ends up with a set of axioms that
correspond to the L of Dunn's pair (M,L). All I'm saying
is that we should state that principle up front so that we
can explicitly talk about what is in L. That can be a
pretheoretic discussion among the KB and DB designers,
or it can be a metalevel addition to the user's language.
>> Then Dov Gabbay suggested the "innovation" of replacing "possible
>> world" with "theory" -- which I heartily applaud.
>
>Do you have a proof that Gabbay's innovation is equivalent to Dunn's
>semantics?
Gabbay's "innovation" was to define a possible world as a
"theory". As far as I can tell from his paper, his "theory"
is the deductive closure of a set of axioms, which can be
interpreted as the axioms L and closure M of Dunn's (M,L).
The reason why I mentioned Gabbay is that you mentioned him
as an example of someone who was using the notion of possible
world. I just wanted to point out that his "innovation"
sounds like a subset of what Dunn did in 1973. (Gabbay did
not show the equivalence of his theories to Kripke's model
structures in as much detail as Dunn.)
John