# Practical Foundations of Mathematics

## 3.7  Closure Conditions and Induction

For any adjunction F\dashv U, it is an easy corollary of Lemma  3.6.2 that the composite M = UoF is idempotent, and in this section we concentrate on its fixed points. In the common situation where the ambient poset S is a powerset P(X), the fixed points of M are often called closed subsets of X. They feature in analysis as those subsets which contain the limits of their convergent sequences. Maurice Fréchet's approach to general topology (1906) was to consider the operations which take an arbitrary subset X to the smallest closed set containing it (often written [`(X)], but called MX here), and to the largest open set inside it (its interior).

DEFINITION 3.7.1 A monotone endofunction M:S® S of a poset such that \idS £ M = MoM is called a closure operation.

LEMMA 3.7.2 For any adjunction, U is injective iff F is surjective iff Fo U = \idA . Every closure operation M arises as UoF like this, where

omitted diagram environment

split the idempotent M (Definition 1.3.12); F takes an element X to the least A which is a fixed point of M above X (Remark 3.6.3). []

PROPOSITION 3.7.3 Let A Ì S be the image of a closure operation, so meets in A agree with those in S by Proposition  3.6.8. To calculate joins in A, we first find them in S and then apply the closure operation. A is already closed under any joins the closure operation preserves. []

In particular, topological closures preserve finite joins, and the finitary closure operations which arise in algebra are Scott-continuous.

Closure conditions   Behind this static definition lies a dynamic point of view, which leads us into a notion of induction. Unfortunately the established terms ``operation'' and ``condition'' convey exactly the wrong idea. This kind of induction is actually more general than that treated in Section  2.5, as it allows for the non-deterministic recursive paradigm which lies behind resolution with backtracking in logic programming.

Given any subset X of some space, let TX be the set of limits t (in the sense of analysis) of sequences (\termui) Ì X. Now TX need not be closed, so we form the set T2X of limits of sequences (\termui) Ì TX , and so on, but, unlike Proposition 3.3.11, even ÈnTnX need not be closed. Nevertheless, MX exists by the Adjoint Function Theorem 3.6.9.

DEFINITION 3.7.4 A system of closure conditions on a set S is given by any relation \triangleright :P(S)\leftharpoondown\rightharpoonup S, without restriction. Then a subset A Ì S is said to be \triangleright -closed if

 "K Ì S."t:S.    omitted prooftree environment
so for example in analysis we would write ``sequence \triangleright limit.'' We shall also write L = (S,\triangleright ) and call A a model of (or algebra for) L.

Let A º Mod(L) be the set of \triangleright-closed subsets, ordered by inclusion, and U:Mod(L)\hookrightarrow P(S). Since this is closed under intersections , the Adjoint Function Theorem 3.6.9 gives F\dashv U, and we call F(X) the closure of X Ì S. (We shall write FX Î A for the closure considered as a model or closed subset, and MX Î S for its underlying set.)

The left hand side of K\triangleright t is called the arity of this instance of the closure condition: the choice of letter reflects our use of k for the arity of operation-symbols. If this is always a finite set, we sometimes write it as a list, and say that \triangleright is finitary.

EXAMPLES 3.7.5 There are many familiar binary closure conditions.

(a)
If \triangleright is a functional relation such as
 {u,v}\triangleright u+v,        ie   "u,v:S.  u,v Î AÞ u+v Î A,
then \triangleright -closed subsets are subalgebras with respect to +.

(b)
Convexity in an affine space: {u,v}\triangleright l u+(1-l)v for 0 £ l £ 1.

(c)
Convexity for an order: {u,v}\triangleright t whenever u £ t £ v.

(d)
Transitivity is a closure condition on pairs (instances of £ ),
 {(x,y),(y,z)}\triangleright (x,z),
rather than on elements. Reflexivity and symmetry are nullary and unary conditions on pairs: Æ\triangleright (x,x) and {(x,y) }\triangleright (y,x).

(e)
Ideals and normal subgroups are subgroups satisfying an extra unary closure condition: {u}\triangleright ru or {u} \triangleright a-1ua respectively.

