 Despite their lack of a finite characteristic matrix, McKinsey (1941) shows that systems S2 and S4 are decidable. To prove these results McKinsey introduces modal matrices \((K, D, -, *, \times)\), with \(-\), \(*\), and \(\times\) corresponding to negation, possibility, and conjunction respectively. A matrix is normal if it satisfies the following conditions: