In this paper I shall give a solution of the decision problem for the Lewis systems S2 and S4; i.e., I shall establish a constructive method for deciding whether an arbitrary given sentence of one of these systems is provable. The method is laborious to apply, since, in order to decide by means of it whether a given sentence is provable, it is necessary to construct a (usually very large) finite matrix. The argument will perhaps be of general interest, however, because it does not seem to depend too closely on the special features of these particular systems, so that it may be possible to apply it in order to solve the decision problem for other such systems.

Section II presents the decision method for S2, and Section III for S4. In Section IV, I shall establish a certain correspondence between S4 and topology, which will provide a solution for a decision problem in topology; this correspondence also enables us to settle a previously unsolved problem with regard to the Lewis systems.

In treating of this system, I shall use the notation of Lewis, with the single exception that I shall use the symbol “≣”, instead of Lewis's symbol “=”, for strict equivalence. I shall use the symbol “=” to denote identity. Thus “p≣q” is a formula of S2, while “x=y” is the statement asserting that x and y are identical. I shall refer to the rules, primitive sentences and theorems of S2 by the names and numbers used by Lewis. Whenever a theorem stated by Lewis involves the symbol “=”, I shall of course suppose that this symbol has been replaced throughout by “≣”: thus, for example, I shall take 19.82 to be “(◇p∨◇q) ≣ ◇(p∨q)”, instead of “(◇p∨◇q) ≣ ◇(p∨q)”.