Leo Simons has shown that H1—H6 below constitute a set of independent axiom schemata for S3, with detachment for material implication “→” as the only primitive rule. He also showed that addition of the scheme (◇ ◇ α ⥽ ◇ α) yields S4, and that these schemata for S4 are independent. The question for S5 was left open. We shall show (presupposing familiarity with Simons' paper) that H1—H6 and S, below, constitute a set of independent axiom schemata for S5, with detachment for material implication as the only primitive rule.

Let S5′ be the system generated from H1—H6 and S with the help of the primitive rule. It is easy to see that Simons' derivations of the rules (a) adjunction, (b) detachment for strict implication, and (c) intersubstitutability of strict equivalents, may be carried out for S5′. We know that (1) (∼ ◇ ∼ α ⥽ ◇ α) is provable in S2, hence also in S3 and S5′; and (1) and S yield (2) (α ⥽ ∼ ◇ ∼ ◇ α). Perry has shown that addition of (2) to S3 yields S5, so S5 is a subsystem of S5′. And it is easy to prove S in S5; hence the systems are equivalent.