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:

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 functionspaces. 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 nonstrict inequalities, fall into a greater error by saying ``nondecreasing'' 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

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

Representation of orders by subsetinclusion 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
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
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 = {yy\preccurlyeq x} to {yy ~ 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. []