Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic

TL;DR

This paper explores Heinrich Behmann's early 20th-century work on second-order quantifier elimination for monadic formulas, highlighting its significance for modern computational logic and decision procedures.

Contribution

It reconstructs Behmann's original results, discusses their relevance to current methods, and provides extensive documentation of his related manuscripts and correspondence.

Findings

Second-order quantifier elimination always succeeds for monadic formulas.

Behmann's elimination method preserves logical equivalence.

Historical insights into the development of modern elimination techniques.

Abstract

For relational monadic formulas (the L\"owenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, projection and forgetting - operations that currently receive much attention in knowledge processing - always succeeds. The decidability proof for this class by Heinrich Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. Here we reconstruct the results from Behmann's publication in detail and discuss related issues that are relevant in the context of modern approaches to second-order quantifier elimination in computational logic. In addition, an extensive documentation of the letters and manuscripts in Behmann's bequest that concern second-order quantifier elimination is given, including a commented register and English abstracts of the German sources with focus on technical material. In the late 1920s Behmann attempted to develop an elimination-based decision method for formulas with predicates whose arity is larger than one. His manuscripts and the correspondence with Wilhelm Ackermann show technical aspects that are still of interest today and give insight into the genesis of Ackermann's landmark paper "Untersuchungen \"uber das Eliminationsproblem der mathematischen Logik" from 1935, which laid the foundation of the two prevailing modern approaches to second-order quantifier elimination.