This presentation focuses on the span between two early seminal papers on second-order quantifier elimination on the basis of first-order logic: Heinrich Behmann's Habilitation thesis Beiträge zur Algebra der Logik, insbesondere zum Entscheidungsproblem (Contributions to the algebra of logic, in particular to the decision problem), published in 1922 as [4], and Wilhelm Ackermann's Untersuchungen über das Eliminationsproblem der mathematischen Logik (Investigations on the elimination problem of mathematical logic) from 1935 [2].
Behmann developed in [4] a method to decide relational monadic formulas (that is, first-order formulas with only unary predicates and no functions other than constants, also known as Löwenheim class) that actually proceeds by performing second-order quantifier elimination with a technique that improves Schröder's rough-and-ready resultant (Resultante aus dem Rohen) [22,10]. If all predicates are existentially quantified, then elimination yields either a truth value constant or a formula that just expresses with counting quantifiers a cardinality constraint on the domain. Although technically related to earlier works by Löwenheim [16] and Skolem [23,24], Behmann's presentation appears quite modern from the view of computational logic: He shows a method that proceeds by equivalence preserving formula rewriting until a normal form is achieved in which second-order subformulas have a certain shape for which the elimination result is known [27,26].
Ackermann laid in [2] the foundation for the two major modern paradigms of second-order quantifier elimination, the resolution-based approach [12], and the so-called direct or Ackermann approach [11,13,21], which is like Behmann's method based on formula rewriting until second-order subformulas have a certain shape for which the elimination result is known, however, now based on more powerful equivalences of second-to first-order formulas, such as Ackermann's Lemma. Another result of Ackermann's paper was a proof that second-order quantifier elimination on the basis of first-order logic does not succeed in general.
As documented by letters and manuscripts in Behmann's scientific bequest [6], between 1922 and 1935 Behmann and Ackermann both thought about possibilities to extend elimination to formulas with predicates of arity two or more. Behmann gave in 1926 at the Jahresversammlung der Deutschen Mathematiker-102
Vereinigung a talk on the decision problem and the logic of relations (Entscheidungsproblem und Logik der Beziehungen), where he falsely claimed a positive result. Its abstract, published as [5], aroused the curiosity of Ackermann, who wrote in August 1928 to Behmann, initiating a correspondence that lasted to November 1928 and comprises five letters. Among the issues discussed were forms of what today is called Skolemization. Their correspondence concerning elimination was resumed in 1934 with a letter sent by Behmann upon receiving the offprint of [2], where he suggests a graphical presentation of the resolutionbased elimination method by Ackermann [2], and Ackermann's reply, where, aside of technical issues, he gratuitously acknowledges that Behmann's work [4], at its time, was for him the impetus to investigate the elimination problem more closely. Their correspondence, as far as archived in [6], then only continues in January 1953, with five more letters until December 1955, in which different topics are discussed.
Apparently, there are very few works that are concerned with the history of second-order quantifier elimination. There is a paper by Craig [10] explicitly dedicated to that subject, with emphasis on Schröder's work, and in [19] Ackermann's results from [2] are discussed and explicitly related to modern approaches. A variant of Behmann's method from [4] is provided along with extensive historic remarks by Church [9, §49]. Further accounts of Behmann's early work with main focus on the Hilbert school and the decision problem (Behmann's talk on 10 May 1921 at the Mathematische Gesellschaft on the topic of [4] seems the first documented use of the term Entscheidungsproblem (decision problem) [28]) can be found in [17,28,18]. Behmann's scientific bequest [6] has been registered in [8], and before in [15]. His correspondence with Gödel has been published in [14]. A further archive source is his personal file as university professor [7], where excerpts have been published in [20]. Aside of the correspondence with Ackermann, also Behmann's correspondences with Russell, Carnap, Scholz and Church touch topics related to elimination. Letters from Ackermann's correspondences published in [1] give further hints on the "pre-history" of Ackermann's paper [2]: He sent the manuscript in 1933 to Bernays, who recommended it to Hilbert for publication and sent six large pages with remarks to Ackermann.
The historical-technical perspective on the archived correspondences and manuscripts provides interesting insight into the development of modern logic, including, in particular, computational logic. Often past technical results and methods that got out of sight turn out to be relevant for the ongoing discourse, as, for example, shown in [25,19] for results from [2], or in [27] for results from [4] and [3].
The workshop presentation is based on parts IV and V of the report [26].
Acknowledgments. This work was supported by DFG grant WE 5641/1-1.