A Short Note on the Early History of the Spectrum Problem and Finite Model Theory

Abstract

Finite model theory is currently not one of the hot topics in the philosophy and history of mathematics, not even in the philosophy and history of mathematical logic. The philosophy of mathematics and mathematical logic has concentrated on infinite structures, closely related to foundational issues. In that context, finite models deserved only marginal attention because it was taken for granted that the study of finite structures is trivial compared to the study of infinite structures. In retrospect, research on finite structures turned out to be neither trivial nor irrelevant but had an important impact on theoretical computer science. A closer look at the early history of the spectrum problem shows that the birth of finite model theory has roots in formal logic, at a time when computer science did not yet exist.

Keywords:

• Heinrich Scholz
• first order logic
• spectrum problem
• finite model theory
• Trakhtenbrot's theorem

1. Introduction

Model theory in mathematical logic deals with the relationship between a formal language (syntax) and its interpretations (semantics) by means of set-theoretic structures. Typically, this formal language is first order-logic or some extension of it. Constructing models for a given axiom system with additional properties which cannot be specified in the axiom system itself, e.g. the cardinality of the model, turned out be an important task of model theory. Furthermore, model theory studies the equivalence of models, e.g. determining (non-isomorphic) models of an axiom system.

Finite model theory is a restriction of model theory to interpretations on finite structures, which have a finite universe. Finite model theory is quite different from model theory insofar as central theorems of model theory do not hold when restricted to finite structures, e.g. the compactness theorem, Gödel's completeness theorem, and the method of ultraproducts for first-order logic.

According to the standard reading, the rise of computer science (and in particular complexity theory and databases) allowed for the development of finite model theory as a distinct field of research. The restriction to interpretations to finite structures turns out to be a strength and an advantage here, because in the case of finite model theory many of the problems of complexity theory and database theory can be formulated as problems of mathematical logic.

In their introduction on Finite Model Theory, Heinz-Dieter Ebbinghaus and Jörg Flum highlight two landmarks for the development of finite model theory: Trakhtenbrot's theorem¹ from 1950 and Scholz's spectrum problem from 1952 (Ebbinghaus and Flum 1995, viii):

In both cases, computational aspects play their part: Trahtenbrot's [sic (spelling error)] proof rests on the undecidability of the halting problem for machines, and the spectrum problem turned out to be intimately linked to the question whether deterministic and nondeterministic polynomial time complexity coincide.

Trakhtenbrot's theorem states that the set of finitely satisfiable sentences is not recursively enumerable. This means that completeness (which is fundamental to first-order logic) fails over finite models. The spectrum problem formulated by Heinrich Scholz asks for a characterization of the spectra of first-order sentences, i.e. sets of cardinalities of finite models of some first-order sentences.

Ebbinghaus and Flum mention Trakhtenbrot and Scholz only in passing. They quickly move on to address databases and programming languages. In this paper, in contrast, the early history of finite model theory will be considered in more detail.

2. About an Unsolved Problem in Symbolic Logic

In 1952, the Journal of Symbolic Logic posted a short note, entitled ‘Ein ungelöstes Problem in der symbolischen Logik’ (Scholz 1952, 160). It was an apparently innocent problem that Heinrich Scholz from Münster was presenting here:

An unsolved problem in symbolic logic. Let IK be the first order predicate calculus with identity. In IK one can formalize an axiom system BP for Boolean algebras with only one binary predicate variable. Let θ be the conjunction of the axioms of BP. Then θ is satisfiable in a finite domain m of enumerable elements m if and only if there is an $n>0$ such that $m=2^n$. This results in the following problem. Let H be an well-formed formula of IK. We call the set of natural numbers, for which H is satisfiable, the spectrum of H. Let M be an arbitrary set of natural numbers. We look for a sufficient and necessary condition that ensures that there exists an H, such that M is the spectrum of H.²

