Practical Foundations of Mathematics

Paul Taylor

3.1  Posets and Monotone Functions

DEFINITION 3.1.1 A poset is a set X together with a binary ``order'' relation £ which is reflexive, transitive and antisymmetric:

EXAMPLES 3.1.2 The following are posets:

(a)

any set with the discrete order, x £ y iff x = y;

(b)

N, Z, Q and R with the usual arithmetical order;

(c)

N with the divisibility order, n| m iff $k .n k = m;

(d)

the two-element set {^,T} with ^ £ T but T\not £ ^;

(e)

P(X) with the inclusion order, Ì , for any set X;

(f)

in particular W = P(·), the type of propositions or truth values under implication, which is reflexive and transitive; antisymmetry in this case is the h-rule for the powerset, which says that inter-provable propositions are equal (Remark  2.8.4);

(g)

the set of open subsets of a topological space under inclusion;

(h)

the set of subgroups of a group, and so on.

(i)

The specialisation order between points in a topological space,

x £ y     if    "U Ì X open. x Î UÞ y Î U,

is in general a preorder; the space is called T₀ if the specialisation order is antisymmetric, and T₁ if it is a discrete order ( cf Leibniz' Principle, Propositions 2.8.7 and 3.8.14).

(j)

The ``bracket nesting'' order on sub-expressions may be regarded as a poset, but its purpose is structural recursion, for which a well founded (and in particular irreflexive) relation is needed.

(k)

Formulae form a preorder under prov ability (\vdash , Definition 1.4.7), though there may be many different proofs.

(l)

Expressions form a preorder under reducibility (\leadsto , Definition 1.2.3), though there may be many different reduction paths.

Remember that the transitivity of a relation has significant mathematical force: don't assume it without checking it ( cf Example  9.4.9(d))!

The word poset is a corruption of ``partially ordered set,'' where a total or linear order is one satisfying

DEFINITION 3.1.3 The earliest use of order relations was arithmetical, where the reflexive order ( £ ) is accompanied by an irreflexive relation ( < ) of equal importance. N, Z and Q have the trichotomy property,

Posets are partial in the sense that there may be pairs of elements which are incomparable, ie fail to stand in the order relation either way round, cf Galileo's remarks after Proposition  2.8.8. (This is what people usually mean by ``equality '' in politics.) As there is no connection between total orders and total functions, or between linear orders and preserving sums, it is best to forget these terms and treat ``poset'' as a bona fide English word for the fundamental notion that it is.

Moving away from arithmetical examples, trichotomy usually fails for posets arising in logic, and is destroyed by products and function-spaces. Imposing trichotomy can be a nuisance in technical situations ( cf Corollary 3.5.13, but see the ordinals in Section  6.7). It has also given rise to a great deal of misleading terminology. For example, without trichotomy, x\not > y (``no more than'') is no longer a synonym for x £ y (``at most''). Some authors, whilst trying to be careful about non-strict inequalities, fall into a greater error by saying ``non-decreasing'' for monotone.

The symbol £ , like subset inclusion (Remark  2.2.6), is irreducible, but unfortunately too well established to replace; an arrow would be better, both graphically and theoretically.

WARNING 3.1.4 Any irreflexive relation < can in fact be recovered from ( < )È( = ), but we need excluded middle to recover the reflexive relation £ from ( £ )Ç( ¹ ) (Exercise 3.3). Sometimes we use < and £ together in the same passage: beware that they are not assumed to be related in this classical fashion.

Monotone functions   Whenever we define predicates such as £ and operations such as Ù, Ú, x or + we are always interested in the functions which preserve them.

DEFINITION 3.1.5 Let (X, £ ^X) and (Y, £ ^Y) be posets (or preorders) and f:X® Y a function. Then we say f is monotone, covariant or order- preserving if

A function which, in the same sense, preserves an irreflexive order is called strictly monotone, cf Definition  2.6.1 for well founded relations.

If we want to say that

EXAMPLES 3.1.6

(a)

The formulae aÙf, fÚa, fÞ a, "x.a and $x.a are monotone functions of the propositional variable a.

(b)

The formulae \lnot a and aÞ f are antitone functions of a.

(c)

The composite of two monotone functions is monotone, as is the identity function.

(d)

A preorder in which £ is symmetric is an equivalence relation. In this case monotone functions are functional in the sense of Remark 1.3.2.

(e)

A bijective monotone function has a (monotone) inverse iff it is full.

(f)

Recall that any function f:X® W is a predicate and so defines a subset U = {x|f(x) = T} Ì X by  comprehension, and conversely by f(x) = (x Î U) ( cf Definition  2.2.5 and Notation  2.8.2).

For a poset X, the function f is monotone iff U is an upper set:

"q,x:X. q ³ x Î UÞ q Î U.

We write x¯ X = {q|x £ q} for the up-closure of the singleton x, ie the upper set which it generates.

Representation of orders by subset-inclusion   The fundamental example of an order relation is provability, to which implication and the containment of subsets are immediately related. Example 3.2.5(f) shows that this also accounts for the arithmetical orders.

DEFINITION 3.1.7 An antitone predicate on X, ie a monotone function X® W^op , defines a lower set A Ì X,

Using lower subsets, every partial order may be seen as an inclusion order. This is called the covariant regular representation. We introduce this terminology here, while the technology remains simple, to prepare for the Yoneda Lemma for categories in Sections 4.2 and 4.8.

PROPOSITION 3.1.8 Let X be a poset and x,y Î X. Then

(a)

(X¯ x) Ì (X¯ y)Û x £ y, ie the function X¯ (-):X® shv(X) is monotone and full;

(b)

for any lower set A Ì X, we have X ¯ x Ì AÛ x Î A. []

Upper sets provide a similar contravariant representation. There are two different senses of ``representation'' here: a subset of the form X¯ x is represent ed by the element x, whereas shv(X) represent s the poset  X.

EXAMPLE 3.1.9 Consider a collection of propositions (a Lindenbaum algebra, Remark 1.4.6), ordered by provability. Then

(a)

the covariant regular representation represents a proposition f by its reasons, ie the set {g| g\vdash f} (a ``reason'' for something may be some other assumption, from which the thing follows), and

(b)

the contravariant representation (using upper sets) represents f by its consequences, Cn(f) = { q|f\vdash q} (Notation  2.4.12). []

The regular representation of a preorder identifies x and y iff both x\preccurlyeq y and y\preccurlyeq x, since then X¯ x = X¯ y. We may cut down the representation from X¯ x = {y|y\preccurlyeq x} to {y|y ~ x}.

PROPOSITION 3.1.10 Let (X,\preccurlyeq ) be a preorder. Then

Moreover if Q is any poset and f:X® Q is a monotone function, then x ~ yÞ f(x) = f(y) and there is a unique monotone function p:X/ ~ ® Q such that f = h;p.

omitted diagram environment

PROOF: First, ~ is reflexive and transitive because \preccurlyeq is, and symmetric by construction. So it is an equivalence relation, of which Example 2.1.5 gave the quotient X/ ~ as the set of equivalence classes, together with the mediating function p. We want [x] £ [y] if x\preccurlyeq y; this is well defined because, if x ~ x¢, y ~ y¢ and x\preccurlyeq y, then x¢\preccurlyeq y¢ by transitivity. Then £ inherits reflexivity and transitivity from \preccurlyeq , and is antisymmetric on equivalence classes by construction of ~ . Finally, p is monotone. []