Re: The role of logic, & planning ...

From: Marchal <marchal.domain.name.hidden>
Date: Tue May 1 12:28:34 2001

Hi Russell,

> I spent a while poring over Bruno's thesis, and borrowed
>Boolos from a local university library to udnerstand more what it was
>about. I didn't go into too great a length into the results and
>structure of Modal logic, although I gained an appreciation, and an
>understanding of the symbology.
>
>However, my main problem with Bruno's work lay not in the technical
>details of Model logic, rather with the phrases of the ilk "We
>modelise knowledge by Bew(|p|)". I can appreciate its only a model,
>but why should I believe that model of knowing has any connection with
>reality? I'm afraid none of the Booloses, nor Bruno's posting helped
>me with this.

I am glad you borrowed Booloses from a library and that you spent a
while poring over my thesis.

I want just made precise that I have never try to modelise knowledge
by Bew(|p|).

This is, actually, a rather sensible point. Most philosopher agree
that S4 is a good *axiomatic* of knowledge. Precisely S4 is KT4 + MP,NEC
or, explicitely (added to the Hilbert Ackerman axioms) :

AXIOMS [](A -> B) -> ([]A ->[]B) K
            []A -> A T
            []A -> [][]B 4

RULES A/[]A (A & (A->B)) / B NEC MP.

That is, most philosopher (since Plato, but I remember having seen a
Buddhist
similar writing) agree that:

-if A->B is knowable and if A is knowable, then B is knowable. (K)
- if A is knowable then A is true. (T)
- if A is knowable than that very fact (that A is knowable) is knowable
(4)

Would you agree with that? 4 makes that knowledge somehow introspective.

Now we will see that if []A represent the formal provability of A, or
(provability by a sound machine), i.e. Bew(|A|), although 4 and K are
verified, we don't have T, that is, we don't have

                           []A -> A

provable for all sentence A. Bew(|A|) -> A is not always provable.
This entails that formal provability
cannot and should not be used for the formalisation of knowledge.

You can guess the reason. Consider []FALSE -> FALSE, this is
equivalent to -[]FALSE which is the statement of (self-) consistency (by
the machine or the formal system), that is <>TRUE, which by Godel's second
theorem is NOT provable (by the sound machine).


But then, how to formalize knowledge ?

When Socrate asked Thaetetus what is "knowledge of p", Thaetetus replied
"justification of p". But then Socrate argues that a justification
of p can be wrong.
Thaetetus proposed then to define knowledge by

            justification of p *and* truth of p,

by definition !
We will see that it is impossible to define "truth of p" in the language
of the machine (Tarski theorem), but still we can define knowledge
of p (for the machine) by

                Bew(|p|) *and* p

If we define KNOW(A) by []A & A, then the modal "KNOW" obeys S4, that is
KNOW(A -> B) ->(KNOW A -> KNOW B), (KNOW A) -> A, etc. (see above).


To sum up:

I never modelized knowledge of p by Bew(|p|), but I will indeed define
knowledge of p (in the language of the machine) by Bew(|p|) & p.


How come? Is not Bew(|p|), for the sound machine, trivially equivalent
with Bew(|p|) & p ?
Yes.
But the point is that the sound machine neither can "bew" it, nor "know"
it!

We will see how precisely the epistemological nuance between
Bew(|p|) & p and Bew(|p|) are made necessary by the incompleteness
phenomenon.


All this will be made transparent with the modal logic G and G* and their
arithmetical interpretations. The atomic sentences are interpreted by
arithmetical sentences.



>I can appreciate its only a model,
>but why should I believe that model of knowing has any connection with
>reality? I'm afraid none of the Booloses, nor Bruno's posting helped
>me with this.


The connection with the reality, as you see, is done in the most platonist
superb manner, I just add it by definition. Nuancing Bew(|p|) by
Bew(|p|) & "truth"(of p).

Well, later I will propose another nuancing of Bew(|p|), more appropriate
for "measuring probability one" on possible "consistent extension").
Bew(|p|)
is nuanced by
Bew(|p|) & consistency of p. (a necessary step by UDA actually).

The embedding in UD* will be "translated" in the language of the machine
by restricting the arithmetical interpretation of p.

And to get George's prize I will still need to extract LASE (the little
abstract schroedinger equation) from that embedding. And of course i will
need
to make clear the relationship between LASE and the quantum histories.


Bruno
Received on Tue May 01 2001 - 12:28:34 PDT