The printed version of the text in the Journal of Symbolic Logic has some marginal grammatical deviations compared to the version Scholz sent to the Journal of Symbolic Logic in typescript to the editors. The term ‘Ausdruck’ (‘expression’) is explained by the English translation in brackets: ‘well-formed formula’; further, ‘sufficient’ (‘hinreichend’) is spelt correctly in the typescript (Figure 1).

Figure 1. Printed version of Heinrich Scholz's note (Scholz 1952).

At the Annual Symposium of the European Association of Computer Science Logic, CSL'05, held in Oxford in 2005, Arnaud Durand, Etienne Grandjean and Malika More organized a special workshop dedicated to the spectrum problem. The article Fifty years of the spectrum problem, jointly written by Arnaud Durand, Neil D. Jones, Johann A. Makowsky and Malika More (Durand et al. 2012) dates back to this conference. The authors examine in detail Scholz's ‘innocent’ question, which formulated for the first time the so-called spectrum problem in the model theory of mathematical logic (Figure 2).³

Figure 2. Heinrich Scholz. ‘An unsolved problem in Symbolic Logic’. Münster i.W. 27. August 1951. Universitäts- und Landesbibliothek Münster. Nachlass Heinrich Scholz. Typoskr. 1 b., 1 l.S., Sig. 122,054.

Scholz defined the spectrum of an arbitrary first order sentence, or formula ψ of first-order logic with identity to be the set of all natural numbers n for which ψ has a model of cardinality n. To put it briefly, the spectrum of a first-order sentence, or formula is the set of the cardinalities of its finite models. Scholz then asked for a characterization of spectra, i.e. sets of natural numbers that are the cardinalities of finite models of first order sentences. Scholz's spectrum can be more or less formally paraphrased in different ways, e.g. as follows (Börger et al. 1997, 49): The spectrum of a first-order sentence ψ is the set of cardinalities of its finite models, i.e. a spectrum $\psi :\{\psi \in \mathbb{N}:\psi \mathrm{has}\mathrm{a}\mathrm{model}\mathrm{with}\psi \mathrm{elements}\}$.

Scholz's problem of characterizing the class of spectra, i.e. the subsets $S\subseteq \mathbb{N}$ for which there exists a first-order sentence ψ such that spectrum $\left(\psi \right)=S$, turned out to be equivalent to the question of possible finite models of cardinality that can be formulated in first-order predicate calculus with identity. This question was not trivial.⁴ In order to understand why the spectrum problem was not a trivial question, it is helpful to recall some classical results about first order logic which were achieved before Scholz formulated the spectrum problem in 1952, namely the completness theorem and the compactness theorem. Gödel's completeness theorem says that a sentence is valid if and only if it is provable. An immediate consequence of this result is that the set of valid sentences is recursively enumerable; this is the Church-Turing theorem. Closely related to the completeness theorem is the compactness theorem which says that if a set of sentences is finitely satisfiable, then it is also satisfiable. Kurt Gödel proved the countable compactness theorem in 1930 and used it to derive a generalization of the completeness theorem (Gödel 1930). Anatoly Ivanovich Maltsev proved the uncountable case in 1936 (Maltsev 1936).

It follows from the compactness theorem that there are no unsatisfiable infinite sets of sentences each finite subset of which is satisfiable. Like the completeness theorem, it has a version related to entailment: if an infinite set of sentences entails something, already a finite subset does. To be more precise, the compactness theorem states that a set of first-order sentences has a model if and only if every finite subset of it has a model. This theorem is an important tool in model theory, as it provides a useful method for constructing models of any set of sentences that is finitely consistent.

It was Boris Trakhtenbrot's undecidability result for finite satisfiability that has led Heinrich Scholz in correspondence with Gisbert Hasenjaeger and Werner Markwald to the formulation of the spectrum problem (Scholz and Hasenjaeger 1961). Trakhtenbrot proved that the problem of validity in first-order logic on the class of all finite models is undecidable (Trakhtenbrot 1950). In fact, the class of valid sentences over finite models is not recursively enumerable (though it is co-recursively enumerable). Thus, there is no effective axiomatization of the set of all finitely valid first-order sentences. Trakhtenbrot's theorem implies that Gödel's completeness theorem (that is fundamental to first-order logic) does not hold in the finite case. Trakhtenbrot's theorem is generally regarded as the first important result in finite model theory. Here, finite models are the object of study, as this result is about finitely valid first-order sentences, i.e. first-order sentences true on all finite models.

