- Contemporary messages sorted: [ by date ] [ by thread ] [ by subject ] [ by author ] [ by messages with attachments ]

From: Marchal <marchal.domain.name.hidden>

Date: Tue May 1 14:21:03 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 - 14:21:03 PDT

Date: Tue May 1 14:21:03 2001

Hi Russell,

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.

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 - 14:21:03 PDT

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