Practical Foundations of Mathematics

Paul Taylor

7.6  From Semantics to Syntax

When we introduced categories in Chapter IV we saw how they capture both semantic things such as topological spaces, and also the syntactic category of contexts and substitutions. The latter has chosen products, function-types etc simply because these have symbolic names, with rules which say just this. In order to give specific values to the interpretation functor [[-]]:Cn[]L S, we therefore have to choose products and function-spaces in any category S in which we want to define semantics. On the other hand, mathematical intuition is that there is no God-given choice of the product of two topological spaces: these objects may always be interchanged with isomorphic copies.

Consequently there are strong and conflicting opinions about whether, when we say that a category has products etc , we mean them to be chosen or merely to exist. The second point of view is important even in formal reasoning, as a systematic way of discarding type-theoretic detail, cf Example 2.4.8. This conflict, to which we have referred in Sections 1.2, 4.5 and 7.1, is the price we have to pay for the versatility of category theory, but now we intend to resolve it, showing that it amounts to the difference between strong and weak equivalences .

Logicians, when they have considered semantics at all, have traditionally called it complete if there are enough models in a fixed universe of sets to distinguish the syntax (Remark 1.6.13). That is, if L\vDash f, ie some property f holds for all models of a theory L, then it is provable ( L\vdashf). We have already achieved this goal (for the fragments of logic we have discussed) by opening out the universe to encompass models built from the syntax itself. Now we want to go further, and treat syntax and semantics as equals - literally - requiring completeness of the syntax for the semantics as well as vice versa .

We aim to construct a language L from any suitable given category C, such that C @ Cn[]L. Theorem 4.2.12 did this for the unary case, where the structure [] just consisted of identities and compositions: the canonical elementary language L = L(C) has a type \qq X for each object of C and an operation-symbol \qq a for each C-morphism. L also names as laws all of the equations which hold in C, so \qqdash preserves the structure [], ie it is a functor, and \CloneL C by Theorem 6.2.8(c).

Recall that we also called L an elementary sketch. Although we shall describe the language for products etc symbolically, many of the ideas of this section come from sketch theory (and others from sheaves).

Encoding operations   We shall consider those connectives [] of type theory which are characterised by universal properties: products, sums, exponentials, quantifiers, List(-) and P(-), but not tensor products.

REMARK 7.6.1 Suppose that the objects X and Y have a product P and a sum S in a category C. This means that there are C-maps

X     p0    P     p1    Y           X     n0    S     n1    Y
satisfying certain universal properties, but we shall ignore the latter for the time being. Adding product and sum types to the canonical elementary language, together with the pairing and case analysis meta-operations, in the syntactic category Cnx+ there are morphisms
\qq P     \qq p0,\qq p1    \qq Xx\qq Y        \qq S     [\qq n0,\qq n1]    \qq X+\qq Y .
Although they are interpreted as identities in the intended semantics, these maps are not invertible in the syntax (or in arbitrary models of it) as it stands. So if we want P to name the product we must add
x:\qq X,y:\qq Y\vdash \pairX,Y,P(x,y):\qq P
as a new symbol ( encoding operation) of the language, with b- rules

\qq p0(pair(x,y))\leadsto x       \qq p1( pair(x,y))\leadsto y

and an h-rule pair(\qq p0(z),\qq p1(z)) = z, which force pair to be the inverse of \qq p0,\qq p1. The definable operation for the sum goes in the opposite direction, so the encoding operation is

z:\qq S\vdash split(z):\qq X+\qq Y.
This difference is attributable to the fact that they are given by right and left adjoints, respectively. In the generic case we shall write

omitted diagram environment

for the encoding operation, in the ``product'' direction.

REMARK 7.6.2 P need not be the chosen product. Let a:Q P be a semantic isomorphism, so we have another product diagram in C ( cf Theorem 4.5.6), and the composite \qq ao\pairX,Y,P obeys the laws for \pairX,Y,Q. Since inverses are unique, if this operation had also been named it would be provably equal to the derived form. For a semantically given category, therefore, it is harmless to name all of the diagrams (or as many as we please) which satisfy the universal property.

On the other hand, some diagrams may be products ``accidentally,'' not because we intended them to be. If we omit the corresponding pair encoding, we get a new product (that is, the syntactic product will not be isomorphic to the unwanted semantic one). Including its encoding operation in the language is how we give our approval to a particular semantic product, and this will ensure that the functor \qqdash preserves it.

EXAMPLE 7.6.3 The theory of monoids was given in Example 4.6.3(f) by a finite product sketch. A traditional syntactic account would say that multiplication has two (separate) arguments, but in this section all operations are treated as unary. We introduce a new object M(2) to be the source, and have to give additional information to force M(2) to be MxM. This is what the upper parts of the diagrams in Example 4.6.3(f) say. An interpretation of this finite product sketch in any category S with finite products is an interpretation of the underlying elementary sketch for which M M(2) M becomes a product cone in S. We have just described the syntax which is needed to do the same thing.