One might wonder how did Scholz know about Trakhtenbrot's theorem? Trakhtenbrot's article appeared in a Russian journal five years after the end of the Second World War, at a time when it was extremely difficult to obtain such material in the Western occupation zone. Although Trakhtenbrot's doctoral dissertation from 1950 dissertation was later widely honored as pioneering for finite model theory, the official mathematical establishment in Russia was hostile to logic at the time and international cooperation was difficult. However, the Heinrich Scholz correspondence in the University and State Library of Münster provides some information about Scholz's early acquaintance with Trakhtenbrot's theorem. In a letter dated on 20 May 1950, Scholz thanks Andrzej Mostowski for the research literature that his colleague sent to his seminar in Münster. At the same time Scholz asked for the latest issue of Fundamenta Mathematica. Scholz maintained close contacts with Polish logicians and mathematicians, among them with Józef Pepis whose works were devoted to the problem of mutual reducibility of the decision problem. Pepis was killed by the Gestapo in August 1941.

During the World Wars and after the Second World War Fundamenta Mathematica ascend to a highly specialized and internationally recognized journal. Due to the Nazi cruelties against the Polish elite, including many mathematicians and logicians, the editors were very hostile and dismissive towards their German colleagues. The shipping of new issues of Fundamenta Mathematica to Germany was prohibited. Not all Polish logicians thought that way. One of the most prominent figure of the postwar logical life in Poland, Andrzej Mostowski, supplied Scholz with the latest research literature from Poland and abroad, including new editions of Fundamenta Mathematica.

When Mostowski was invited in 1948/49 as a ‘temporary member’ to the prestigious Institute for Advanced Studies in Princeton he reported to Scholz in detail about his conversations with Kurt Gödel, Albert Einstein, Alonzo Church, et al. (Figure 3). In a letter dated on 26 May 1951, Scholz thanks his Polish colleague, as he so often does, for the newest literature. Then, Scholz tells Mostowski that in the summer semester of 1951 his research team in Münster would study the theory of recursive functions in detail, ‘to which Fräulein Peter [Rózsa Péter] has provided a new excellent approach through her beautiful monograph. […] The work Trachtenbrot has also come to our attention. It is indeed highly interesting'.⁵

Figure 3. Letter from Andrzej Mostowski to Heinrich Scholz. 26.03.1949. Universitäts- und Landesbibliothek Münster. Nachlass Heinrich Scholz, Sig. 112,074.

The first colleagues who published papers in response to Heinrich Scholz's problem were Andrzej Mostowski (1956) and Günter Asser (1955). Asser belonged to the working group around Karl Schröter, a student of Heinrich Scholz, who had been appointed from Münster to Berlin in 1948 and established the ‘Berlin School’ of mathematical logic there. Asser became Schröter's first doctoral student and soon his most important collaborator. Together they founded the ‘Zeitschrift für Mathematische Logik und Grundlagen der Mathematik’ in 1954, which quickly gained international importance.

In a letter to Heinrich Scholz dated 7 September 1956, Asser sended Scholz a copy of a paper which appeared in the ‘Zeitschrift für mathematische Logik und Grundlagen der Mathematik’ (Asser 1956). He would give, Asser explained, a lecture on this topic at the DMV (Deutsche Mathematiker Vereinigung) conference in Würzburg from 10 September to 15 September 1956. He had pursued Scholz's ‘proposal to examine the predicate calculus with functionals in relation to the representation problem. I have found that in the predicate calculus with functionals the same sets of natural numbers can be represented as in the predicate calculus without functionals, both in the case with identity and in the case without identity '.⁶

