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.