🚀 go-pugleaf

  The deluge of requests for further information concerning this
matter [*] prompts me to report my latest findings. Horn's original
article, "On sentences which are true of direct unions of algebras"
(JSL Volume 16, No 1, March 1951) has been unearthed from the
Sjoland Archive. I quote from the introduction:

    It is well known that certain sentences corresponding to
    similar algebras are invariant under direct union; that
    is, are true of the direct union when true of each factor
    algebra. An axiomatizable class of similar algebras, such
    as the class of groups, is closed under direct union when
    each of its axioms is invariant. In this paper we shall
    determine a wide class of invariant sentences. We shall
    also be concerned with determining sentences which are
    true of a direct union provided they are true of some factor
    algebra. In the case where all the factor algebras are
    the same, a further result is obtained. ..it will be shown
    that these criteria are the only ones of their kind.

  Now, on examining his results, one finds that he proves that the
formulas Shoenfield calls "Horn formulas" - in our terminology,
formulas in prenex form with a matrix consisting of a conjunction
of Horn clauses [**] - are preserved under direct products. Startlingly,
he also proves the converse, i.e. that every formula preserved under
direct products is equivalent to a Horn formula. Anyway, I was
startled. However, on closer examination, Horn is only concerned
with algebras - structures in which identity is the only relation.
So his theorem characterizes the identity formulas preserved under
direct products. If we allow other formulas, there are counterexamples
to the converse. For example

     (x)p(x,x) & (x)q(x,x) & ExEy(~x=y & (p(x,y) v q(x,y)))

is preserved under direct products, but is not equivalent to a Horn
formula. (By the theorem I quoted earlier, there is no purely universal
counterexample.)


  [*] Somebody I met in the corridor mentioned it.

  [**] The Horn formulas, then, are those formulas that upon prenexification
and skolemization and splitting into clauses - the preprocessing needed
to feed them to resolution theorem provers - turn into a set of Horn
clauses.