Countable Countermodels: Löwenheim.

Löwenheim's 1915 paper

• opened the door to the serious study of model theory by bringing in the size of an infinite model of a first-order sentence
• gave a canonical procedure to build a countable countermodel to a first-order sentence - this initiated some of the most popular work in automated theorem proving (mainly attributed to Herbrand)
• showed that statements in the first-order predicate calculus (with equality) for monadic predicates which were valid in finite domains were valid in all domains
• pointed out that first-order relational logic with equality was adequate to express all mathematical problems
• showed that one only needed binary relations for the previous item.

This paper was such a turning point in the development of logic that it is worth discussing each section. In particular we will later see how much Skolem was influenced by it.

Löwenheim presents his framework for the paper, namely working in the calculus of relations as presented by Schröder. He introduces first-order statements under the name numerical equations.

Schröder seems to claim that first-order formulas are equivalent to quantifier-free formulas. Löwenheim sketches Korselt's argument that this cannot be the case: a first-order statement asserting the existence of 4 distinct elements cannot be expressed by an equation in the Calculus of Relations.

After thus establishing the usefulness of quantifiers in first-order expressions he turns to a remarkable blending of logic and set theory by showing that

given an infinite domain D and a first-order statement which holds in all finite structures, but not in all structures, then it is impossible for to hold in all structures on D.

In 1920 this would be restated and reproved, by Skolem, to give the famous Löwenheim-Skolem theorem.

The method by which Löwenheim proved this theorem is as fascinating as the theorem itself (indeed more fascinating for those in automated theorem proving). Given a first-order statement , he first puts into a normal form by treating a universal quantifier as an AND over the domain, and an existential quantifier as an OR over the domain; and then distributes to get a disjunctive form. .

From the normal form one takes the universally quantified part and uses the fact that has a model on a given domain iff has. ( will later become the Skolemized form of ). Thus has a countermodel [on a given domain] iff is satisfiable [on that domain].

Next Löwenheim gives a canonical procedure to build a finitely branching tree of finite partial structures, successive nodes being extensions of previous nodes, such that:

• either every branch has a node which does not ``satisfy'' , and this will imply that , hence , cannot be satisfied; or
• some branch is such that every node ``satisfies'' . Then the union of the nodes along the branch gives a countable (perhaps finite) model of , and thus a countable countermodel to .

He claims that he can use his results to establish some independence and dependence results for various systems of axioms of the Calculus of Classes. He only shows how one such system (of Müller) can be expressed in first-order form (using a binary predicate for subsumption), and says he will give details of the independence proofs in a later paper (which never appeared).

Löwenheim goes on to show that such a theorem cannot be proved for higher-order logic because one can write down a sentence which says the domain is not finite or countably infinite. Thus for the first time a powerful distinction is made between first-order and higher-order logics.

The main theorem of this section is that

a first-order sentence with only monadic relations (i.e., relations with only one argument) which is true on all finite domains (no matter how the relations are interpreted) must be true on all domains.

At the end of this section he gives, by example, his algorithm to determine if such a sentence is true on all domains.

Finally he turns to the expressive strength of the first-order calculus of relations, and says that anyone familiar with the development of logic as in Principia Mathematica can see that mathematical assertions can be expressed by first-order statements in the calculus of relations. Then he goes on to show in some detail that it suffices to use only binary relations. (The last statement had been made, without justification, by Schröder in his Vol. III.)

References

1

L. Löwenheim, Über Möglichkeiten im Relativkalkül. Math. Ann. 68 (1915), 169-207. [translated in From Frege to Gödel, van Heijenoort, Harvard Univ. Press, 1971.]