Elimination problems in logic: a brief history (Q1024114)

The kind of elimination problem the author refers to in this paper is of the following type: If \(R\) and \(S\) are disjoint sets of predicate letters and \(A(R,S)\) is a sentence (or a conjunction of sentences) such that every predicate symbol that occurs in \(A(R,S)\) belongs to \(R\cup S\), find a sentence (or a conjunction of sentences) \(A^{\bigtriangledown}(S)\) that axiomatizes the set of \(S\)-logical consequences of \(A(R,S)\). Interest in elimination may be seen to go back to Aristotle's syllogistic, later to be emphasized by G. Boole (whose line of thought has long been considered deficient, until S. Burris (2001) managed to clarify it) and E. Schröder, who turned it into an algebra problem to be solved inside Boolean algebras. The author presents in detail Schröder's solution to the elimination problem, followed by an outline of Skolem's proof of what the author considers to be ``the most important elimination result in logic'': Given any formula \(A\) in the language of monadic second-order logic, one can find a formula \(A'\) in monadic first-order logic with equality, such that \(A\) and \(A'\) are logically equivalent. The paper ends with questions regarding quantifier elimination and some problems raised by the author's paper [J. Symb. Log. 25, 97--142 (1960; Zbl 0108.00304)].