Re: Proposed definition of "possible world"
On Sat, Aug 05, 2000 at 12:28:28PM -0500, John F. Sowa wrote:
> ...
> 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.
Simpler is good!
> 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".
This is inaccurate on several counts, John. First, no proof theoretic
notions are used in the definition of a model set at all. A model set
is any set of formulas satisfying certain syntactically specified
closure conditions, e.g., if p&q is in the set, so are both p and q.
There is also what can intuitively be called a consistency condition
C(~), viz., if p is atomic and in the set, then ~p isn't in it, but
again this is not proof theoretic; there are no rules of inference or
other finite processes involved. (Note also that model sets needn't be
maximal; indeed the empty set is a model set.) Satisfiability for a set
of formulas is defined in terms of its (not necessarily recursive)
embeddability into a model set. For a modal language, Hintikka
generalizes to systems of model sets (intuitively, "partial"
descriptions of possible worlds) and adds relevant closure conditions
for the modal operators; satisfiability is similarly generalized.
Again, no proof theory. And it is critical that there is no proof
theory so that one can have some sort of completeness theorem, as
completeness theorems are designed precisely to show that the
conceptually independent and distinct notions of model theory and proof
theory are extensionally equivalent -- as you know.
Proof theory enters Hintikka's picture in the form of a *procedure* for
demonstrating satisfiability (compare semantic tableaux.) Indeed, one
can map any proof of a formula A in a more standard deductive system of
modal logic to a demonstration that any attempt to embed ~A into a
system of model sets is bound to fail (i.e., the condition C(~) is
always violated). Completeness then amounts to showing that any
unsatisfiable set of formulas (i.e., any set that is not embeddable into
a system of model sets) is *demonstrably* unsatisfiable in this fashion
(i.e., "proof theoretically" inconsistent). In order to have anything
interesting to prove, proof theoretic and model theoretic notions must
be kept distinct.
> 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".
Only *after* one has a completeness theorem.
> 3. Dunn's innovation is to add a new feature L to Hintikka's
> model set M. 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.
Well, if he's using some notion of a model set similar to Hintikka's,
then I finally see what you mean. The problem was that your earlier
description, like your exposition of Hintikka above, used explicitly
proof theoretic notions in ways that appeared to muddy the distinction
between proof theory and model theory in the account.
> 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.
The one, as it happens, that everyone else uses.
> But the word "tautology" is much older than model theory.
So is the word "proof", but I wouldn't propose, in the context of
mathematical logic, to alter its current, universally accepted meaning.
It puzzles me why you would choose to use "tautology" in a manner that
is out of step with the rest of the logical community.
> 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.
Only extensionally, because we are fortunate enough to have soundness
and completeness theorems. You can't rely on similarly fortuitous states
of affairs in general. In other cases your distinctive usage will no
longer be innocuous.
-chris
--
Christopher Menzel # web: philebus.tamu.edu/~cmenzel
Philosophy, Texas A&M University # net: chris.menzel@tamu.edu
College Station, TX 77843-4237 # vox: (979) 845-8764