Hi Jacques,
>What is the NEC rule ?
In modal logic it is the NECESSITATION RULE.
It means that if the machine proves p, then it will prove Bp.
Smullyan says such a machine is normal.
Put in another way, with Smullyan's self-referential
interpretation of the B logic: it means that Bp->BBp is true
for the machine. If furthemore the machine knows (correctly
believe) that she is normal, then we call it a type 4 reasoner
(again following Smullyan).
>>Do you see how to derive Godel second theorem
>>of incompleteness theorem?
>I think I see how to derive Gödel theorem :
>if we take p=F (false) we get B(BF->F)->BF
>or B(~BF)->BF. BF means that the machine
>is inconsistent, ~BF that it is consistent.
>If C means that the machine is consistent,
>then B(~BF)->BF becomes BC->~C,
>which means that if the consistency is
>provable, then the machine is not consistent.
Exact.
JB:
>It is more clear to me if B means "provable" rather than "believe".
>But I wonder if the notion of provability is equivalent to the notion of
>belief. Intuitively I have the impression that if I don't believe that Santa
>Claus exists, then I believe that I don't believe that Santa Claus exists.
>One can believe sonething without having a proof of it. If it is a checkable
>belief, why not say that the machine is sure that p, rather than believes p
BM:
B represents indeed "justifiable third person belief". But now, by GODEL II
this does not allow a "sure of" interpretation, and this justify somehow
the use of belief. This reminds us also that science (third person justifiable
propositions) is on the side of belief, and never on certainty. Now, as I told
you, I use the term "believe" because Smullyan uses it and it is quite
coherent with our psychological view of Godel's result.
The "proof" reading of B leads also to the belief that Bp->p, which is
actually true for Self-referentially correct machine, but unprovable
by those machine. Any choice of word has some defect. We are
in the counter-intuition country. "To be sure of p" will be defined by
p & Bp
following Theaetetus (and Boolos, Goldblatt ...).
Bruno
PS Again, I did not get your post but find it in the archive.
Did you get mine? I wrote to Wei but did not get answers, perhaps
he is on Holiday.
http://iridia.ulb.ac.be/~marchal/
Received on Fri Sep 10 2004 - 06:23:42 PDT