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

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

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.

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

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:

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 )

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

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

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