Hi Bruno,

From: Bruno Marchal <[EMAIL PROTECTED]> To: [EMAIL PROTECTED] Subject: Re: Lob + New Views On Mind-Body Connection Date: Thu, 09 Sep 2004 15:46:10 +0200

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.

What is the NEC rule ?

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.

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.

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 )

I had a look at it.

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

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

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

I don't have this book.

Bruno

http://iridia.ulb.ac.be/~marchal/

Jacques.

_________________________________________________________________ Bloquez les fenêtres pop-up, c'est gratuit ! http://toolbar.msn.fr