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



(if this survives its teleportation in the archive!)



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?


Reply via email to