We shall now use closure conditions to fashion the first of our ``exotic'' worlds containing a generic model, and use it to prove completeness of Horn logic. Actually, it's not very exotic, but really rather common: we show that every semilattice arises in this way, for which we have to set out the socalled ``internal language.'' The aim is to make syntax and semantics equivalent. We prefer to call the language canonical, because the construction first arose in sheaf theory; in particular, the most important closure condition is that under arbitrary unions, called the canonical coverage of a (complete) semilattice. Example 3.8.15(g) showed that this is the Galois dual of the convergence of sequences in analysis with which we opened Section 3.7.
As sheaf theory is outside the scope of this book, we just develop it far enough for lattices to illustrate the connection. The notion of stable saturated (Exercise 3.36) coverage (Definition 3.9.6) is the analogue for posets of a Grothendieck topology on a category, which is itself an intuitionistic version of the forcing technique invented by Paul Cohen (1963) to show independence of Cantor's continuum hypothesis. Saul Kripke used similar ideas to model intuitionistic logic (1965). For a full account, see [ MLM92]; the propositional analogue of this subject, the theory of locales, is expertly described in [Joh82] .
The Lindenbaum algebra for conjunction
THEOREM 3.9.1 For any Horn theory L = (S,\triangleright ) there is a semilattice Cn^{\land}_{L} which classifies its models in the sense that there is a bijection