REMARK 3.7.6 A nullary closure condition Æ\triangleright t says that t must be in every closed set. If \triangleright consists only of such conditions, for t Î G, then F(X) = GÈX and A is the upper set G¯ S (Example  3.1.6(f)).

For any system of closure conditions, in order to find the closure F(G) of a set G (of generators), we may instead consider the extended system \triangleright ¢, with an extra nullary closure condition Æ\triangleright ¢x for each x Î G. We write \triangleright +G for \triangleright ¢. Without loss of generality we therefore need only consider F(Æ), which is the smallest \triangleright -closed set, so long as we study closure conditions in general, for example in Corollary 3.9.2.

Unary closure conditions are considered in detail in the next section.

REMARK 3.7.7 In any situation A Ì S, we may always regard S as a set of propositions: each element x:S names the proposition ``x Î A .'' Then we can read any finitary closure condition

 {f1,¼,fk}\triangleright q       as     f1Ù···ÙfkÞ q ,
ie a propositional Horn clause (Remark  1.7.4). A nullary condition is called an axiom. Conversely, any (single, predicate) Horn clause is a scheme of closure conditions given by instantiating terms for its free variables. A system of finitary closure conditions is therefore also called a Horn theory (a system of Horn clauses involving predicates is the dependent type analogue, Chapter VIII).

In logic programming (Remark 1.7.2), the collection of terms generated by the constants and operation-symbols (of the underlying term calculus) is known as the Herbrand base, and the set S of all instances of the predicates is the Herbrand universe. A program is then a Horn theory.

Induction on closures   Each instance K\triangleright t of a closure condition may be seen as an introduction rule for the (term t of) type A = F(Æ). Conversely there is an elimination rule, with a premise corresponding to each case of introduction. This manifests itself as an induction scheme, which is to propositions what structural recursion is to types.

DEFINITION 3.7.8 The induction scheme for a system of closure conditions  \triangleright  is

 omitted prooftree environment
where A = F(Æ) is the smallest closed subset. This is valid because the premise says that Q = {x:S|q[x]} is itself a \triangleright -closed subset.

EXAMPLES 3.7.9

(a)
By Remark 3.7.7, the induction scheme says that if the Horn clauses are sound then all of the propositions in A = F(Æ) are true.

(b)
Structural induction is of this form, eg to prove associativity of concatenation of lists (Proposition  2.7.5), put

 t\triangleright cons(h,t)    and    q[x] = æè "l1,l2.(x;l1);l2 = x;( l1;l2) öø .

(c)
Course-of-values induction on N is given by {0,1, ¼,n-1}\triangleright n.

(d)
The correctness of a logic program is established by induction on the system of closure conditions which it codes. Conversely, any Horn theory has a procedural reading, the goal being to prove x Î A.

(e)
For any binary relation \prec on a set S, let {u |u\prec t}\triangleright t for each t Î S. Then induction on \triangleright as a closure condition is the same as well founded induction for \prec (Definition 2.5.3).

