Practical Foundations of Mathematics

Paul Taylor

3.9  Constructions with Closure Conditions

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 so-called ``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 reflexive-transitive closure of)

(a)

weakening: G,f\vdash G, so D\vdash G whenever G is a subset of D, and

(b)

the axioms: K\vdash f if K\triangleright f.

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 single-proposition 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_Lf). 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_Lq, 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 reflexive-transitive 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_LD 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₀,\covers₀), then the new S is bigger than S₀ 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 order-reversing 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

(a)

is a coverage if whenever K\triangleright t we already have K £ t,

(b)

and is subcanonical if whenever K\triangleright t and K £ x then t £ x; in particular, if x = ÚK then t = x, so the coverage is only used to nominate actual joins for preservation by the embedding h below.

(c)

The canonical coverage of a complete join-semilattice S has K\triangleright ÚK for all K Ì S.

(d)

A \triangleright -closed £ -lower subset A Ì S is called a \triangleright - sheaf or \triangleright -ideal:

x £ a Î AÞ x Î A       K\triangleright t  &  K Ì AÞ t Î A.

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:S|a £ 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 join-semilattice 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¯ a|a Î A}. There is a right adjoint to p, which is given by q® {a|f(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. []

EXAMPLES 3.9.10

(a)

Let Æ\triangleright ^ and {u,v} \triangleright uÚv for each u,v Î S (a join-semilattice). Then A is in A iff it is a directed lower set, so A = Idl(S), which is an algebraic lattice (Definitions 3.4.1 and 3.4.11). The map S\hookrightarrow Idl(S) preserves finite joins by construction, but if S also has meets ( ie it is a lattice) then these are preserved too, cf Exercise  3.17. If S is a distributive lattice then Idl(S) is a frame.

(b)

Let K\triangleright t if K is directed with join t. Then A is \triangleright -closed iff it is Scott-closed (Definition  3.4.7). In fact A = A⁺È{Æ} , where A⁺ is defined in the same way but with K semidirected (so Æ\triangleright ^ and ^ Î A for all A Î A⁺). A⁺ is called the Smyth powerdomain.

(c)

Let K\triangleright t if K is inhabited with join t. Then any inhabited subset A is \triangleright -closed iff it has a greatest element, but Æ is also \triangleright -closed. Then A is the lifting LiftS for complete semilattices, cf Definition  3.3.7.

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. []

EXAMPLES 3.9.12

(a)

Let A Ì X be any subset of a topological space, with the subspace topology, and F:S\twoheadrightarrow A the inverse image induced by the inclusion. This preserves meets and has a right adjoint U. Indeed A is the image of a nucleus M on S, ie a meet-preserving closure operation.

(b)

In particular, if A Ì X is open, then M = (AÞ (-)). In this case, M has a left adjoint AÙ( = ), and A º S¯ A .

(c)

If A is the complementary closed subset to B then M = (BÚ(-)).

(d)

Double negation \lnot \lnot is a nucleus, for which A is a Boolean algebra. The open subsets of X that are fixed by \lnot \lnot are called regular; in R these are unions of non-touching intervals, so (0,1)È(2,3) is regular open but (0,1)È(1,2) isn't.

(e)

Let X and Y be the frames of open subsets of topological spaces X and Y. Put S = Xx Y with the componentwise order. Where a Î X and b Î Y represent open subsets (``intervals'') in X and Y, (a,b) will be the open ``rectangle'' in XxY . Whenever a = ÚK Î X and b = ÚJ Î Y , let {(a,j)|j Î J}\triangleright (a,b) and {(k, b)|k Î K}\triangleright (a,b). This is a stable coverage and shv(S, £ ,\triangleright ) is the Tychonov product, which is the topology on XxY [ Joh82, pp. 59-62].

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.