-
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
MathematikerVereinigung 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.