 These conditions correspond to Lewis’s rules of strict inference, adjunction and substitution of strict equivalents. The structure of McKinsey’s proof is as follows. The proof employs three steps. First, using an unpublished method of Lindenbaum explained to him by Tarski which holds for systems that have the rule of Substitution for propositional variables, McKinsey shows that there is an S2-characteristic matrix \(M = (K, D, -, *, \times)\) that does not satisfy condition (iii) and is therefore non-normal. M is a trivial matrix whose domain is the set of formulas of the system, whose designated elements are the theorems of the system, and whose operations are the connectives themselves. The trivial matrix M does not satisfy (iii) given that for some distinct formulas A and B, \(A\Leftrightarrow B\) is an S2-theorem. Second, McKinsey shows how to construct from M a normal, but still infinite, S2-characteristic matrix \(M_1 = (K_1, D_1, -_1, *_1, \times_1 )\), whose elements are equivalence classes of provably equivalent formulas of S2, i.e., of formulas A and B such that \(A\Leftrightarrow B\) is a theorem of S2, and whose operations are revised accordingly. For example, if \(E(A)\) is the set of formulas provably equivalent to A and \(E(A)\in K_1\), then \(-_1 E(A) = E(-A)= E(\neg A). M_1\) satisfies exactly the formulas satisfied by M without violating condition (iii), hence it is a characteristic normal matrix for S2 (\(M_1\) is the Lindenbaum algebra for S2). Finally, it is shown that for every formula A that is not a theorem of S2 there is a finite and normal matrix (a sub-algebra of \(M_1)\) that falsifies it. A similar proof is given for S4.