Hi Jacques,
Nice to see you back. Actually I just discovered your message
in the archive, I did not got them by the mail (?). Sorry for the delay.
I quote you from the archive:
>The axiom B(Bp->p)->Bp seems very strange to me.
I think it *is* strange. It is at the heart of "counter-intuition" in the sense
that you can derive from it (together with K = B(p->q)->(Bp->Bq) and the
two inference rule MP and NEC) all the consequences of incompleteness.
Do you see how to derive Godel second theorem of incompleteness theorem?
Boolos gives 5 reasons to find Lob's formula, that is B(Bp->p)->Bp,
"utterly astonishing", and he does not mention the placebo effect.
(have you read my last paper?
http://iridia.ulb.ac.be/~marchal/publications/SANE2004MARCHAL.htm )
>Is it applicable only to machines or also to humans ?
It is applicable to any consistent believer in
(classical) arithmetic, when belief are
checkable. If you prefer the B is for
provable, or Beweisbar (Godel).
For any machine-like entity (with or without
oracle) it gives even their complete
(propositional)
logic of provability and consistency.
It *is* the main axiom of G.
(Note that there is a corresponding
version for intuitionist arithmetic.)
>I don't believe that Santa Claus exists (~Bp).
>If I consider the proposition "Bp->p" which
>means "If I believe that Santa Claus exists,
>then Santa Claus exists", this proposition
>seems true to me, because of le
>propositional logic rule "ex falso quodlibet
>sequitur" or false->p : the false proposition
>Bp implies any proposition, for example p.
>So I can say thay I believe in the proposition
>Bp->p : B(Bp->p). According to the lobian
>formula B(Bp->p)->Bp, this implies Bp (I believe
>that Santa Claus exist) !
It is all correct .... except that you cannot
prove (believe) your own consistency; so that
you cannot prove that you don't believe that Santa
Klaus does not exist. All formula beginning by ~B
are not believable (provable) by the consistent machine.
>More formally : The axiom ~Bp->B(~Bp)
>seems correct to me, isn't it ? <snip>
It seems, but not for a notion of checkable or
verifiable belief. Any machine capable of proving
there is a proposition she cannot prove, would
be able to prove its consistency, and that's impossible
by Godel II. (this follows from your "ex falso quodlibet":
a machine proving the f, will prove all propositions, so if
there is a proposition (like Santa Claus exists) that
you pretend you will never believe (prove) then you
are asserting that you prove (believe) you are consistent!.
All right? I use "believe" instead of "prove" because
we are following a little bit Smullyan's "Forever Undecided".
But this suits well with the "machine psychology".
Do you have that FU book?
Bruno
http://iridia.ulb.ac.be/~marchal/
Received on Fri Sep 24 2004 - 06:10:19 PDT