Practical Foundations of Mathematics

Paul Taylor

8.1  The Language

In the mathematical vernacular (Section 1.6), let and suppose introduce hypothetical things and properties. Formally, they expand the context in the sequent style, or open nested boxes in the box presentation. Things introduced by ``let'' are denoted by typed variables. Hypothetical properties may of course depend on entities which have already been introduced in the argument; now the types of the variables may also be dependent on what has gone before. This means that, as a precondition of opening the box or expanding the context, these types must themselves be shown to be well formed.

DEFINITION 8.1.1 The steps in an argument are called judgements. Amongst the direct algebraic steps (those within a fixed context G), we distinguish the following forms:

(a)
Term formation (G\vdash a:X): the term a is well formed and of type X.

(b)
Truth ( G\vdash holdsf): that f is true in the context, ie that there is a well formed proof p of (type) f, where p is implicit in the history of the deduction. This is a special case of the previous form, where we omit proof(-term)s because no distinction is made between them.

(c)
Term equality (G\vdash a = b:X): that a and b are equal qua terms of type X. What notion of ``equality'' we mean needs some discussion.

(d)
Proof equality.

(e)
Type formation ( G\vdash X type or G\vdash f prop ): that X is a well formed type (or f a proposition).

(f)
Type equality (G\vdash X = Y or

G\vdash f = y): that these propositions or types are intensionally equal.

For the postulates at the beginning of an argument we need

(g)
Context formation:
omitted prooftree environment omitted prooftree environment
Having shown that a type or proposition is well formed in a certain context, we may expand the context by a new variable. The rule above belongs to the sequent style; in the box idiom we open a nested box which begins with a term- or proof-formation judgement saying that the new variable x is a well formed term of type X or f.

We discuss context formation in the next section, where it will become clear that we must also say when two contexts are equal, using equality of their types. The provision of arguments of types and operation-symbols also needs formation and equality rules for substitutions.

The idioms which close boxes or make the contexts smaller arise from the quantifiers (Remark 9.1.6 and the whole of the final chapter). For the time being, therefore, boxes never get closed. Despite the boxes and sequents, this chapter generalises, not the predicate calculus as we saw it in Sections 1.4- 1.5, but just resolution of Horn clauses involving atomic predicates, as in PROLOG (Remark  1.7.2ff).

At the algebraic level the only distinction between the behaviour of types and propositions is that elements (terms) of the same set (type) are distinguished , but proofs are anonymous. By giving names to the Horn clauses, proof-terms may be assigned to propositions (Remark 6.2.10); the main point of Section 2.4 was to do the same for implicational logic, using l-terms. Alternatively, we may simply assert that any two proofs of the same proposition in the same context are equal.

The classification of judgements also applies to the rules which justify them. These are the subject of the rest of this section.

Terms   In this chapter, a term is an algebraic expression: just as in Definition  1.1.3, it is either a variable x belonging to the context, or an operation-symbol r applied to (zero or more) sub-terms.

REMARK 8.1.2 Let r be an operation-symbol, from the object-theory. It is applied to arguments,

omitted prooftree environment
where now the types of the second and subsequent sub-expressions may depend on the preceding terms, and the type of the result may depend on all of them. If there is no such dependency, as in Section  4.6, we can allow the sub-expressions to have been born simultaneously - at any rate there is no restriction on their order of formation. If \typeX2 really does depend on \arga1 then we must have had a fragment of proof like

omitted proofbox environment

and so on (with intermediate steps). The operation-symbol r might for example be composition, the types being the set of objects and hom-sets of a category. For propositions r names a Horn clause:

a1,a2,,ak\vdash f.
The arity of an operation-symbol r is given by listing the types on the left and right of the turnstile. Now, in order to express the dependency of the later types, the earlier ones must be accompanied by variables. In the dependent-type situation it is convenient to regard the operation-symbol not as the letter r alone, but as applied to a list of variables:
x1:\typeX1,x2:\typeX2[x1],, xk:\typeXk[x1,,x k-1] \vdash r(
x
 
):Y[
x
 
].
The informal notation r([(a)\vec]) and X[[(a)\vec]] quickly becomes inadequate, so we shall develop a formalism in which the arguments are delivered to r by substitution of [(a)\vec] for [(x)\vec], writing
r[
x
 
: =
a
 
]     for    r(
a
 
).
This notation allows substitution into expressions (t[[(x)\vec]: = [(a)\vec]]) as well as operation-symbols, repeated substitutions and weakening ( [^(x)]*t).