PROOF: The elements of Cn^{\land}_{L} are contexts G, ie lists or finite subsets of elements of S considered as conjunctions of propositions. The preorder relation \vdash is generated by ( ie is the reflexivetransitive closure of)
Recall that, for us, lists on both sides of the turnstile mean conjunction , not disjunction. So G\vdash D iff each proposition q in D has a proof tree with root q whose leaves are certain subsets of G and whose nodes are instances of the \triangleright relation. Remark 1.7.2 showed how to find such a proof. The union of two contexts defines the meet in this preorder: we can obtain a semilattice in the sense of Definition 3.2.12 as a quotient using Proposition 3.1.10.
omitted diagram environment
In the presence of a subset A Ì S, Remark 3.7.7 gave a propositional meaning, which we now write as [[f]] , to each element f Î S. We extend this to contexts by conjunction, so that [[]]:Cn^{\land}_{L}® W is a semilattice homomorphism. At least it is so long as we ensure that it is monotone. We have to check the two generating cases of \vdash , but clearly [[G,f]]Þ [[G]] . For the other case, A obeys the closure condition K\trianglerightf iff [[K]]Þ [[f]] , so A has to be a model. The restriction to singleproposition contexts recovers (the characteristic function c_{A} of) the model from [[]]. []
COROLLARY 3.9.2 Horn logic is complete in the sense of Remark 1.6.13.
PROOF: The smallest \triangleright closed subset A = F(Æ) Ì S consists of the \triangleright provable propositions, ie f Î AÛ (\proves_{L}f). All such f are identified with T Î Cn^{\land}_{L} when the order on Cn^{\land}_{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.
We deduce completeness by varying \triangleright . Suppose that G\satisfies_{L}q, ie for every model G Ì A Ì S, also q Î A. In particular q Î A = F(G). Consider the theory \triangleright +G in which the propositions in G are added to \triangleright as axioms (Remark 3.7.6). Now A is the smallest closed subset (model) of \triangleright +G, so q is provable in this theory, ie from the hypotheses G in the theory \triangleright. (Notice the change of demarcation of G, cf page 1.1.) []
By the completeness theorem, \vdash coincides with the semantic entailment \vDash in Example 3.8.15(d); then since there are enough models, to prove q we need only show (classically) that there is no counterexample, ie a model which distinguishes q from T.
This way of constructing the relation \vdash in Cn^{\land}_{L}, as the reflexivetransitive closure of two generating cases, will be developed in Sections 4.3 and 8.2.
As promised, we have a stronger completeness result:
PROPOSITION 3.9.3 Every semilattice C classifies some Horn theory.
PROOF: In the canonical language L = L^{Ù} (C) = (S,\triangleright ), S is the set of elements of the semilattice C, with the closure conditions Æ\triangleright T and {u,v}\triangleright uÙv. The elements of the preorder Cn^{\land}_{L} are finite subsets of S, with G\proves_{L}D iff ÙG £ _{C}ÙD, so the quotient poset is the given C. []
Beware that if C = Cn^{\land}_{L0} was the classifying semilattice for some Horn theory (S_{0},\covers_{0}), then the new S is bigger than S_{0} and the systems of closure conditions are also different.
Algebraic lattices Now we consider the lattice Mod(L) of models of a finitary Horn theory. The classifying semilattice is static, and loses the dynamic information in the original theory; as the lattice of models is also static, there is no harm in using the classifying semilattice C to represent the theory in the next result.
THEOREM 3.9.4 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.
PROOF: By Proposition 3.7.3, any directed union of models (\triangleright closed subsets) is a model, and a model is finitely generable in the sense of Definition 3.4.11ff iff it is the closure of some finite subset. By Theorem 3.9.1, models of C correspond to semilattice homomorphisms C® W, and so to upper subsets containing T and closed under Ù. Since such subsets are ideals of C^{op} (Example 3.4.2(d)),

COROLLARY 3.9.5 There is an orderreversing bijection between finitely generated models A Î \A_{fg} and contexts G Î Cn^{\land}_{L}. []
This justifies the name algebraic lattice: recall that subalgebras and congruences were described by Horn theories. In fact any algebraic lattice arises as the lattice of subalgebras of some algebra for some theory.
Any system of (possibly infinitary) closure conditions has a complete lattice of closed subsets. This lattice is algebraic  characterised in terms of directed joins  iff every instance K\triangleright t of the closure condition contains a finite condition K¢ Ì K with K¢\triangleright t. Given that directedness can be defined by a nullary and a binary condition, this result sheds some light on the notion of finiteness, but we shall defer a full discussion (using closure conditions) to Section 6.6.
Adding and preserving joins Now we turn our study of closure conditions back onto the order theory from which it came, repeating for arbitrary joins the treatment which we have just given to finite meets. Beware that we have dropped stability under meets from the way in which the following ideas are usually presented. Recall that P(S) has arbitrary joins, which in fact it freely adds to the set S. Similarly, shv(S, £ ), which consists of the £ lower subsets of a poset (S, £ ), freely adds joins respecting the order £ (Proposition 3.2.7(b)).
Now we want to force some of the joins to have particular values, and in the extreme case retain all joins which already exist in S. This can be done with the closure condition K\triangleright ÚK which we have already met in Proposition 3.7.11, Example 3.8.15(g) and (for Ù) Proposition 3.9.3.
The order relation x £ y can be coded using joins (xÚy = y), and so by a closure condition, as in the previous section. However, we prefer to take the lattice shv(S, £ ) of £ lower subsets as our raw material.
DEFINITION 3.9.6 Let (S, £ ) be a poset. A closure condition \triangleright on S

In particular a coverage \triangleright is subcanonical iff every representable lower subset S¯ x (Definition 3.1.7) is a \triangleright sheaf.
THEOREM 3.9.7 Let \triangleright be a subcanonical coverage for a poset (S, £ ). Write A = shv(S, £ ,\triangleright ) for the lattice of sheaves; these are the elements of shv(S, £ ) which ``think'' that t is the join of K.
For each x Î S, the set h(x) º S¯ x º {a:Sa £ x} belongs to A, and h:S®A is monotone and obeys K\triangleright t Þ h(t) = Ú_{A}{h(u)u Î K}.
Moreover it is universal: let Q be another complete joinsemilattice and f:S® Q a monotone function such that f(t) = Ú_{Q}{f(u)u Î K} whenever K\triangleright t. Then there is a unique function p:A® Q which preserves all joins and satisfies h;p = f.
The map h is also full and preserves arbitrary meets.
omitted diagram environment
PROOF: For a subcanonical coverage, each S¯ x is \triangleright closed, whence h is full and preserves arbitrary meets by Proposition 3.2.7(a). Similarly p(S¯ x) = Ú{f(a)a £ x} = f(x) by monotonicity of f. If the mediator p exists then it must be given by the formula in the diagram, since A = Ú_{A}{S¯ aa Î A}. There is a right adjoint to p, which is given by q® {af(a) £ q}, so p preserves joins.
We can also show that p preserves joins by \triangleright induction. Let \typeA_{i} Î A for i Î Á such that "i.p(\typeA_{i}) £ q Î Q. We have to show that f(a) £ q for all a Î A = Ú_{A}\typeA_{i}, given that it holds for all a Î \typeA_{i}. To satisfy Definition 3.7.8 we need ("u.u Î KÞ f(u) £ q) Þ f(t) £ q whenever K\triangleright t, but this was the hypothesis on f. []
THEOREM 3.9.11 Let \triangleright be a subcanonical coverage on a semilattice (S, £ ). Suppose that it is stable, ie
whenever K\triangleright t and t¢ £ t then {uÙt¢ u Î K}\triangleright t¢.
Then A º shv(S, £ ,\triangleright ) is a frame (Definition 3.6.16) and the left adjoint F of its inclusion in shv(S, £ ) preserves finite meets. If Q is also a frame and f:S® Q preserves finite meets then so does p:A® Q.
PROOF: We always have F(XÇY) Ì FXÇFY. A typical element of the right hand side is aÙb with a Î FX and b Î FY, so consider

Since shv(S, £ ), whose elements we call presheaves, is a frame, and p preserves joins, algebraic manipulation easily shows that A is also a frame, and p preserves finite meets if f does and Q is a frame. []
Generalising from propositions to types The remainder of the book will develop the analogues for categories and types of the poset and propositional ideas in this chapter. In the propositional terminology, Chapter IV studies posets, monotone functions, the transitive closure, universal properties, Horn theories, Heyting semilattices and the pointwise order. The phenomena in Chapter V are largely new to the level of types, but it does discuss distributive lattices (and use closure conditions to construct quotient algebras). Chapter VI is about induction on infinitary closure conditions. Most of the categorical developments are to be found in Chapter VII: adjunctions, closure operations, adding meets and joins, the adjoint function theorem and the canonical language; we only touch on Galois connections, modal logic and sheaf theory. Chapter VIII restores the predicates to Horn theories, and in the final chapter we see how types and propositions interact in the behaviour of the quantifiers.