Le 06-juil.-05, à 00:56, Russell Standish a écrit :

## Advertising

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/