8  Comprehension

Now we develop a λ-calculus for S, just as Section A 8 did for SS.

The new calculus is based on a type-theoretic presentation [Tay99, Section 2.2] of Zermelo’s original set theory, with Σ^X playing the role of the powerset (℘ X) and the object {X ∣ E} from Section 4 that of comprehension. Whereas comprehension is often presented in a way that allows each term to belong to many types, the new operators admit, i and I in our calculus, whilst perhaps being a little bureaucratic, ensure that each term has a unique type.

Writing D for the category obtained from the new calculus as explained in [Tay99, Sections 4.3 & 4.7] and more briefly in Remark A 2.7, we shall show in the following sections that S≃D. This will be done by means of a weak normalisation theorem, thereby showing that we have stated enough equations. It is a categorical equivalence, rather than the isomorphism that we had for SS, because we’re now manipulating types.

Remark 8.1 In the calculus that we have in mind for set theory, the rules for the powerset ℘ X≡Ω^X are those of the restricted λ-calculus, where ξ[a] means a∈{X ∣ ξ}. Then comprehension has formation and introduction rules,

elimination rules,

and β and η-rules

x:{X ∣ ξ}   ⊢   x=admit( iX,ξ x).

The intent of these rules is to specify when there is a term admita that makes the triangle commute:

Notice that we have required ξ:℘ X to be a closed term (defined in the empty context), because we do not want to get involved in dependent types in this paper.

Remark 8.2 The rules that we give below for our own monadic situation are not very pretty if seen as a piece of pure λ-calculus. But they are in the spirit of the treatment of comprehension above, so long as we read the the type-formation rule as

where any predicate ξ:℘ X provides subtype data in set theory, and the nucleus E (Definition 4.3) does so for our own calculus. Similarly, the introduction rule means

where our admissibility condition is unfortunately more complicated and less intuitive than that in set theory.

You may think of

but this can only be internalised if Σ^X is compact (so ∀φ:Σ^X is meaningful) and Σ is discrete (so ⇔ is internal). These conditions (along with what is needed in Example 2.6(a) to define I_X,Eθ in terms of ∃) would make S into a topos (Theorem C 11.12), and thereby bring the comprehension calculus back to that for Zermelo type theory.

Remark 8.3 As we have learned throughout this paper, we need to be explicit about the subspace topology. The elimination rule for elements ({}E₀) below provides the restriction of an open subset φ of X to the subspace {X ∣ E}, which we may re-interpret as the introduction rule for predicates,

For the corresponding elimination rule, we need a new operator I_X,E to expand an open subset θ of the subspace to the whole space.

For reference, we repeat Definition A 2.1,A 8.1,A 8.2 and 4.3.

Definition 8.4 The restricted λ-calculus has just the type-formation rules

1 type

but with the normal rules for λ-abstraction and application,

together with the usual α, β and η rules.

Definition 8.5 Γ⊢ P:Σ^ΣX is prime if  Γ,  F:Σ³ X ⊢ F P   ⇔   P(λ x.F(λφ.φ x)).

Definition 8.6 The sober λ-calculus has the additional rules

focusI

focusβ

T0

Definition 8.7 φ:Σ^Y⊢ Eφ:Σ^Y is called a nucleus if

Definition 8.8 The {}-rules of the monadic λ-calculus define the subspace itself.

⎧ ⎨ ⎩ ⎫ ⎬ ⎭

F

⎧ ⎨ ⎩ ⎫ ⎬ ⎭

I

⎧ ⎨ ⎩ ⎫ ⎬ ⎭

β

Definition 8.9 The Σ^{}-rules say that it has the subspace topology, where I_X,E expands open subsets of the subspace to the whole space.

The β-rule says that the composite Σ^X↠Σ^{{X ∣ E}}↣Σ^X is E:

Notice that this is the only rule that introduces E into the λ-expressions. The η-rule, which we first saw in Remark 2.8, says that the other composite Σ^{{X ∣ E}}↣Σ^X↠Σ^{{X ∣ E}} is the identity:

