Practical Foundations of Mathematics

Paul Taylor

3.8  Modalities and Galois Connections

This section characterises the covariant and contravariant adjunctions between full powerset lattices. In each case, the adjunction is fully determined by a binary relation between the sets, and gives rise to useful idioms in many areas of mathematics. We can say more about these idioms when the relation is transitive, functional, etc .

Modal logic   Consider the special case of a system of unary closure conditions, where we abbreviate {u}\triangleright t to u < t. A subset is closed under such a condition iff it is an upper subset with respect to the reflexive-transitive closure £ of < . (Recall Warning  3.1.4, in particular < need not be transitive.) The ``one-way'' closure of a point under a unary closure condition is called its trajectory, and the ``two-way'' closure under a symmetric relation is known as the orbit.

EXAMPLES 3.8.1 The orbits of

(a)

an equivalence relation are equivalence classes;

(b)

u < uⁿ or u < nu in a monoid are cycles;

(c)

u < g^-1;u;g in a group are conjugacy classes.

These examples illustrate that the relation < may arise naturally as a function, and we do not always replace it in our considerations by its transitive closure. For this reason we shall allow the relation < :X\leftharpoondown \rightharpoonup Y to have different sets for its source and target.

Recall that, for finitary closure conditions, the functions U, M and T preserve directed joins, ie ``all but'' finitary joins (Exercise 3.14). In the unary case they preserve all joins, so have right adjoints, which we write as < º T\dashv[ > ] and £ º M\dashv [ ³ ]. It may help to think of x < y as meaning that x is the present and y is a potential future world. Modal logic has medieval and even ancient roots, but its modern study was begun by Clarence Lewis (1918) and models based on order relations were first given by Saul Kripke (1963).

DEFINITION 3.8.2 The modal operators are defined as follows:

omitted eqnarray* environment

for V Ì Y. If the relation is unambiguous, we just write < > and []. With the opposite relation, > U and [ > ]U Ì Y are similarly defined for U Ì X. Other adverbs used for [] include hereditarily and stably.

EXAMPLE 3.8.3 In Sections 4.3, 5.3 and  6.4 we shall show how to prove correctness of (imperative) programs by means of statements of the form U Ì < V and U Ì [ < ]V, ie if the initial state belongs to U then

(a)

some execution which terminates does so with a final state in V, or

(b)

every execution which terminates does so with a final state in V.

For deterministic programs, the first is simply that

(c)

[(a¢)] the program does terminate, and the final state is in V,

which is called total correctness. For terminating deterministic programs, the statements are the same, but partial correctness, that

(d)

[(b¢)] if the program terminates, then the final state is in V,

is more useful for while programs (Remark  6.4.16).

EXAMPLE 3.8.4 Let H Ì G be a subgroup of a group, and u < g^-1;u;g the conjugacy relation (Example 3.8.1(c)). Then the core of H,

Modal logic is the fragment of predicate calculus consisting of formulae with just one free variable. Since the predicate quantifiers $ and " bind a variable, in order to stop the calculus from degenerating altogether, we allow the quantifiers < > and [] to introduce a new free variable for each bound one, by means of a binary relation < .

PROPOSITION 3.8.5 There are adjunctions

omitted diagram environment

so < > preserves disjunction and [] preserves conjunction, and they obey the intuitionistic (\lnot < > = []\lnot ) de Morgan law. They also satisfy

PROOF: < V Ì U and V Ì [ > ]U say respectively that

The usual features of binary relations translate directly into properties of modal operators (Lemmas 3.8.8 and  3.8.12). Since we're interested in < -closed subsets, we consider preorders first, and functions later.

The transitive closure   The following account is due to Gottlob Frege (1879), and is the propositional analogue of the unary treatment of lists in Remark  2.7.10. It will be used for while programs in Section 6.4.

DEFINITION 3.8.6 Let ( < ),Q:X\leftharpoondown \rightharpoonup X be binary relations, which need not be transitive (Warning  3.1.4). Instead of using the binary closure condition on pairs (x,y) that was used to axiomatise transitivity in Example  3.7.5(d), consider the nullary and unary ones

Q Ì S = XxX of pairs); by Definition 3.7.8 it satisfies an induction scheme of the form

PROPOSITION 3.8.7

(a)

£ is transitive,

(b)

it satisfies a base/step parsing rule ( cf empty/head+ tail),

x £ z   Û   x = z   Ú  $y.x < y £ z,

(c)

and a binary induction scheme ( ie it is the transitive closure),

omitted prooftree environment

