kube@cogsci.berkeley.edu (Paul Kube) (06/02/87)
In article <19190@ucbvax.BERKELEY.EDU> kube@cogsci.berkeley.edu.UUCP (I) write: > >Well, actually, this only shows that L(P&-LP) can't be a theorem, >not that -L(P&-LP) is. I take it back. I now have a proof of the conjecture, but this message is too small to contain it. No, really, derivations in T using only modus ponens and necessitation from truth-functional tautologies and the axioms are too tedious to post. If you want to try for yourself, I suggest starting with -P v LP v (P & -LP) and proceeding "by cases". (The first and second disjunct are easy.) It's more illuminating to make a semantical argument: Suppose L(P&-LP) is true in some model structure M for T. Then in M, P&-LP is true in every world accessible from the actual world; so P is true in every such world; so LP is true in the actual world. But, P&-LP being true in every accessible world, -LP is in particular true in the actual world (by reflexivity of accessibility). So M (making both LP and -LP true in the actual world) cannot be a model structure. Therefore L(P&-LP) is true in no model; so -L(P&-LP) is true in every model; and thus, since T is complete, -L(P&-LP) is a theorem of T. Since the argument makes no use of transitivity or symmetry of the accessibility relation, it applies as well to T, S4 and S5. (So LP -> LLP is not needed to get the result.) --Paul kube@berkeley.edu, ...!ucbvax!kube