In any type theory where terms are embedded in the definitions of types, we must check that, when two terms are equal according to the rules of the calculus, they give rise to interchangeable types. This result has the flavour of the normalisation proof that follows (Proposition 9.11), whilst being a lot simpler, so you may find it helpful to fill in the details of the verifications as a preparatory exercise.

Lemma 8.10 If E₁=E₂ then there is an isomorphism {X ∣ E₁}≅{X ∣ E₂} that commutes with the structure (admit, i and I).

Proof    The isomorphism for values is x₁↦admit₂(i₁ x₁) and vice versa. This is well formed, i.e. the side condition for {}I is satisfied and justifies the use of admit₂, because of the equation E₁=E₂. The isomorphism for properties is θ₁↦Σ^i₂(I₁θ₁). The equations for the isomorphisms and commutativity with the structure follow easily from the β- and η-rules for the two sides.         ▫

Before embarking on the main normalisation theorem, we investigate some of the interactions between the new admit operation and the underlying sober and recursive structures. The first result is the symbolic analogue of Remark 4.11, showing that admit does the same for a general Σ-split inclusion as focus does for η.

Lemma 8.11 The standard resolution defines an isomorphism

where E≡η_Σ^X·Σ^η_X.

Proof    The term x:X⊢admit(λφ.φ x) is well formed because of the unit law. The right hand side of Definition 8.5 is EF P, so the subspace {Σ² X ∣ E} exactly captures the primes and

is well formed. Then focus(i(admit(λφ.φ x)))  =  focus(λφ.φ x)  =  x by {}β and focusη. Conversely, admit(η_X(focus(i P)))  =  admit(i P)  =  P by focusβ and {}η.         ▫

The interaction between admit and substitution, i.e. cut elimination, is as expected, cf. Lemma A 8.4.

Lemma 8.12 Let Γ⊢admit_X,E a:{X ∣ E} be a well formed term and u:Δ→Γ a substitution [Tay99, Section 4.3]. Then Δ⊢admit_X,E u^*a:{X ∣ E} is also well formed, and

Proof    In the context [Δ, φ:Σ^X], since E and φ do not depend on Γ,

This is consistent with the {}β- and η-rules when we put u^*(i_X,Ea) ⇔ i_X,E(u^*a), and with the Σ^{}-rules since u^*(I_X,Eθ) ⇔ I_X,E(u^*θ).         ▫

Much of the business of Section A 8, which introduced the focus operation to handle sobriety, was to eliminate it. In particular, Proposition A 8.10 showed that focus is redundant for logical terms (i.e. of type Σ^U), whilst Section A 9–10 replaced it with descriptions for numerical terms (i.e. of type ℕ). The following result adds a new case to that reduction, for terms of type {Y ∣ E}, so focus can still be pushed to the outside of any term of the comprehension calculus, or eliminated altogether.

Lemma 8.13 If Γ⊢ P:Σ² {Y ∣ E} is prime then

So {Y ∣ E} is sober, cf. Lemma 6.9.

Proof    Since Γ⊢Σ² i P:Σ² Y is also prime (Lemma A 4.6), we may form

which satisfies

so we may then form Γ⊢admit_Y,E(focus_Y(Σ² i P)). Applying θ:Σ^{{X ∣ E}},

whence the result follows by T₀.         ▫

Finally, admit can also be moved to the outside of the term, although that is in fact the normalisation theorem to which the next two sections are devoted. Here we just consider the interaction with recursion, which is the symbolic analogue of Proposition 6.14.

[This proof requires equational hypotheses (Remark E 2.7).]

Lemma 8.14 Let X={Y ∣ E} with terms

such that Γ⊢admitz:X and Γ,  m:ℕ,  x:X⊢ admits(m,i x):X are well formed. Then

omitting the subscripts on i_Y,E and admit_Y,E.

Proof    Using the {}β- and η-rules, the claim is equivalent to

and is valid for n=0. In order to use the rec η-rule to prove the claim, we have to check the same equation as for the induction step in an ordinary proof by induction, namely