George Levy wrote:
>
>So far so good....
:-)
>sorry with the delay....
*I*'m sorry for the delay, and the forthcoming delays (!).
>let's move ahead...
OK.
>just a
>question:
I will first answer your question and then proceed.
>
>>>A realist world is one with access to at least one terminal
>>>world. w---->w1 --|
>
>
>>You mean a realist frame, I guess.
>
>A frame is a set of world. Therefore, I would expect a frame to be in a
>different
>classification level than a world. Hence a connection from a frame to
>world may
>not be appropriate. How about talking about connection from any world
>within a
>frame to a world. So the above statement would become:
>
>"Any world belonging to a realist frame is a world with access to at least
>one
>terminal world."
That is correct.
Let us sum up.
A Kripke frame (W, R) is just a set W with a binary relation R.
A Kripke model (W,R,V) is a Kripke frame with a function V which
attribute a truth value (among {TRUE FALSE}) to each atomic
proposition at each world.
The frame (W,R) respects A iff A is true in all worlds of
all models based on the frame (W,R)
iff is put for *if and only if*
Another way to put that: is to first define a notion of satisfaction
by a model:
(W,R,V) satisfies A iff A is true in all worlds of W.
The "meaning" of A is true in a world is of course given by V.
It is important to see clearly the three semantical level in
Kripke semantics:
Truth of A in a world (given by V and Kripke semantics)
Satisfaction of A in a model (truth in all worlds of the model)
Respect by a frame (satisfaction by all models based on the
frame).
And now the results are ... but I realize I have forget to give
you the name of the formula. These names are more or less standart
and historical. Although Naming Theory is a speciality in modal
logic, the names are bad and unpedagogical! (Now a worth pedagogy
would consist in changing the names, because then you will be lost
in the literature!).
K (for Kripke) is the standart name of [](p->q) -> []p->[]q
T is the name for []p -> p
4 is the name of []p -> [][]p (4th formula in Lewis System)
5 is the name of <>p -> []<>p (5th formula in Lewis System)
D is the name of []p -> <>p (D for deontic)
B is the name of p -> []<>p (B for Brouwer, but Brouwer has almost
nothing to do with it.
You recognize LASE !)
C is the name <>p -> -[]<>p (C for consistency or consciousness!).
(You recognize FTMP !)
Other important formula will appear in the drama which will evolved):
L is the name of []([]p -> p) -> []p (L is for Loeb).
In some sense L is the most important formula we will meet. You should
try to show that all the frames respect L->C (This *is* obvious once
you are familiar with the definitions, and basic classical propositional
calculus, you can use the fact that p->q is equivalent with -q -> -p).
Grz, which will play only some indirect role. That's a good thing
because Grz is not so obvious:
Grz is the name of []([](p-[]>p)->p)->p (Grz is for Grzegorczyk,
an important polish mathematician).
And we have as results (including the exercices!):
Any frame (W,R) respects K
A frame (W,R) respects T iff R is reflexive
A frame (W,R) respects 4 iff R is transitive
A frame (W,R) respects 5 iff R is euclidian
(where R is Euclidian means that if xRy and xRz then yRz,
for x, y z in W).
A frame (W,R) respects D iff (W,R) is ideal
A frame (W,R) respects C iff (W,R) is realist.
We will talk on the semantics of L and Grz later.
Remark: 1) A frequent "beginner error" is to believe that if
T, for exemple, is true in all worlds of a model, then the model
is reflexive. This is false, and you should be able to draw a
little non reflexive model M in which T is true in all worlds.
What the theorem says is only that if T is true in all worlds of
a frame, whatever V is; that is whatever the model is, then the
frame must be reflexive. You should see that if you change the
truth value (V) in your little model you can falsify T at some
world.
2) Don't confuse the formula T and the truth value TRUE.
In most book TRUE is written T.
Well. Now, with these result the right (semantical) brain can
be happy. But remember that logician want theories.
Here are some important theories, and because they play some role,
and we will meet them again it will be useful I tell you their
(still rather stupid) name.
Recall that a (formal) theory is the giving of axioms (formula)
and inference rule (to derive syntactly new formulas called
theorems).
The rules of inference are MP and NEC. This gives the so-called
normal modal logics. Unfortunately we will meet some non normal
modal logics too.
We make the "abus de langage" by accepting that some systems
have the same name that its principal formula.
Here are the definitions:
K is K (MP, NEC)
T is KT (MP, NEC)
S4 is KT4 (MP, NEC)
S5 is KT5 (MP, NEC)
B is KTB (MP, NEC)
D is KD (MP, NEC)
C is KC (MP, NEC)
G is KL (MP, NEC)
When I write B is KTB (MP, NEC), I really mean that B
is the formal logical system having as axioms the classical
tautologies (or just the three Hilbert Ackerman axioms)
+ the formulas K, T, B and which has as rules of inference the
modus ponens and necessitation.
Now, I give you two exercices:
1) Not really difficult:
We know that the formula K is respected in all frames. Show that
the system K is sound with respect to all frames. That means that
not only K is respected by all frames, but that anything you can
prove (syntactly) in the logic K will be respected in all frames.
Similarly, show that the system KTB is sound for the class of
reflexive and symmetric frames. Enunciate the equivalent
soundness theorem for all the systems above.
2) Really difficult (easy when you will know the technic to prove
that; the important point is that you realise it is not obvious).
The converse is true. Any formula which is respected in all
reflexive and symmetric frames is provable in the system B.
Enunciate the other "completeness" theorem for the system above.
All are true.
I must go now. We have quasi-finished the introduction to
Kripke semantics.
A+ Bruno
Received on Wed Apr 25 2001 - 04:32:29 PDT
This archive was generated by hypermail 2.3.0
: Fri Feb 16 2018 - 13:20:07 PST