EXAMPLE 7.6.4 The canonical elementary language of a poset (S, ) lists the elements of S and all instances of the order relation between them; a general language L of this kind is simply a set S with any binary relation < , and \CloneL is the reflexive- transitive closure (Section 3.8).

Analogously to Cn×L we have the classifying semilattice Cn\landL of a Horn theory (S,\triangleright ) constructed in Theorem 3.9.1. By Proposition 3.9.3, any meet-semilattice arises in this way, where, if we want to specify that p = xy, we must add this fact to the language L, by writing

{x,y}\triangleright p        or       pair :\qq x\qq y \qq p
in the notation of the two sections. Otherwise we get Example  3.2.8.

Canonical language   The tradition of sketches is a minimalist one: to include only enough objects to determine the theory. We also want to show that categories which have all finite products, specified or not, arise as classifying categories. To deal with each of these applications, we give three versions of the definition.

The equational laws ought be treated in the same way as the additional structure such as products and function-types. However, it is technically simpler to assume in part (a) below that the unary part of the structure, which includes all of the equational laws amongst expressions, has been dealt with already (we did this in Theorem 3.9.7 for the lattice case too). The underlying elementary sketch is therefore a category.

To this we add encoding operations such as pair, split and (for function-types) \abs , together with the b- and h-rules that force them to be inverse to the corresponding definable operation in Remark 7.6.1.

DEFINITION 7.6.5 A language L for a small category C is

a subcanonical language for C if it consists of (the whole of) the elementary language L(C), together with some encoding operations for constructions which obey the appropriate universal properties in C (there need only be a few of these, or maybe none at all, but it is important that we only nominate products etc for the language if they really were products in the semantics, cf Definition 3.9.6(b)) ;

the weakly canonical []-language L [](C) if it has at least one encoding operation for each tuple of sub-types;

a strongly canonical []-language for C if it has exactly one object and one encoding operation for each tuple of sub-types. That is, it makes an assignment of []-structure, which it registers by including these particular encoding operations in the language. (The word ``canonical'' is carrying two senses here: the plain English one that it is making a choice, and the one from sheaf theory, Definition 3.9.6, that it accounts exactly for all of the semantic structure.)

In the last case the interpretation [[-]] of L in S is defined, by Remarks 4.6.5, 4.7.4 and 5.5.2. Besides the operations and meta-operations of [], it must define the elementary language ( ie the objects, maps and composites) of C , and the encoding operations. These must be

[[x:\qq X]] = X        [[\qq a(x)/y]] = a       [[e]] = id,
where e is the encoding operation for the chosen product, etc .

The quoting operation \qqdash preserves just that structure of C which L names. In particular it is a functor because the identities and composites \qq a;\qq b = \qq a;b are named as laws of L.

REMARK 7.6.6 Let X P Y be any cone in C.

The functor \qqdash sends it to a product cone in Cn[]L iff there is some definable term pair in the syntax such that pair:\qq Xx\qq Y \qq P. Either pair is an encoding operation obeying the b- and h-rules above, or there is some other definable term which does this job.

In this case \qqdash is full and faithful for morphisms G P iff P was a product in the semantics, since otherwise \qq P has mediators in Cn[]L which either did not exist or were not unique in C ( cf subcanonical coverages, Definition 3.9.6).

PROPOSITION 7.6.7 The role of categorical equivalence.

Let (F,U,h,e):C @ D be a strong equivalence of categories, where D has assigned categorical structure of some kind, such as products. Then the equivalence transfers it to C.

Suppose that products etc exist as a property in D and that there is an equivalence functor F:C D. Then C also has products.


omitted diagram environment

However, the unit h is also needed - and it must be natural - to show that U P = XxCY. []

DEFINITION 7.6.8 The structure [] is said to be conservative if, for any category C and subcanonical []-language L, the functor

\qqdash :C Cn[]L
is full and faithful. That is, every map a:G [x:\qq X] [y:\qq Y] is of the form [y: = \qq a(x)] for a unique a:X Y in C. If the interpretation is defined then a = [[a]], so the issue is uniqueness, ie to show that a = \qq [[a]]; in particular there is nothing more to do in the poset case.

Conservativity is a theorem that we must prove for each fragment [] of structure, along with giving its interpretation. Traditionally, this term means the relative property of the extension of a theory by some new connective, for example adding function-types to algebra. According to our definition, [] is conservative if the extension to the full []-structure is conservative relative to every intermediate structure L.

The equivalence  

THEOREM 7.6.9 Let [] be a conservative structure, C a small category which has this structure and L a subcanonical []-language for C .

Suppose C has and L names a choice of all []-structure; that is, it is a strongly canonical []-language (Definition 7.6.5(c)). Then the corresponding []-type theory has an interpretation [[-]] in C, which is a []-preserving functor, and

the syntax of the canonical language Cn[]L interpretation [[-]] 
\lTo quoting \qqdash   C semantics