Posets and Lattices

O rder structures provide some simple tools for investigating
semantics. For us, they serve a double purpose, describing *systems*
of propositions, and also as the substance of *individual* types.

The *system* of propositions is an order structure with respect to
the provability relation, in which the logical connectives are characterised
as algebraic operations (meet, join, *etc* ) satisfying certain
laws. In the later chapters we shall discuss the analogous operations for
types. For example implication is discussed here briefly using Heyting
algebras, and the function-type in Chapter IV with cartesian
closed categories.

Similar operations, sometimes with weaker laws or in infinitary form, arise
in many mathematical situations beyond logic. For example, the lattice
of sub *algebras* often throws much light on the structure of an algebra,
topological spaces are described by their *open* sets and programs
in terms of partial evaluation. This ubiquity has led some authors to try
to force other concepts such as well founded relations (Section
2.5) into the same mould, a tendency which we aim to reverse.

Our other use of order structures is as *individual* types. As we remarked
in Section 2.2, we need something subtler than sets (as
described by Zermelo type theory) to illustrate many of the phenomena of
reasoning, especially about non-terminating computation. We do this using
posets that have directed joins in Sections 3.3-
3.5. Later in the book we shall give examples where types
are interpreted as topological spaces.

Implication, the quantifiers and infinitary meets and joins are just a few
examples of adjunctions or universal properties. We study them in detail
here because many of the features of this central concept of category theory
can already be seen in the simpler order-theoretic context. In practice,
if a function preserves all meets then its left adjoint tends to be used
formulaically, without appreciating the important *theorem* which
is involved. Here and in subsequent chapters we shall indicate some of the
huge number of mathematical results which can be obtained from simple
observations about adjunctions.

The last three sections are devoted to adjunctions between powersets. To fulfil a promise that everything which is later done for categories is treated first for posets, some material has been included that is disproportionately more difficult than the rest of the chapter, so you should feel free to skip it on first reading. The intermediate status of posets, ambiguously individual types or systems of them, is unfortunately also reflected in some schizophrenic notation.

Sections 1.4, 1.5 and
2.3 defined the logical connectives in terms of their
*introduction* and *elimination* rules. Algebraic operation-
symbols can also be seen as introduction rules; at the propositional level,
these are known as *closure conditions*. They arise as the conditions
for subalgebras and congruences, including reflexivity, symmetry,
transitivity and convexity, and also as logic programs. The corresponding
elimination rules are familiar or novel induction schemes, which Section
3.7 also describes.

The final section introduces the construction of semantics from syntax which will be developed throughout the book.