 Skolem (1920) gave an elegant solution to the Elimination Problem posed by Schröder for the calculus of classes by showing that if one added predicates to express “has at least \(n\) elements”, for each \(n = 1, 2, \ldots\), then there was a simple (but often lengthy) procedure to convert a first-order formula about classes into a quantifier-free formula. In particular this showed that the first-order theory of the calculus of classes was decidable. This quantifier-elimination result was used by Mostowski (1952) to analyze first-order properties of direct powers and direct sums of single structures, and then by Feferman and Vaught (1959) to do the same for general direct sums and direct products of structures.