102 Early Steps of Second-Order Quantifier Elimination beyond the Monadic Case: The Correspondence between Heinrich Behmann and Wilhelm Ackermann 1928–1934 (Abstract) Christoph Wernhard TU Dresden, Germany 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 Unter- suchungen über das Eliminationsproblem der mathematischen Logik (Investiga- tions on the elimination problem of mathematical logic) from 1935 [2]. Behmann developed in [4] a method to decide relational monadic formu- las (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 cardinal- ity constraint on the domain. Although technically related to earlier works by Löwenheim [16] and Skolem [23,24], Behmann’s presentation appears quite mod- ern 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 pos- sibilities to extend elimination to formulas with predicates of arity two or more. Behmann gave in 1926 at the Jahresversammlung der Deutschen Mathematiker- Copyright c 2017 by the paper’s authors In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 – Pro- ceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics, Dresden, Germany, December 6–8, 2017, published at http://ceur-ws.org. 103 Vereinigung a talk on the decision problem and the logic of relations (Entschei- dungsproblem 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 resolution- based 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 dedi- cated 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 correspon- dences 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. 104 References 1. Ackermann, H.R.: Aus dem Briefwechsel Wilhelm Ackermanns. History and Phi- losophy of Logic (4), 181–202 (1983) 2. Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathematis- chen Logik. Mathematische Annalen 110, 390–413 (1935) 3. Ackermann, W.: Zum Eliminationsproblem der mathematischen Logik. Mathema- tische Annalen 111, 61–63 (1935) 4. Behmann, H.: Beiträge zur Algebra der Logik, insbesondere zum Entschei- dungsproblem. Mathematische Annalen 86(3–4), 163–229 (1922) 5. Behmann, H.: Entscheidungsproblem und Logik der Beziehungen. In: Jahresbericht der Deutschen Mathematiker-Vereinigung. vol. 36, no. 2. Abt. Heft 1/4, pp. 17–18 (1927) 6. Behmann, H. (bestandsbildner): Nachlass Heinrich Johann Behmann, Staatsbib- liothek zu Berlin – Preußischer Kulturbesitz, Handschriftenabteilung, Nachlass 335 7. Behmann, H. (bestandsbildner): Personalakte Heinrich Behmann, Archiv der Martin-Luther-Universität Halle-Wittenberg, PA 4295 8. Bernhard, P., Thiel, C.: Der wissenschaftliche Nachlass Heinrich Behmanns: ein Verzeichnis seines Bestandes am 20.1.2000 (2000), Printed working copy with handwritten corrections and updates in Staatsbibliothek Berlin, Handschriften- abteilung. Second printed copy in [6, Kasten 1]. 9. Church, A.: Introduction to Mathematical Logic, vol. I. Princeton University Press, Princeton, NJ (1956) 10. Craig, W.: Elimination problems in logic: A brief history. Synthese (164), 321–332 (2008) 11. Doherty, P., Łukaszewicz, W., Szałas, A.: Computing circumscription revisited: A reduction algorithm. Journal of Automated Reasoning 18(3), 297–338 (1997) 12. Gabbay, D., Ohlbach, H.J.: Quantifier elimination in second-order predicate logic. In: KR’92. pp. 425–435. Morgan Kaufmann, San Francisco, CA (1992) 13. Gabbay, D.M., Schmidt, R.A., Szałas, A.: Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications. College Publications, Lon- don (2008) 14. Gödel, K.: Collected Works, vol. IV: Selected Correspondence, A-G. Oxford Uni- versity Press, Oxford (2003) 15. Haas, G., Stemmler, E.: Der Nachlaß Heinrich Behmanns (1891–1970). Gesamtverzeichnis. Aachener Schriften zur Wissenschaftstheorie, Logik und Logikgeschichte, RWTH Aachen (1981) 16. Löwenheim, L.: Über Möglichkeiten im Relativkalkül. Mathematische Annalen 76(4), 447–470 (1915) 17. Mancosu, P.: Between Russell and Hilbert: Behmann on the foundations of math- ematics. The Bulletin of Symbolic Logic 5(3), 303–330 (1999) 18. Mancosu, P., Zach, R.: Heinrich Behmann’s 1921 lecture on the algebra of logic and the decision problem. The Bulletin of Symbolic Logic 21(2), 164–187 (2015) 19. Nonnengart, A., Ohlbach, H.J., Szałas, A.: Elimination of predicate quantifiers. In: Ohlbach, H.J., Reyle, U. (eds.) Logic, Language and Reasoning, Trends in Logic, vol. 5, pp. 149–171. Springer, Berlin (1999) 20. Schenk, G., Mayer, R. (eds.): Philosophisches Denken in Halle: Personen und Texte, vol. 2: Beförderer der Logik. Schenk, Halle (Saale) (2002) 21. Schmidt, R.A.: The Ackermann approach for modal logic, correspondence theory and second-order reduction. Journal of Applied Logic 10(1), 52–74 (2012) 105 22. Schröder, E.: Vorlesungen über die Algebra der Logik, vol. 1. Teubner, Leipzig (1890) 23. Skolem, T.: Untersuchungen über die Axiome des Klassenkalküls und über Produktations- und Summationsprobleme welche gewisse Klassen von Aussagen betreffen. Videnskapsselskapets Skrifter I. Mat.-Nat. Klasse(3) (1919) 24. Skolem, T.: Logisch-Kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen. Videnskapsselskapets Skrifter I. Mat.-Nat. Klasse(4) (1920) 25. Szałas, A.: On the correspondence between modal and classical logic: An auto- mated approach. Journal of Logic and Computation 3, 605–620 (1993) 26. Wernhard, C.: Heinrich Behmann’s contributions to second-order quantifier elimi- nation from the view of computational logic. Tech. Rep. KRR 15-05, TU Dresden (2015), http://cs.christophwernhard.com/papers/behmann.pdf 27. Wernhard, C.: Second-order quantifier elimination on relational monadic formulas – a basic method and some less expected applications. In: TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 249–265. Springer, Berlin (2015) 28. Zach, R.: Completeness before Post: Bernays, Hilbert, and the development of propositional logic. The Bulletin of Symbolic Logic 5(3), 331–366 (1999)