L are contexts G , ie lists or finite subsets of elements of S considered as conjunctions of propositions. Recall that, for us, lists on both sides of the turnstile mean conjunction , not disjunction. Remark 1.7.2 showed how to find such a proof. L W is a semilattice homomorphism. At least it is so long as we ensure that it is monotone.
L is made antisymmetric.
But A is also a model, satisfying exactly those propositions that are true in all models, since it is the set of propositions which are in all models. L , as the reflexive-transitive closure of two generating cases, will be developed in Sections 4.3 and 8.2 . Every semilattice C classifies some Horn theory. The models of a finitary Horn theory form an algebraic lattice. Every algebraic lattice arises uniquely in this way, in the sense that the classifying semilattice is unique up to unique isomorphism.