Re: Kripke semantics

From: Marchal <>
Date: Sat Apr 7 09:02:28 2001

Hi George,

I finish my post yesterday a little too quickly.

I 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):
> p->[]<>p,
> 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!).

Of course this is not entirely correct. You should "give me
the prize" only:

 1) when you will see what I mean when I say that
<>p -> -[]<>p is a fundamental theorem in machine's psychology.

+ (above all):

 2) when you understand why I dare to call the formula p->[]<>p the
little abstract schroedinger equation.

+ (of course):

 3) when it will be clear how I translate
the UDA TE and how that translation isolates a derivation of

I explain informally a little bit.


When the box []p is interpreted in english as provable(p), i.e.
provable by a honest UTM, the <>p, which is -[]-p, can be read as
p is consistant. This follows from the fact that if -p is not provable
then you can add p to the set of axioms used by the machine without
being lead to a contradiction. (Indeed if the machine derives the
false from -p, then the machine derives (-p -> FALSE), which is --p,
which is p). More directly <>TRUE is the same as -[]-TRUE = -[]FALSE,
= I do not prove the FALSE = I am consistent.
So <>p -> -[]<>p is just a modal form of a generalisation of Godel's
second incompleteness theorem, and in English you can read that
formula in the following way. if p is consistent then I cannot prove
that p is consistent.

When the machine proves the particular case (<>TRUE -> -[]<>TRUE),
that is Godel's second theorem, it is as if the machine was telling
us: if I am consistent I cannot prove it.

A more psychological reading of that formula is, by identifying
(audaciously perhaps) consistency with consciousness (or awakeness)
you get "if I am conscious then I cannot prove it.

Note that any formula with the form <>p can be read there is an
accessible observer-moment (world) with p true at it. So when the
talk about <>p, the machine talk about a consistent extension of

To sum up, the 1) above is linked to Godel's theorem, seen as a
psychological limitation of machine. Later I will be hopefully
a little more rigorous about the link consciousness/consistency.


Why do I consider the formula p->[]<>p as an abstract form
of SE ?
Surely that deserves some words of explanation. Unfortunately
to explain this, we must leave the cocooning logic of plato
heaven (classical logic) for the jungle of what is called
The theorems of a weak logic makes a subset of the theorems
of classical logic.

We will meet essentially two principal weak logics:
intuitionistic logic and quantum logic.

For exemple a typical classical tautology which is not a theorem
for intuitionnistic logic is the principle of excluded middle

                     p v -p

And a classical tautology which is not a theorem of quantum logic
                p & (q v r) <-> (p & q) v (p & r)

That is, in quantum logic there is a failure of the distributivity
It has been proved that both intuitionist and quantum logic
doesn't have truth table semantics. But modal logics can help
us to handle those weak logics without leaving plato heaven.

In particular the modal logic, known as B, with the axioms
[]p ->p, p->[]<>p and with the rule of modus ponens and necessitation
has a non trivial relationship with quantum logic.
In fact we have a representation theorem (by Goldblatt) which
says that when B proves []<>A, QL proves A. (I simplify a
little bit). Sometimes []<>A is called the quantization of A.
Isolating the formula p->[]<>p is also a good step toward
defining a measure on the relative set of consistant extension.

ABOUT 3). (later).

I stop here. I hope you are not overwhelmed by the information.
Here I have just try to anticipate a little. I must say that I
not to busy now, but unfortunately I will be quickly more and more
busy. So I give you something to eat for a long period.
(except that I will try to say a little more about 3) still
this week).
Nevertheless, don't hesitate to tell me "enough!" or one of your
"hmmmmmmmmmmmmmmmmmm". I would understand. Of course it is not
so easy to understand my work which is not only transdisciplinar
but also goes accross very different kind of logics.

Received on Sat Apr 07 2001 - 09:02:28 PDT

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