Marchal wrote:
>
> 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.
>
Thanks for this extended discussion. It does help a lot, and makes
even more sense if one assumes COMP (which actually I don't, but for
the sake of argument, wil do).
Just one further question. Is it possible for one machine to know p
and another machine to know -p? It seems from the above discussion,
you are only considering consistent machines, which of course
cannot know p and -p simultaneously without being
inconsistent. However, you're not ruling out a society of such
machines who argue over what statements they know to be true (just
like my ardent theists and atheists in Australia - actually this last
example is largely hypothetical - when it comes to religions,
Australians are amongst the most apathetic in the world - an important
fact in us enjoying peace and prosperity).
Cheers
----------------------------------------------------------------------------
Dr. Russell Standish Director
High Performance Computing Support Unit, Phone 9385 6967
UNSW SYDNEY 2052 Fax 9385 6965
Australia R.Standish.domain.name.hidden
Room 2075, Red Centre
http://parallel.hpc.unsw.edu.au/rks
----------------------------------------------------------------------------
Received on Sun May 06 2001 - 17:54:36 PDT