Hi Brent,

`You didn't answer my last post where I explain that Bp is different`

`from Bp & p.`

`I hope you were not too much disturbed by my "teacher's" tone (which`

`can be enervating I imagine). Or is it because you don't recognize the`

`modal form of Godel's theorem:`

## Advertising

~Bf -> ~B(~Bf),

`which is equivalent to B(Bf -> f) -> Bf, by simple contraposition`

`"p -> q" is equivalent with "~p -> ~q", and using also that "~p" is`

`equivalent to "p -> f", where f is put for "false".`

`This shows that for a consistent (~Bf) machine, although Bf -> f is`

`true, it cannot be proved by the machine. Now (Bf & f) -> f trivially.`

`So Bf and Bf & f are not equivalent for the machine`

(although they are for the "guardian angel"). Bruno http://iridia.ulb.ac.be/~marchal/