This result was also affirmed by Wilhelm Ackermann in his review of Asser's paper in the Journal of Symbolic Logic: ‘the addition of functionals does not lead to an expansion of the expressiveness (expressive capacity)’ (Ackermann 1958, 39) of the predicate calculus.⁷ Ackermann did not mention here that Asser dedicated this work ‘to the memory to Heinrich Scholz, who died on 30 December 1956. In his 1956 paper Asser noted (Asser 1956, 250):

Following my work on the representation problem in first-order predicate calculus with identity, Prof. Scholz [in a letter of May 24, 1955] raised the question of which sets of natural numbers are definable in first-order predicate calculus with functionals. In the present work it is to be shown that with regard to the problem of representation and in even more general respects, the predicate calculus with functionals is no more expressive than that without functionals.⁸

In his 1955 paper, Asser did not use the term ‘spectrum’ (Asser 1955). But it is quite clear from the introduction and the footnotes⁹ that Asser is referring to Scholz's spectrum problem. Asser described the general question of classes of cardinal numbers (not only natural numbers) so-called 'representable’ by a sentence of first-order logic with identity, both in the framework of satisfiability and validity. In the appendix of their paper, Durand, Jones, Makowsky, and More offer a detailed reconstruction of Asser's paper (Durand et al. 2012, 539):

Here, a first-order sentence ϕ represents a given (finite or infinite) cardinality m regarding satisfiablity if there is a structure which domain has cardinality m which is a model of ϕ, and regarding validity, if ϕ holds in every structure with cardinality m. Asser first noticed that ϕ represents m regarding satisfiability if and only if $\mathrm{\neg \varphi }$ does not represent m regarding validity, so that validity reduces to satisfiability via complement. The author added: Given the Löwenheim-Skolem Theorem the representation question in satisfiability theory for infinite cardinalities is trivial: the first-order sentence ϕ either has no infinite model (and in this case it has finite models in finitely many finite cardinalities only) or has models in every infinite cardinality. Hence, the problem actually is about exactly which sets of natural numbers are the set of cardinalities of finite models of first-order sentences, i.e. what we would call spectra.

Asser proved that every set which is representable by an expression of the ‘Identitätskalkül’ is elementary decidable, but not every elementary decidable set is representable. Subsequently, Asser proposed some questions. The third and most famous question whether the class of spectra is closed under complement remained open up to now and is usually known as ‘Asser's Problem’, or ‘Asser's question’: ‘Is the complement of a first order spectrum a first order spectrum?’

In 1956, Andrzej Mostowski adressed the recursive characterization of spectra almost simultaneous with Asser's paper, explicitly using the name ‘spectrum’ (Mostowski 1956). Mostowski remarked that (Mostowski 1956, 210)

G. Asser […] has established a number of interesting results pertaining to a problem proposed by H. Scholz. The results of Asser overlap in part with results which I have found in 1953 while attempting (unsuccessfully) to solve Scholz's problem (cf. Roczniki Polskiego Towarzystwa Matematycznego, series I, vol. 1 (1955), p. 427). I shall give here proofs of my results which do not overlap with Asser's.

Mostowski deduced positive solutions to Scholz's problem in a number of special cases, among them the theorem: The sets of natural numbers, whose characteristic functions are in the second level of the Grzegorczyk hierarchy ${\mathcal{E}}^2$, are first-order spectra. In his thesis written under the supervision of Mostowski in 1950, Grzegorczyk defined a hierarchy of low complexity recursive functions, today known as the Grzegorczyk hierarchy (Grzegorczyk 1953).

Originally, Scholz's problem has been approached in terms of recursion theory. The early authors like Günter Asser and Andrzej Mostowski looked for characterization of spectra in terms of recursion schemes, or hierarchies of recursive functions, most prominently in terms of László Kalmár's (1943) and Paul Csillag's (1947) elementary functions, the Grzegorczyk hierarchy and hierarchies of arithmetical predicates.