Proof: These follow from the unary induction scheme for various Q.

(a)

[[a]] Consider xQy º ("z.y £ z Þ x £ z).

(b)

[[b]] Put Q for the right hand side, so D Ì Q and

w < x  Q  z  Û   w < x = z  Ú $y.w < x < y £ z,

which implies w < x £ z and so wQz.

(c)

[[c]] From the premise of the binary rule we have ( < );Q Ì Q;Q Ì Q, so the unary rule applies. []

Modal logic for preorders   This insight into the relationship between [ < ] and [ £ ] will enable us to complete some unfinished business from Section  2.6, where we promised that modal logic would greatly facilitate the study of well-foundedness.

LEMMA 3.8.8 A binary (endo)relation < on a set S is

(a)

reflexive iff > is reflexive iff id £ < iff id ³ [ < ], and

(b)

transitive iff > is transitive iff < ² £ < iff [ < ]² ³ [ < ].

So for a preorder £ , £ = M is a closure and [ £ ] a coclosure.

The propositional calculus extended with these two modalities arising from a preorder is known as the modal logic S4. Both [] and < > split into adjunctions, which combine with those which we identified earlier.

REMARK 3.8.9 For any subset U Ì S, £ U is the down-closure of U and [ ³ ]U is the largest lower subset contained in U, so these closure and coclosure operations have the same image.

omitted diagram environment

Moreover every complete sublattice A Ì P(S) arises in this way. []

An informal way of putting this is that, whereas any closure operation rounds up, in the unary case we can also round down to a closed subset.

The lattices shv(S, £ ) and shv(S, ³ ) are the covariant and contravariant regular representations (Example 3.1.6(f)ff) of £ , or of any relation < of which it is the reflexive-transitive closure.

Now we turn to well founded relations, for which we need

LEMMA 3.8.10 The parsing rule for the transitive (irreflexive) closure is

THEOREM 3.8.11

(a)

The well founded induction scheme (Definition  2.5.3) is equivalent to its strict (Û ) form.

omitted prooftree environment               omitted prooftree environment

(b)

The transitive closure of a well founded relation is also well founded.

PROOF: Put y = [\succ \succ ]q ( hereditarily q, Definition 2.5.4) in both cases.

(a)

[[a]] Suppose that q satisfies the lax \prec - induction premise, [\succ ]qÞ q, and the strict \prec -induction scheme is valid: if [\succ ]y Û y then "x.y[x]. So [\succ ][\succ \succ ]q = [\succ \succ ][\succ ]qÞ [\succ \succ ]q by the lax \prec -premise, but by parsing

[\succ \succ ]q = [\succ ][\succ \succ ]qÙ[\succ ]q Þ [\succ ][\succ \succ ]q, so y º [\succ \succ ]qÛ [\succ ]y. Hence y holds by strict \prec -induction, and a fortiori so does [\succ ]q, whence q follows by the lax \prec -premise again. (The other way is trivial.)

(b)

[[b]] Suppose that q satisfies the \prec \prec - induction premise, [\succ \succ ]qÞ q, and the \prec -induction scheme is valid, ie if [\succ ]y Þ y then "x.y[x].

Parsing says [\succ \succ ]q = [\succ ][\succ \succ ]q Ù[\succ ]q, but this is just [\succ ][\succ \succ ] q, since the first term implies the second by the \prec \prec - premise. So y º [\succ \succ ]q holds by \prec - induction, so q follows by the \prec \prec -premise again. []

Functions and quantifiers   Since modal logic is its unary fragment, in order to recover the predicate calculus we must make use of pairs to encode many-place predicates. Consider (g,x) < g, the product projection p₀ = [^(x)]:GxX® G. For a context G consisting of typed variables, recall that Cn(G) is the set of formulae in these variables. For an extra variable x, there is an inclusion [^(x)]^*:Cn(G) Ì Cn([G,x:X]) called weakening (Remark 2.3.8). Similar results hold for any functional relation in place of p₀.

LEMMA 3.8.12 From Definition 1.3.1, < :X\leftharpoondown \rightharpoonup Y is

(c)

functional (single valued) iff < £ [ < ], iff < preserves binary Ù, iff [ < ] preserves binary Ú, iff < o > £ D, iff id £ [ > ]o[ < ] , iff > o < £ id, where D is the identity relation on Y, cf Lemma  1.2.11 and Exercise  1.16, and

(d)

total (entire) iff [ < ] £ < , iff < preserves T, iff [ < ] preserves ^, iff \idrel_X £ > o < , iff [ < ]o[ > ] £ id, iff id £ < o > .

Injectivity and surjectivity are characterised by similar conditions on the opposite relation. []

REMARK 3.8.13 $x º p₀^op and "x º [p₀^op].

(a)

The adjoints to weakening are the quantifiers, cf Remark 1.5.5. omitted diagram environment Consequently $x.- and "x.- preserve joins and meets respectively.

(b)

For any function, f = [f] = f^* is the inverse image map, and this has adjoints on both sides, the guarded quantifiers, cf Remark 1.5.2.

fop = \funf! = $f \dashv  [f] = f* = f  \dashv  [fop] = \funf* = "f

Such adjunctions give a deeper analysis of the quantifiers in Chapter  IX.

Galois connections   Evariste Galois's name was given to Definition 3.6.1(b), by Ø ystein Ore, not because he spent his short life (1811-32) considering such definitional minutiae, but because the correspondence between intermediate fields and subgroups of the Galois group of a field extension (Example  3.8.15(j)) was the first such situation known.

But the basic properties of the correspondence do not at all depend on groups and fields, so they are repeatedly re-proved in the literature. In fact any binary relation ^:S\leftharpoondown \rightharpoonup A gives rise to a Galois connection. It must not be confused with bottom or falsity, although it often has a negative connotation: for x^a we read ``x is orthogonal to a.''

PROPOSITION 3.8.14 For X Ì S and A Ì A,

omitted diagram environment

Conversely, any Galois connection between powersets is of this form:

The ^-closed subsets on either side are also closed under any algebraic operations or other closure conditions that ^ respects: for example they are automatically subgroups, subfields, etc .

We may also define a specialisation order on S, cf Example 3.1.2(i),

EXAMPLES 3.8.15

(a)

(Abraham Lincoln, 1858) ``You can fool all the people some of the time, and some of the people all the time, but you cannot fool all the people all the time.''

(b)

Let S = A be any set and x^a the inequality relation, x ¹ a, on S. Then \orthr X = S\X , and there are enough As iff \lnot \lnot (x = y)Þ x = y (a presheaf S with this property is separable in sheaf theory).

(c)

Let S = A be a preorder and (^) º ( £ ) its order relation. Then x Î \orthl A iff x is a lower bound for A Ì S, and similarly a Î \orthr X iff a is an upper bound. Then each \orthr X is an upper set and each \orthl A is a lower set. There are enough As iff £ is antisymmetric, and S is a complete lattice iff every closed set is of the form \orthl {a} or \orthr {x}. For S = QÇ[ 0,1], the closed subsets are one-sided Dedekind cuts ( cf Remark  2.1.1).

(d)

Let S be a collection of ``individuals'' and A be some ``properties'' with (^) º (\vDash ) the satisfaction relation. The set \orthr {x} of properties of an individual is closed with respect to the logical connectives. If there are enough properties then \orthr {x} is a description and Leibniz' principle holds, cf Proposition 2.8.7. The specialisation order on properties (\vDash ) is semantic entailment, and it coincides with \vdash iff there are enough models, ie the system is complete (Remark 1.6.13).

(e)

Let S be the set of points and A the set of lines in the plane, with ^ the incidence relation. Then \orthl {a} is the set of points which lie on a line a and \orthr {x} the pencil of lines passing through a point x.

(f)

As a special case of (d), let A be a topology on S and x^a the relation that a point belongs to an open set; this even- handed view is the one taken in [Vic88]. Then \orthr X consists of the neighbourhoods of the subset X and is closed under arbitrary unions and finite intersections. \orthl {a} is the extent (set of points) of an open set. A spatial locale is one with enough points, a T₀ space has enough open sets ( cf Proposition 3.4.9).

(g)

In topology à la Fréchet, let x^a be instead the relation x Ï a. This respects convergence of sequences ( accumulation points) in S and arbitrary unions in A.

(h)

Let S be a vector space and A = (S\multimap K ) the dual space, with x^a if a(x) = 0. Then \orthr X and \orthl A are both called annihilators; they are closed under addition and scalar multiplication.

(i)

Let S = A be a group and x^a the property that they commute. Then \orthr X is the centraliser subgroup for a subset X.

(j)

Let S be a field of numbers, A its group of automorphisms and ^ the relation that the automorphism a Î A fixes the number x Î S, ie a(x) = x. The pair (F,U) is the original Galois connection. Each \orthr X is a subgroup which is closed in a certain topology, whilst \orthl A is a subfield such that if x^p Î \orthl A then x Î \orthl A, where p ¹ 0 is the characteristic of the field.