Re: Kripke semantics

From: Marchal <>
Date: Thu Apr 5 08:08:38 2001

George Levy wrote:

>My binder is getting fatter but I am catching up. Thank you for all this
>wonderful information...

You are welcome.

>I have a couple of questions:
>Could you please define belief and knowledge in terms of a machine's states
>or potential states...

I will define only believable and knowledgeable. It will not be done
directly in term of machine's state or potential states but in term of
provability (consistency) and truth. I will define it in some other

>Is there a relationship between belief, knowledge, consistency and

That is a key question. At some point a form of communicable belief and
communicable knowledge will be defined with the notion of provability
consistency and truth, indeed.
Accepting those definitions could depend on the acceptance of some modal
logical axioms for those concept.
I could have proceed in another way and start directly from the
provability concept bypassing all modal logics. But modal logic
will simplify greatly the reasoning and its translation in arithmetic.
And it helps also to illustrate classical logics.
Nevertheless the fundamental notion will be the godelian formal
provability notion *beweisbar*.

The pedagogical problem we will encounter here is that we must
explain how to translate *beweisbar* in formal aritmetic (which
BTW has not yet been defined) or in the language of the sound
machine (not yet defined too). This is easy but very long to do
in all details, and very tedious too: it looks a little like
defining higher concepts like addition, multiplication, sorting, in
some assembly languages. Perhaps I will, at that moment refer
you toward some books. One of the clearest exposition
is the one given by Godel himself in the original 1931 paper, which
has been published by Dover in 1992. It is cheap.
Using Church thesis it is also possible to bypasse that "assembly
programming" passage, but then some familiarity with theoretical
computer science is needed. Mmmh... We will see.
Let us try not to anticipate to much. But I aknowledge that some
time I should provide motivation, because if I don't, the list
will be completely sleepy when we will arrive to the interesting
matter (interesting with respect to the contemplation of the

>In the physical world, if I see a supernova, then all the worlds within the
>light cone of the supernova see it. Worlds outside the supernova's light
>cone do not.
>Accessibility could also be defined in terms of information flow in a social
>or economic environment. In a perfectly competitive market, perfect
>information must be available to all buyers and sellers. So for example, the
>(lowest) price P for a particular item is known to be X. .Let this be p
>defined as P=X. Then []p = p. When information flow is restricted, buyers
>and sellers may not have the same information, and therefore []p = p for a
>particular market segment but not for another.

Interesting remarks. You will discover numerous similar applications of
modal logic in the literature.

You get a good intuition but for the sake of precision and shortness I
will recall the definition of "The frame (W,R) respects a modal
sentence S", and state precisely some theorems, instead of commenting
precisely the rest of your post. But please continue to tell me
if you follow.

(W, R) respects S
       (where W is a set of "worlds", and R an "accessibility" relation)

means that

all model (W,R,V) satisfies S. Where V are valuations. V transforms
the frame into a model, that is V attributes truth values to the
atomic propositions p, q, r, ... inside each world.

I recall of course that a model (W,R,V) satisfies S if S is true
in all the worlds in W, when we take the valuation V.

iff = an abreviation of if and only if, or <=>

I don't recall Kripke semantics, except that []p is true in w, if
p is true in all worlds accessible from w.

I will say that a frame (W,R) is reflexive (resp. transitive, ...)
when R is reflexive (resp. transitive, ...). I will perhaps
do other "abus de langage" of this kind without mentionning.


1. (W,R) respects []p -> p iff (W,R) is reflexive,

2. (W,R) respects []p -> [][]p iff (W,R) is transitive,

3. (W,R) respects p -> []<>p iff (W,R) is symmetric,

4. All frames respect [](p->q) -> ([]p -> []q).

Let us prove 1. and 4. (I leave 2. and 3. as exercice)

Proof of 1.

Because of the "iff" we must prove two things.

we must prove a) if R is reflexive then (W,R) respects []p -> p,
and we must prove b) if (W,R) respects []p -> p then R is reflexive.

Let us prove a).
To prove that "if A then B", a traditional way consists in supposing
that we have A and not B, and showing that this leads to a
contradiction. (BTW you can verify that ((A & -B) -> FALSE) <-> (A->B))
is a tautology).
So, let us suppose that R is reflexive and that (W,R) does not
respect []p -> p.
To say that (W,R) does not respect []p -> p means that there is at
least one world w in which []p -> p is false. Remember that worlds
obeys classical logic, so that if []p -> p is false at w, it means
that []p is true at w and p is false at w (and -p is true at w).
But (by Kripke semantics) if []p is true at w, it means p is true
at every world accessible from w. But R is reflexive, so we have wRw.
So p and -p are true at w. But then w does not obey to classical logic.

