 Using the above rules and axioms Lemmon defines four systems. System P1, which is proved equivalent to the Lewis system S1, employs the propositional basis (PC), rules (a′)—necessitation of tautologies and axioms—and (b′), and axioms (2) and (3). System P2, equivalent to S2, employs (PC), rules (a′) and (b), and axioms (2) and (1′). System P3, equivalent to S3, employs (PC), rule (a′), and axioms (2) and (1). System P4, equivalent to S4, employs (PC), rule (a), and axioms (2) and (1). In Lemmon’s axiomatization it is easy to see that S3 and von Wright’s system M (Feys’ T) are not included in each other, given M’s stronger rule of necessitation and S3’s stronger axiom (1) in place of (1′) = K. In general, Lemmon’s axiomatization makes more perspicuous the logical distinctions between the different Lewis systems.