🚀 go-pugleaf

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