The first greedy construction?

Stream: Equational

[Stanley Burris]

Perhaps historically the first use of the greedy construction was in the second section

Lösung des Problems zu entscheiden, ob eine gegebene Aussage des
Gruppenkalkuls beweisbar ist oder nicht

of Skolem's 1920 paper

Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theorem über dichte Mengen

where he studied lattices, treating the two binary operations as ternary relations, and using the binary relation ⩽ instead of equality =.

Given an initial finite structure with these three relations, he uses among his relational version of the lattice axioms those which were expressed as universal Horn properties (or as he put it, as production rules) to fill out first the binary relation ⩽ and then the two ternary relations on the given domain. His 6th axioms said that the ternary join and meet relations captured the notion that every pair of elements had a join and a meet. He showed that one could make 1-element extensions of his relational structures to gradually realize these axioms without distorting what had been achieved on the original domain. The union of the resulting tower of finite structures was a "relational" lattice. (To get a modern "functional" lattice one needs to mod out by the equivalence relation determined by the quasi-order ⩽.)

In modern terms, what was particularly notable about his result was that it gave a polynomial time algorithm to decide if partial tables on a finite set for the join and meet operations gave a partial algebra that could be embedded in a (possibly infinite) lattice, and thus a polynomial time algorithm for the word problem for lattices, and for the universal Horn theory of lattices. This implies that the universal theory of lattices (the universally quantified sentences true for lattices) was decidable. (The first-order theory of lattices is undecidable.)

As an example he used it to show that the distributive law did not follow from the axioms for lattices .

Perhaps as a spin-off of the work on greedy constructions in the study of magma equations one also has some results on the word problem, etc., for certain magma equations?

[Terence Tao]

Thanks! I've added a reference to this in the paper at the begnning of the greedy section.

The proof of the Godel completeness theorem is arguably another greedy construction, although that was a few years after Skolem's paper.

[Stanley Burris]

A two-page note "Skolem 1920 Greedy" has been added to my PR to describe how Skolem used the Greedy construction in 1920 to justify his algorithm to determine which universally quantified first-order sentences hold in what are now called lattices. One of his examples was the application of this algorithm to show that the distributive law does not hold in all lattices---this example is described in the note.

P.S. When Bill McCune used his computer to prove the Robbins' Conjecture concerning axioms for Boolean algebra ca 1990 I thought the revolution in computer assisted theorem proving was here. Perhaps now it really has arrived!