A lot of work remains to be done in the next section to define general substitutions u and their action u*t on terms - the calculus is highly recursive, and we have to break into the circle somewhere - but, in anticipation of this, here are the first of the formal rules.

DEFINITION 8.1.3 The term-formation rules are as follows:

(a)
resolution ( cf Remark  1.7.6) of an operation-symbol r,
omitted prooftree environment
by substitution u = [[(x)\vec]: = [(a)\vec]] of arguments [(a)\vec], and

(b)
variables considered as terms,
omitted prooftree environment
of which the identity axiom (x:X\vdash x:X) is a special case.

Both of these rules incorporate weakening, cf Definition  1.4.8 and Remark 2.3.8. We study the structural rules in the next section.

Equality of terms   The notion of equality needed in the foundations of dependent type theory is that from algebra: congruence. The judgement G\vdash a = b means that, for any valid judgement G,Y\vdash J in which a is a sub-expression, replacing it with b gives another valid judgement.

DEFINITION 8.1.4 The intensional term-equality rules are:

(a)
the laws of the object-theory, as in Definition  4.6.1(d);

(b)
the rules for an equivalence relation (Definition  1.2.3),

omitted prooftree environment            omitted prooftree environment            omitted prooftree environment

(c)
and pre- and postsubstitution, including in particular congruence for each operation-symbol r,
omitted prooftree environment
The formal rule, cf Definition 8.1.3(a) , is
omitted prooftree environment

The anonymity of proofs is expressed by an indiscriminate equality rule:

omitted prooftree environment

REMARK 8.1.5 Intensional equality G\vdash a = b:X remains at the level of judgements: it does not (within the basic calculus) provide us with a term of some propositional type eq[a,b]. We discuss extensional equality briefly in Section 8.3. If we want to do something conditionally on the equality of a and b, it is extensional equality that we need.

Dependent types   The dependency of types on terms (in predicates, hom-sets, arities, etc ) is expressed in a similar way to the application of operation-symbols to arguments, but there are no type variables.

DEFINITION 8.1.6 The direct type formation rule is

omitted prooftree environment
where Y is a dependent type-symbol in the object-theory. As we did for the operation-symbols (Definition 8.1.3(a)), it is convenient to regard the primitive form of the dependent type as having variables for its arguments: [(x)\vec]:[(X)\vec]\vdash Y[[(x)\vec]]. The formal type-formation rule is then
omitted prooftree environment

Equality of types   The instantiation of a dependent type Y[[(x)\vec]] at equal terms [(a)\vec] = [(b)\vec] gives rise to equal types. We have not addressed this phenomenon before - indeed we have gone to some lengths to exclude it - but how can we deny that Factors[9×4] = Factors[6×6]? There must at least be a canonical isomorphism between the two, but if we chose to make this explicit we would be obliged to introduce formation and equality rules for it, which would have to obey further coherence rules with respect to other substitutions. Predicates at equal subjects also give rise to equal types; again there is a canonical way of translating a proof of one into a proof of the other, which must also obey coherence.

Rather than enter this labyrinth, we accept that types can be intensionally equal, ie if they have a common history of formation. Whereas set theory allows independently given types to be tested for equality or inequality, we do not. Section 9.2, however, does look at some of the categorical consequences of replacing equality by isomorphism .

DEFINITION 8.1.7 The type equality rules are

(a)
reflexivity, symmetry, transitivity,

omitted prooftree environment            omitted prooftree environment            omitted prooftree environment

(b)
and congruence,
omitted prooftree environment
for which the formal rule is
omitted prooftree environment

(c)
But the most important consequence of type equality is that terms may acquire new types:

omitted prooftree environment            omitted prooftree environment
Notice that the congruence rules in Definition  8.1.4(c) don't even make sense without this ability to transfer types of sub-terms.

For the sake of giving a little more thought to the all-important coercion rule, we pause to consider its one-way version.

REMARK 8.1.8 Subtyping generalises equality between types to a non- symmetric relation(-judgement) G\vdash U X satisfying

omitted prooftree environment            omitted prooftree environment            omitted prooftree environment