At that time, Scholz's problem was obvious lying in the air: Axiom systems of many theories are non-categorical, so that the question of the classification of non-isomorphic models of such theories arose. Scholz, however, realized that, according to Trakhtenbrot's theorem, the classification of the classes of cardinalities of finite models (of finitely axiomatized first order theories) was non-trivial. Because, according to Trakhtenbrot's theorem, finite validities cannot be axiomatized, i.e. the set of finitely first-order sentences is not recursively enumerable, in contrast to Gödel's completeness theorem which states that validities can be axiomatized, i.e. the set of valid first-order sentences is recursively enumerable – which does not hold for finite models.

In the following years, various ways and attempts to solve Scholz's and Asser's problems were published. Dieter Rödding and Helmut Schwichtenberg, for example, related spectra to n-fold exponential time-bounded deterministic register machine computations, starting with the Grzegorczyk class ${\mathcal{E}}^2$. The authors provided an nth order logical description of n-fold exponential time-bounded register machine computations and showed that nth-order spectra form a strict subelementary hierarchy and exhaust the class of Kalmár-elementary sets (Schwichtenberg 1972).

Another example: Neil D. Jones and Alan L. Selman related first-order spectra to non-deterministic time bounded Turing machines (Jones and Selman 1974). They showed that a subset of $\mathcal{N}$ is a spectrum iff it can be accepted by some nondeterministic Turing machine in time $2^{O\left(n\right)}$. It follows that if $\mathcal{NP}$ is closed under complements, i.e. $\mathcal{NP}$ = co-$\mathcal{NP}$, then spectra are also closed under complements. Consequently to show that spectra are not closed under complements is at least as difficult as showing $\mathcal{NP}\ne$ co-$\mathcal{NP}$, and hence $\mathcal{P}\ne \mathcal{NP}$.

During the late 1970s, 1980s and 1990s, several results were published that generalized Jones and Selman's result to higher order spectra on the one hand, and that refine this result, in order to obtain correspondences between certain complexity classes and the spectra of certain types of sentences. Here came descriptive complexity and its applications to database theory and to computer-aided verification into play. A ground breaking theorem of this area was Fagin's theorem which states that the set of all properties expressible in existential second-order logic is precisely the complexity class $\mathcal{NP}$. This gives a precise correspondence between a logic and a complexity class: a property of finite structures is decidable in non-deterministic polynomial time exactly when it is definable in existential second-order logic (Grädel et al. 2007, 144).

That said, after the first attempts on Scholz's problem (the works of Mostowski and Asser), the breakthroughs by Jones and Selman and later by Fagin considering generalized spectra, quickly connected these kind of questions with similar ones in the early days of complexity theory. So, from the early 1970s the field of finite model theory developed independently with motivations that were more and more influenced by (theoretical) computer science.

Recall also that in that period (early 70s) the relational model was mainly adopted in databases (followed by the design of the SQL programming language) and that early results in finite model theory could also be interpreted as studies of expressive power of logical formalisms in computational terms which appears to be very helpful for the design of database query languages and algorithms. In particular, complexity theory and databases allowed for the development of finite model theory beyond the early question.

Despite the plethora of exciting results in finite model over the past fifty years, a couple of questions and problems remain open. Just to mention one example: In 1981, Christian Blatter and Ernst Specker gave an application of logic to combinatorics dealing with modular periodicity of combinatorial sequences (Blatter and Specker 1984). This arguably was the first statement of a ‘meta-theorem’ in finite model theory. It states that combinatorial sequences (counting functions) definable in monadic second order logic are ultimately periodic modulo every integer m. In current research some extensions and limits of the Specker–Blatter theorem are discussed and new applications are tested (Fischer and Makowsky 2003).

3. Conclusion

This paper aimed to shed light on some aspect of logic and its history which are not well known within the community of philosophers and historians of logic. Connections between logic and computer science are often more associated with proof theory than through a model theoretic point of view.

One of the lessons we can learn from the history of the spectrum problem is the heuristic power of ‘innocent’ problems for research. This is not that a problem is given and then solved. And, after the solution is put aside, a new problem is presented. Heinrich Scholz's ‘innocent question’ inaugurated the development of finite model theory and descriptive complexity. Thus, it inaugurated a new research program across disciplinary boundaries.

