The type-theoretic interpretation of constructive set theory

-- Not yet mechanised by Miëtek Bak
-- TODO: rest of text

module mi.Aczel1978 where

By adding to Martin-Löf’s intuitionistic theory of types a ‘type of sets’ we give a constructive interpretation of constructive set theory. This interpretation is a constructive version of the classical conception of the cumulative hierarchy of sets.

Introduction

Intuitionistic mathematics can be structured into two levels. The first level arises directly out of Brouwer’s criticism of certain methods and notions of classical mathematics. In particular the notion of ‘truth’ that gives rise to the law of excluded middle was rejected and instead the meaning of mathematical statements was to be based on the notion of ‘proof’. While implicit in this first level of intuitionism was a theory of meaning quite different from the classical one, it was nevertheless the case that the body of mathematics that could be developed within this level remained a part of classical mathematics. Because Brouwer felt that mathematical analysis could not be developed adequately on this basis he was led to formulate his own conception of the continuum. This conception involved the mathematical treatment of incompletely specified objects such as free choice sequences. The second level of intuitionism builds on the first level but also includes these radical ideas that turn out to be incompatible with classical mathematics. Although considerable effort has been made over the years to make these ideas more transparent they have remained rather obscure to most mathematicians and the mathematics based on them has had a very limited following.

Since Bishop’s book [3] appeared, it has become clear that, in spite of Brouwer’s views, constructive analysis can be developed perfectly adequately while staying within the first level of intuitionism. This fact has led to a renewed interest in this part of intuitionism. The desire has been to find an analogue, for Bishop’s constructive mathematics, of the generally accepted formal system ZF for classical mathematics. Several approaches have been tried and there has been some controversy over their relative merits. Two such approaches are ‘Constructive Set Theory’ (see [7] and [13]) and ‘Intuitionistic Type Theory’ (see [11]). In this paper we take the view that these, and perhaps other approaches, are not necessarily in conflict with each other. Constructive set theory suppresses all explicit constructive notions in order to be as familiar as possible to the classical mathematician. On the other hand type theory aims to give a rigorous foundation for the primitive notions of constructive mathematics.

The appeal of Bishop’s book is that it wastes little time on the analysis of constructive concepts but instead develops analysis in a language mostly familiar to the classical mathematician. In constructive set theory this is taken a stage further. As in ZF there are just the notions of set and set membership with an axiom system that is a subsystem of ZF using intuitionistic logic, and including the axiom of extensionality. In such a system the direct constructive content of Bishop’s notions has been lost and there arises the crucial question: What is the constructive meaning of the notion of set used in constructive set theory? We aim to answer that question in this paper. What is needed is a rigorous framework in which the primitive notions of constructive mathematics are directly displayed, together with a natural interpretation of constructive set theory in that framework. We shall give such a framework based on the intuitionistic type theory of [11]. We could have taken instead a system of ‘Explicit Mathematics’ (see [5] and [2]). But systems of explicit mathematics leave the logical notions unanalysed, whereas type theory is a logic free theory of constructions within which the logical notions can be defined. For this reason we consider type theory to be more fundamental.

The axiom system CZF (Constructive ZF) is set out in §1 and some elementary properties are given in §2. The system is closely related to the systems considered by Myhill and Friedman in their papers. In §3 we summarise the type-theoretic notions of [11] and introduce the type of sets. The interpretation of CZF is set up in §4 and its correctness is proved in §5 and §6. Finally in §7 we consider a new principle of choice for constructive set theory.

Formally, the type of sets was first introduced by Leversha in [10] where it was used to give a complicated type-theoretic interpretation of Myhill’s original formulation of constructive set theory in [13]. Unfortunately it was not realised at that time that the type itself gave a constructive notion of set. Instead it was only used as an appropriate constructive notion of ordinal to use in indexing the stages of Leversha’s construction.

1. The axiom system CZF

We formulate CZF in a first order language \mathcal{L} having the logical primitives \bot, ∨, ∧, →, ∀x, ∃x,, the restricted quantifiers (∀x∈y), (∃x∈y) and the binary relation symbols ∈ and =. We assume a standard axiomatisation of intuitionistic logic. The remaining axioms of CZF are divided into two groups.

Structural axioms

Defining schemes for the restricted quantifiers.

\begin{aligned} (∀x∈y)φ(x) & ↔ ∀x(x∈y → φ(x)) \\ (∃x∈y)φ(x) &↔ ∃x(x∈y ∧ φ(x)) \end{aligned}

Equality axioms.

\begin{aligned} x = y & ↔ ∀z(z∈x ↔ z∈y) \\ x = y ∧ y∈z & ↔ x∈z \end{aligned}

Set induction scheme.

∀y ((∀x∈y)φ(x) → φ(y)) → ∀xφ(x)

Set existence axioms

Pairing.

∃z(x∈z ∧ y∈z)

Union.

∃z(∀y∈x)(∀u∈y)(u∈z)

Restricted separation.

For restricted φ(x)

∃z((∀y∈z)(y∈x ∧ φ(y)) ∧ (∀y∈x)(φ(y) → y∈z))

If φ(x,y) is a formula let φ'(a,b) denote

(∀x∈a)(∃y∈b)φ(x,y) ∧ (∀y∈b)(∃x∈a)φ(x,y)

Strong collection.

(∀x∈a)∃yφ(x,y) → ∃bφ'(a,b)

Subset collection.

∃c∀u((∀x∈a)(∃y∈b)φ(x,y) → (∃d∈c)φ'(a,d))

where u may occur free in φ(x,y).

Infinity.

∃z\text{Nat}(z)

where \text{Nat}(z) is the conjunction of (∀x∈z)(\text{Zero}(x) ∨ (∃y∈z)\text{Succ}(y,x)), (∃x∈z)\text{Zero}(x), and (∀y∈z)(∃x∈z)\text{Succ}(y,x.) Here \text{Zero}(x) is (∀y∈x)\bot and \text{Succ}(y,x) is (∀z∈y)(z∈x) ∧ y∈x ∧ (∀z∈x)(z∈y ∨ z=y).

Remarks.

Our formulation has been designed to make the correctness proof for our interpretation as smooth as possible. The axioms could have been written in a more standard way. Our formulation of the axiom of infinity expresses the existence of a set ω such that

n∈ω ↔ n = \emptyset ∨ (∃m∈ω)(n = m ∪ \{m\}).

The mathematical induction scheme can be proved in CZF using set induction. Recall that in the usual way strong collection implies replacement. Ordinary collection is not good enough in the presence of only restricted separation. The significance of subset collection will become clear in the next section.

2. Elementary properties of CZF

We give some simple results that spell out the relationship of CZF to ZF. In particular we reformulate the subset collection scheme as a single axiom and bring out its relationship to the power set axiom and Myhill’s exponentiation axiom. We show that ZF results from CZF by adding classical logic.

We use standard set-theoretic notation and definitions. So ordered pairs ⟨x,y⟩, cartesian products A × B, and the notion of a function f : A → B etc … are all defined as usual.

-- TODO

References