omitted prooftree environment        omitted prooftree environment        omitted prooftree environment
in which is contravariant in its first argument. Comprehension gives the most familiar example (Remark 2.2.4). In principle terms may be equal with respect to one type but not another, for example because the second consists of ``tokens'' for the first, this having finer equality rules ( cf PERs, Exercise 5.10 ).

Subtyping also arises in object-oriented programming languages, in which complex types are developed from simpler ones by the addition of constructors and properties. As a mathematical analogy to this style, we may define a field as an Abelian group, with multiplication as an extra operation and the field axioms as extra conditions.

Terms of the narrower type inherit the covariant properties (positive, in the sense of Remark 1.5.9) associated with the wider one to which we coerce them; negative properties pass the other way. The coercion functions, like forgetful functors, need not be injective, but if they are suppressed from the notation then there must be at most one between any two types. (This has non-trivial consequences for function-types.)

REMARK 8.1.9 Some authors allow axioms stating equality of types, so that Heyting semilattices can be treated in the same framework. We forbid them, because interchangeability of objects should be expressed as isomorphisms, ie by means of two operation-symbols and two laws between their composites ( cf Section 7.6). See Exercise 4.7 regarding the quotient of a category by a system of canonical isomorphisms. As we commented before Proposition 3.2.11, the antisymmetry law for posets is a side-effect of the imposition of algebraic notation (, , ), and is not an intrinsic feature of logic.

The restriction drastically simplifies the issue of type equality, as type- expressions can be equal only as a result of making equal substitutions into the same ``outermost'' type-symbol. This is essential to the validity of the structural recursion used in the interpretation (Section  8.4).

Definitional equality need not be excluded: it is of course very useful to define R = {(L,U):P(Q)|} as in Remark 2.1.1. This is harmless to the interpretation of dependent type theory, as we may simply replace the left hand side of the definition by the right. Inter-provability as a notion of equality of propositions will be discussed in Remark  9.5.6.

The object-language   The pure theory cannot prove the existence of anything apart from the empty context [  ], so an object-theory is needed. As in simply typed algebra, it has types, operation-symbols and laws.

DEFINITION 8.1.10 A generalised algebraic theory L is given by

(a)
type-symbols D\vdash X type and proposition-symbols D\vdash f prop , each defined in a context D;

(b)
operation-symbols, D\vdash r:X, which are typed and in context;

(c)
laws between terms D\vdash a = b:X of the same type in context.

In order to give meaning to the ``contexts'' which occur in these data, we have to generate a small part of the language - as we did to state laws for an algebraic theory in Section 4.6. However, the ubiquitous dependencies must not be allowed to become circular, so we require that

the types and operation-symbols which occur in D must have been declared in advance.

Abstractly, the presentation defines a relation between each new symbol being defined and the type-symbols and operation-symbols that are used in the formation of its defining context D (there are operation- symbols in the terms that are the arguments of the type-expressions). This relation must be well founded.

DEFINITION 8.1.11 A stratified algebraic theory is one which obeys a stronger well- foundedness condition, that all of the operation-symbols r:X and laws a = b:X must be declared before variables x:X may be used as arguments of further type-symbols Y[x]. We shall not impose this condition in this chapter, as it is violated by the canonical language in Definition  8.4.6. See Exercises 8.1- 8.5 and Examples 9.2.4.

EXAMPLE 8.1.12 The theory of categories, with cm(f,g) for f;g.

omitted eqnarray* environment

In Remark 4.1.10 we said that the maps of a category C with O = obC could be collected together and presented by src,tgt:(mor C) OxO instead of using the dependent type H[x,y]. In fact src,tgt will serve as the display map [^(f)] that corresponds to this dependent type, which we introduce syntactically and semantically in the next two sections.

omitted diagram environment

Before composition can be defined, its support - the set of composable pairs (f,g) with tgt(f) = src(g) - must be constructed. There is a natural syntactic description of this set, namely the context of the rule which introduces c. It is also the pullback of tgt and src, as marked in the diagram above, cf transitivity of a kernel pair (Proposition  5.6.4).

This chapter shows how to translate between the symbolic and diagrammatic idioms. The next section constructs the classifying category for L, ie the category in which this diagram is drawn, and shows that squares like the one marked really are pullbacks. In fact pullback performs all of the substitutions u* in Definitions 8.1.3(a), 8.1.4(c), 8.1.6 and elsewhere. In Section  8.4 we shall give the interpretation of the language, for which we shall need a sharper form of the induction which generates it.