Professor Prior (Formal logic (1955), pp. 305–307) gives alternative postulate sets for Lewis's S5, one substantially Lewis's own set (p. 305, 6.1) and another, considerably simpler, due to Prior himself (pp. 306–307, 6.5). This note aims at showing that the systems based on these two postulate sets are in fact equivalent. We label the system based on Lewis's postulates ‘S5’, as usual, and that on Prior's postulates ‘P’.

The form of the postulate set for P considered here is as follows. We add to the full propositional calculus one definition:

Df. M: M = NLN;

and two special rules:

L1: ⊦Cαβ → ⊦CLαβ;

L2: ⊦Cαβ → ⊦CαLβ, if α is fully modalized (a propositional formula is fully modalized, if and only if all occurrences of propositional variables in it lie within the scope of a modal operator).

Prior's text (pp. 201–205) indicates sufficiently how it could be shown that any thesis of S5 is a thesis of P and that the rules and definitions of S5 are obtainable as derived rules of P. We turn, therefore, to the problem of showing that any thesis of P is a thesis of S5 and that the rules and definition of P are obtainable as derived rules of S5.