🚀 go-pugleaf

  Since Alfred Horn and preservation theorems are apparently not
universally familiar even among those who subsist largely on a crunchy
diet of Horn clauses, some further remarks are clearly in order.

  Hear ye, hear ye. This is the tale of the Horn clause, as it has come
down to us from the masters of old.

  Preservation theorems were an early development in model theory. The
classical preservation theorems are nice and elementary.

  In mathematics, what is required for a subset G' of a group G to yield
a subgroup? A little reflection tells us that being closed under the group
operation and under inverses will suffice. Associativity and (if we
are talking about Abelian groups) commutativity are taken care of
automatically.

  Similarly with substructures of other kinds of algebraic structures -
fields, linear spaces, and so on. Some of the conditions definining these
structures are automatically satisfied by any subset. What these conditions
have in common is that they can be expressed by purely universal predicate
logic formulas, i.e. formulas

[1]            (x1)...(xn) A(x1,...xn)

where A has no quantifiers. Once we have noted this, it is a simple matter
to prove that all conditions thus expressible are "preserved under
substructures". What this is means is the following:


  T is a theory all axioms of which are purely universal formulas, and
  M is a model of T, then every substructure M' of M is a model of T.


  Now the question inevitably arises whether the converse holds. Or rather,
since theories can be axiomatized in different ways, whether it holds that

  If every substructure of a model of T is a model of T, then T has
  an axiomatization consisting of purely universal formulas.

  The proof of this converse yields the first classical preservation theorem:

  T is preserved under substructures - i.e. every substructure of a model
  of T is itself a model of T - if and only if T has a purely universal
  axiomatization.

  And so it goes on. For every natural way of getting new structures out of
old ones, we try to characterize the theories preserved under that operation.
There are many natural and nice results. For example:


  T is preserved under homomorphic images if and only if T has an
  axiomatization consisting of positive formulas.


  Horn considered a more difficult problem, namely that of preservation
under direct products. The direct product of a (finite or infinite) set of
structures is the generalization of the ordinary direct product of linear
spaces etc.

  Now I don't remember exactly which result Horn formulated (though we have
his original paper somewhere in the archives here at SICS), but as far as
I know there is no natural characterization of the theories preserved under
direct products. However, if we add the condition of being closed under
substructures we get the theorem

   T is preserved under substructures and direct products if and only if
   T has an axiomatization consisting of Horn clauses

where "Horn clause" is the term we now use for formulas of the form [1]
where A is a disjunction of literals (atomic or negated atomic formulas),
at most one of which is atomic.

  (Shoenfield calls them McKinsey formulas, reserving "Horn formulas" for
prenex formulas whose matrix is a conjunction of McKinsey formulas.)