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
reflexivetransitive closure £ of < . (Recall Warning
3.1.4, in particular < need not be transitive.)
The ``oneway'' closure of a point under a unary closure condition is called
its trajectory, and the ``twoway'' 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^{n} 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,
[]H = {x:G"g:G. g^{1};x;g Î H}, 

is the kernel of the regular action of G on the cosets 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
which is the Frobenius law, cf the I A I syllogism (Exercise
1.25). The relation < can be recovered from
any of the modalities (Exercise 3.65), and every
(covariant) adjunction between powersets arises like this.
PROOF: < V Ì U and V Ì [ > ]U say respectively
that
"x.($y.x < y Î V)Þ x Î U and "y.y Î VÞ ("x.x < yÞ x Î U), 

which are equivalent. The Frobenius law is

æ è

"y.x < yÞ y Î U 
ö ø

Ù 
æ è

$y.x < y Î V 
ö ø

Þ 
æ è

$y.x < y Î UÇV 
ö ø

, 

and x < yÛ x Î < {y}Û y Î > {x}. []
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
Æ\triangleright (x,x) for all x and {(y,z)}\triangleright (x,z) whenever x < y, 

so Q is \triangleright closed iff it is reflexive (
D Ì Q) and "x, y, z.x < y Q zÞ xQz.
We write £ for the smallest such relation (set
Q Ì S = XxX of pairs); by Definition 3.7.8 it satisfies
an induction scheme of the form
omitted prooftree environment 

This corresponds to unary Peano induction for cons and
listrec (Remark 2.7.10). We now show that
£ with this definition is the smallest reflexivetransitive
relation which contains < . The binary closure condition which states
transitivity and its associated induction scheme correspond to
append and fold for lists in Definition
2.7.4ff.
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 wellfoundedness.
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 < ^{2} £ <
iff [ < ]^{2} ³ [ < ].
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 downclosure
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 reflexivetransitive 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
v\prec \prec t Û v\prec t Ú $u.v\prec u\prec \prec t. 

So the transitive \prec \prec and reflexivetransitive £
closures of any binary relation \prec satisfy the parsing formulae
[\succ \succ ] = [\succ \succ ]o[\succ ]Ù[\succ ] and [ ³ ] = [ ³ ]o[\succ ]Ùid. 

Moreover [\succ \succ ]o[\succ ] = [\succ ]o[\succ \succ ]
and [ ³ ]o[\succ ] = [\succ ]o[ ³ ]. []
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 manyplace predicates. Consider
(g,x) < g, the product projection
p_{0} = [^(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_{0}.
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_{0}^{op} and
"x º [p_{0}^{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.
f^{op} = \funf_{!} = $_{f} \dashv [f] = f^{*} = f \dashv [f^{op}] = \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 (181132) 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 reproved 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,
= 2pt omitted array environment 

form a Galois connection S\rightleftarrows A, where
S = P(S) and A = P(A).
(This is what suggested the notation
\leftharpoondown\rightharpoonup for relations in Section 1.3.)
Notice that the implication is in the opposite direction from that defining
[ < ]. By Lemma 3.6.2,
\orthr X = 
æ è

\orthl (\orthr X) 
ö ø

^{^} and \orthl A = \orthl 
æ è

(\orthl A)^{^} 
ö ø

. 

So the composites X® \orthl (\orthr X) and
A® (\orthl A)^{^} are closure operations, and there is an orderreversing
bijection
omitted diagram environment
Conversely, any Galois connection between powersets is of this form:
a Î F({x}) Û x ^a Û x Î U({a}). 

A Galois connection is often presented as the lower set
{X,A 
æ è

X £ \orthl A 
ö ø

º 
æ è

A £ \orthr X 
ö ø

º 
æ è

"x Î X."a Î A. x^a 
ö ø

}, 

which is closed under unions in each component (separately).
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),
which is reflexive and transitive. If this is antisymmetric (a poset)
we say that there are enough A s ( viz
to distinguish the Ss). []
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 onesided 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_{0} 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.
For us, the most important example of a Galois connection will be that defining
the factorisation of functions into epis and monos in Section
5.7, which we shall use to study the existential quantifier
in Sections 5.8 and 9.3. Unary theories
are considered further in Sections 4.2 and
6.4, but the unary closure condition that most concerns
us is invariance under substitution or pullback in Chapter
VIII.