To complete the equivalence between syntax and semantics, it remains to prove confluence, strong normalisation for the l-calculus and the disjunction property for intuitionistic logic. The conceptual content of these results, when proved syntactically, is drowned in a swamp of symbolic detail which cannot be transferred to new situations. The remarkable construction which we use illustrates how much can be discovered simply by playing with adjoints and pullbacks.
The origin of the name gluing is that this is how to recover a topological space from an open set and its complementary closed set (Exercise 3.71). The construction for Grothendieck toposes was first set out in [AGV64, Exposé IV, §9.5]. Considered as inverse images, functors between toposes with the rich properties of (p0,p1):S¯ U® SxA or p1:S¯ U® A are called surjections and open inclusions respectively (geometrically, SxA is the disjoint union of S and A.)
The gluing construction Recall from Example 7.3.10(i) that, for any functor U:A® S, the gluing construction is the category S¯ U whose objects consist of I Î obS, G Î obA and f:I® UG in S, and whose morphisms are illustrated by the diagram below. We shall say that (I,G,f) is tight if f is an isomorphism.
omitted diagram environment
Since it preserves everything in sight, p1 is also called a logical functor.
PROPOSITION 7.7.1 Let U:A® S be any functor. (We emphasise the case where it preserves finite products and maybe pullbacks, and S is a topos; the dotted lines signify even stronger assumptions which we do not wish to make. See Exercise 3.70 for posets.) Then
omitted diagram environment
|
COROLLARY 7.7.2 Assuming only that U preserves finite limits, if A and S have the following structure, so does S¯ U, and p1 preserves it:
If U preserves this structure then so does p0. []
Implication and the function-type are considered in Exercise 3.72 and Proposition 7.7.12; Exercises 7.50- 7.51 deal with factorisation systems (and so the existential quantifier, Section 9.3) and W (higher order logic).
Conservativity Let C be a category and L a subcanonical []-language for it (Definition 7.6.5(a)), ie L names all of the objects and maps of C, stating all of the laws which hold between them, possibly with encoding operations for some []-structure. Recall from Definition 7.6.8 that [] is called conservative if the functor \qqdash :C® Cn[]L is full and faithful.
|
|
|
EXAMPLE 7.7.4 Let C = {1} and suppose that L says that \qq 1 is indeed the terminal object (so there is a nullary encoding operation \vdash *:\qq 1 with one h-rule x:\qq 1\vdash x = *). Then
|
LEMMA 7.7.5 Q is full and faithful.
PROOF: An (S¯ U)-map QX® QY is a pair (x,a) making the square below commute, but by the Yoneda Lemma (Theorem 4.8.12(a)) any S-map (natural transformation) x:C(-,X)® C(-,Y) is of the form post(a) for some unique (semantic) map a = xX(\idX):X® Y in C.
omitted diagram environment
The other map, a, belongs to Cn[]L, ie it is syntactic, a substitution. We must show that a = \qqa without assuming the theorem we're trying to prove, that \qqdash is full and faithful. In fact this follows from the fact that the square commutes at \idX Î C(X,X). Hence (x,a) = Qa. []
Then \qqdash is full and faithful, ie [] is conservative.
In practice, p1 preserves []-structure on the nose, and [[-]] is defined by structural recursion so that [[G]] = ([[G]]0,G,\qG ), where [[-]]0 = p0[[-]].
The functor [[-]] reflects the existence of isomorphisms: if [[G]] º [[D]] somehow then G º D. (This is the categorical analogue of an injective function between posets.) For higher order logic, [[-]] need not be full.
PROOF: Since Cn[]L is the classifying category, and using the axiom-scheme of replacement to justify the recursion, the model Q extends to a []-preserving functor [[-]]:Cn[]L® S¯ U making the upper triangle commute, uniquely up to unique isomorphism:
omitted diagram environment
The lower Cn[]L is also a model, for which both id and p1[[-]] serve as the mediator from the classifying category (since [[-]] and p1 preserve []- structure), so they are isomorphic, p1[[G]] º G. Hence [[-]] is faithful, whilst Q is full and faithful, so \qqdash is also full and faithful. []
EXAMPLES 7.7.7 The first clause of the theorem is applicable to the structures [] listed in Corollary 7.7.2 (and more). The difficulty lies in condition 7.7.6(c), ie what structure is named by the language L.
The construction relies on the fact that S, which is a topos, has all of the extra structure [] (plus the axiom-scheme of replacement) and the Yoneda embedding is full and faithful and preserves it. However, S does not freely adjoin this structure (except in the case of arbitrary stable colimits), and the question is whether the embedding into the free category Cn[]L is full and faithful.
REMARK 7.7.8 In the case C = {1}, an object If® UG º Cn[]L(1,G) of S¯ U is a family of closed terms or proofs of G, indexed by I. More generally, it is a cocone \Fredi:\qq \typeXi®G of such proofs under a certain diagram \typeX(-):Á® C of base types or hypotheses. This diagram is the discrete fibration corresponding to the sheaf I:Cop® Set by Proposition 9.2.7.
Notation 7.7.3(b) provided a specific sheaf of closed terms \qX of each base type X Î obC, so we shall call it the realisation of X. Theorem 7.7.6 showed that this is an isomorphism (the realisation is tight) for base types, and extended the notation to general contexts. We already know that the full subcategory of tight objects in S¯ U is closed under definable limits, so the same is true of the class of tightly realised contexts. We shall see that this extends to colimits and exponentials, so if [] consists only of this (first order) structure then A is already the interpretation [[-]], and this is full as well as faithful.
For higher order logic the realisation is no longer tight. Andre Scedrov and Philip Scott [SS82] trace the method back in the symbolic tradition to Stephen Kleene's realisability methods (1962), and link it to the categorical construction. Peter Freyd found this after hearing the presentation of Scott's work with Joachim Lambek [ LS80] at a conference, and not at first believing the theorem below which their results implied.
Existence and disjunction properties Recall that [[-]]0 º p0·[[-]].
LEMMA 7.7.9 The realisation q:[[-]]0® U is naturally split epi.
PROOF: First observe that, by the Yoneda lemma (Theorem 4.8.12(c)),
|
|
omitted diagram environment
Then the diagram in Set commutes and the required law follows from its effect on \idX Î C(X,X). []
THEOREM 7.7.10 [Freyd] U:Cn[]L® S preserves colimits named in [], but not necessarily those named in L . In particular, the global sections functor (Example 7.7.4) preserves
PROOF: We have just shown that U is a retract of [[-]]0, which preserves whatever colimits are in [], and hence so does U (Exercise 7.13). []
COROLLARY 7.7.11 In terms of proof theory, the fragment []
S can prove consistency of [] because it has been strengthened with the axiom-scheme of replacement, to which we return in Section 9.6.
Exponentials Recall that [I® J](X) = S(\HXxI,J) by Exercise 4.41, whilst UG(X) = Cn[]L(\qq X,G) by Notation 7.7.3(a).
PROPOSITION 7.7.12 Suppose A and S are cartesian closed, S has pullbacks and U preserves finite products. Then S¯ U is cartesian closed and p1 and A (but not p0 or U) preserve exponentials. (See Exercise 3.72 for the version for Heyting semilattices.)
PROOF: Given (If® UG) and (Jg® UD) in S¯ U, we form an internal version of the hom-set (S¯ U)(f,g), namely the pullback
omitted diagram environment
in S, where the lower left map is the exponential transpose of
|
omitted diagram environment
Notice that if g is an isomorphism, then so is h. []
COROLLARY 7.7.13 Q preserves any exponentials that are named in L. If D has tight realisation then so does [G® D] for any G whatever.
PROOF: In computing Q(X® Y), the edges of the pullback square above are all invertible, the vertices being isomorphic to \HX® Y. []
THEOREM 7.7.14 [Yves Lafont, [Laf87, Annexe C]] The l- calculus is a conservative extension of algebra. []
This is as much as is needed for the equivalence between semantics and syntax in Theorem 7.6.9. We haven't proved the normalisation theorem as such, but by a variation on this technique every term is provably equal to a normal form [MS93, AHS95,CDS98]. It seems likely that a purely categorical proof will be found for strong normalisation itself, handling reduction paths in the fashion of Exercise 4.34. We return to consistency and the axiom of replacement in Section 9.6.