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 
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 

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 ?
But the point is that the sound machine neither can "bew" it, nor "know" 

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

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").  
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 
to make clear the relationship between LASE and the quantum histories.


Reply via email to