Let us prove b), that is: if (W,R) respects []p -> p then R is
Suppose (W,R) respects []p -> p and that R is not reflexive.
And let us search a contradiction from that.
If R is not reflexive, it means that there is a world w in W such that
we don't have wRw. Let us build a model on that frame by defining
a valuation V such that V(p) = FALSE in w, and V(p) = TRUE on all
world accessible from w (if there is any()).
By Kripke semantics we have []p true in w. So now we have both
[]p and -p true at w. But we have suppose that (W,R) respects
[]p -> p, so []p -> p is true at w, so p is true at w (because []p
has been shown true at w, and w obeys classical logic). But then
again p and -p are true at w. Contradiction.

OK? For theorems 2. and 3. you should perhaps find the proofs
yourself. It is almost more easy to find the proof than to read
someone else proof. The only difficulty is in the case b) and
consists in finding the valuation which leads to the contradiction.
Hint: put V(p) = FALSE in w, and V(p) = TRUE on all
world accessible from w; or, for 3. put V(p) = TRUE in w, and
V(p) = FALSE on all world accessible from w.

() Hey! but what if w is a cul-de-sac or terminal world?
    Then []p, or even []False is always true in w. This follows
    easily from classical logic: []p is true at w because
    "(it exists x such that wRx) entails p true at x", this
    last sentence is true because wRx is always false for a
    terminal world, and "false implies whatever you want" is
    always true.
    Another way to swallow this tricky point is to remember
    that []p is -<>-p, but -<>(what you want) must be
    automatically true in a terminal world, by simple
    Kripke semantics for <>.
    Terminal world are are disquieting: everything is necessary
    and nothing is possible in a terminal world.

Proof of 4.
We want to show that [](p->q) -> ([]p -> []q) is respected in all
frames. This means [](p->q) -> ([]p -> []q) is true in all world
in all model in all frame!

It will be easier to show that the theorem holds for the equivalent
sentence ([](p->q) & []p) -> []q
Do you see the equivalence? It is just propositional logic:

     A -> (B -> C) <-> (A & B) -> C

Suppose now that ([](p->q) & []p) is true in some world w.
We must show []q is true in w.
If w is a terminal world then []q is automatically true as
we have seen above.
If w is not a terminal world, then there are worlds x, z, y ...
with wRx, wRz, wRy, ...
The fact that ([](p->q) & []p) is true at w entails that
both [](p->q) and []p are true at w. But this, by Kripke
semantics, entails that both (p->q) and p are true in
the accessible worlds x, z, y, ..., and so, q is true
in all those worlds (all world obeys classical logics and are
thus closed for modus ponens). But if q is true in all
accessible worlds from w, then, by Kripke again, []q must be
true in w.

                          * * *

In fact some other frames will play an important role, so let us
introduce them now. (The definition which follows are somehow
less standart).

I will say, by definition, that a world is transitory iff it is
not terminal.

A frame (W,R) will be said ideal if all worlds in W are transitory.
(there is simply no cul-de-sac worlds in an ideal frame).

A frame will be said realist if there is a terminal world accessible
from any transitory world of that frame.
(You can "die" at every world in a realist frame, as you are
"immortal" in an ideal frame).

The corresponding theorems (exercice) are

5. (W,R) respects []p -> <>p iff (W,R) is ideal,

6. (W,R) respects <>p -> -[]<>p iff (W,R) is realist,

Do you have recognize <>p -> -[]<>p ?
Yes. It is our modal form of Godel theorem (with TRUE instead of p).
More will be said.

I hope your binder will not explode.
My next post will anticipate toward the end of my proof to glimpse
the "quasi-appearance of Hilbert Space" when we explain the UDA TE
to the guardian angel of the sound machine.

And, just because you promise me a prize for deriving SE from
the "psychology of machine" I tell you that I have decided
to call the modal formula (the one for the symmetrical frame):


    the little abstract Schroedinger Equation (LASE),

as I have called before the (godel-like) formula

                          <>p -> -[]<>p

    the first theorem of machine's psychology. (FTMP)

And our goal is to find a natural bridge from FTMP to LASE.

I must say that I have believe for a quite long time that this was
impossible. But then when you take the definition of knowledge
belief, observation/perception in Plato's thaetetus, then the
aritmetical translation of the UDA TE will lead us directly toward
the solution.
And so you will be obliged to give me the prize (at least
a little abstract price!).

Infinite thanks for your patience. All of you.

Received on Thu Apr 05 2001 - 08:08:38 PDT

This archive was generated by hypermail 2.3.0 : Fri Feb 16 2018 - 13:20:07 PST