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:
~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/
Received on Mon Jun 13 2005 - 10:16:06 PDT