Le 06-juil.-05, à 00:56, Russell Standish a écrit :
You are right, my apologies. I read the necessitation rule backwards
in your thesis. You do in fact say P => []P. I'll take your word for
it that consistency destroys necessitation, but I don't have the
intuitive understanding of it yet. Never mind, it is enough for my
present purposes.
OK. Be careful not to confuse the formula A-> B, and the rule A => B.
The first is just a formula (equivalent with ~A v B in classical
logic). The second is a dynamical rule saying that if the machine
proves A it proves B. In general A => B is written
A
_
B
(if this survives its teleportation in the archive!)
:-)
Bruno
PS We loose the necessitation rule for the new box Cp = Bp & ~B~p,
because although the tautology t is provable, Ct is not. Indeed Ct is
Bt & ~B~t, but ~B~t = ~Bf, and this is the self-consistency statement
no consistent machine can prove. OK?
http://iridia.ulb.ac.be/~marchal/