(f)
To recover \prec from \triangleright , for each t Î S there must be a unique set K with K\triangleright t. (It's called parse(t) in Example 6.3.3 .) This typically fails for subalgebras, for example {u,v} \triangleright u+v in a vector space does not allow the recovery of u and v. It is also the reason why backtracking is needed in logic programs (Remark 1.7.3).

Using results from earlier in this chapter, we can derive stronger idioms of induction for the set A = F(Æ). In particular, there is a `` systematic'' way of generating it.

LEMMA 3.7.10 Define T:P(S)® P(S) by

 TX = {t:S|\$K.K Ì XÙK\triangleright t },
ie the application of the conditions once. Then A is \triangleright -closed iff TA Ì A, and the smallest \triangleright-closed subset of S is the least fixed point of T. Every monotone endofunction T arises in this way, with K\triangleright ¢t if t Î TK. Then any subset is \triangleright ¢-closed iff it is \triangleright - closed, though the original \triangleright itself cannot be recovered from T. []

Exercises 3.40 and 3.42 give the induction scheme in terms of T. We can use induction on closure conditions to investigate the least fixed point.

PROPOSITION 3.7.11 Let S be a complete (join-semi)lattice and T a monotone endofunction of it. Then T has a least fixed point A Î S, whose properties may be deduced from the following induction scheme:

 omitted prooftree environment

PROOF: Define a closure condition on S = S by Á\triangleright ÚÁ for all Á Ì S, and also {U}\triangleright T(U). (Notice that we have not said U ³ VÞ U\triangleright V: see Exercise  3.41. Nor is this the closure condition derived from T in the lemma.) In particular Æ\triangleright ^, and any closed subset A has a greatest element A = ÚA Î A. By \triangleright -induction, "X.X Î AÞ X £ T(X), whilst "X.X Î AÞ X £ q for any fixed point q = T(q). But T(A) Î A so A = T(A) is the least fixed point of T. Other properties of A may be proved by instantiation of \triangleright -induction at A Î A = F(Æ). []

REMARK 3.7.12 For finitary closure conditions, the function T defined in Lemma  3.7.10 is Scott-continuous, and F(Æ) = \dirunionn Î NTn(Æ) is the least fixed point by Proposition 3.3.11. Then in the induction scheme it is enough to consider countable directed subsets Á, or just w-sequences. This idiom of induction is due to David Park (1976). When S = P(S), as in Lemma  3.7.10, this construction says that if X Î F(Æ) Ì S then X Î Tn(Æ) for some n. Classically, the least such n is called the rank of X, but in general this is not well defined intuitionistically.

It is a common but very clumsy idiom to prove something over a closed set by induction on the first time n when each element X gets in. For example, the rank of a goal in a logic program is the depth of its proof tree, which gives a lower bound on the execution time. But it is both difficult to calculate, and extremely crude, as the corresponding upper bound is kn, where k is the maximum arity. As in Remark 2.5.7, the assumption that n is least is unnecessary: it would be clearer to use induction on the closure condition directly. By Lemma  3.7.10 these two idioms of induction are equally expressive.

We have seen that Tarski's Theorem can be proved without the Scott-continuity assumption, and so can properties of the least fixed point:

THEOREM 3.7.13 Let \triangleright be a (possibly infinitary) system of closure conditions on a set S and q[X] any predicate on S = P(S) such that

(a)
q[Æ] holds;

(b)
if q[X] holds and X É K\triangleright t then q[XÈ{t}] also holds;

(c)
if X = È­ \typeXi such that each q[ \typeXi] holds then q[X] holds.

Then q[A] holds, where A is the smallest \triangleright -closed subset.

PROOF: (Thierry Coquand) Let q be the least such predicate. Consider

 f[X]  º  "Y.q[Y]Þ q[XÈY] ,
and check that it satisfies (a)-(c), so q[X]Þ f[X], since q is least. Then q[X]Ùq[Y]Þq[XÈY], so q preserves arbitrary unions by (a) and (c), and there is a greatest \typeX0 with q[\typeX0] by the adjoint function theorem. By (b), \typeX0 is \triangleright -closed, so A Ì \typeX0. The predicate y[X] º (X Ì A) also satisfies the conditions, so q[X]Þ y[X] and A = \typeX0. []

Classically, the least fixed point can be approached by a transfinite union, which we investigate in Section 6.7, but Exercise  3.40 defines an intrinsic notion of ordinal for a particular problem.

For the obvious reasons of constructivity, we are primarily interested in finitary algebra, and we shall find in Section 5.6 that there is a significant obstacle to the extension of equational reasoning to infinitary operations. Why, then, should we be interested in infinitary algebra at all? Since there is a duality between finiteness and (infinitary) directed joins, the more we concentrate on the finitary, the more we need to know about infinitary operations and Scott-continuous functions between domains.

Section 3.9 considers the lattice of models of any Horn theory, and the semilattice which ``classifies'' models, making use of induction on closure conditions. We shall study algebraic theories in Section  4.6, using closure conditions in Sections 5.6 and 7.4 to impose relations. Recursion for free algebraic theories is the subject of Chapter  VI. Closure operations are generalised to reflective subcategories in Examples 7.1.6 and further to monads in Section 7.5.