Another lesson to be learned from the early history of the spectrum problem is a political one—concerning the transnational collaboration between East and West. The collaboration of scientists across discipline and national boundaries is essential to the effectiveness of problem-solving and innovation, not only in mathematical logic, but in science in general. Committed to this research ethos, Scholz deliberately ignored national, political, social, and disciplinary boundaries in his constant search for justifiable and provable exhaustion of epistemological limits within a spectrum of theoretical possibilities.

Notes

1 Boris Avraamovich Trakhtenbrot, Ворис Авраамович Трахтенброт, also spelled ‘Trachtenbrot’, was a Russian-Israeli mathematician in logic, algorithms, theory of computation, and cybernetics.

2 Translated by the author. A slightly different translation is given by Arnaud Durand, Neil D. Jones, Johann A. Makowsky and Malika More (Durand et al. 2012, 506). I have choosen the more literal translation ‘binary predicate variable’ instead of ‘binary relation variable’. Further, I propose to translate ‘Ausdruck’ with the more technical term ‘well-formed formula’ instead of ‘expression’. Some further points make an English translation difficult: Scholz does not use the term ‘domain’ and he speaks of ‘postulates’ instead of ‘axioms ’. In addition, it is not entirely clear what Scholz means by ‘m-zahlig ’, here translated as ‘enumerable elements ’.

3 Scholz's problem inaugurated a new column of problems to be published in the Journal of Symbolic Logic and edited by Leon Henkin. Other questions published in the same issue were authored by Georg Kreisel and Leon Henkin. They deal with a question about interpretations of non-finitist proofs dealing with recursive ordinals and the no-counter-example interpretation (Kreisel), the provability of formulas asserting the provability or independence of provability assertions (Henkin), and the question whether the ordering principle is equivalent to the axiom of choice (Henkin).

4 In his doctoral thesis on the spectrum problem Claude-André Christen pointed out that the problem formulated by Scholz would become trivial if one did not allow predicate calculus with identity (Christen 1976): If then a theory has a model at all, then also a model of every greater cardinality. Scholz's problem would also become trivial if one allowed an axiom system with an infinite number of axioms: Every subset of the set of positive integers is representable in this way, because every finite cardinality can already be characterized with identity without a free variable; the negated formula then excludes precisely this cardinality.

5 German original: ‘zu der Frl. Peter durch ihre schöne Monographie einen neuen vortrefflichen Zugang geschaffen hat. […] Die Arbeit Trachtenbrot ist auch an uns zur Anzeige gekommen. Sie ist in der Tat höchst interessant ’.

6 German original: 'Anregungen, auch den Prädikatenkalkül mit Funktionalen in bezug auf das Repräsentantenproblem zu untersuchen. Ich habe festgestellt, daß im Prädikatenkalkül mit Funktionalen diesselben Mengen von natürlichen Zahlen repräsentierbar sind, wie im Prädikatenkalkül ohne Funktionalen, uns zwar im Falle mit Identität als auch im Falle ohne Identität ’.

7 German original: ‘Demnach entsteht durch die Hinzunahme von Funktionalen keine Erweiterung der Ausdrucksfähigkeit’.

8 German original: ‘Im Anschluß an meine Arbeit über das Repräsentatenproblem im Prädikatenkalkül der ersten Stufe mit Identität hat Herr Prof. Scholz [in einem Brief Mai 24.5.1955] die Frage aufgeworfen, welche Mengen von natürlichen Zahlen im Prädikatenkalkül der ersten Stufe mit Funktionalen definierbar sind. In der vorliegenden Arbeit soll gezeigt werden, daß im Hinblick auf das Repräsentatenproblem und in noch viel allgemeinerer Hinsicht der Prädikatenkalkül mit Funktionalen nicht ausdrucksfähiger ist als der ohne Funktionale’.

9 In a footnote, Asser explicitly refers to Scholz's problem. He also mentions Karl Schröter's support and Hans Hermes and Scholz's joint work on mathematical logic in the first volume of the second edition of the Enzyklopädie der mathematischen Wissenschaften (Hermes and Scholz 1952).