Realizability, Set Theory and Term Extraction ^{∗}

In Memoriam Stephen Kleene

James Lipton Dept. of Mathematics ^{†} Wesleyan University Middeletown, CT 06459

Contents

1 Introduction 1

2 Axioms, and the “Naïve” Theory 7 2.1 Justifications of some of the choices and omissions of ZF-axioms . . . . . . . . . 8 2.2 Powell Ordinals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3 Recursive Realizability Interpretations 16 3.1 Abstract Applicative Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.2 Realizability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3 Soundness for IZF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.4 Term Extraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.5 Strong Intuitionistic Counterexamples . . . . . . . . . . . . . . . . . . . . . . . . 24 3.6 Some famous “nonstandard” consistency results . . . . . . . . . . . . . . . . . . . 25

4 Forcing in Constructive Set Theory (Unramified) 26 4.1 Kripke models over V (K) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 4.2 Soundness of IZF Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 4.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

5 Ω-sets, Categories and Toposes 34 5.1 From Kripke Models to cHa’s . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 5.2 Logic in a cHa, Ω-sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 5.3 Presheaves, Sheaves and Topoi . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 5.4 Logic in a Topos: three views . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

5.4.1 The Mitchell-Benabou Language . . . . . . . . . . . . . . . . . . . . . . . 46 5.4.2 Kripke-Beth-Joyal Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 48 5.4.3 The Fourman-Hayashi interpretation of IZF . . . . . . . . . . . . . . . . . 51

5.5 PERs and the Effective Topos . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

A A sketch of Kleene’s 1952 realizability interpretation 58 A.1 Realizability for HA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58

B APP and the logic of partial terms 59

∗To appear in The Curry-Howard Isomorphism: 8-ème volume des cahiers du centre de logique de l’Universite Catholique de Louvain.

†This work was partially supported by ONR grant 4331-001-srp-01

1 Introduction

For most of this century, set theory has enjoyed the reputation of a universal language for mathematics, a reputation perhaps increasingly shared with (and even ceded to) categorical foundations. Can we expect comparable utility for computer science? In computer science, constructive formal systems based on type theory, or on the Curry-Howard isomorphism have become increasingly widespread for program development and language design. These systems seem to be inherently more constructive than set theory, and more amenable to syntactic analysis. But a good look at many topics set theory reveals that there is nothing intrinsically nonconstructive about sets. Many operations with sets are natural from a computational point of view. Over the past thirty years the features of a truly constructive type-free set theory have begun to emerge, first in the pioneering work of Myhill and Friedman, and since then of many others: Scedrov, Aczel, Hyland, Feferman, Grayson, Powell, to name a few. An almost parallel endeavor in the study of category-theoretic generalizations of the universe of sets, known as Toposes, began in the 1960’s with the pioneering work of Lawvere, Tierney, Freyd and many others. These two lines have merged in the past ten to fifteen years, so that one can broadly speaking call them both approaches to a constructive set theory, although categorical studies are closer to the typetheoretic approaches in flavor. Both lines will be surveyed here, as approaches to constructive set theory in the broadest sense.

Is “∈” dead?

How relevant is the study of set theory being considered here, that is to say the study of the family of ontologies in which the membership relation plays a basic role? It is the author’s belief that while “set-theory-as-foundations” no longer reigns today, sets continue to play an important role in computation and logic as a data type, and as a powerful semantical framework for analyzing calculi and constructive mathematics. Set-theoretic notions are very much alive, and their constructive formalizations deserve to be better understood, and by a wider community, than they are today.

It is worth stressing that in “alternative foundations” such as type theory, there has been extensive study of sets as a data type (in, e.g. Martin-Löf type theory, Calculus of Constructions) and of the connections between various constructive set theories and type theories (see e.g. Aczel’s [1] and also [118, 8] for further discussion). Whereas classical set theory has been shown inadequate for providing standard^{1} interpretations of polymorphic type disciplines [95], constructive set theory does admit such an interpretation [94]. Also, vis-à-vis the latest and most sweeping turn in foundations in Computer Science, namely the advent of Category theory, set theoretic concepts remain a significant subject of study. A great deal of work has been done done to capture a more abstract notion of set within category theory itself. As mentioned above, Topos theory, which has been a central field in category theory for close to 30 years, studies categories with enough structure to permit formalization of (local) set-theoretic notions such as membership and power-set. Certain toposes with stronger closure properties (Grothendieck toposes) have been shown to admit a global (uniform across all individuals) notion of membership, and provide categorical models of type-free constructive set theory. More general notions of membership and powerset underlie an important class of structures (hyperdoctrines) called triposes.

We will touch upon many of these approaches, but we begin, however, with a thorough study of the conventional (constructive) theory of ∈ as formalized in intuitionistic Zermelo-Fraenkel set theory, or IZF.

ZF and relatives As suggested by Beeson in [8] two possible approaches to formalizing a constructive set theory are to define an intuitionistic theory from the ground up, or to “correct” existing classical ontologies until one is “safe in intuitionistic territory”. The latter approach, which aims to save some of the desirable features of the classical ontologies, is exemplified by such type-free theories as CZF and IZF, explored by Myhill and Friedman in the early 1970’s ^{2} and by many others since then.

1i.e. where inhabitation “ : ” is interpreted by “∈”.

This derived character makes constructive ZF-like set theories an unusual subject, seemingly halfway between two worlds. They have some of the appearance of the powerful, descriptive foundation of classical mathematics found in ZF. Shorn of the excluded middle and a few other “dangerous axioms”, they turn out to be closer that one might first suspect to the typed, computational, guardedly constructive theories often studied for computer science applications, such as Martin Löf’s type theory, Coquand’s Theory of Constructions [21], etc.

Metamathematical issues Before exploring the theory, a few general remarks are in order. We will not go into the general motivation for ZF set theory here^{3} although the axioms are briefly presented and discussed in the first section of the paper. We assume that the reader has seen the elements of some axiomatic presentation of set theory (if not, an excellent discussion can be found in Johnstone’s lecture notes [56]) Nonetheless, let us highlight a few, perhaps obvious points. First, the study of Set Theory, like that of a few very special theories (Constructions, Martin-Löf Type theory, etc.) is special in one respect: it is an ontology, i.e. a proposed mathematical universe. This gives rise to very special problems since a formal study of such an ontology and its semantics is often done within the theory itself, or at least within a similar one: we do not wish to postulate a new notion of universe for the sole purpose of studying our picture of the world^{4}.

Different foundations have special devices for doing this sort of self-study, e.g. universes in Martin-Löf’s Theory^{5}. Because of its type-free, impredicative nature, in developing set theory we must also take special care in defining the right notion of models and meta-mathematical machinery, to avoid paradoxes (see [67] for an excellent discussion of the metamathematical issues).

Set theory was seen from its early days as a candidate for placing much of known mathematics within a single metamathematical framework. Despite the paradoxes and some of the problems one faces in defining and dealing with cardinality, choice, proper classes, etc., it must be remarked that the world that Cantor built, and which Zermelo and others formalized, has been remarkably successful. Many mathematicians still view set-theoretic language in practice as a kind of machine-code for mathematics, as well as a testing ground for the accuracy of one’s notions: “if you can’t define it in set theory, it isn’t a well-defined idea”. It is probably misguided to think of set theory as an absolute foundation for mathematics, and equally misguided to think that any one ontology can play such a role for Computer Science. D. Scott has remarked that it may be the business of logicians in computer science today to construct ontologies in the plural, depending on the application. But set theory remains one of the more powerful ontologies, and its sweeping expressive power makes the prospect of a truly computational set theory attractive for computer science.

A type-free theory for higher-order term extraction. Set theory is a first-order theory: we never quantify over formulas. But it is capable of formalizing higher order theories in a natural way, since what we usually mean by quantifying over all functions, say, on the natural numbers

∀F : N → N(… ψ(F) …)

2The earliest papers on the subject known to the author were presented at the “Intuitionism and Proof Theory”

Symposium, in Buffalo, 1970, and later at the 1971 Cambridge Summer School in Mathematical Logic [88, 89, 36]

3See [118, 8] for a comparative discussion of different classical and intuitionistic set theories.

4We may then have to postulate yet another one for validating the second one. This possibility of infinite proliferation of meta-worlds was –in essence– pointed out over two thousand years ago by Aristotle.

5which have been exploited for reflection in the Nuprl system, see e.g. [19]

can be expressed in set theory as

∀x(func_{N}(x) → … ψ(x) …)

where func_{N}(x) is the statement that x is a function from N to N, i.e., a set of ordered pairs ⟨n, m⟩ ⊆ N × N with the usual properties. In this sense, studying set theory is studying one way of formalizing higher order reasoning.

Thus, a suitably constructive development of the subject might provide us with an ontology which is computationally useful, and where we can place a discussion of numbers, reals, sets of reals, sets of sets of reals, functions, etc., on the same footing, via a universal data type of sets. But what do we mean by suitably constructive? This depends on the applications one has in mind. I am partly guided here by projects like Nuprl, PX, Coq, Alf, Ergo, etc. (see e.g. [20, 48]) that permit the automatic extraction of algorithms from proofs. One of the aims of such systems is to produce algorithms which are guaranteed to be correct ^{6}, i.e. to satisfy a given specification. A specification is a logical description of a property to be satisfied by the input-output values of the algorithm. For example, a function f that computes the greatest proper divisor of its inputs satisfies ∀xψ(x, f(x)) where ψ(x, y) is the formula

div(y, x) ∧ (∀z)(div(z, x) → z ≤ y)

We will consider a specification of this function to be the formula ψ(x, y) together with a proof of totality of the specification, meaning a proof of the formula ∀x ∈ N∃y ∈ Nψ(x, y) in some formal system. Term extraction refers to an automated procedure for producing –given the specification– an algorithm that computes such a function in a given programming language.

In a system based on automated term extraction one programs by building proofs in a certain formal system. This means that one substitutes the possibly painful task of proof construction within a (possibly quite rigid) formal system for that of writing code in one’s favorite programming language: not necessarily a pleasant discipline, but a price one pays for the guarantee of correctness. ^{7}

Systems based on type theory have proven very useful for term extraction, but the rigidity of typing (which offers many benefits, to be sure) makes it difficult to pass between concepts at different type-levels. Considerable work must sometimes be done to get around this, and move freely between e.g. sets of individuals and individuals. Since type-free set theory makes no formal distinction between different levels, it is of interest to develop a term extraction system based on such a theory.

What does it mean to be constructive?

We assume here that the reader has encountered at least an elementary exposition of constructive principles, and in particular some notion of constructive proof^{8}. We briefly recap some essential points, making no claim to be comprehensive. There are today many schools of thought that voice adherence to some notion of intuitionism (and our own presentation of set theory does not attempt to follow any specific tendency). Nonetheless, certain points of view are common to most. We can think of the conceptual origin of constructivism as a critique of certain kinds of arguments that began to appear in 19th and 20th century mathematics. Such arguments included proofs by contradiction of the existence of certain mathematical objects (e.g. numbers, roots of equations, points in a space, functions). Inspection of these proofs showed that they supplied neither the objects whose existence they purportedly established nor the means for computing them. To cite one example: a certain fixpoint theorem states that a continuous function f from the unit disk {(x, y) : x^{2} + y^{2} ≤ 1} in the real plane to itself must have a fixpoint, that is to say, there must be an x in its domain for which f(x) = x. Inspection of the customary proof of this theorem^{9} shows that it derives absurdity from the supposition that such a fixpoint does not exist. No means of computing such a fixpoint is to be found in the proof .

6up to the point, of course, that the system implementation has been painstakingly proven correct!

7Engineering practice is quite another issue here: often one wants to incorporate “validated” code in the library into code extracted from proofs. Also one may wish to partially automate the most repetitive parts of proof construction, or write code to manage large libraries of theorems and lemmas, and make it possible to hide trivial fragments of proofs from the user.(see e.g. [19, 20]) Building a system that does this in an efficient and useful way is as much or more of an engineering challenge as devising the right formal system is a mathematical one.

8If not, we recommend [23] for a quick introduction, [118, 25] for a more thorough one, and for further references, and [26] for a detailed discussion of the philosophy and metamathematics of intuitionism.

The constructivist critique resulted in rejection of such an argument as a proof of an existential assertion. The use of such principles as

¬¬A → A or A ∨ ¬A

was found to be responsible for the unwarranted conclusion. In fact, from this perspective, the true conclusion of the fixpoint theorem is ¬¬∃x f(x) = x, which is weaker.

It would be inaccurate to say that constructivist critique can be reduced to a question of restricting the allowable means of inference, or even that it is an inherently logical critique.^{10} Nonetheless, it ultimately led to a recasting of the proof theory and semantics of logic itself. Gentzen (see e.g. [99, 118, 25]) defined several formal systems for carrying out intuitionistic reasoning. Heyting and others came to spell out a constructivist restatement of the meaning of the logical connectives, which underlies both the Curry-Howard and the Realizability approaches, and which we briefly sketch here. It is known, in one form or another, as the Brouwer-Heyting-Kolmogoroff interpretation (see, e.g. [8, 118, 25]). We restate it here in terms of evidence, a formulation inspired by [18].

• Evidence for A ∧ B is given by supplying evidence for A and evidence for B.

• Evidence for A ∨ B is given by supplying evidence for A or for B and some indication of which one is involved (and possibly an indication of the fact that it is to be regarded as evidence for A ∨ B).

• Evidence for A → B is given by supplying a rule or procedure that constructs evidence for B from evidence for A.

• Evidence for (∃x)A is given by supplying a “witness” c from the intended domain of the variable x and evidence that A(c) holds.

• Evidence for (∀x)A is given by supplying a rule or procedure that constructs evidence for A(c) from each individual c in the domain of the variable x.

The reader should think of this more as statement of principle than a definition. It leaves unspecified the meaning of the words “rules”, “procedures”, “constructs”, “domain” and it does not state what constitutes evidence for an atomic proposition! The reader may replace “evidence” by the word “proof”, and in the process make a step towards natural deduction, type theory and the Curry-Howard isomorphism. If the intended domain is the natural numbers, the language ⟨+, ×⟩, and if rules or procedures are read as algorithms, evidence as some sort of finite code (e.g. a number) and e.g. any number is considered evidence for a true atomic proposition, one has virtually defined Kleene realizability, as described in the appendix. Note, however, that if one lets “rule” mean an arbitrary function and uses classical reasoning, the interpretation is sound for classical logic! In fact given a classical Tarski model M if we declare atomic formulas to be realized by all the natural numbers if true in M, and by nothing if false, then a proposition has evidence if and only if true in M (see [118], introduction). So these precepts do not pin down constructive reasoning, they merely provide a way of carrying one’s intuitively acceptable notion of rules and construction into an interpretation of logic.

9due to Brouwer himself, and ultimately rejected by him.

10Brouwer, the originator of intuitionism, certainly never felt that formal systems had much to do with intuitionistic mathematics. We urge the reader to consult the first chapter of [118] for an outline of the different schools and the sources mentioned for a further discussion.

Realizability and ZF

For readers familiar with constructive mathematics or with other intuitionistic formal systems, the idea of carrying such an eminently non-constructive theory as Zermelo-Fraenkel set theory over into a constructive, or even computational domain may seem misguided. Nonetheless, some features of IZF are not entirely unreasonable for such a domain. As stressed by many authors (see e.g. Shoenfield’s discussion in [107]), ZF can be thought of as a theory issuing from an iterative, stratifiable, and hence in a (very weak) sense, constructive picture of the mathematical universe. One can think of the world as being built in stages corresponding to ordinals. Every set has an ordinal rank which one can think of as a time stamp indicating when the object was created, and which objects had to already exist prior to its creation. The restriction of fragments of classical ZF to intuitionistic arguments retains many of these features, while removing some of the ones that prove incompatible with the constructive standpoint. But the fundamental interest in throwing out classical axioms is to obtain new consistent extensions. New, “highly non-classical” interpretations are now available. It is these interpretations that are of interest computationally, far more than the theory itself. One aim of our study is to show that inherently computational semantics of the entire ontological framework –the realizability interpretations– are now possible. In some of these interpretations, certain strongly non-classical principles are seen to hold: all total functions from N to N are recursive, all total, real-valued functions on the reals are continuous. Within certain limits, the body of results known as recursive mathematics, (that is to say the development of recursive versions of the main results in Algebra, Analysis, Topology, starting with Turing, the Russian Constructivist school, Nerode, Metakides, etc., see e.g. [8, 22]) can be understood to be what takes place within a realizability interpretation (see e.g. remarks in [52]), although efforts to exploit this in a systematic way have as yet been limited (see e.g. Scedrov’s article in [102]).

To sum up, IZF and related constructive systems, viewed within the realizability interpretations, provide a powerful formalism for synthesizing correct algorithms from proofs of totality of recursive specifications that use the full, impredicative apparatus of IZF, and the same specification language found in ordinary mathematical practice. Realizability in IZF is an after-the-fact computational analysis of proofs and propositions, a bit like typing untyped expressions: it amounts to a systematic wringing out of recursive content.

Organization of these notes

We start with an exposition of the basic theory: the axioms, and the way semantics (of different kinds) are formalized within the theory. We supply most of the details in proofs at the beginning, to make the early exposition as close as possible to being “self-contained”. We also feel that the reader benefits more from a close look at one or two developments than a catalogue of the many systems that now bear the name “constructive set theory” and which can be found in the references.

The final section is devoted to a sketch of several ways of interpreting (typed and untyped) constructive set-theory categorically. It is intended more as a guide to the ideas and the literature than an exposition, which would require a book length treatment, and for which some excellent references exist (see e.g. [77, 33, 68, 58, 92]). There is more emphasis here on the tools, which have become central to the field and to theoretical computer science, and the approach is primarily semantical. We conclude our discussion with an outline of the effective topos and related models.

2 Axioms, and the “Naïve” Theory

We will now give the formal axiomatization of Intuitionistic Zermelo-Fraenkel Set Theory, IZF, and several related theories, here denoted IZF′ and CZF. Except where the demands of intuitionism require modification, the axioms are identical to those of older classical theories: IZF and variants of KP set theory (in fact they are all classically equivalent to their parent theories).

It is in the restriction of the logic that this theory becomes constructive. The excluded middle (LEM) may not be used. Let us underscore the fact that the theories considered here are all extensional: two sets are equal precisely when they have the same elements. Intensional theories are also of computational interest and are studied in e.g. [8], where a coding, due to Friedman, of extensional set theory into intensional is also discussed.

A more detailed discussion of these axioms can be found in [83], op.cit. and [8] and [89] .

Axioms of IZF, IZF′ and CZF

(1) Extensionality ∀x, y∀z(z ∈ x ⟺ z ∈ y) → x = y

Two sets are equal iff they have the same elements.

(2) Pairing ∀x, y∃z∀w(w ∈ z ⟺ w = x ∨ w = y)

If x and y are sets then there is a set {x, y} consisting of precisely the members x and y.

(3) Union ∀x∃z∀w(w ∈ z ⟺ ∃y ∈ x · w ∈ y)

⋃ x exists.

(4) Power ∀x∃z∀w(w ∈ z ⟺ ∀y ∈ w · y ∈ x)

The power set of x, P(x) ≡ {y : y ⊆ x} exists.

(5) Infinity ∃x(∃y(y ∈ x) ∧ (∀y)(∃z)(y ∈ x → z ∈ x ∧ y ∈ z))

There is an infinite set: i.e. an inhabited set x whose every member y is a member of another member of x.

(6) Separation_{φ} ∀x∃z∀w(w ∈ z ⟺ w ∈ x ∧ φ) z not free in φ

The collection of members of a given set having a certain (first-order) property is a set: If φ is a formula, and x is a set, then there is a set consisting of all members of x for which φ holds, usually denoted {w ∈ x : φ}.

(6′) Bounded Separation_{φ} ∀x∃z∀w(w ∈ z ⟺ w ∈ x ∧ φ)

The same, but only for properties definable by bounded quantification: φ must be a Δ_{1}^{0} formula.

(7) Collection_{φ} ∀x[(∀y ∈ x∃zφ) → ∃W ∀y ∈ x∃z ∈ W φ] W not free in φ

If every member of a given set x has a first-order definable collection of associated elements, then there is a set W containing at least one of these associates for each member of x.

(7′) Replacement_{φ} ∀x∀y ∈ x∃!zφ → ∃W ∀y ∈ x∃z ∈ W φ

A functional image of a set is a set.

(8) ∈-Induction ∀x[(∀y ∈ x φ(y)) → φ(x)] → ∀xφ(x)

Analog to induction on numbers: If a property holds for any set whenever it holds for its members then it must hold for every set.

IZF is the unprimed set of axioms (1) through (8), IZF′ is (1) - (6), (7′) and (8), CZF is (1) - (5), (6′) (7′) and (8).

The theory we shall be most concerned with here is IZF. However, in certain regards, IZF′, CZF are the more constructive theories: they have the existence property EP and the disjunction property DP^{11} while IZF does not. EP for CZF was shown by Myhill in 1975. The failure of EP in IZF was established by Friedman and Scedrov in [38]. Our decision to take IZF as the first ontology to study is based on the following property: IZF is strong enough to formalize and establish soundness of (the standard) semantics for set theory, i.e., it is self-validating:

1. IZF ⊢ “cHa semantics are sound for IZF” (see Grayson 1977 paper [44]).

2. IZF ⊢ “forcing and sheaf semantics are sound for IZF” (see e.g., Grayson, op.cit., Fourman, 1980 [31]), and section 4, below.

3. IZF ⊢ “realizability is sound for IZF” (McCarty, 1984 Ph.D. Thesis [83]).

(2) and (3) will be shown in some detail below. IZF′ is not known to have the corresponding self-validation property.

2.1 Justifications of some of the choices and omissions of ZF-axioms

Why is the foundation axiom stated in terms of ϵ-induction, rather than in the traditional way: “every set has minimal members”? Because this statement of foundation would give us back all of classical set theory!

Lemma 2.1 (Myhill) “Classical Foundation” (≡ Every inhabited set has an ∈-minimal element) ⇒ LEM (the law of the excluded middle), i.e.,

CF (∀z)[∃x(x ∈ z) → (∃w)(w ∈ z) ∧ ∀t(t ∈ w → t ∉ z)]

gives us back every instance φ ∨ ¬φ of the excluded middle.

proof: Assume “classical foundation” (CF), and let S = {x|(x = 0 ∧ φ) ∨ x = 1} where 0 = {};

1 = {0}. This set is often written {0⌈φ, 1}, the set of “0 when φ, 1”. We will use such sets often. The reader accustomed to classical set theory may want to think of S as a nonstandard subset of {0, 1}, which classically must be either {1} or {0, 1}, but intuitionistically must be thought of as neither (in general).

Since 1 ∈ S we have some s_{o} ∈ S which is minimal, i.e., ∀t(t ∈ s_{o} → (t ∈ S →⊥)). Now s_{o} ∈ S → (s_{o} = 0 ∧ φ) ∨ s_{o} = 1. Suppose s_{o} = 0 ∧ φ. Then φ, hence φ ∨ ¬φ. Suppose, on the other hand s_{o} = 1, then ∀t(t ∈ 1 → (t ∈ S →⊥)) and, in particular, 0 ∈ 1 and 0 ∈ 1 → (0 ∈ S →⊥), so 0 ∈ S →⊥, i.e., (0 = 0 ∧ φ) →⊥, forcing φ →⊥ i.e., ¬φ hence φ ∨ ¬φ. So, for any sentence φ, IZF ⊢ CF → φ ∨ ¬φ.

Notice that only the axioms of Separation, Union, Extensionality and Pairing were used in the proof.

Why the absence of Choice?

Definition 2.2 Define AC to be the axiom

∀S(∃x ∈ S → (∃f : S → ⋃ S)(∀x ∈ S)(f(x) ∈ x))

11the Existence and Disjunction properties for a theory T over a language with closed terms state:

T ⊢ ∃xφ(x) ⇒ T ⊢ φ(a) for some closed term a, and T ⊢ A ∨ B ⇒ T ⊢ A or T ⊢ B. They have long been regarded as fundamental criteria of constructivity of a theory. (See [118]). In the absence of closed terms, as in IZF, the existence property must be stated in terms of a formula D(x) whose extension is precisely a singleton set {a} i.e T ⊢ ∃xφ(x) ⇒ there is a formula D(x) such that T ⊢ ∃xD(x) and T ⊢ ∀x D(x) → φ(x) ∧ ∀x, y(D(x) ∧ D(y) → x = y).

Lemma 2.3 (Diaconescu, 1975)

IZF ⊢ AC → LEM.

i.e. Choice gives us back all instances φ ∨ ¬φ of the Law of the Excluded Middle.

In fact, inspection of the proof shows

Separation + Union + Extension + Pairing + AC ⊢ LEM

Proof: Let S = {{0⌈φ, 1}, {1⌈φ, 0}} i.e., S = {a, b} where:

a = {x|x = 0 ∧ φ or x = 1} b = {x|x = 1 ∧ φ or x = 0}

and assume there is a choice function f : S → ⋃ S such that (∀x ∈ S)f(x) ∈ x. Then, it is easy to see that (f(b) = 1) ∨ (f(a) = 0) ∨ (f(b) = 0 ∧ f(a) = 1). We consider each case.

\underline{case 1:} f(b) = 1. Then 1 ∈ b, so (1 = 1) ∧ φ or 1 = 0 (1 = 1) ∧ φ → φ

(1 = 0) → φ  (by ⊥→ φ)  so we get φ.

\underline{case 2:} f(a) = 0. Then φ.

\underline{case 3:} f(b) = 0 ∧ f(a) = 1. In this case, we obviously have f(a) ≠ f(b), so, in particular, a ≠ b since by hypothesis f is a function ^{12}. But a ≠ b → ¬φ, since φ → (0 = 0 ∧ φ) ∧ (1 = 1 ∧ φ), which implies that a and b are both the set {0, 1}, hence a = b, and therefore, in all cases φ ∨ ¬φ.

So we can’t allow choice in without getting back classical logic. Remark: The countable axiom of choice (for ω, the natural numbers) does not give us so much trouble:

AC^{ω,ω} (∀x ∈ ω)(∃y ∈ ω)φ(x, y) → (∃f ∈ ω^{ω})(∀x ∈ ω)φ(x, f(x))

holds in many non-classical models of IZF^{13} including the realizability model, as we shall see below, but it is not a theorem. (See Fourman’s [31].)

The technique shown above to “refute” AC and CF is known as the method of weak counterexamples, i.e., a proof that IZF ⊢ φ → LEM is called a weak counterexample to φ. We still need to show IZF ⊬ LEM (e.g., using cHa models, non-Boolean toposes, or Realizability interpretations) to establish that φ is not a theorem of IZF.

But first: a few more topics in “naive IZF”

2.2 Powell Ordinals

Definition 2.4 An ordinal is a transitive set of transitive sets, i.e.,

ON(α) ≡^{def} (∀x ∈ α)(T rans(x)) ∧ T rans(α)

where

T rans(x) ≡ ∀z∀w(z ∈ w ∧ w ∈ x → z ∈ x).

12i.e., to be precise:

func(f, D, E) ≡ ∀x∃y(x ∈ D → y ∈ E ∧ ⟨x, y⟩ ∈ f) ∧ ∀x∀y∀z(⟨x, y⟩ ∈ f ∧ ⟨x, z⟩ ∈ f → y = z) so: f(a) ≠ f(b)

means we must have ∃z∃w⟨a, z⟩ ∈ f ∧ ⟨b, w⟩ ∈ f ∧ z ≠ w and also a = b → ∀z∀w⟨a, z⟩ ∈ f ∧ ⟨b, w⟩ ∈ f → z = w, hence f(a) ≠ f(b) ∧ func(f) ⊢ a = b →⊥

13so we don’t have AC^{ω,ω} ⇒ LEM.

Observe that: ON(α) ∧ z ∈ α → ON(z).

The following “positive” and “negative” results may help elucidate the preceding definition, apparently first put forth as a candidate for ordinals in constructive set theory in Powell’s ([97]).

“Negative” Results

Definition 2.5 An ordinal α is decidable if ∈ is decidable in α, i.e., ∀β, γ ∈ α(β ∈ γ ∨ β ∉ γ). α is trichotomous if

∀β, γ ∈ α(β ∈ γ ∨ γ ∈ β ∨ γ = β)

The reader can establish by ∈-induction that the two properties are equivalent. Lemma 2.6 All ordinals decidable ⇒ LEM. Proof: Consider α = {0, {0⌈φ}}, where φ is an arbitrary sentence.

α is an ordinal since x ∈ y ∈ α ⇒ x ∈ 0 ∨ x = 0 ∧ φ ⇒ x = 0 ⇒ x ∈ α. Suppose y ∈ α. Then y = 0 ∨ y = {0⌈φ}

• if y = 0 then y transitive (vacuously).

• if y = {0⌈φ} and w ∈ x ∈ y then x = 0 and w ∈ 0 so w ∈ y, so y transitive.

Now suppose α were decidable: γ, β ∈ α → γ ∈ β ∨ γ ∉ β. Then 0 ∈ {0⌈φ} ∨ 0 ∉ {0⌈φ} Hence φ ∨ ¬φ. Definition 2.7 For α an ordinal, the successor of α, called

α + 1 ( or α^{+})

is defined to be the set

α ∪ {α}.

An ordinal α is a weak limit if ∀β ∈ α∃γ ∈ α(β ∈ γ))

Note that α^{+} is an ordinal: x ∈ y ∈ α^{+} ⇒ x ∈ y ∈ α ∨ x ∈ y = α hence x ∈ α so x ∈ α^{+}. Therefore α^{+} is transitive. Its members are α or members of α, hence they are also transitive. Lemma 2.8 The following imply the excluded middle:

1. α ⊆ β → α ∈ β ∨ α = β ( take α = {0⌈φ}, β = {0})

2. α ∈ β → α^{+} ∈ β ∨ α^{+} = β (try α = 0, α^{+} = {0}, β = {0, {0⌈φ}})

3. Every ordinal is 0 or a successor or a weak limit. proof: Let α = {0, {0⌈φ}} (shown an ordinal in the proof of lemma (2.6)). Then α ≠ 0. α a successor ⇒ α = β ⋃{β} ⇒ β ∈ α, so β = 0 ∨ β = {0⌈φ}

− β = 0 ⇒ β ⋃{β} = {0} ⇒ α = {0} ⇒ ¬φ

− β = {0⌈φ} ⇒ β ⋃{β} = {0⌈φ, {0⌈φ}} ⇒ φ

α a weak limit ⇒ 0 ∈ {0⌈φ}, hence φ. Thus, in all cases, we have φ ∨ ¬φ.

The preceding lemmas show that if we wish to retain the constructivity of our set theory, we cannot hope to preserve such familiar features as the linear ordering of ordinals, nor, more importantly, can we induct on the traditional ordinal cases of successor and limit. So what are ordinals good for in IZF? A lot. They supply us with a non-linear but useful ranking of the universe and with a case-less transfinite induction, We thus retain many of the hallmarks of classical ZF. The following results make this precise.

“Positive” Results

Perhaps the main justification of the Powell Ordinals and the formulation of foundation that IZF retains is that:

∈-induction ⇒

transfinite inductive definitions on ordinals that do not make case distinctions work in IZF.

in a way made precise in the indictive definability theorem below. Note that in the statement of the theorem we use the informal term class function below to denote a formula which is functional for all arguments in its domain, but is not necessarily a set, for reasons we briefly discuss here. We remind the reader that certain “large collections” such as that of all sets (to be called “V” below), cannot be counted as sets, by an argument due to Russell (1906) and known as Russell’s paradox. This runs as follows. If {x : x = x} is a set, then by separation (and validity of x = x), so is {x : x ∉ x}. But the reader can check that

({x : x ∉ x} ∈ {x : x ∉ x}) ⟺ ¬({x : x ∉ x} ∈ {x : x ∉ x})

From A ⟺ ¬A one easily derives falsity, for any A, just in intuitionistic propositional logic.

As just mentioned, we use the letter V to denote the “standard model” of all sets, which is something of a fiction, but one we will have to live with until more semantic notions have been developed. V is officially a formula V (x) whose extension is “all sets”, for example V (x) ≡ x = x. Thus, officially, the statement “x ∈ V ” is a euphemism for V (x). Submodels M of V will be formulas that restrict the choice of x. Properties are then said to be “true in M” if they hold when their quantifiers ∀x, ∃x are relativized to M, that is to say, replaced by ∀x ∈ M, ∃x ∈ M. The reader may want to think of these classes informally as worlds, i.e. models according to the reader’s notion of model, perhaps a set or Kripke model interpreting ϵ as a binary relation.^{14} Since we have not yet developed the model theory we proceed formally in terms of formulas as models.

The ranked universes we will define several times in this article (once we have established the validity of transfinite inductive definitions) are themselves formulas, however these actually denote sets, as can be readily seen applying power set, collection and ϵ-induction to the inductive definition of the hierarchy. Thus the reader may think of these semantics in terms of ranked set-theoretic approximations to the “totality” of the world of sets.

We begin by giving an informal statement of the inductive definability theorem. The formal statement of the theorem follows immediately after.

Theorem 2.9 (Inductive Definability) Let A be a set, ON the ordinals, G a “class function” V × A × V → V. Then there is a unique class function F : ON × A → V such that (∀α ∈ ON)(∀x ∈ A)F (α, x) = G(α, x, (F ↾ α, x)) (1) where F ↾ α, x = {⟨x, β, F (β, x)⟩ : β ∈ α}. The formal statement of this is perhaps a bit less readable: assume φ_{G} is a formula such that ∀a ∈ A∀y∀z∃!wφ_{G}(a, y, z, w) (2) Then we can construct a formula U such that the following holds (∀α ∈ ON)(∀x ∈ A)(∀z)[U(α, x, z) ⟺ φ_{G}(α, x, {⟨x, β, w⟩|β ∈ α ∧ U(x, β, w)}, z)] (3) and

14The metamathematical issues here are delicate. We cannot prove that a set-model of IZF exists within IZF by Gödel’s second incompleteness theorem. We refer the reader to appendix 3, ch. 1 of [67] for an excellent, precise discussion of the issues in a classical context. A constructive outlook poses even greater challenges. A radical constructivist would challenge the existence of mathematical objects independent of their construction, and would not accept anything like a mathematical object containing “everything”. The reader must proceed according to his or her own intuitions!

∀α∀x ∈ A∃!zU(α, x, z)

and, if W (α, x, z) satisfies (3) when substituted for U then

(∀α ∈ ON)∀x z W (α, x, z) ⟺ U(α, x, z).

Intuitively, f is built by taking ordinal-bounded approximations to the class function. We show existence and uniqueness by ∈-induction. The arguments are the same ones used in classical ZF but with some care taken not to invoke ordinal case distinctions in our induction. Definition 2.10 Let A and G be as in theorem (2.9) and δ an ordinal. We define a δ- approximation (to G on A) to be a function f with domain δ × A satisfying DA_{G}(f, δ, A) , which is the formula (∀x ∈ A) (∀α ∈ δ) f(α, x) = G(α, x, (f ↾ α, x)). (4) Lemma 2.11 If g is a δ-approximation and g′ a δ′-approximation then (suppressing the second argument x ∈ A)

g ↾ δ ∩ δ′ = g′ ↾ δ ∩ δ′.

proof: The proof is by ∈-induction on the first ordinal δ. Fix δ′ and a δ′ approximation g′. Suppose, inductively, for every β ∈ δ and every β-approximation h we have

h ↾ β ∩ δ′ = g′ ↾ β ∩ δ′.

Then suppose ξ ∈ δ ∩ δ′. Then α ∈ ξ → α ∈ δ ∩ δ′. Observe also that if g is a δ-approximation it is also a ξ-approximation. Thus, for every x ∈ A, by induction hypothesis

g(ξ, x) = G(ξ, x, (g ↾ ξ, x)) = G(ξ, x, (g′ ↾ ξ, x)) = g′(ξ, x)

Therefore, g(ξ, x) = g′(ξ, x) for every ξ ∈ δ ∩ δ′ which is what we wanted to prove.

Lemma 2.12 Fix G and A as above. Then, for every ordinal δ there is a δ-approximation. proof: By induction: we assume ∃hDA_{G}(h, β, A) for smaller ordinals β, that is to say, for every ordinal β in δ we have a function h with domain β × A satisfying for every ξ ∈ β and x ∈ A

h(ξ, x) = G(ξ, x, (h ↾ ξ, x)).

Then define the ternary relation φ by

φ(β, x, y) ≡^{def} β ∈ δ ∧ (∀h)(DA(h, β, A) → G(β, x, (h ↾ β, x)) = y). (5)

It is easy to check that φ is functional (by the preceding lemma two different witnesses h and h′ to the existential quantifier would agree on δ), and has domain δ. So let

f(x) = y ⟺ φ(β, x, y)

It is easy to show by induction now that f agrees with every γ-approximation for γ ∈ β so f ↾ β, x = h ↾ β, x whence f(β, x) = G(β, x, (f ↾ β, x)) and is therefore a δ approximation.

Now let U(δ, x, y) be the result of ∀β quantification of the right hand side of (5). U is the formula whose existence is asserted in (3), which proves theorem (2.9).

Of course our foundation axiom allows us to make inductive definitions directly on the ϵstructure of sets.

Lemma 2.13 Let A and B be sets, g a function from A × (A × P (B)) to B. Then there is a unique function f : A → B satisfying

∀x ∈ A f(x) = g(x, f ↾ x)

The proof is a straightforward induction, and left to the reader. See remarks after def. (2.19) about induction on other kinds of relations.

We will repeatedly make tacit use of the preceding results in our definitions. For example, we are now able to define, constructively, a unique rank function, as in classical set theory.

Definition 2.14 For any set x we define rk(x) ≡^{def} ⋃{rk(y) + 1 : y ∈ x}

Recall that x + 1 ≡^{def} x ∪ {x}. This definition is justified by lemma (2.13) for x a member of any set A and, letting π_{1} denote right projection,

g(x, z) = ⋃{π_{1}u ∪ {π_{1}u} : u ∈ z}

One must then show that the value of rank(x) is independent of the choice of A. The details are left to the reader.

Lemma 2.15 (∀x)rk(x) ∈ ON

Proof: Recall that α ∈ ON → α + 1 ∈ ON. Also, if x is a set of ordinals ⇒ ⋃ x is an ordinal. For, suppose w ∈ v ∈ r ∈ ⋃ x. Then w ∈ v ∈ r ∈ z ∈ x for some ordinal z. Therefore v must be a member of z, and hence v ∈ ⋃ x and w ∈ r. This shows that ⋃ x transitive and that r is transitive, but then ⋃ x is an ordinal.

Now suppose (∀y ∈ x)rk(y) ∈ ON. Then rk(y) + 1 ∈ ON and ⋃{rk(y) + 1 : y ∈ x} ∈ ON so, ((∀y ∈ x)rk(y) ∈ ON → rk(x) ∈ ON) and by ∈-induction, (∀x)rk(x) ∈ ON.

Lemma 2.16 ∀α ∈ ON rk(α) = α.

Proof: Suppose ∀β ∈ α rk(β) = β (Recall that β ∈ α ⇒ β ∈ ON) Then, if β ∈ α we have β ∈ β + 1 so β ∈ rk(α). Suppose β ∈ rk(α). Then β ∈ γ + 1 for some γ ∈ α forcing β ∈ γ or β = γ. But then β ∈ α. Hence rk(α) = α. With the Powell ordinals we are also able to define a constructive analogue of the ranked “standard model” of set theory.

Definition 2.17 (The Von Neumann Hierarchy) The formula V, the Von Neumann universe of sets, is defined in terms of the stratified or ranked levels V_{α} in the same spirit as classical ZF:

V_{α} = ⋃{P(V_{β}) : β ∈ α}
V = ⋃{V_{α} : ON(α)}

Strictly speaking V is a unary formula satisfying

V (x) ⟺ ∃αON(α) ∧ V (α, x)

where V (α, x) is a formula whose existence is guaranteed by the inductive definability theorem (2.9) with

V (α, x) ⟺ φ_{G}(α, x, {⟨β, x⟩ : β ∈ α ∧ V (β, x)})

and where φ_{G}(α, x, y) ≡^{def} x ⊆ ⋃(π̂_{∗}(y)) ,with π̂_{∗}(y) = {π_{3}z : z ∈ y} and π_{3}(⟨a, b, c⟩) = c.

There is a well-defined notion of rank associated with this hierarchy, namely the function rk(x) we just saw:

Lemma 2.18 (∀x)x ∈ V_{rk(x)+1}

Proof: Say (∀y ∈ x)y ∈ V_{rk(y)+1} i.e., y ∈ ⋃{P(V_{β}) : β ∈ rk(y) + 1}. Then y ∈ P(V_{β}) for some such β. But rk(y) + 1 ⊆ ⋃{rk(z) + 1 : z ∈ x} = rk(x) so β ∈ rk(x). Therefore

y ∈ ⋃{P(V_{β}) : β ∈ rk(x)} = V_{rk(x)}.

But then we have shown x ⊆ V_{rk(x)}, hence x ∈ P(V_{rk(x)}) ⊆ V_{rk(x)+1}. Thus in IZF we can prove ∀x∃α(ON(α) ∧ x ∈ V_{α}), which is to say everything in the universe is ranked. A few more nice facts (left to the reader to prove):

1. V_{α} is transitive.

2. x ∈ V_{α} → rk(V_{α}) ∈ V_{α}

3. α ⊆ V_{α} ∩ ON = rk(V_{α}) but the containment is, in general, strict: IZF⊢ (2 = V_{2} ∩ON) → LEM. (take {0⌈φ} ⊆ {0} so {0⌈φ} ∈ V_{2} ∩ON but if {0⌈φ} ∈ 2 then = 0 or 1 and we can decide φ!)

This makes development of an analogue to Gödel’s L not so straightforward. This property (α = V_{α} ∩ ON) is usually a key part of proving that the constructible sets L are a model of the Axiom of Constructibility (see e.g. Kunen’s [67], or Devlin’s [24]). However, recently, R. Lubarsky has shown that V = L in intuitionistic L [75].

4. rk(x) = ⋂{α : x ∈ V_{α+1}}

Exercise: IZF⊬ ∀α ∈ ON(0 ∈ α + 1) (trivial if you use counterexamples above, but where does the induction argument break down?)

Definition 2.19 A well-founded relation on a set A is a binary relation that is inductive on A, i.e.,

∀X ⊆ A[∀x ∈ A((∀y < x)y ∈ X → x ∈ X) → A ⊆ X]

The following facts are easily established using arguments like those just given for ∈.

• The existence of < -minimal elements for well-founded order relations < gives LEM.

• A well-founded < -relation has no infinite descending chains.

• There is a unique rank function ρ_{<}, such that for each x in A

ρ_{<}(x) = ⋃{ρ_{<}(y)^{+}|y < x}

The rank of any <-relation itself is ρ(<) ≡^{def} {ρ_{<}(x)|x ∈ A}. Since ∈ is well-founded on every ordinal, ρ(∈) is the identity (for ∈ restricted to that ordinal). Thus well-founded orderings are those relations order-isomorphic to ∈ restricted to some ordinal. As in classical set theory, we can define:

α + β = α∪{α + δ|δ ∈ β}
α · β = {α · δ + γ|γ ∈ α, δ ∈ β}
α^{β} = 1∪{α^{δ} · γ + ϵ|γ ∈ α, δ ∈ β, ϵ ∈ α^{δ}}

Since we are stressing analogies with the development of classical set theory, we can supply a “definition” of the natural numbers ω within the set-theoretic universe. The reader is warned, however, that it is a basic tenet of intuitionism (especially of intuitionists who see no need for formal systems) that we can grasp the natural numbers prior to most or all other constructions in mathematics. For many intuitionists, then, the idea of defining the natural numbers within set theory, as if we did not already know what they were (and had already used them to define everything from formulas to finite sets!) is philosophically unacceptable. Perhaps the following result should be stated as: we can recover a copy of the natural numbers within set theory. Many authors (e.g. Beeson [8]) prefer to add the natural numbers as a separate sort in set theory. Nonetheless, we proceed with our constructive analogy of modern ZF.

Definition 2.20 We define ω to be the unique set satisfying

0 ∈ X ∧ ∀x(x ∈ X → x ∪ {x} ∈ X) (6)

and

∀z(0 ∈ z ∧ ∀x(x ∈ z → x ∪ {x} ∈ z) → X ⊆ z) (7)

This definition requires some justification: existence and uniqueness of ω must be established. This is left as an exercise. In IZF, however, the subset structure P(ω) holds surprises: it is consistent to have “nonstandard” proper infinite subsets of the natural numbers which are ordinals, that is to say infinite sub-ordinals α such that α ∉ ω ∧ α ≠ ω. (see section 4.3 ) In fact even the power set of a singleton set has unexpected structure.

A few remarks on P(1) (the powerset of {ϕ}):

Let L = Lindenbaum Algebra for IZF ≡^{def} ⟨S/ ∼, ≤⟩ where

φ ∼ ψ ≡^{def} IZF ⊢ φ ↔ ψ  with  |φ| ≡^{def} {θ|θ ∼ φ}

and

|φ| ≤ |ψ| ≡^{def} IZF ⊢ φ → ψ

and S is the set of sentences over the language ⟨∈, =⟩ of IZF. Then we have the following fact:

The association: |φ| ↦ {x|x = 0 ∧ φ} induces a monotone map ⟨L, ≤⟩ → ⟨P(1), ⊆⟩. It is consistent with IZF that this map be injective.

Monotonicity is obvious. To show that a model exists in which the map is injective, we must show how to build a model for IZF (an Ω-set) out of a given cHa, and apply this to the Lindenbaum algebra. Ω-set models are covered in a later section of this article. But before that we will build a model for IZF, the realizability model, in which P(1) is infinite, in fact not even subcountable (i.e.: we cannot find a subset A ⊆ ω and a surjective function f : A → P(1)) despite the fact that it is consistent with IZF to have R, N^{N}, or any separable metric space subcountable! P(1) is, in fact, the sub-object classifier in any topos model of set theory, and is therefore the object of truth-values of a given model, potentially as rich as the Lindenbaum algebra.

But we have not yet given any semantics for IZF. We begin with a computational approach to the subject, based on the realizability semantics first proposed by Kleene in 1945 [59] and further developed by Kleene [61, 62, 63, 64] and others, and first applied to IZF and CZF by Myhill[89] and Friedman[36]. Many researchers have applied realizability to type theory, analysis and other fields, most notably Kleene and Vesley, Troelstra, Kreisel, Tait, Goodman, Dragalin, Scedrov (and many more). More recently, realizability models of set theory were investigated by Beeson [8] and McCarty [83, 82]. Our presentation is based largely on the work of McCarty.

3 Recursive Realizability Interpretations

3.1 Abstract Applicative Structure

In order to define a realizability interpretation we must have a set of realizing functions on hand, for example the partial recursive functions. We obtain a more general and flexible semantics if we make use of an abstract applicative theory APP of the sort introduced by Feferman in the seventies ([29, 27]) or similar ones developed by e.g.Scott, Fourman, Troelstra, Beeson. This is covered in appendix B.

We will need to talk about models of this kind of applicative theory, called combinatory algebras in the literature. References to sets and operations in the following definition are given informally. The reader should note that (at considerable notational expense) the entire discussion can be formalized within IZF itself. (For a coding of APP and the logic of partial terms within IZF, see McCarty op.cit.

Definition 3.1 A partial combinatory algebra or PCA

A = ⟨A, ·, k, s, d, p, p_{0}, p_{1}, N , s_{N}, p_{N}, 0⟩

is given by a set A (the carrier set, also denoted |A |) with a partial binary operation ·, and the distinguished constants shown interpreting the corresponding constants in the language of APP (see appendix B) and satisfying the following axioms.

pca1 kx ↓ ^{&} kxy ≃ x sxy ↓ ^{&} sxyz ≃ (xz)(yz)

pca2 k ≠ s

pca3 pxy ↓ ^{&} p_{0}(pxy) = x^{&} p_{1}(pxy) = y

where we indicate application u · v by juxtaposition uv and where uv ↓ means uv is defined. Furthermore, N is a subset of A with 0 ∈ N satisfying the following (with N(a) interpreted as a ∈ N ) pca4

N(a)^{&} N(b)^{&} a = b → dxyab = x
N(a)^{&} N(b)^{&} a ≠ b → dxyab = y

pca5

∀x(N(x) → N(s_{N}(x))^{&} p_{N}(s_{N}(x)) = x^{&} s_{N}(x) ≠ 0)

and

∀x(N(x)^{&} x ≠ 0 → N(p_{N}x)^{&} s_{N}(p_{N}(x)) = x).

and induction

φ(0) ∧ ∀x(N(x) ∧ φ(x) → φ(s_{N}(x))) → ∀x(N(x) → φ(x)).

We will sometimes work in the “standard” PCA ω ≡ ⟨N, ·, ↓, 0⟩ on ω, (where N is the natural numbers, e · x ≡ {e}(x) is application of the e^{th} Turing machine code to x also denoted simply by juxtaposition ex), ↓ is the usual convergence in finitely many steps.

We will make repeated use of the fact that the theorems of APP covered in the appendix hold in every PCA: especially combinatory completeness and the recursion theorem.

Now we are ready to discuss the Recursive Realizability Interpretation of IZF as set forth in Charles McCarty’s Ph.D. thesis, in 1984 [83, 82].

The Structure V (A)

Let A be a partial combinatory algebra, i.e. a set with the operations described in the preceding section, defined in IZF. In what follows, A will stand for |A |, the carrier set for the applicative structure A. Any reference to the set of natural numbers ω refers to the extension of the natural number N of the PCA A.

We now define a formula V (A) by transfinite induction, which we can informally think of as a proper class, i.e. a new universe of sets similar to the Von Neumann Hierarchy (see definition 2.17). But now, the universe of sets is built from the ground up together with “ratifying algorithms” that serve as computational witnesses for their creation and properties. As with the definition of the Von Neumann hierarchy, existence and uniqueness (up to logical equivalence) of such a formula follows from Theorem (2.9).

(8)  V (A)_{α} = ⋃_{β<α} P(A × V (A)_{β})
(9)  V (A) = ⋃_{α} V (A)_{α}

For readers familiar with classical set theory: V (A) is the class of A -names in unramified forcing (Shoenfield [108]), with A = set of conditions.

We denote the corresponding model for the standard PCA, also called the realizability “universe” by V (ω).

3.2 Realizability

We begin by expanding L_{ZF} to a (proper-class sized) language L(A) with names for all individuals in V (A)^{15}. We refer the reader to appendix B for discussion of the language and properties of the applicative structure A. Now define:

e ⊩ φ for e ∈ A; φ a sentence over (L(A))

by induction on the structure of φ:

(⋀) e ⊩ φ ∧ ψ ⟺ e_{0} ⊩ φ and e_{1} ⊩ ψ

(where e.g. we abbreviate π_{0}e ⊩ φ by e_{0} ⊩ φ)

(⋁) e ⊩ φ ∨ ψ ⟺ e_{0} = 0 and e_{1} ⊩ φ or e_{0} ≠ 0 and e_{1} ⊩ ψ

in particular e ⊩ φ ∨ ψ ⇒ (e_{0} = 0 ∨ e_{0} ≠ 0)

(¬) e ⊩ ¬φ ⟺ for every f, \underline{not} f ⊩ φ

(⇒) e ⊩ φ → ψ ⟺ for every f, if f ⊩ φ then ef ↓ and ef ⊩ ψ (∃) e ⊩ ∃xφ ⟺ there is an a ∈ V (A) such that e ⊩ φ[x/a]

15We remind the reader that in IZF a “proper class” is abusive language for saying that L(A) is a predicate whose extension is the collection of names of individuals in V (A)

(∀)  e ⊩ ∀xφ ⟺ for every a ∈ V (A)  e ⊩ φ[x/a]

The unusual treatment of quantifiers as compared with e.g. Kleene’s realizability for arithmetic (see appendix) or his second model (see [8]), namely to ignore them computationally, is due to Kreisel and Troesltra (1970, see [65]). The soundness theorem for this realizability interpretation will tell us that it works, and further results stated below will show that it really gives us a picture of the recursive universe. But first, no inductive definition is complete without

BASE CASES

(∈) e ⊩ a ∈ b ⟺ ∃c(⟨e_{0}, c⟩ ∈ b^{&} e_{1} ⊩ a = c)
(=) e ⊩ a = b ⟺ ∀f, d[(⟨f, d⟩ ∈ a ⇒ e_{0}f ↓ ^{&} e_{0}f ⊩ d ∈ b) ^{&}
(⟨f, d⟩ ∈ b ⇒ e_{1}f ↓ ^{&} e_{1}f ⊩ d ∈ a)]

Definition 3.2 V (A) ⊧ φ ≡^{def} (∃e ∈ |A |) e ⊩ φ. In such a case we say “φ is true in the realizability interpretation”.

Theorem 3.3 The realizability semantics defined above (for arbitrary applicative structure A) is sound for IZF. That is to say, if IZF ⊢ φ then φ is true in the realizability interpretation. The soundness property can be established in IZF (the so-called self-validation property).

Proof: (sketch) Note that we have to prove soundness for:

1. intuitionistic logic

2. equality

3. set theory

We illustrate the ideas by carrying out a few examples for each of the above. The reader can check that

k ⊩ φ → (ψ → φ)  i.e., u ⊩ φ ⇒ ku ⊩ ψ → φ  (a)
s ⊩ φ → (ψ → χ) → ((φ → ψ) → (φ → χ)) (b)

(In fact, this justifies the combinators s and k. Combinatory completeness of these two combinators is equivalent to the fact that the deductive closure (under Modus Ponens) of (a) and (b) is the full set of theorems of Propositional Implicational Intuitionistic Logic.)

The reader can easily check that:

λxy · ⟨x, y⟩ ⊩ φ → (ψ → φ ∧ ψ)
λx · x ⊩ ∀y(∀xφ → φ[x/y])
λx · ⟨0, x⟩ ⊩ φ → φ ∨ ψ

and that the term

λxyz · d(y(π_{1}x))(z(π_{1}x))(π_{0}x)

realizes ∨-elimination, that is to say, the axiom scheme

φ ∨ ψ → [(φ → χ) → (ψ → χ) → χ].

EQUALITY Realizing the axiom of identity (∀x(x = x)) is not entirely trivial! We want i such that for every a

i ⊩ a = a.

We will need to make use of the Recursion Theorem for applicative structures (B.2) and the following Closure lemmas:

Lemma 3.4 For each ordinal α the following two properties hold:

(1_{α}) b ∈ V (A)_{α} ⇒ (∃β < α)(∀c)(V (A) ⊧ c ∈ b ⇒ c ∈ V (A)_{β}) i.e., Let E_{⊩}(b) = {c : V (A) ⊧ c ∈ b}. Then b ∈ V (A)_{α} ⇒ E_{⊩}(b) ⊆ V (A)_{β} for some

β < α.

(2_{α}) a ∈ V (A)_{α} and V (A) ⊧ a = b ⇒ b ∈ V (A)_{α}.

We need to prove the above two lemmas by simultaneous ordinal induction, e.g., assume that for β < α (1_{β}), (2_{β}) hold. Let b ∈ V (A)_{α} i.e., b ∈ P(|A| × V (A)_{β})for some β < α. Now suppose e ⊩ c ∈ b. The ∃d⟨e_{0}, d⟩ ∈ b, e_{1} ⊩ c = d. So d ∈ V (A)_{β}. So by (2_{β}) c ∈ V (A)_{β}.

Theorem 3.5 There is an index i such that for any a ∈ V (A) i ⊩ a = a.

What do we need? Assume true for all b ∈ V (A)_{β} with β < α, and let a ∈ V (A). Suppose ⟨f, d⟩ ∈ a. We want i_{0}f ⊩ d ∈ a, and i_{1}f ⊩ d ∈ a, so i_{0} = i_{1} would work. Now to obtain i_{0}f ⊩ d ∈ a we must have ∃c⟨(i_{0}f)_{0}, c⟩ ∈ a (i_{0}f)_{1} ⊩ c = d We can take c to be d itself, but we also need (i_{0}f)_{0} = f and (i_{0}f)_{1} = i. Now we use the inductive hypothesis that i ⊩ b = b for b ∈ V (A)_{β} with β < α. Then we only need to make (i_{0}f)_{0} = f and (i_{0}f)_{1} = i to ensure i ⊩ a = a. In other words, we have; the requirement i_{0} = λf · ⟨f, i⟩ and hence

i = ⟨λf · ⟨f, i⟩, λf · ⟨f, i⟩⟩ = \underbrace{(λw · ⟨λf · ⟨f, w⟩, λf · ⟨f, w⟩⟩)}_{H} i,

so we just need to apply the recursion theorem, or, e.g., let i = Y H, where Y is Curry’s leastfix-point combinator, formalized in the obvious way in AP P.

The realizability of the remaining axioms of equality:

x = y → y = x

x = y ∧ y = z → x = z

x = y ∧ z ∈ y → z ∈ x

φ[x/z] ∧ z = y → φ[x/y] have similar proofs. They require somewhat more intricate use of the (single or double) recursion theorem. (A nice exercise. Answers in McCarty, op.cit.)It will be convenient to have a slight strengthening of the last identity above, which we state as a separate fact, also easily shown by inspection of the proof of soundness of equality:

Lemma 3.6 There is a realizer Sb_{φ} (uniformly computable from a code for the formula φ) which realizes the equality axiom

y = x ∧ φ(x) → φ[y/x] (10)

for any x and y in V (A).

3.3 Soundness for IZF

EXTENSIONALITY Suppose e ⊩ t ∈ a ↔ t ∈ b. We need some u, a function of e, such that u ⊩ a = b

⟨f, d⟩ ∈ a ⇒ u_{0}f ⊩ d ∈ b ⟨f, d⟩ ∈ b ⇒ u_{1}f ⊩ d ∈ a

Let i be the uniform realizer of x = x from above, and observe that ⟨f, d⟩ ∈ a ⇒ ⟨f, i⟩ ⊩ d ∈ a so e_{0}⟨f, i⟩ ⊩ d ∈ b. Hence u = ⟨λx · e_{0}⟨x, i⟩, λx · e_{1}⟨x, i⟩⟩ works. Therefore

λw · ⟨λx · w_{0}⟨x, i⟩, λx · w_{1}⟨x, i⟩⟩ ⊩ EXT .

SEPARATION Given φ, a ∈ V (A) we want c such that, for some e,

e ⊩ ∃c(x ∈ a ∧ φ) ↔ x ∈ c.

Define c = Sep_{φ}^{A}(a) ≡^{def} {⟨f, x⟩ : f ⊩ x ∈ a ∧ φ}. c is easily shown to have the right properties.

This is a typical trick: Build an “internalized” version of desired set. Then show that “inside the realizability interpretation”, it has the right properties.

POWER SET Let

P ow^{A}(a) = {⟨h, x⟩ : h ⊩ x ⊆ a} = c

then

λx · ⟨x, i⟩ ⊩ x ⊆ a → x ∈ c

for, if u ⊩ x ⊆ a, then ⟨u, x⟩ ∈ c so ⟨u, i⟩ ⊩ x ∈ c.

INFINITY Let \overline{n} = \{⟨\underline{m}, \overline{m}⟩ : m ∈ n\}, where \underline{0} = 0, and \underline{n + 1} = ⟨\underline{n}, 0⟩. Then we have, e.g.,

(11)  \overline{0} = ϕ
(12)  \overline{1} = \{⟨0, ϕ⟩\}
(13)  \overline{2} = \{⟨⟨0, 0⟩, \{⟨0, ϕ⟩\}⟩, ⟨0, ϕ⟩\}

⋮ (14)

(15)  \overline{ω} = \{⟨\underline{n}, \overline{n}⟩ : n ∈ ω\} ∈ V (A)_{γ} for any γ > ω

Theorem 3.7 The statements: \overline{0} ∈ \overline{ω}, \overline{n} ∈ \overline{n + 1}, \overline{n + 1} ∈ \overline{ω} are realizable, as is the fact that \overline{ω} witnesses the axiom of infinity. In fact, for any φ, V (A) ⊧ P_{ω}^{φ}(\overline{ω}) where

P_{ω}^{φ}(Z) ≡^{def} φ(0) ∧ (∀x)[(∀y ∈ x)(φ(y)) → φ(x)] → (∀x ∈ Z)(φ(x))

The proof is straightforward, along the lines of lemma (3.9), below.

COLLECTION We wish to establish the realizability, for any φ, and any a ∈ V (ω), of

∀y ∈ a∃zφ → ∃W ∀y ∈ a∃z ∈ W φ.

Suppose u ⊩ ∀x ∈ a∃yφ. Then v ⊩ b ∈ a ⇒ uv ⊩ φ(b, c) (some c ) So let a^{A} = {⟨v, b⟩|v ⊩ b ∈ a} ∈ V (A) (which is a set by the closure lemmas 3.4). By collection in the metatheory, ^{16} there is a C in V with ∀⟨v, b⟩ ∈ a^{A} ∃c ∈ C(uv ⊩ φ(b, c)), and by separation we can cut C down to {c : uv ⊩ φ(b, c)}. Then, by closure again, for some β,C ⊆ V (A)_{β}, so W = A × V (A)_{β} is the witnessing set, and λxλy · ⟨⟨0, i⟩, xy⟩ realizes.

16This is what is meant by self validation of IZF. The assumption of collection in the metatheory validates the assumption of collection in the interpretation. No comparable result is known for IZF’.

Remark

1. The proof of soundness can be carried out in IZF. P rov_{IZF} (^{⌈}(∃e ∈ A)e ⊩ φ^{⌉}) can be established for each axiom φ of IZF.

2. The proof of soundness is uniform in the underlying proofs. There is a recursive function F such that if p is a code for a proof of φ in IZF, then F (p) ⊩ φ

3.4 Term Extraction

In this section we will only consider the standard realizability universe V(ω). A look at the theorems will show that many proofs are sensitive to the way a number of concepts (e.g. arithmetic, computability) are coded into IZF and into the realizability interpretation. Some of the results have a straightforward translation to theorems that hold in V (A) for other PCA’s. The statement that Church’s Thesis holds in the realizability interpretation must be relativized. If non-recursive functions are representable in a PCA, there will be many new instances of the excluded middle realized (see e.g. [8] on this point). The main result of this section, on term extraction, is more delicate. One needs to restrict attention to PCA’s with a recursive diagram. We will not develop this point further here, however. We will stick to the standard PCA, as the example serves to illustrate the possible applications of the realizability interpretation. The development in terms of the Kleene T -predicate is clearly inessential, and done more for mathematical expediency than anything else. One could formulate the term extraction results in terms of a fix-point operator or other implementations of recursion. Also, as remarked below, set theory permits much more straightforward encodings of computation than are used in defining the T-predicate, exploiting complex data types and the strengths of different programming languages. These are precisely the details of interest for applications, and a great deal of work needs to be done here to make efficient use of these results.

We refer the reader to the appendix for a definition of Kleene realizability for intuitionistic arithmetic. Before proving the main result of this section, on term extraction in V (ω) we need a few results about the realizability universe over the standard model ω.

Lemma 3.8 For ω-bounded quantification, IZF-realizability over the standard applicative structure ω = ⟨ω, ·⟩ reduces to Kleene-realizability over ω. That is to say

1. V (ω) ⊧ ∃x ∈ \overline{ω}φ iff (∃g)g_{0} ⊩ φ(\overline{g_{1}}) where g can be effectively constructed from the realizer for ∃x ∈ \overline{ω}φ and a code for the structure of φ

2. V (ω) ⊧ (∀x ∈ \overline{ω})φ iff there is a total recursive \{e\} such that

∀n{e}(n) ↓ ^{&} {e}(n) ⊩ φ[x/n]

Lemma 3.9 (ω-absoluteness of ∈ and =) Let m, n be members of ω. Then, for any e

(16)  e ⊩ m̄ ∈ n̄ ⟺ m < n
(17)  e ⊩ m̄ = n̄ ⟺ m = n

The proof is a straightforward simultaneous induction on n. For the first claim, in the ⇒ direction, observe that we must have ⟨e_{0}, c⟩ ∈ n̄ for some c which is forced to be (the image of) an integer k̄, with k < m by the definition of n̄. But also e_{1} ⊩ m̄ = k̄, whence by the induction hypothesis for the second claim, m = k, and so m ≤ n. The remaining details are left to the reader.

The following lemma refers to Kleene’s T and U predicates (covered in detail in e.g. [118, 90]) which formalize computation, convergence and output of partial recursive functions in arithmetic, and which are used to define a PCA structure on ω. Depending on how one chooses to represent integers and arithmetic in set theory, a similar scheme can be used to formalize computation in the language of IZF. In fact, in IZF one may directly formalize more easily any computational paradigm: Turing machines or one’s favorite programming language, since one has available sets, sequences and arbitrary functions to carry out the coding. In fact, because of the widespread use of set theory in formalizing mathematics, most automata or recursion theory textbooks already state their definitions in this language (and describe, e.g. Turing machines as “sets of quintuples”). The reader has much less work to do than in the natural numbers! Nonetheless, for the sake of a uniform presentation, we refer to Kleene’s predicates in the results below. The reader may substitute his or her favorite paradigm of computation in what follows.

Lemma 3.10 Let T (x, y, z) and U(x) be the Kleene T and U predicates, formalized in the language of IZF. Then for any n, m, u ∈ ω we have, in IZF,

V (ω) ⊧ T (\overline{m}, \overline{n}\overline{u}) ⟺ T (m, n, u)
V (ω) ⊧ U(\overline{u}) ⟺ U(u)

The proof is a straightforward but tedious induction on the clauses defining the T -predicate, and makes use of the fact that atomic formulas for ω are absolute. We can strengthen the preceding result to the following set-theoretic generalization of a result of Kleene’s ([61], § 82) which McCarty calls “Kleene absoluteness”.

Theorem 3.11 If R(m, n) recursive, then there is an index e_{R} such that

V ⊧ φ_{R}(m, n) ⇒ \{e_{R}\}(m, n) ⊩ φ_{R}(\overline{m}, \overline{n})
V (ω) ⊩ φ_{R}(\overline{m}, \overline{n}) ⇒ V ⊧ R(m, n)

where φ_{R} is the formalization of R in set-theory.

Once again the proof is straightforward but lengthy. The reader is advised to look at the proof of Lemma 47^{N}, §82 of Kleene’s [61]. A predicate is general recursive iff numeralwise representable in arithmetic, and hence, for each numerical instance of its arguments, either provable or disprovable, from which one obtains (using the soundness of realizability for HA) the equivalence of its numerical realizability in ω with its truth in ω. This argument can, of course, be lifted to IZF, and depends exactly on the choice of coding of arithmetic and computation as already discussed above.

Corollary 3.12 (Term extraction in V (ω)) There are algorithms u and v which map a realizer e of the existence and totality of a functional specification to an index, ue for the function, and a realizer, ve that the index computes the right values. More precisely, if:

e ⊩ (∀x ∈ ω)(∃y ∈ ω)(φ(x, y))

then

(ve)(n) ⊩ φ(\overline{n}, ue(\overline{n}))

If, in addition φ, as a numerical predicate, is recursive, the algorithm ue computed by umeets the specification (∀x ∈ ω)(∃y ∈ ω)(φ(x, y)), in the sense that, in IZF, for every n in ω, we have φ(n, {ue}(n)).

proof: We are given e ⊩ \overline{n} ∈ ω → ∃y ∈ ωφ(\overline{n}, y) Now, using the uniform realizer i of x = x computed in Theorem 3.5 we have ⟨n, i⟩ ⊩ \overline{n} ∈ ω and

\{e\}(⟨n, i⟩) ⊩ ∃y ∈ ωφ(\overline{n}, y)

Thus for some a in V (ω) we have \{e\}(⟨n, i⟩) ⊩ a ∈ ω ∧ φ(\overline{n}, a). which implies

\{e\}(⟨n, i⟩)_{0} ⊩ a ∈ \overline{ω}
\{e\}(⟨n, i⟩)_{1} ⊩ φ(\overline{n}, a)

Thus, for some m ∈ ω we have ⟨\overline{m}, (\{e\}(⟨n, i⟩))_{00}⟩ ∈ ω, hence

(18)  ({e}(⟨n, i⟩))_{00} = m

and

(19)  (\{e\}(⟨n, i⟩))_{01} ⊩ \overline{m} = a.

Now recall that there is a uniform realizer Sb_{φ} of substitution in formulas φ (lemma 3.6). Therefore

Sb_{φ} · ⟨(\{e\}(⟨n, i⟩))_{01}, (\{e\}(⟨n, i⟩), ⟩ ⊩ φ(\overline{n}, \overline{(\{e (⟨n, i⟩))_{00}}).

So, letting

(20)  u = ΛeΛn[({e}(⟨n, i⟩)})_{00}]
(21)  v = Sb_{φ} · ⟨({e}(⟨n, i⟩))_{01}, {e}(⟨n, i⟩), ⟩

we have the indices claimed in the statement of the theorem.

Notice that in the absence of the fact that φ is recursive, we only know that the witnessing function u works in the realizability universe, i.e., v realizes that u meets the specification. Now assume φ is recursive as a number-theoretic predicate. Then we have, by the preceding work:

1. If a recursive predicate is realized, it’s true.

2. If ∀x ∈ ω∃y ∈ ωφ(x, y) is IZF-provable, it’s realized by some code uniformly computable from the proof.

3. There are u,vsuch that e ⊩ ∀x ∈ ω∃y ∈ ωφ(x, y) ⇒ (∀n ∈ ω)(ve)n ⊩ φ(n, (ue)n).

Numbers (1), (2) and (3) above imply that there is an algorithm which compiles IZF proofs of ∀y ∈ ω∃x ∈ ωφ(x, y) for recursive φ into an algorithm which computes y in terms of numerical x.

This means IZF is a suitable (impredicative, and arbitrarily high order^{17}) formalism for extracting computations from proofs.

The reader seeking a more careful statement of this fact should note that the point of painstakingingly developing the semantics in IZF is to make it possible to formalize all the arguments within IZF. That is to say, given a recursive number-theoretic predicate φ with Gödel number ^{⌈}φ^{⌉}, there is a recursive function F such that for every proof-code p

IZF ⊢ P rov_{IZF} (p,^{⌈}∀x ∈ ω∃y ∈ ωφ(x, y)^{⌉})  →  ∀n ∈ ωφ(n, {F (p,^{⌈}φ^{⌉})}(n))

where P rov is a (primitive recursive) binary provability predicate formalizing (in the language of IZF) the fact that the first argument encodes a proof of the formula whose Gödel number is the second.

Countable Choice and Church’s Thesis By formalizing the term extraction argument above in two different ways we obtain a number of important corollaries about the realizability universe.

Corollary 3.13 (Countable Choice) V (ω) ⊧ AC^{ω,ω} i.e.

∀x ∈ ω∃y ∈ ωφ(x, y) → ∃f ∈ (ω ⇒ ω)∀x ∈ ωφ(x, f(x)) (22)

is realized in V(ω).

17in the sense discussed in the introduction

Corollary 3.14 (Church’s Thesis) V (ω) ⊧ CT_{0} (Church’s Thesis for total functions), i.e.,

∀n ∈ ω∃m ∈ ωφ(n, m) → ∃e∀n∃m∃p(T (e, n, p) ∧ U(p, m) ∧ φ(n, m)) (23)

In (22), we formalize functionality within the realizability structure. In (23) we formalize computability. See McCarty’s [83] or [82] for the details. Note: CT_{1}, the partial analogue of CT_{0}, namely:

“ All partial functions on N are partial recursive”

FAILS in V (ω) (otherwise we can solve halting problem recursively in the real world, see Mc-Carty’s op.cit.). We can recover a weaker CT_{1} by restricting the domain of functional relations to ω-stable sets. A ⊆ ω is ω-stable whenever ∀x ∈ ω(¬¬x ∈ A → x ∈ A) The collection of ω-stable sets is called P(ω)^{st}.

3.5 Strong Intuitionistic Counterexamples

Note that in Section 2 we argued that unrestricted Choice AC or Classical Foundation could not be admitted into IZF because they imply all instances of the excluded middle and hence make our theory classical, and much of our hard work fruitless. In fact a proof that

IZF + φ ⊢ LEM

for some classically valid sentence φ amounts to a proof of independence from IZF provided we know that IZF doesn’t already imply the law of the excluded middle.

Theorem 3.15 If ψ is closed and IZF ⊢ ψ → ∀x(φ ∨ ¬φ) for arbitrary φ then V (ω) ⊧ ¬ψ, hence if ψ is a theorem in classical ZF then it is independent of IZF.

Proof: Let K = the set of solutions to the halting problem

K = {n ∈ ω : {n}(n) ↓} ≡ {n ∈ ω : ∃uT (n, n, u)}

As remarked prior to lemma (3.10), the T predicate can be formalized in IZF via the same sort of coding scheme used to formalize it in HA. By the lemma, this formalization is absolute: if T (m, n, u) is realized, it is true. By lemma (3.8) and the absoluteness of ∈ and = on ω (lemma (3.9) and of recursive predicates ( theorem 3.11), we can easily show that K is absolute as well:

Lemma 3.16 Let \overline{K} = \{⟨n, \overline{n}⟩ : n ∈ K\}. Then:

(\overline{K} ∈ V (ω)_{w+1})

and

∀n ∈ ωV (ω) ⊧ \overline{n} ∈ \overline{K}  iff  n ∈ K

proof: An easy consequence of the cited lemmas. Left to the reader.

Now, back to the proof of the theorem (3.15) above.

Suppose V (ω) ⊧ ψ. Then, by soundness V (ω) ⊧ ∀x ∈ \overline{ω}(x ∈ \overline{K} ∨ ¬x ∈ \overline{K}) ⇒ ∃ total index g such that {g} : ω → 2 and for each n

\{g\}(n) = 0 and V (ω) ⊧ \overline{n} ∈ \overline{K} or \{g\}(n) = 1 and V (ω) ⊧ ¬\overline{n} ∈ \overline{K}

By Lemma (3.16) {g} solves the halting problem (in the metatheory) which is impossible, so nothing realizes ψ. Therefore, V (ω) ⊧ ¬ψ.

Corollary 3.17 IZF ⊬ LEM.

Observe that both results are intuitionistically valid. Other “famous” weak counterexamples are so treatable: Regularity, AC, the function succ is not strictly monotone on ON. By similar treatment we obtain the failure other famous classical theorems in V (ω):

1. Every bounded monotone sequence of reals converges.

2. Totality of ()^{−1} on R − {0}

3. Intermediate Value Theorem

4. Maximum Theorem for continuous functions on compact sets.

3.6 Some famous “nonstandard” consistency results

The following are realized in V (ω) hence consistent with IZF (and, for that matter with IZF + AC^{ω,ω} + CT_{0} + DC^{ω}, the latter axiom being countable dependent choice, see e.g. [83]), where we recall that set X is subcountable if there is a function from ω onto X, i.e., more precisely, ∀x ∈ X∃y ∈ ω⟨y, x⟩ ∈ f (so X may be empty).

• UP ∀x∃n ∈ ωφ → ∃n ∈ ω∀xφ (the uniformity principle)

• Ω = P({0}) is not subcountable

• UZ ∀x(φ ∨ ¬φ) → ∀xφ ∨ ∀x¬φ

• Every metric space, in particular R, is subcountable.

Theorem 3.18 V (ω) ⊧ UP

Proof: Let e ⊩ ∀x∃y(y ∈ \overline{(}w) ∧ φ). Since quantification is generic, e ⊩ ∃y ∈ \overline{ω}φ uniformly for all a ∈ V (ω). Thus, there is a b such that uniformly for all a e_{1} ⊩ φ(a, b) and e_{01} ⊩ b = \overline{e_{00}} and, in fact, by lemma (3.8), there is a g effectively computable from e and a code for the structure of φ such that g_{1} ⊩ φ(a, \overline{g_{0}}). Therefore ⟨⟨g_{0}, i⟩, g_{1}⟩ ⊩ ∃\overline{n} ∈ \overline{w}∀xφ

Corollary 3.19 V (ω) ⊧ Ω is not subcountable

Proof: Work in IZF assuming UP: Say Ω is subcountable. Then ∃f such that ∀x ∈ Ω∃y ∈ ω⟨y, x⟩ ∈ f. Thus ∀x∃y ∈ ω⟨y, x ∩ {0}⟩ ∈ f by UP ∃y∀x⟨y, x ∩ {0}⟩ ∈ f, which contradicts functionality of f. Thus

IZF + UP ⊢ ¬Ω subcountable.

Hence V (ω) ⊧ Ω is not subcountable by soundness.

We now proceed to define a Kripke style semantics for IZF. The reader interested in pursuing realizability (in Analysis, Set Theory, Arithmetic) further should consult the references below especially the work of Friedman, Myhill, Dragalin, Beeson, McCarty, Hyland, Pitts, Phoa, van Oosten. In McCarty’s work, there is also a detailed discussion of finiteness and its many nonequivalent varieties (subfinite, Dedekind finite) in IZF and in the realizability interpretation, as well as a series of results linking the arithmetic of finite and infinite cardinals in IZF to isols and Recursive Equivalence Types, studied by Myhill, Nerode, Dekker and others. McCarty also establishes a number of “transfer theorems” showing that, over a restricted class of sets, there is a translation θ^{∗} of IZF formulas θ, such that θ holds in IZF iff its translation is realizable. This translation exhibits a certain correspondence between “recursion theoretic” concepts in the real world, and their constructive counterparts in the realizability interpretation (e.g. unsolvability of the halting problem vs. failure of the excluded middle). Finiteness in topoi is also analyzed in [58].

4 Forcing in Constructive Set Theory (Unramified)

In this section we develop a “standard” intuitionistic semantics for IZF, formalizable in IZF. Following the definitions and soundness proof, we discuss embedding a Kripke model of a firstorder theory into a model of set theory. We conclude with a simple independence result.

4.1 Kripke models over V (K)

Take IZF for a metatheory. Let K be a partially ordered set, with a minimal element, called 1. Its members will be called nodes. Define the class V (K) as follows: (by transfinite recursion in IZF)

V_{α}(K) = ⋃{P(V_{β}(K) × K) : β ∈ α}
V (K) = ⋃_{α∈ON} V_{α}(K).

Notice that:

1. Since the definition is by induction on all predecessors, it is legitimate induction in IZF.

2. V (K) is a proper class, hence its official status is a predicate: x ∈ V (K) is shorthand for

(∃α)(ON(α) ∧ x ∈ V_{α}(K)).

3. V (K) is just the usual class of names from unramified Cohen forcing.

x ∈ V (K) → x ∈ V_{α}(K)  some α
→ x ∈ P(V_{β}(K) × K)  some β ∈ α
→ x ⊆ V_{β}(K) × K.

Thus x is a name: a set of ordered pairs {⟨x_{1}, p_{1}⟩, ⋯, ⟨x_{n}, p_{n}⟩, ⋯ } where each x_{i} is itself a “name” (∈ V_{β′}(K) for some β′ ∈ β) and p_{i} is a member of K (also called a node, a stage or condition) in the literature).

(Readers familiar with unramified Cohen forcing should note that we adhere to the “Kripke” order convention in V (K): the order on K is the reverse of that of a “notion of forcing”, so in particular in V (K), 1 is the minimal element.)

Definition of Forcing

Forcing is a relation ⊩ between nodes p and formulas built up from atomic sentences and formulas:

a = b, a ∈ b

where individuals a, b are members of V (K) and quantifiers range over members of V (K)

p ⊩ a = b ⟺ \{ \begin{matrix}∀⟨c, q⟩ ∈ a & ∀r ≥ p, q & r ⊩ c ∈ b \\ ∀⟨c, q⟩ ∈ b & ∀r ≥ p, q & r ⊩ c ∈ a \end{matrix}

p ⊩ a ∈ b ⟺ (∃c)(∃q ≤ p) (⟨c, q⟩ ∈ b and p ⊩ a = c)
p ⊩ ∃xφ(x) ⟺ (∃a) p ⊩ φ(a)
p ⊩ ∀xφ(x) ⟺ ∀a∀q ≥ p q ⊩ φ(a)

Note: Forcing is only defined for sentences. p ⊩ ψ(x) means p ⊩ ∀xψ(x).

The remaining clauses are the usual ones:

p ⊩ φ ∧ θ ⟺ p ⊩ φ and p ⊩ θ
p ⊩ φ ∨ θ ⟺ p ⊩ φ or p ⊩ θ
p ⊩ φ → θ ⟺ ∀q ≥ p q ⊩ φ ⇒ q ⊩ θ

Lemma 4.1 (monotonicity lemma)

p ⊩ φ ^{&} q ≥ p ⇒ q ⊩ φ.

Proof: straightforward induction on formulas.

Definition 4.2 V (K) ⊧ φ, i.e., φ is true in the forcing interpretation just in case

(∀p ∈ K) p ⊩ φ.

Theorem 4.3 (Soundness)

IZF ⊢ φ ⇒ V (K) ⊧ φ.

Proof: The soundness of forcing for pure intuitionistic logic is routine and covered in any text on Kripke forcing. The reader is referred to e.g. [118] for details. We check a few clauses of soundness for the theory of equality and the nonlogical axioms. equality axioms:

∀x(x = x) (24) ∀x, y(x = y → y = x) (25) ∀x∀y∀z(x = y ∧ y = z → x = z) (26) ∀x∀y∀z(x = y ∧ x ∈ z → y ∈ z) (27) ∀x∀y∀z(x = y ∧ z ∈ x → z ∈ y) (28)

The arguments are also straightforward inductions on rank in V (K). Only two clauses are sketched here. We establish soundness of transitivity (26) and atomic substitution (27) by simultaneous induction (on rank of x, y). Assume (26) and (27) hold for x′, y′ of lower rank (< α) and now suppose x, y and z are of rank α and that p ⊩ x = y ∧ y = z i.e.,

∀⟨a, r⟩ ∈ x ∀q ≥ p, r q ⊩ a ∈ y and vice-versa.
∀⟨b, s⟩ ∈ y ∀t ≥ p, s t ⊩ b ∈ z and vice-versa.

Now q ⊩ a ∈ y implies that ∃⟨b, s⟩ ∈ y such that s ≤ q and q ⊩ a = b. Also, q ≥ s, p so q ⊩ b ∈ z. Now a, b are of lower rank than x, y so by the inductive hypothesis for (27) q ⊩ a ∈ z, hence p ⊩ x = z, establishing (26) for rank α.

Now suppose p ⊩ x = y ∧ y ∈ z. Then there is a pair ⟨b, s⟩ ∈ z with s ≤ p and p ⊩ b = y. But then by (26) and (26) we have p ⊩ b = x. But then ⟨b, s⟩ ∈ z and s ≤ p and p ⊩ b = x, which is the definition of p ⊩ x ∈ z. Now we sketch the proof of soundness of the nonlogical axioms of IZF, not all that different from the corresponding proof of soundness for realizability.

4.2 Soundness of IZF Axioms

Once again we carry out the proof of soundness of the set theoretic arguments constructively, using arguments formalizable in IZF. Appeal to certain specific axioms in the proof will be pointed out. extensionality

We must show that for any p,

p ⊩ ∀t(t ∈ x ↔ t ∈ y) → x = y

Suppose q ∈ K and a ∈ V (K) and q ⊩ (a ∈ x → a ∈ y) ∧ (a ∈ y → a ∈ x), that is to say,

∀s ≥ q ∃⟨c, r⟩ ∈ x r ≤ s ^{&} s ⊩ a = c ⇒ ∃⟨c′, r′⟩ ∈ y, r′ ≤ s^{&} s ⊩ a = c′ (29)

and conversely. Now suppose ⟨d, l⟩ ∈ x and k ≥ l, q. Then ⟨d, l⟩, and k satisfy the hypothesis of (29), namely k ≥ q and ⟨d, l⟩ ∈ x, l ≤ k and k ⊩ d = d i.e.,k ⊩ d ∈ x. Then k ⊩ d ∈ y by the conclusion of (29). But this fact and its symmetric counterpart with a and b reversed imply q ⊩ x = y.

pairing

We want to show for any p that p ⊩ ∀x, y∃z(∀t)(t ∈ z ↔ t = x ∨ t = y). We just construct a formal internal pair in V (K). Let UP_{K}(x, y) = {⟨s, 1⟩, ⟨y, 1⟩} which we can build, by the axiom of pairing in the metatheory. Suppose p ⊩ t ∈ UP_{K}(x, y), i.e., for some pair ⟨c, q⟩ ∈ UP_{K}(x, y) we have q ≤ p and p ⊩ t = c which implies (c = x ∨ c = y) and q = 1, so either p ⊩ t = x or p ⊩ t = y which is what we wanted to show. Conversely, if p ⊩ t = x ∨ t = y then since 1 ⊩ x ∈ UP_{K}(x, y) and 1 ⊩ y ∈ UP_{K}(x, y), by soundness of logic and equality axioms p ⊩ t ∈ UP_{K}(x, y). So UP_{K}(x, y) is the unordered pair z whose existence we are trying to establish.

union

We resort again to the formalization technique. For each x ∈ V (K) define the formal or internal union

U^{K}(x) ≡^{def} {⟨w, p⟩ : p ⊩ ∃z(w ∈ z ∧ z ∈ x)}.

We want to show that for any p

p ⊩ ∀x∃A(∀t)[(∃z(t ∈ z ∧ z ∈ x) → t ∈ A)].

We take U^{K}(x) as our A. For suppose that p ⊩ ∃z(a ∈ z ∧ z ∈ x) then ⟨a, p⟩ ∈ U^{K}(x) hence p ⊩ a ∈ U^{K}(x).

subset formation

We must show p ⊩ ∀z∃a(∀t)(t ∈ a ↔ t ∈ z ∧ φ).

Define S ≡ S^{K}(z, φ) ≡^{def} {⟨a, p⟩ : p ⊩ a ∈ z ∧ φ}. And now let p ⊩ t ∈ z ∧ φ. Then ⟨t, p⟩ ∈ S so

p ⊩ t ∈ S. Conversely, if p ⊩ t ∈ S then ∃⟨c, r⟩ ∈ S with r ≤ p and p ⊩ c = t. Hence r ⊩ c ∈ S ∧ φ. By substitution of equals (27) p ⊩ t ∈ z ∧ φ.

power set

We must show p ⊩ ∀z∃a(∀t)(t ⊆ z → t ∈ a) where t ⊆ z is shorthand for ∀ω(ω ∈ t → ω ∈ z). Let P^{K}(z) = {⟨a, p⟩ : p ⊩ a ⊆ z} and let p ⊩ a ⊆ z. Then ⟨a, p⟩ ∈ P^{K}(z) so p ⊩ a ∈ P^{K}(z).

∈-induction

We want to show that for every p

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

so suppose that for any x,

p ⊩ ∀y(y ∈ x → φ(y)) → φ(x) (30)

and assume that for any b ∈ V_{β}(K) with β ∈ α we have p ⊩ φ(b). Let a ∈ V_{α}(K). Now take q ≥ p and observe that q ⊩ ∀y(y ∈ a → φ(y)) i.e., if r ≥ q and r ⊩ b ∈ a then for some ⟨c, s⟩ ∈ a with s ≤ r we have r ⊩ c = b. Now ⟨c, s⟩ ∈ a ⇒ c ∈ V_{β}(K) for some β ∈ α and r ⊩ c = b ⇒ b has the same rank as c (this is the forcing version of the rank lemma, from Section 3.2). i.e., c ∈ V_{β}(K) ∧ r ⊩ c = b ⇒ b ∈ V_{β}(K) so p ⊩ φ(b) hence r ⊩ φ(b). But

(∀r ≥ q r ⊩ b ∈ a → r ⊩ φ(b)) → q ⊩ ∀y(y ∈ a → φ(y))

by (30) and the fact that q ≥ p and q ⊩ φ(a). In particular, for p itself, p ⊩ ∀y(y ∈ a → φ(y)) so p ⊩ φ(a). By ∈-induction in the metatheory ∀α∀a ∈ V_{α}(K) p ⊩ φ(a) i.e., p ⊩ ∀xφ(x).

4.3 Examples

A two-node model of IZF

Let K be the ordered set

\begin{matrix}n_{1} \\ n_{0} \end{matrix}

Then observe that e.g. V_{0}(K) = ∅ and that V_{1}(K) includes such members as ∅ and {x : x = 0 ∧ φ} for each φ in the language of IZF. V_{2}(K) contains (but is much larger than)

{∅, ⟨∅, n_{0}⟩, ⟨∅, n_{1}⟩}. We now consider two members of V (K), where 0 ≡^{def} ∅, 1 = {∅} and

2 ≡^{def} {0, 1} (not to be confused with the names of the nodes, in boldface!).

(31)  a = {⟨0, n_{0}⟩, ⟨1, n_{0}⟩, ⟨2, n_{1}⟩}
(32)  b = {⟨0, n_{0}⟩, ⟨2, n_{0}⟩, ⟨1, n_{1}⟩}

a and b look alike at “stage” n_{1}but are distinguishable at the root node n_{0}of K. We leave as an easy exercise for the reader the proof of the following facts which make this observation precise.

1. n_{1} ⊩ a = b

2. n_{0}¬ ⊩ a = b

3. n_{0} ⊩ ¬¬a = b

We can think of a forcing model V (K) with K linearly ordered as describing “sets through time” ( a name given by Lawvere to the corresponding topos, see section (5)). At each node p (in any V (K)) we can define an equivalence relation

x ∼_{p} y ≡^{def} p ⊩ x = y.

We can think of each node p of this model as having a (proper-class) domain V (K)(p) = {[x]_{p} : x ∈ V (K)} where [x]_{p} is the equivalence class of x under ∼_{p}, which may prove to be empty, if no node ≤ p occurs in some pair belonging to x. For p ≤ q there are maps

ι_{p}^{q} : V (K)(p) → V (K)(q).

given by ι_{p}^{q}([x]_{p}) = [x]_{q}. Thus V (K) is a Kripke-model with transition or restriction functions as discussed in section (5).

Forcing preserves truth over Kripke models

Let K = ⟨K, D, ≥_{K}, ⊩_{K}⟩ be a Kripke model over any language. We are going to show how K can be extended to a forcing model of set theory in a way that preserves truth in the original model.

It will be convenient to reverse the order of K and attach a maximal root node 1 (if it doesn’t already have one) in the usual way. We have to be a bit meticulous with notation, since we are going to be talking about truth “⊧”in the Kripke model, forcing in the original Kripke model, denoted by ⊩_{K}, and forcing in the resulting model V (K) of set theory, which we will simply denote ⊩. Let D be the domain function of K. Now form V (K) as in the preceding section and define, for x ∈ V , x̂ = {⟨ŷ, 1⟩ : y ∈ x}. The association x ↦ x̂ defines a well-known canonical embedding of V into V (K) i.e.

Lemma 4.4 The association x ↦ x̂ is injective and if x ∈ y then x̂ ∈ ŷ is forced in V (K)

Proof: exercise.

In addition we also have:

Lemma 4.5 Equality of canonical objects is absolute, i.e., p ⊩ â = b̂ iff a = b in V for any p.

Now, back to our “interpreted Kripke model”. For each relation R of the language of K define

R^{∗} = {⟨â, p⟩ : p ⊩_{K} r(a)}  and  D^{∗} = {⟨â, p⟩ : a ∈ D(p)}

The relation K ⊧ φ will now be defined within V (K). This really means that ^{18} we are defining a new binary relation ⊧ between Kripke models (sets with binary relation ≥ and monotone atomic assignment and domain function) and codes for formulas. In set theory, such codes will, of course, be sets. But we will let formulas φ stand for their own codes ^{⌈}φ^{⌉}, to avoid putting brackets everywhere. Now we have to spell out how the atomic formula K ⊧ φ is interpreted in V (K). The definition is by induction on the structure of φ.

Definition 4.6

p ⊩ (K ⊧ r(a)) ≡^{def} p ⊩ â ∈ R^{∗}
p ⊩ (K ⊧ φ ∧ ψ) ≡^{def} p ⊩ (K ⊧ φ and K ⊧ ψ)
p ⊩ (K ⊧ φ ∨ ψ) ≡^{def} p ⊩ (K ⊧ φ or K ⊧ ψ)
p ⊩ (K ⊧ φ → ψ) ≡^{def} p ⊩ (K ⊧ φ ⇒ K ⊧ ψ)
p ⊩ (K ⊧ ∀xφ(x)) ≡^{def} ∀⟨a, r⟩ ∈ D^{∗} ∀q ≥ p, r q ⊩ (K ⊧ φ(a))
p ⊩ (K ⊧ ∃xφ(x)) ≡^{def} ∃⟨a, r⟩ ∈ D^{∗} r ≤ p and p ⊩ (K ⊧ φ(a))

Theorem 4.7 ∀φ p ⊩ (K ⊧ φ) ⟺ p ⊩_{K} φ

Proof: straightforward.

18just as with formalized Tarski semantics for classical set theory

Forcing Nonstandard Ordinals

This example is an adaptation of a result of Grayson [44]. We show using a model quite different in flavor from realizability models that “every ordinal is decidable” and “every ordinal is trichotomous” (see def. (2.5)) are not theorems of IZF.

We start with the standard partial order K = ⟨N, ≤⟩. We want to produce a model in which we can build an ordinal α such that

1. x ∈ y ∈ α → x ∈ α (α transitive)

2. ¬¬(m ∈ α) (weakly infinite)

3. ¬(ω ⊆ α) (ω ≠ α)

i.e., α is a nice example of a “nonstandard” infinite ordinal mentioned earlier. From these properties it will follow: that α is not trichotomous and that equality is not decidable on α.

Our strategy is to have, in V (K), the critical property (2) satisfied by

p ⊩ m ∈ α iff p ≥ m.

We can think of this as the satisfaction of the positive requirement

P_{m} : ∃p ≥ m p ⊩ m ∈ α

and the negative requirement

R_{m} : ∃p ≥ 0 p¬ ⊩ m ∈ α

where R_{m} is guaranteed by the restraint q ⊩ m ∈ α only if q ≥ m, i.e., q’s below m are restrained from meeting P_{m}, somewhat in the spirit of injury arguments in recursion theory. The forcing construction: We work in the forcing structure V (K). We recall that members of V can be embedded in V (K) as follows: for x ∈ V, let x̂ = {⟨ŷ, 0⟩ : y ∈ x}. In particular,

m̂ = {⟨n̂, 0⟩ : n ∈ m}
ω̂ = {⟨n̂, 0⟩ : m ∈ ω}

The non-standard ordinal α We now define α = {⟨n̂, n⟩ : n ∈ ω}.

Recall that

p ⊩ a ∈ b ≡ ∃c∃q ≤ p(⟨c, q⟩ ∈ b ∧ p ⊩ c = a)
p ⊩ a = b ≡ ∀⟨c, d⟩ ∈ a ∀r ≥ p, d (r ⊩ c ∈ b)
∀⟨c, d⟩ ∈ b ∀r ≥ p, d (r ⊩ c ∈ a)

Lemma 4.8 (Absoluteness of Equality and ∈ ) For any p ∈ K

1. p ⊩ m̂ ∈ n̂ iff m ∈ n,

2. p ⊩ m̂ = n̂ iff l = n.

proof: By simultaneous induction on n. Suppose the claim is true for k < n, that is to say, the formulas m ∈ k and m = k are true if and only if their hatted counterparts are forced at any node.

1. Suppose p ⊩ m̂ ∈ n̂.

Then there is a c and q ≤ p with ⟨c, q⟩ ∈ n̂ and p ⊩ c = m̂. By definition of n̂ we have c = k̂ for some k ∈ n and q = 0. By induction hypothesis k = m so m ∈. Conversely, suppose m ∈ n. Then (by soundness of the equality axioms) 0 ⊩ m̂ = m̂ and by definition ⟨m̂, 0⟩ ∈ n̂, so 0 ⊩ m̂ ∈ n̂ (so this is forced by any p ∈ K by mononicity).

2. Suppose p ⊩ m̂ = n̂ and that k ∈ m. Then ⟨k̂, 0⟩ ∈ m̂ so k̂ ∈ m̂ is forced by 0 and hence by any p ∈ K. By part 1, which has just been established for n, we must have k ∈ n. Thus m ⊆ n. The same argument with m and n reversed yields m = n.

Conversely, suppose m = n. Then m̂ = n̂ is forced by soundness of the identity axiom.

Lemma 4.9 p ⊩ m̂ ∈ α if and only if p ≥ m

proof: p ⊩ m̂ ∈ α if and only if for some c and q ≤ p we have ⟨c, q⟩ ∈ α and p ⊩ m̂ = c which implies c = m̂ by the preceding lemma, hence also q = m by the definition of α. So m ≤ p must hold. Since ⟨m̂, m⟩ ∈ α and p ≥ m will force m̂ ∈ α.

Lemma 4.10 0 ⊩ x ∈ y ∧ y ∈ α → x ∈ α.

proof: Say p ⊩ x ∈ y ∧ y ∈ α. Then ∃c∃q ≤ p ⟨c, q⟩ ∈ α and p ⊩ y = c. Thus, for some m ∈ ω we have c = m̂, q = m, m ≤ p, and p ⊩ y = m̂. By soundness p ⊩ x ∈ m̂ which yields p ⊩ n̂ = x for some n ∈ m and, by lemma (4.9) p ⊩ n̂ ∈ α since p ≥ m ≥ n. Thus, by soundness p ⊩ x ∈ α.

Lemma 4.11 0 ⊩ ¬¬m̂ ∈ α for every m ∈ ω.

proof: This translates to (∀p ≥ 0)(∃q ≥ p) q ⊩ m̂ ∈ α, which, by lemma (4.9) holds if and only if (∀p ≥ 0)(∃q ≥ p) q ≥ m which is trivially true.

Lemma 4.12 0 ⊩ x ∈ y ∧ y ∈ z ∧ z ∈ α → x ∈ z.

Pick p ≥ 0 and suppose p forces the antecedent of the formula in question. From the proof of 4.10, p̂ ⊩ z = m̂ for some m ∈ ω. By soundness and transitivity of m, p̂ ⊩ x ∈ z.

Lemma 4.13 0¬ ⊩ ω̂ ⊆ α.

In fact more is true: 0 ⊩ ¬ω̂ ⊆ α. proof: Let m > p. By lemma (4.9) p¬ ⊩ m̂ ∈ α. But p ⊩ m̂ ∈ ω so p¬ ⊩ ω̂ ⊆ α.

Now we can establish the properties of interest for α.

Corollary 4.14 In V (K) we have:

α ∉ ω̂ ∧ α ≠ ω̂ ∧ ω̂ ∉ α.

proof: If α ∈ ω̂ we could not have ¬¬m̂ ∈ α for every m̂. i.e., 0 ⊩ α ∈ ω̂ ⇒ 0 ⊩ α = n̂ so 0 ⊩ ¬¬m̂ ∈ α would give 0 ⊩ ¬¬m̂ ∈ n̂ i.e., ∀p∃q ≥ p q ⊩ m̂ ∈ n̂ which will fail for m ≥ n.

Now from the preceding lemma, we know that ω̂ ⊈ α, so in particular → ω̂ ≠ α

Finally, ω̂ ∈ α together with transitivity of α would force ω̂ ≤ α.

Corollary 4.15 α ≤ ω̂ ∧ α ∉ ω̂ ∧ α ≠ ω̂.

Corollary 4.16 α is not zero, successor, or a weak limit.

proof: α ≠ 0 is obvious. Recall that α a weak limit means ∀_{β} ∈ α∃γ ∈ α(β ∈ γ). But m ⊩ m̂ ∈ α but for no n ∈ ω with m̂ ∈ n̂ do we have m ⊩ n̂ ∈ α, so m does not force “α a weak limit” Successor: If α = β + 1 ≡ β ⋃{β}, then the fact that α ⊆ ω̂ would give β ⋃{β} ⊆ ω̂, hence β ∈ ω̂. This means 0 ⊩ β = n̂ for some n, and for that matter that β + 1 ∈ ω̂ i.e., α ∈ ω̂ which is false in V (K).

5 Ω-sets, Categories and Toposes

We now explore a powerful extension of our semantics for constructive set theory using the tools of category and sheaf theory, developed in the 1940’s to study algebraic geometry and topology. Before looking at IZF we will look at other formulations of constructive set theory (so-called local set theory) which are more type-theoretic in flavor, and which preceded the interpretation of IZF in a topos.

5.1 From Kripke Models to cHa’s

Definition 5.1 A Heyting Algebra is a lattice with a binary operation → in which, for every member a, b, c

a ≤ b → c ⟺ a ∧ b ≤ c. (33)

We will also have use for a slightly weaker notion, namely that of a Heyting prealgebra, a pre-order ⟨A, ≤, ∧, ∨, ⊤, ⊥⟩ with finite meets, joins, top and bottom elements satisfying (33). The pre-order is sometimes denoted ⊢.

Another concept that will prove useful is that of a partial equivalence relation, (a PER), which has found extensive use in theoretical computer science, to interpret types in the polymorphic lambda calculus and in dependent type theories.

Definition 5.2 Let X be a set. A partial equivalence relation (or PER) R on X is a symmetric, transitive relation, i.e., equivalence relation on a subset of X. The domain of R is the set {x ∈ X : xRx}.

Definition 5.3 A cHa or complete Heyting algebra Ω is a Heyting algebra with a join or supremum operation ⋁ defined for arbitrary subsets D of the carrier set. Equivalently, a cHa is a complete lattice satisfying the ∧ ⋁-distributive law

a ∧ (⋁ D) = ⋁{a ∧ d : d ∈ D}.

with implication given by

a → b = ⋁{x : x ∧ a ≤ b}.

as the reader can check (or see e.g. [57] for a proof). Recall that in a Boolean algebra, i.e. a complemented distributive lattice, the complement ā of an element a (the unique element x satisfying a ∨ x = ⊤ and a ∧ x = ⊥) is the largest member disjoint from a

ā = ⋁{x : x ∧ a ≤ ⊥}

where ⊥ is the least member of the algebra. Thus

ā = a → ⊥.

However, in a cHa, we no longer have a ∨ (a → ⊥) = ⊤. Thus a → ⊥ is sometimes called a “pseudocomplement”, and a → b a relative pseudocomplement.

Perhaps the most important example of a cHa is afforded by topological spaces ⟨X, O(X)⟩ consisting of a set X together with a collection O(X) of subsets of X satisfying

• ϕ ∈ O(X) and X ∈ O(X).

• O(X) is closed under finite intersections and arbitrary unions.

Members of O(X) are called open subsets of the topology. If X is a topological space then the collection O(X) of open subsets of X is a cHa with ⋁ as ⋃, ∧ as ∩, the order given by inclusion, and

U_{1} → U_{2} = Int(\overline{U_{1}} ∪ U_{2}).

where for any subset A, Int(A), the interior of A, is defined by

⋃{U ∈ O(X) : U ⊆ A}.

There are a number of categories associated with cHa’s, depending on the properties one wishes morphisms to preserve. The category of frames has cHa’s as objects and, as morphisms, functions preserving the order relation, ∧ and ⋁. The category of locales is the opposite category: it has the same objects, but a frame morphism from A to B is regarded as a locale morphism from B to A. (In the case of topological cHa’s, the former category corresponds to open maps and the latter continuous maps).

The cHa semantics developed in this section is fully constructive, and formalizable in IZF. We must take a little care, from a constructive point of view, to show that a given Heyting algebra is indeed complete. Even finite Boolean Algebras are not necessarily complete constructively. As some of the examples studied in the first section may suggest, one cannot prove in intuitionistic logic that the two element lattice {⊤, ⊥} is complete. (Its completeness implies the schema ¬P ∨ ¬¬P , but is not quite as strong an assertion as the full scheme of the excluded middle LEM. See e.g. [32] pp. 313-314).

5.2 Logic in a cHa, Ω-sets

Let K be a Kripke model over some language. A natural topology on K is given by taking all upwards closed sets

O(K) = {S ⊆ K : ∀x ∈ S∀y ∈ K y ≥ x → y ∈ S}.

The monotonicity property of Kripke models guarantees that for any sentence θ, the set [[θ]] = {p ∈ K : p ⊩ θ} is an open set in this topology. θ is true in K iff it is forced at all nodes, i.e. iff [[θ]] = K. Sentences forced only at some nodes, will have [[θ]] a proper subset of K. Thus the cHa O(K) is an object of truth values for the model, with the maximal set K playing the role of ⊤. It is easily checked, for example, that

(34)  [[A ∧ B]] = [[A]] ∩ [[B]]
(35)  [[A ∨ B]] = [[A]] ∪ [[B]]
(36)  [[A → B]] = [[A]] ⇒ [[B]].

If K has a growing domain, elements d ∈ D ≡ ⋃_{K} D(p) will have a “degree of existence” or extent given by Ed = {p ∈ K : d ∈ D(p)}. The reader can think of this example as motivating the following definition.^{19}

Ω-set Semantics

Definition 5.4 Let Ω be a cHa. An Ω-set A = ⟨A, Ω, [[· = ·]]⟩ consists of a set A together with a cHa-valued partial equivalence relation [[ ]] : A × A → Ω (whose action is usually denoted [[x = y]]) satisfying symmetry and transitivity:

[[x = y]] = [[y = x]]  and  [[x = y]] ∧ [[y = z]] ≤ [[x = z]].

19This definition, in the case of topological cHa’s, predates Kripke’s semantics by more than a decade. It was proposed by Tarski and McKinsey’s in the 1940’s [85, 23]

It will be convenient to define the extent of a member a of A to be [[a = a]] and a singleton to be a map s : A → Ω satisfying

s(a) ∧ [[a = b]] ≤ s(b)  and  s(a) ∧ s(b) ≤ [[a = b]].

There is a natural induced notion of weak equality, or equivalence [[a ≡ b]] defined by (Ea ∧ Eb) ⇒ [[a = b]].

We now show how to interpret first order logic in an Ω set. We consider models over arbitrary languages and then consider the case of IZF. First some preliminaries. Let V be a set of variables and A the set of atomic formulas over L.

Definition 5.5 If D is a set, a function η : V → D is called a D-environment. The set of D-environments will be denoted E_{D}. Let ⟨A, ⟨⟨· = ·⟩⟩⟩ be an Ω-set. Then an n-ary Ω-relation R is a mapping

R : D × ⋯ × D → Ω

satisfying

⋀⟨⟨a_{i} = b_{i}⟩⟩ ∧ R(a_{1}, …, a_{n}) ≤ R(b_{1}, …, b_{n})
R(a_{1}, …, a_{n}) ≤ ⋀⟨⟨a_{i} = a_{i}⟩⟩

A n-ary Ω-function f : M → N from an Ω set M to another N is an n-ary function on the underlying sets satisfying, for every a in M

⟨⟨F a = F a⟩⟩ ∧ ⟨⟨a = b⟩⟩ ≤ ⟨⟨F a = F b⟩⟩ and ⟨⟨F a = F a⟩⟩ ≤ ⟨⟨a = a⟩⟩

An Ω function is total if the last inequality is replaced by equality.

Now we define interpretations. Fix a language L, and once again, let ⟨A, ⟨⟨· = ·⟩⟩⟩ be an Ω-set.

Definition 5.6 An Ω-Interpretation D = ⟨D, Ω, [[.]], η⟩ for the language L consists of a set D, a D-environment η and a meaning function [[.]]_{η} which assigns an Ω-relation [[R]] to each relation symbol R in L, and an (n-ary) Ω-function [[F ]] from D to D for each (n-ary) function symbol F in L (in particular it assigns values [[c]] ∈ D to constant symbols c).

An Ω-interpretation is called total if it assigns only total functions to function symbols in the language. An Ω-interpretation assigns values [[t]]_{η} in D for every open term t over the language L and truth values [[A]]_{η} ∈ Ω as follows:

terms:

• [[c]]_{η} ≡^{def} [[c]] for constants c

• [[x]]_{η} ≡^{def} η(x) for variables x

• [[F (t_{1}, …, t_{n}) ]]_{η} ≡^{def} [[F ]]( [[t_{1} ]]_{η}, …, [[t_{n}]]_{η})

formulas: For atomic formulas we have

• [[R(t_{1}, …, t_{n}) ]]_{η} ≡^{def} [[R]]( [[t_{1} ]]_{η}, …, [[t_{n}]]_{η})

• [[t_{1} = t_{2} ]]_{η} ≡^{def} ⟨⟨ [[t_{1} ]]_{η} = [[t_{2} ]]_{η}⟩⟩

For nonatomic formulas:

(37)  [[A ∧ B]]_{η} = [[A]]_{η}∧ [[B]]_{η}
(38)  [[A ∨ B]]_{η} = [[A]]_{η}∨ [[B]]_{η}
(39)  [[A → B]]_{η} = [[A]]_{η} ⇒ [[B]]_{η}
(40)  [[(∃x)A(x) ]]_{η} = ⋁_{d∈D} [[A(x) ]]_{η[x/d]}
(41)  [[(∀x)A(x) ]]_{η} = ⋀_{d∈D} [[A(x) ]]_{η[x/d]}

where, if η is an environment, d ∈ D and x ∈ V, we define the environment η[x/d] by

η[x/d](y) = \{ \begin{matrix}η(y) & if y ≢ x \\ d & if y ≡ x \end{matrix}

We say a sentence A is true in the Ω-interpretation D

D ⊧ A

if [[A]]_{η} = ⊤. A formula A is valid if for every Ω interpretation D we have D ⊧ A. We write this ⊧ A. If Γ is a set of sentences, we write Γ ⊧ A if for every Ω-interpretation in which all sentences in Γ are true A is also true.

Theorem 5.7 (Soundness and Completeness) Γ ⊢ A  iff  Γ ⊧ A.

The proof of soundness is is a straightforward induction. One can prove completeness (in a classical metatheory) by showing that each Kripke model gives rise to an elementarily equivalent O(K)-interpretation, where O(K) is the topology discussed at the beginning of section (5.2), and using the completeness of Kripke semantics. Completeness can also be established directly by building a Lindenbaum algebra for a given theory (which is a Heyting algebra with some infinite suprema and infima but not all), and then embedding it in a cHa in a way that preserves all meets and joins. We refer the reader to e.g. chapter 13 of [118] for details.

Ω-set semantics for set theory

As with models for classical set theory, we can extend the notion of Ω-interpretation to proper class domains (i.e. predicates) D ≡ V (Ω). As with the class-models V (ω) and V (P) we defined for realizability and Kripke forcing, we will write d ∈ D to mean D(d) and think of the “extension” of D as a domain of interpretation.

Definition 5.8 Let Ω be a cHa. We now define the Ω-hierarchy of ranked universes V (Ω)_{α} and W (Ω)_{α} for each ordinal α.

(42)  W (Ω)_{α} ≡^{def} ⋃_{β∈α} V (Ω)_{β}

(43)  V (Ω)_{α} ≡^{def} {f : W (Ω)_{α} → Ω}
(44)  V (Ω) ≡^{def} ⋃_{α∈ON} V (Ω)_{α}

Observe that the last line defines the formula V (Ω)(x) to be

(∃y)(ON(y) ∧ V (Ω)_{y}(x))

where V (Ω)_{α} is defined by transfinite induction in IZF.

Truth in V (Ω) We now define by simultaneous induction an interpretation [[·]] mapping atomic formulas to Ω. Let b, a ∈ V (Ω).

(45)  [[b ∈ a]] ≡^{def} ⋁{ [[b = x]] ∧ a(x) : x ∈ dom(a)}
(46)  [[b = a]] ≡^{def} ⋀{ [[x ∈ b]] ↔ [[x ∈ a]] : x ∈ dom(a) ∪ dom(b)}

Sentences are now interpreted as with ordinary Ω-interpretations (37-41).

(47)  [[A ∧ B]] = [[A]]∧ [[B]]
(48)  [[A ∨ B]] = [[A]]∨ [[B]]
(49)  [[A → B]] = [[A]] ⇒ [[B]]
(50)  [[(∃x)A(x) ]] = ⋁{ [[A(d) ]] : d ∈ V (Ω)}
(51)  [[(∀x)A(x) ]] = ⋀{ [[A(d) ]] : d ∈ V (Ω)}

Note that this definition is formalizable in IZF: by the axiom of separation { [[A(d) ]] : d ∈ V (Ω)} i.e. {x ∈ Ω : ∃d V (Ω)(d) ∧ x = [[A(d) ]]} is a subset of Ω. Since Ω is a cHa, this subset has a supremum and an infimum in Ω.

Definition 5.9 Given a cHa Ω, and a closed formula φ in the language of IZF, we say the formula is true in the Ω-set interpretation, and write

V (Ω) ⊧ φ

iff ⊤_{Ω} ≤ [[φ]]. We write ⊧_{Ω} φ to mean φ is true in every Ω-set interpretation.

The following theorem can be established within IZF as a metatheory, along the lines of the soundness proof in section (4).

Theorem 5.10 Let φ be a closed formula in the language of IZF. Then

IZF ⊢ φ ⇒ ⊧_{Ω} φ

Scott-presheaves

Definition 5.11 Let Ω be a cHa. A Scott-Ω-presheaf A is a triple ⟨A, E, ↿⟩ consisting of a set A, and maps of extent E : A → Ω (whose action on a member a of A is written Ea), and of restriction ↿: A × Ω → A satisfying, for all a ∈ A and all p, q ∈ Ω.

1. a ↿ Ea = a.

2. (a ↿ p) ↿ q = a ↿ (p ∧ q)

3. E(a ↿ p) = Ea ∧ p.

We define equality on Scott-presheaves as follows:

[[a = b]] = ⋁{p : p ≤ Ea ∧ Eb^{&} a ↿ p = b ↿ p}

Lemma 5.12 Scott-presheaves (with the induced equality defined above) are Ω-sets, and are partially ordered by the relation

a ≤ b ≡^{def} a = b ↿ Ea.

proof: Exercise (or see [32]).

With the induced partial order just defined, we can speak of joins of subsets of a Scott presheaf.

Definition 5.13 A Scott presheaf A is separated if whenever a subset B of A has a join it is unique. An Ω-set A is separated if for every a, b ∈ A

[[a ≡ b]] = ⊤  ⇒  a = b.

The reader can check that a presheaf is separated if and only of it is separated as an Ω-set.

5.3 Presheaves, Sheaves and Topoi

In the remainder of this article we assume some elementary familiarity with category theory, in particular, the definitions of functors, adjoints, (co-) products, pullbacks, (co-) equalizers, limits, natural transformations, equivalence of categories, along the lines of, e.g. the first 25 pages of [68], or chapter 1 of [77]. We use the notation Ar(A) for the collection of arrows (or morphisms) of a category, | A | for its collection of objects. The opposite category of A is denoted A^{o}. The notation will be reserved for monic arrows and [figure] for epics. We denote the Hom-set of arrows in a category C from A to B by C (A, B). We also use the terminology “x is a generalized element of A” if x is an arrow from some object C to A, and will sometimes write this x ∈_{C} A. We will also call x “an element of A at stage C”. All categories are assumed locally small: the class of arrows from one object to another is a set.

We begin with some definitions and facts that will prove useful. We refer the reader to the cited references for proofs.

Definition 5.14 A category is said to be small if the class of arrows in the category is a set. If A and B are categories, the functor category A^{B} has as objects the functors from A to B, and as morphisms natural transformations. If C is a category and A an object, then the slice category C /A has as objects the arrows ^{p} A in C targeted at A. A morphism between two objects p A and ^{q} A is an arrow θ of C making the resulting diagram commute:

\overline{θ}

[figure: p; q]

A

When C is the category Set , we can think of an object X ^{f} A in the slice category as an A-indexed family {X_{a} : a ∈ A} where X_{a} = f^{−1}(a). Morphisms are just maps which preserve A-indexing. Thus, up to isomorphism, objects in this category can be thought of as functors from A viewed as a category, the discrete category ( whose objects are members of A and whose morphisms are just the identities a a) to Set . This observation can be made precise as follows.

Lemma 5.15 There is an equivalence of categories Set ^{A} ≅ Set /A.

Set -valued functor categories Set ^{A} (and their duals Set ^{A^{o}}) constitute an extremely important class of examples. In particular when A is a monoid (a category with only one object), a group (a monoid in which every arrow is an iso) or even an arbitrary small category, Set ^{A} is called the category of monoid actions, group-actions, or, respectively, of (right) A -sets (see [33]). These are sets X endowed with an index operator □ : X →| A |, and a partial binary operation from X and Ar(A) to X, indicated by juxtaposition xa, defined whenever the index x□ of x is equal to the source of a and satisfying (xa)b = x(ab).

Lemma 5.16 The category of left (resp. right) A -sets is equivalent to Set ^{A^{o}} (resp. Set ^{A}).

Given an object X in a category C, we recall that the operations

A ↦ C (X, A)  and  A ↦ C (A, X)

define the covariant and contravariant Hom-functors from C to Set , whose actions on arrows are given by composition. Given (A ^{f} A′) in C, the morphism C (X, f) : C (X, A) → C (X, A′) takes X ^{ξ} A to X ^{f∘ξ} A′. C ( , X) acts contravariantly by right-composition. These functors are called representable. The object X is called the representative of C ( , X) (and its dual).

Lemma 5.17 (Yoneda) The embedding C → Set ^{C^{o}} induced by mapping an object X to the contravariant Hom-functor represented by X is a full and faithful functor (with action on arrows given by composition).

If F is a contravariant functor from C to Set then there is a bijection

Nat(C ( , X), F) ≅ F (X)

given by mapping α in Nat(C ( , X), F) to α(X)(𝕀_{X}) which is natural in both F and X.

When considering Kripke-Joyal semantics, below, we will use the fact that every natural transformation α in Nat(C ( , X), F) acts by α(Y)(φ) = F (φ)(a) where Y ^{φ} X and a = α(X)(𝕀_{X}). We will sometimes refer to the natural transformation α by the name â.

The proof is straightforward, one has to check that the given functor and bijection have the required properties. We refer the reader to [76, 33] for proofs, further discussion, and on how to make the naturality statement precise. We remark for the time being that representable functors play an important role in the categorical semantics for logic defined below, and that the preceding lemma also tells us that every category can be fully and faithfully embedded in a Set -valued functor category (hence, cf. definitions below, in a topos of presheaves).

Definition 5.18 A presheaf F is a contravariant functor from a cHa Ω to Set . F is called a presheaf on X if Ω is the cHa O(X) associated with a topological space X. A morphism of presheaves λ : F → G is a natural transformation of the functors. For a given topological space X we write preSh (X) for the category of presheaves on X with presheaf morphisms.

Every Scott presheaf is easily construed a presheaf and conversely. Suppose A = ⟨A, E, ↿⟩_{Ω} is a Scott-presheaf. Define the contravariant functor F_{A} : Ω → Set by

F_{A}(p) ≡^{def} {x ∈ A : p ≤ Ex}

on objects and let the action on morphisms F_{A}(p ≤ q) = ι_{p}^{q} : F_{A}(q) → F_{A}(p) be given by ι_{p}^{q}(x) = x ↿ p. The reader can check functoriality of F_{A}. Conversely if F is a contravariant functor from a cHa Ω to Set then, letting

A^{F} = ⨆_{Ω} F (p)  E⟨p, x⟩ = p  ⟨p, x⟩ ↿ q = ⟨p ∧ q, x⟩

it is easily checked that ⟨A^{F} , E, ↿⟩ is a Scott-presheaf.

Suppose F is a presheaf. A sheaf on X is a presheaf F : O(X)^{op} → Set satisfying an additional glueing or compatibility property.

Definition 5.19 Let F be a presheaf on X. Let U be an open subset of X, and suppose {V_{i} : i ∈ I} is a family of open subsets of U such that

U ⊆ ⋃ V_{i}

Such a family is called an open cover of U. Since F is a contravariant functor, we have, for each pair of open sets U ⊆ V a restriction map

ι_{U}^{V} ≡^{def} F (U ↪ V) : F (V) → F (U)

satisfying ι_{W}^{U} ∘ ι_{U}^{V} = ι_{W}^{V}. Now suppose that S = {s_{i} : i ∈ I} satisfies s_{i} ∈ F (U_{i}) for all i. We call S a family of sections. We call S compatible if for every pair of members s_{i}, s_{j} in S we have

ι_{U_{i}∩U_{j}}^{U_{i}}(s_{i}) = ι_{U_{i}∩U_{j}}^{U_{j}}(s_{j}). (52)

F is called a sheaf on X if given any open set U ⊆ X, any open cover of U and compatible family of sections S there is a unique section s in F (U) of which each member in S is a restriction, that is to say, for each U_{i} in the cover and s_{i} in S

s_{i} = ι_{U_{i}}^{U}s

The sheaves on a space X form a category with natural transformations as morphisms, which we denote Sh (X).

A slight generalization of the definition given above helps make the link with Kripke models precise.

Definition 5.20 Let K be a partial order viewed as a category. Then a K-presheaf is a functor from K to Set , whose action on morphisms p ≤ q is is called restriction or transition ι_{p}^{q} : K(p) → K(q).

It is straightforward to show that K-presheaves are Kripke models with transition maps ι_{p}^{q} : K(p) → K(q) from the domain at node p to that at node q (see e.g. [118] for a discussion of how they can be viewed as sheaves over an appropriate completion of K).

Sheaves can be defined over an arbitrary category endowed with a Grothendieck topology, also called a site. This yields a generalization of Beth semantics, or of classical Cohen forcing, and plays an important role in the application of topos theory to independence results in intuitionistic and classical ZF. The details are beyond the scope of this treatment. We refer the reader to e.g. [115, 57, 33, 68] for further discussions of these notions.

Definition 5.21 We say a category is finitely complete if it has finite products, a terminal object 1, (the limit of the empty diagram) and equalizers. It is finitely co-complete if the opposite category is complete, i.e. if it has an initial object, coproducts and coequalizers. A category C is said to have exponents if for each pair of objects A, B there is an object B^{A} (also written [A ⇒ B]) and an arrow

ev_{A,B} : B^{A} × A → B

which represents the Hom-set C (A, B) in the sense that, for any object C there is a unique arrow λ_{A}f, called the transpose of f making the following diagram commute.

B^{A} × A

[figure: ev] B

[figure: C × A; λ_{A}f × 𝕀_{A}; f]

Equivalently, there is a bijection

C (A × B, C) ≡ C (A, C^{B})

natural in A, B and C, that is to say, × B and ^{B} are adjoints. If f : A → B then the transpose of fπ_{1} : 1 × A → B is often written ^{⌈}f^{⌉} : 1 → B^{A} and called the name of f.

A category with finite products and exponents is called cartesian closed.

The definition of finitely complete is equivalent to the assertion that the category C has all finite limits.

Definition 5.22 A topos is a finitely complete category with exponents and a subobject classifier, that is to say, an object Ω and a morphism

⊤ : 1 → Ω

often called “true”, such that for every object A and subobject B ^{m} A there is a morphism χ_{m} making the following diagram a pullback

[figure: B; m; A; 1; !_{B}; ⊤; Ω; χ_{m}]

χ_{m} is called the classifier or characteristic morphism of m. The subobject B ^{m} A is said to be classified by χ_{m}, and is also referred to by some authors [68] as its kernel.

Definition 5.23 (Power objects and epsilon) If A is an object in a topos E , then Ω^{A} is called the the power object of A (and often written P A). We then define the ∈_{A}-relation to be the object classified by the evaluation map composed with the twist:

A × Ω^{A} ^{↶} Ω^{A} × A ^{ev} A.

The object classified by ev is called epsiloff (Freyd) and written ∋_{A}.

A relation U_{C} ^{u} B × C is called universal (for C) if every relation R ^{r} A × C with range C factors through a morphism A ^{f} B and U_{C}, that is to say, for some morphism f the following is a pullback

[figure: R; U_{C}; A × C; r; f × 𝕀_{C}; B × C; u]

Freyd and Scedrov give the following nice characterization of power objects and ∋ “from basics” and use it as a starting point for defining topoi.

Lemma 5.24 A cartesian category is a topos iff each object C has a universal relation

U_{C} ^{u} B × C

in which case u is the ∋_{C} relation, and the domain B is the power object Ω^{C}.

We conclude our general discussion of topoi with a few more important results.

Lemma 5.25 In a topos every arrow A ^{f} B has an image Im(f): a minimal subobject of B through which f factors, and a factorization

A ^{e} [figure] Im(f) ^{m} B

with e epic and m monic (called an epi-mono factorization). The factorization is unique up to isomorphism.

Lemma 5.26 (Kock, Mikkelsen) Every topos is finitely co-complete.

We refer the reader to [68] for a simple proof that makes use of the internal logic. Up to now, the only topos we have seen is Set . There are many others.

Lemma 5.27 For any topological space X, preSh (X) and Sh (X), the categories of presheaves and sheaves on X, are topoi.

A topos is said to be spatial if it is Sh (X) for some X. Not every topos is spatial (e.g. the effective topos, below).

Lemma 5.28 In a topos, the set Sub(A) of subobjects of an object A, forms a cHa.

The following result, due to Freyd, allows us to uniformly extend the notion of quantification, as understood in Set , to topoi, in a very general way.

Lemma 5.29 (Fundamental lemma of topos theory) Every slice E /A of a topos is a topos, and the canonical functor Δ : E → E /A preserves finite limits and power objects. Thus, in particular, the functor

f^{#} : E /B → E /A

(induced by the arrow A ^{f} B in E by pulling back) has a right adjoint.

The import of this lemma for interpreting quantification is discussed below.

5.4 Logic in a Topos: three views

With this machinery, we are able to interpret set-theoretic logic formalisms in a topos in several related ways that extend their conventional meaning in the category of sets, or in some of the categories we have seen, to arbitrary topoi. The first two interpret a typed language (with bounded quantification and sorts) which has been dubbed by some authors [13] local set theory. The third interprets type-free IZF, and is a straightforward generalization of the Ω set semantics of the preceding section. We briefly motivate the definitions with a look at how logic and the basic set-theoretic notions are captured in some familiar categories.

Let us denote by Ω_{c} the classical object of truth-values {⊥, ⊤} that is to say the subobject classifier in Set . Then we recall that classical Boolean propositional operators ∗ : Ω_{c} × Ω_{c} → Ω_{c} are given by:

• ∧z = ⊤ ⟺ z ∈ {⟨⊤, ⊤⟩}.

• ⇒ z = ⊤ ⟺ z ∈ {⟨⊤, ⊤⟩, ⟨⊥, ⊥⟩, ⟨⊥, ⊤⟩}.

If we think of logical predicates p, q as maps from some domain A to Ω_{c}, and ⟨p, q⟩ : A → Ω_{c} ×Ω_{c} the canonical product map a ⟼ ⟨p(a), q(a)⟩, then p ∧ q and p ⇒ q are equal as functions to ∧ ∘ ⟨p, q⟩ and ⇒ ∘ ⟨p, q⟩. Also observe that the object classified by ⇒ (i.e. the subset it maps to ⊤) is precisely the ≤ relation on Ω_{c} × Ω_{c}. We would like to define this relation in a way that does not make reference to elements of Ω_{c}, so as to use it in an arbitrary topos. A simple characterization is suggested by the fact that

≤= {⟨x, y⟩ ∈ Ω_{c} × Ω_{c} : x = x ∧ y}

i.e. ≤ is the largest subset of Ω_{c} × Ω_{c} on which left projection and conjunction agree, hence the equalizer of the corresponding arrows.

Observe that bounded universal quantification maps an open formula p defined on some domain B × A to a new formula ∀_{x∈A}p : B → Ω_{c}. Its action can be captured algebraically by defining

∀_{A} : Ω_{c}^{A} → Ω_{c}

to be the characteristic function of the singleton set {A} ∈ ℘(A), and observing that

∀_{A} ∘ λ_{B}p : B → Ω_{c}

is the characteristic function of {b ∈ B : {a ∈ A : p(b, a)} = A}, that is to say, it is precisely the predicate ∀_{x∈A}p(x, y) (where y ranges over B).

Logical Connectives as Adjoints There is another perspective on the interpretation of logic in a topos, due to Lawvere, which is of independent interest because it generalizes to categories with less than the full structure of a topos and has played a fundamental role in categorical formulation of type theory and of realizability-style semantics. We have already seen how ∧ and → can be viewed as adjoints in a cHa (this adjunction is expressed in (33)). We can do the same for universal and existential quantification in a topos. Let p be a predicate on B × A, i.e. a member of Ω_{c}^{B×A}. As we remarked before, quantification over A is a map from Ω_{c}^{B×A} → Ω_{c}^{B}. We can view it as an operation induced by the projection π : B × A → B, as follows. In the foregoing discussion in Set we identify the set of characteristic functions Ω_{c}^{X} with the power set ℘(X). Let ℘ be the contravariant power set functor from Set to itself mapping sets to their power sets, and functions f from X to Y to the map f^{∗} : ℘(Y) → ℘(X) given by Z f^{−1}(Z). Then its action on π gives rise to a map

π^{∗} : ℘(B) → ℘(B × A)

which is a covariant functor if we view power sets as categories (with objects the members of the power set and morphisms given by inclusions). The reader can easily check that ∀_{A} : ℘(B×A) → ℘(B) as defined above, or, equivalently, by

∀_{A}(Z) = {b ∈ B : ∀a ∈ A ⟨b, a⟩ ∈ Z}

is a right adjoint to π^{∗}. A left adjoint also exists: ∃_{A} : ℘(B × A) → B given by

∃_{A}(Z) = {b ∈ B : ∃a ∈ A ⟨b, a⟩ ∈ Z}.

The interest of this construction it that it can be generalized considerably. First, we can replace π by any function f : X → Y and define quantification along f by adjunction to the induced functor.

Theorem 5.30 If X ^{f} Y is an arrow in any topos E , the induced functor on power objects f^{∗} : Ω^{Y} → Ω^{X} has left and right adjoints:

∃_{f} ⊣ f^{∗} ⊣ ∀_{f}.

The construction mimics the definitions of quantification given above. The definition of the right adjoint is given below, in the discussion of the Mitchell-Benabou language. The construction of ∃_{f} is also straightforward. See e.g. [77] for details. We will also make use of the following property which holds in any topos.

Lemma 5.31 (Beck-Chevalley conditions) If q is a subobject of D in a topos E and the diagram on the left is a pullback then the one on the right commutes

[figure: A; g; B; Ω^{B}; g^{∗}; Ω^{A}; C; m; f; D; p; Ω^{D}; ∃_{p}; f^{∗}; Ω^{C}; ∃_{m}]

as does the dual diagram for ∀_{f}.

The ∃-condition is sometimes called “Frobenius reciprocity”.

Corollary 5.32 If B ^{m} C is a subobject in a topos, then Ω^{B} ^{∃_{m}} Ω^{C} is monic.

proof: Apply the Beck-condition lemma to the pullback diagram

\begin{matrix}B & = = = = = & B \\ B & ‖ & \overline{m} & C & ^{m} \end{matrix}

and observe that m^{∗} ∘ ∃_{m} = 𝕀_{Ω^{B}}.

Instead of carrying these constructions out with the power-set functor in a topos, we can take any category with pullbacks, and let f^{∗} be the so-called change of base functor on the slice categories C /Y → C /X given by pulling back along any f : X → Y

[figure: f^{#}(A); A; X; f^{#}(α); f; Y; α]

When they exist, the corresponding adjoints

Σ_{f} ⊣ f^{#} ⊣ Π_{f}.

constitute a pair of generalized quantifiers in the category. Σ_{f} will always exist if C has pullbacks. The existence of Π_{f} is guaranteed if C is LCC, or locally cartesian closed: every slice is cartesian closed. By the fundamental lemma (5.29) every topos is LCC, and admits this interpretation of quantifiers. But so do other categories. This adjoint situation is the starting point for the so-called hyperdoctrine formulation of logic over an indexed category, used for interpreting dependent type theories, and further discussed below in section (5.5).

Connectives in an arbitrary topos By analogy with the preceding discussion in Set , we can define the logical connectives ∧, →, ∀_{A} as classifying arrows on suitable domains.

Definition 5.33 Let E be a topos and Ω its subobject classifier.

• Ω × Ω ^{∧} Ω is the classifier of 1 ^{⟨⊤,⊤⟩} Ω × Ω.

• Ω × Ω ^{⇒} Ω is the classifier of ⧀ ^{≤} Ω × Ω where

≤ ≡^{def} equalizer(Ω × Ω [figure: ∧; π_{0}] Ω).

• Ω^{A} ^{∀_{A}} Ω is the classifier of the name 1 ^{^{⌈}⊤_{A}^{⌉}} Ω^{A} of the arrow ⊤_{A} ≡ A ^{!_{A}} 1 ^{⊤} Ω.

The reader should compare these definitions with the characterizations of logical connectives in Set , above. In particular, ∀_{A} is defined in essentially the same way: it is the classifier of the arrow that “names” the subobject {A} of the power set Ω^{A}.

5.4.1 The Mitchell-Benabou Language

Let E be a topos. We define the internal Mitchell-Benabou language of E to be given by the following types and terms:

\underline{types} There is type A for each object A of E (we identify the two classes notationally from here on). Thus, the class of types includes, amongst many others, 0 and 1 (initial and terminal object), Ω, and for each pair of types A and B, the types A × B, B^{A}.

\underline{terms}

• For each type A, variables of type A: x, y, z … We indicate type membership by writing x: A (and distinguish terms from morphisms by displaying source-target information with a labeled arrow for the latter).

• ⊛: 1 and ⊤: Ω

• if a: A and b: B then ⟨a, b⟩: A × B. We can express this as the familiar rule

\frac{a : A b : B}{⟨a, b⟩ : A × B}

•

\frac{t : A u : B^{A}}{u(t) : B}

• For each arrow A ^{τ} B in E and each term t : A there is a term τ ∘ t : B.

• For each arrow X×A ^{τ} B in E and each variable x : A there is a term λx: A.τ : B^{A}, in which x is a bound variable.

In addition there are certain terms of type Ω called predicates or formulas.

\underline{formulas}

•

\frac{t : A t′ : A}{t = t′ : Ω}

•

\frac{t : A u : Ω^{A}}{t ∈ u : Ω}

• If p and q are formulas then so are p ∧ q, p ∨ q, p ⇒ q, ¬p. If p is a formula with the variable x free, and if A is a type, then ∀_{x∈A} p, ∃_{x∈A} p are formulas, with the variable x bound.

We will also speak about the term {x : p(x)} : A for x a variable of type A and p a formula with x free in p.^{20} All terms t(x_{1}, …, x_{n}) : B with free variables among the x_{1}, …, x_{n} of types A_{1}, …, A_{n}, respectively, have an interpretation [[t]] in E as arrows A ^{[[t]]} B where A = A_{1} × ⋯ A_{n}, as follows:

• If x is a variable of type A then [[x]] is A 𝕀_{A} A.

20Many authors (e.g. [58, 68]) call this a term of type Ω^{A}. See the comments following the definition of its interpretation.

• If U ^{[[a]]} A and V ^{[[b]]} B then [[⟨a, b⟩]] is U × V ^{[[a]]× [[b]]} A × B.

• If A ^{[[t]]} B and B ^{τ} C then [[τ ∘ t]] is just the composition A ^{[[t]]} B ^{τ} C.

• If T ^{[[t]]} A and U ^{[[u]]} B^{A} then [[u(t) ]] is

U × T ^{[[t]]× [[u]]} A × B^{A} ^{ev} B

• For (λx: A.τ) : B^{A} as above [[λx: A.τ ]] is the transpose (see def. 5.21) X ^{λ_{A}τ} B^{A}.

Atomic formulas (with the types and constituents given above) have the following interpretation,

for U ^{[[t]]} A, V ^{[[t′ ]]} A and V ^{[[u]]} Ω^{A}:

(53)  [[t = t′]] is U × V ^{[[t]]× [[t′ ]]} A × A ^{δ̄_{A}} Ω
(54)  [[t ∈ u]] is U × V ^{[[t]]× [[u]]} A × Ω^{A} ^{ev∘↶} Ω

where ↶ is the twist map ⟨π_{1}, π_{0}⟩ : A × Ω^{A} Ω^{A} × A, and where δ̄_{A} classifies the diagonal A ^{δ_{A}} A × A. If p and q have the interpretation A ^{[[p]]} Ω and B ^{[[q]]} Ω, compound formulas are interpreted as follows.

(55)  [[p ∧ q]] is A × B ^{[[p]]× [[q]]} Ω × Ω ^{∧} Ω
(56)  [[p ⇒ q]] is A × B ^{[[p]]× [[q]]} Ω × Ω ^{⇒} Ω

If B × A ^{[[p]]} Ω then [[∀_{x∈A} p]] is

B ^{\overline{[[p]]}} Ω^{A} ^{∀_{A}} Ω.

where, we recall that \overline{[[p]]} is the transpose (see 5.21) of [[p]]. The remaining formulas can be viewed as derived expressions via the standard “second-order” coding

(57)  ⊥ ≡^{def} ∀_{t∈Ω} t
(58)  ¬p ≡^{def} p ⇒ ⊥
(59)  p ∨ q ≡^{def} ∀_{t∈Ω} (((p ⇒ t) ∧ (q ⇒ t)) ⇒ t)
(60)  ∃_{x∈A} p(x) ≡^{def} ∀_{t∈Ω} (∀_{x∈A} (p(x) ⇒ t) ⇒ t)

or via the corresponding compositions ¬∘ [[p]], ∨∘( [[p]]× [[q]]), and ∃_{A} ∘(λ_{A}p) along the lines just given using the corresponding HA-operations of the subobject lattice (see e.g. [58, 77, 68, 40, 84] for further discussion).

If p(x) is a formula with a free variable of type A then

[[{x : p(x)}]] is the subobject of A classified by p.

We warn the reader that many authors define {x : p(x)} in such a way that its meaning in a topos E is the name of the arrow [[{x : p(x)}]] we have defined above, and hence a (unique) member 1 Ω^{A}. However, we prefer to follow the convention of e.g. [77] in keeping the meaning of {x : p} as close to its “familiar” set-theoretic meaning as a subobject of the domain of [[p]]. But it is unique only up to isomorphism, and best thought of as an equivalence class of subobjects. In Set we are able to select a preferred representative of the class of subobjects of a set A isomorphic to some B A, namely the one that is mapped to A by inclusion. But not all topoi admit a notion of canonical subobject making this possible (see [68, 33, 30] for a discussion of canonical objects in categories ).

Generalized elements and substitution In Set there is a one to one correspondence between members of an object A and the set of arrows 1 ^{a} A, called the global elements of A. In a topos, it might seem that these arrows are reasonable candidates for capturing the notion of “element” categorically. We then think of a composition

1 ^{a} A ^{f} B

as analogous to the set-theoretic “f of a”. But a weak point in the analogy is that the behavior of f on global elements does not determine f in an arbitrary topos: the following diagram may commute for every global element a

1 ^{a} A [figure: f; g] B

without f = g. (A topos in which global elements suffice to determine equality of arrows is called well-pointed). It is therefore necessary to consider generalized elements C ^{a} A as well.

Following this analogy, any arrow A ^{f} B can be thought of as defining a function with an indeterminate argument x of type A and the composition

C ^{a} A ^{f} B

as substitution f[a/x]. We will also call a formula p with interpretation A ^{[[p]]} Ω a formula on A. ^{21}

Truth in a topos Now we can define what it means for a formula in the internal language of a topos E to be true in E (or true “in the internal logic of E ”).

Definition 5.34 Let p be a formula, with interpretation

A ^{[[p]]} Ω

classifying the object P A. Then we say that p is true in E , and write E ⊧ p if [[p]] factors through “true”, i.e. if the following diagram commutes.

\begin{matrix}A & = = = = = = = = = & A \\ 1 & ^{!_{A}} & \overline{⊤} & Ω & ^{[[p]]} \end{matrix}

Equivalently, [[p]] = ⊤∘!_{A}. Notice that if this holds, there must be a unique map A P through which 𝕀_{A} factors, which asserts, in topos terms, that “the subobject of A on which p holds is A itself”.

5.4.2 Kripke-Beth-Joyal Semantics

A look at the diagram in def. (5.34) suggests that the definition of truth in E can be localized, much in the spirit of Kripke semantics, by replacing A in the upper left corner by one of its subobjects.

21For a categorical treatment of variables in terms that captures more of their “true role” in logic, the reader should consult [68], who define polynomial categories C [x] in an indeterminate arrow, in an analogous manner to e.g. polynomial rings.

Definition 5.35 Suppose p(x) is a formula as above and C ^{a} A is a generalized element of A (i.e. an arrow with target A) in a topos E . Then we define the forcing relation in E by

C ⊩ p[a/x]  iff  [[p]] ∘ a = ⊤∘!_{C}. (61)

Note that since {x ∈ A : p(x)} is the pullback of (⊤ along) [[p]], the above condition is equivalent to saying that C ^{a} A factors through {x ∈ A : p(x)}. It also follows immediately that a formula (with interpretation given above) is true in E iff it is forced by every every generalized

element C ^{a} A iff it is forced by the “generic element” A = 𝕀_{A} A.

One can now show that the forcing relation behaves much like Beth or Kripke forcing.

Lemma 5.36 Suppose p is a formula, with interpretation

A ^{[[p]]} Ω

in E and let C ^{a} A be an arrow in E .

monotonicity: If D ^{c} C and C ⊩ p[a/x] then D ⊩ p[ac/x].

covering: If D ^{c} [figure] C is epic and D ⊩ p[ac/x] then C ⊩ p[a/x]. We also have:

C ⊩ p[a/x] iff E ⊧ ∀_{y∈C} p[ay/x].

Theorem 5.37 Suppose C ^{a} A is a generalized element of A and p and q are formulas (on A) with a free variable x. Then

∧: C ⊩ p[a/x] ∧ q[a/x] iff C ⊩ p[a/x] and C ⊩ q[a/x]

∨: C ⊩ p[a/x] ∨ q[a/x] iff there are arrows u : U → C and v : V → C such that U + V ^{[u,v]} [figure] C and C ⊩ p[au/x] and C ⊩ q[av/x].

⇒: C ⊩ p[a/x] ⇒ q[a/x] iff for every D ^{c} C whenever D ⊩ p[ac/x] then D ⊩ q[ac/x].

¬: C ⊩ ¬p[a/x] iff for every D ^{c} C whenever D ⊩ p[ac/x] then D ≅ 0.

Suppose p is a formula with free variables x of type A and y of type B, with interpretation A × B ^{[[p]]} Ω. Then

∃_{B}: C ⊩ ∃_{y∈B} p[a/x] iff there is an epic D ^{c} [figure] C and a generalized element D ^{d} B such that D ⊩ p[ac/x, d/y].

∀_{B}: C ⊩ ∀_{y∈B} p[a/x] iff for every D ^{c} C and every generalized element D ^{d} B, D ⊩ p[ac/x, d/y].

proof: (See e.g. [77, 68], whose development we follow for the remaining discussion of Kripke-Joyal semantics).

If instead of considering an arbitrary topos one considers a topos of presheaves or sheaves, the forcing clauses become quite a bit simpler. For example, consider the case E = Set ^{C}. Then objects (hence “nodes” forcing sentences) are functors F : C → Set . But it suffices to restrict attention, in Kripke-Joyal semantics, to a generating set of objects.

Definition 5.38 A class C of objects in a category E is said to generate E if every pair of arrows in E

A  [figure: f; g] B

are equal if and only if for every C ∈ C and every C ^{x} A we have fx = gx. In other words, equality is determined by actions on generalized elements from C.

Thus, in a well-pointed Topos, {1} generates.

It is easily shown that generalized elements from a generating class of objects determine truth in E .

Lemma 5.39 Let p(x) be a formula with interpretation A ^{[[p]]} Ω, and suppose C generates E . Then p is true in E iff for every C ∈ C and C ^{a} A we have C ⊩ p[a/x].

The proof is immediate: if p is forced on a generating set, then [[p]] ∘ a = ⊤∘!_{C} for any C ^{a} A with C in C. But then for all such a, [[p]]∘a = ⊤∘!_{A} ∘a hence [[p]] = ⊤∘!_{A} which is the definition of p true in E .

In a presheaf topos, the representable functors E (C, ) form a generating set, for if two arrows λ, ν : F → G in E = Set ^{C} disagree then for some object A of C and some element a ∈ F (A) they must differ: λ(A)(a) ≠ ν(A)(a). By the Yoneda lemma (5.17) there is a natural transformation â : C (A, ) → F such that â(A)(𝕀_{A}) = F (𝕀_{A})(a) = a, so λ(A)(a) = λ(A)(â(A)(𝕀_{A})) = (λ ∘ â)(A)(𝕀_{A}) so λ ∘ â and ν ∘ â disagree, with the source of â representable.

We now apply Yoneda again to note that for each representable functor C (C, ) and each generalized element λ : C (C, ) → F in E , there is a unique representative a ∈ F (C) such that λ = â with â satisfying â(C)(𝕀_{C}) as in the preceding paragraph. Thus we can think of the “nodes” of the associated Kripke-Joyal interpretation as objects C of C and generalized elements as images C (C, ) ^{â} F of members a ∈ F (C). Thus, for objects C of C, we write C ⊩ p to mean C (C, ) ⊩ p.

With this revised notation, some of the clauses become much simpler.

Lemma 5.40 Let E be the topos Set ^{C}, and ⊩ the Kripke-Joyal forcing relation for E .

∧: C ⊩ p[â/x] ∧ q[â/x] iff C ⊩ p[â/x] and C ⊩ q[â/x]

∨: C ⊩ p[â/x] ∨ q[â/x] iff C ⊩ p[â/x] or C ⊩ q[â/x]

⇒: C ⊩ p[â/x] ⇒ q[â/x] iff for every C ^{k} D whenever C ⊩ p[â[k]/x] then C ⊩ q[â[k]/x], where [k] is the induced C (k, ) : C (D, ) → C (C, ).

Suppose p is a formula with free variables x of type A and y of type B, with interpretation A × B ^{[[p]]} Ω. Then

∃_{B}: C ⊩ ∃_{y∈B}p[â/x] iff there is a generalized element C (C, ) ^{b̂} G such that C ⊩ p[â/x, b̂/y].

The simplified existence and disjunction clauses follow from the fact that each representable functor in Set ^{C} is an indecomposable projective. An object C in a category is indecomposable if whenever it is the target of an epic arrow

A + B ^{[h,k]} C

with [h, k] the canonical co-product map induced by a pair of maps from A and B into C, one of A ^{h} C, B ^{k} C is epic. It is projective if every epic D ^{e} [figure] C has a splitting, i.e. a left inverse C ^{f} D with f ∘ e = 𝕀_{D}. (A simple example of an indecomposable is the open set p ↑≡ {q : q ≥ p} in the topology O(K) of upward closed subsets of a Kripke model. Such an open set is generated by a “point” p ∈ K and has the property p ↑⊂ O_{1} ∪ O_{2} ⇒ p ↑⊂ O_{1} or p ↑⊂ O_{2}, which is not satisfied by an arbitrary open U in place of p ↑. If the reader translates this condition to the opposite category O(K)^{o}, it gives the indecomposability of p ↑). In case C is just a partial order viewed as a category, the Kripke-Joyal clauses reduce essentially to ordinary Kripke semantics (for local set theory) We refer the reader to [68] for details.

5.4.3 The Fourman-Hayashi interpretation of IZF

We now define a topos-theoretic semantics for IZF which extends the forcing and Ω-set semantics that were developed in earlier sections. We interpret the untyped, global, first order language of set theory, with unbounded quantification, by means of the same sort of ordinal induction over ranked universes we used before. This interpretation was developed by Fourman (who applied it to Fraenkel-Mostowski permutation models in [31]) and (in an essentially equivalent way) independently by Hayashi [47]. It was further developed by Scedrov in [103] to obtain a number of independence results.

We sketch Fourman’s development of IZF (without urelements) in a complete and co-complete topos. Here complete means that all set-indexed diagrams have limits. The problem one must address in adapting earlier type-free set theoretic interpretations is the absence of any immediately obvious analogue in an arbitrary topos of the ordinal hierarchies we have used in Set . That is to say, we must construct a model “V (E )” of IZF in a topos, which consists of ranked objects

V (E )_{α} together with maps V (E )_{α} ^{ι_{α}^{β}} V (E )_{β} whenever α ⊆ β. Each such V (E )_{α} is itself a co-limit of the preceding ones. This is why such strong completeness conditions are required. As it turns out, such topoi are not hard to find: every presheaf and sheaf topos is complete and co-complete and is also locally complete: for any object A each hom-set E (A, Ω) is a cHa. A proof of these facts (and a powerful converse: Giraud’s theorem) can be found in e.g. [58].

Definition 5.41 For each ordinal α define

(62) W (E )_{α} ≡^{def} lim_{β∈α} V (E )_{β}
(63)  V (E )_{α} ≡^{def} Ω^{W (E )}
(64)  V (E ) ≡^{def} the full subcategory of E containing the objects W (E )_{α}, V (E )_{α}.

We henceforth refer to these objects as W_{α}, V_{α}.

Note that in particular W_{0} is the co-limit of the empty diagram, which is 0. Strictly speaking, the colimit W_{α} defined above is of a diagram consisting of all lower V_{β} together with the (monic) arrows

V_{γ} ^{ι_{δ}^{γ}} V_{δ}. (65)

for γ ≤ δ, satisfying

ι_{δ}^{γ} ∘ ι_{ρ}^{δ} = ι_{ρ}^{γ}. (66)

We denote by e_{α} the evaluation map

V_{α} × W_{α} Ω.

To show that our construction of the V_{α} is well-defined, we must show, by induction, that monics (65) satisfying (66) exist. So we assume that they do for all pairs of ordinals γ ≤ δ below α and show that they do for the pair β, α, where β ≤ α. Observe that there is a natural monic ν : W_{α} → W_{β} for α ≤ β (since W_{α} is the colimit of the subdiagram of V_{γ} below α, we obtain the embedding as a unique map commuting with all ι_{γ}^{γ′} between the V_{γ}, which in a topos must be

monic). ν induces the direct image embedding Ω^{W_{α}} ^{∃_{ν}} Ω^{W_{β}} which is the internal left adjoint to Ω^{W_{β}} ^{ν^{∗}} Ω^{W_{α}} induced by the power-object functor. By corollary (5.32) if ν is monic, so is ∃_{ν} (in fact its right inverse is ν^{∗} by the proof of the same corollary). This shows, by induction, that the ι_{α}^{β} exist for all comparable ordinals.

The objects classified by the evaluation maps e^{α} give the local ∈-structure on each V_{α}. We are now able to interpret ordinal-ranked formulas at each V_{α} as follows. We define limited formulas to be those formulas in the expanded language of set theory containing the constants V_{α}, built up with the connectives ∧, ⇒ , ∨, ¬ and bounded quantification ∀_{x∈Vα} , ∃_{x∈Vα} . A ranking is a map # : V ars → ON. A ranking is admissible for a formula φ if for every free occurrence of x in φ in a subformula of the form x ∈ V_{α} we have #x ≥ α. We now define an interpretation of limited formulas [[φ]]_{x⃗;α⃗} where x⃗ = ⟨x_{1}, …, x_{n}⟩ is the sequence of variables occurring free in φ and α⃗ = ⟨α_{1}, …, α_{n}⟩ the sequence of values of a φ-admissible ranking # of x⃗. In all cases [[φ]]_{x⃗,α⃗} is an arrow V_{α_{a}} × ⋯ × V_{α_{n}} Ω

(67)  [[x = y]]_{⟨x,y⟩;⟨α,α⟩} = V_{α} × V_{α} ^{δ} Ω
(68)  [[x = x]]_{x;α} = V_{α} ^{⊤∘!_{Vα}} Ω
(69)  [[x ∈ y]]_{⟨x,y⟩;⟨α,α⟩} = V_{α} × V_{α} ^{e_{α}} Ω
(70)  [[x ∈ x]]_{x;α} = V_{α} ^{⊥} Ω
(71)  [[x ∈ V_{α}]]_{x;β} = V_{β} ^{χ_{ι}} Ω

where ι has the appropriate sub-and super-scripts. Logical connectives are interpreted exactly as with the Mitchell-Benabou language, as are the bounded quantifiers:

(72)  [[∀_{x∈Vα} φ]]x⃗ = ∀_{π} [[x ∈ V_{α} → φ]]_{⟨x,x⃗⟩}
(73)  [[∃_{x∈Vα} φ]]x⃗ = ∃_{π} [[x ∈ V_{α} ∧ φ]]_{⟨x,x⃗⟩}

where some fixed ranking # is assumed, and where ∀_{π}, ∃_{π} are the quantifications along the projection map corresponding to the variable bound by the quantification, e.g. V_{α_{0}} × V_{α_{1}} × ⋯ V_{α_{n}} ^{π} V_{α_{1}} ×⋯ V_{α_{n}}. As with the Ω-set semantics, we define the interpretation of arbitrary formulas (with unbounded quantification) by taking suprema and infima over the subobject lattices E (D, Ω) for suitable D.

(74)  [[∀xφ]] = ⋀ [[∀_{x∈Vα} φ]]
(75)  [[∃xφ]] = ⋁ [[∃_{x∈Vα} φ]]

Soundness of the interpretation is established in [31].

Several other interesting approaches to categorical models of IZF have appeared. Hayashi’s model [47] is based on Johnstone’s formalization [58] of the collection of transitive objects E_{tr} within a topos. Hayashi shows how to build a model of IZF by taking filtered colimits of local models in a Grothendieck Topos. In the case of ordinal-indexed Ω set models, Hayashi’s construction gives the Ω-set interpretation defined above. An interesting reformulation of this for A -sets (see discussion prior to lemma 5.16), A any category, is developed by Freyd and Scedrov [33]. A translation is provided (similar to one due to Friedman [36] also discussed in [8]) that reduces soundness for IZF to soundness for a related non-extensional theory with a much simpler semantics, which they then use to give (for the Boolean case) simple proofs of ZF-independence of Choice and the Continuum Hypothesis.

5.5 PERs and the Effective Topos

We now consider a category closely linked to the realizability interpretation, which will be used to construct the effective topos. The category of partial equivalence relations, known as PER for short has played an interesting role recently in computer science applications, since it provides a natural model for polymorphism. An extensional subcategory of PER (ExPER) first defined by Freyd, Mulry, Rosolini and Scott, makes precise the denotational semantics implicit in realizability.

Definition 5.42 Let A be a partial combinatory algebra. The category of PERs over A, Per (A) has as objects, all pairs ⟨X, R⟩ such that R is a partial equivalence relation on A with domain X. A pre-morphism in Per (A) is a term e in A satisfying, for every x, y ∈ X,

xRy → exSey

Morphisms [e] : ⟨X, R⟩ → ⟨Y, S⟩ in Per (A) are equivalence classes of pre-morphisms of A under the equivalence

e ∼ e′ ≡^{def} ∀x ∈ X(exSe′y).

Definition 5.43 Let A be a PCA (cf. def. 3.1). Then we define PA, the A -realizability pre-algebra to be the Heyting pre-algebra PA with carrier set ℘(A) and structure given by

(76)  U ∧ V = {⟨u, v⟩ : u ∈ U ^{&} v ∈ V }
(77)  U ∨ V = {⟨0, u⟩ : u ∈ U} ∪ {⟨1, v⟩ : v ∈ V }
(78)  U ⇒ V = {t : (∀u ∈ U) tu ↓ ^{&} tu ∈ V }

and partial order given by U ≤ V iff there is a t in U ⇒ V (a state of affairs we sometimes

denote by U ≤^{t} V). Top and bottom elements are given by A and ∅ respectively.

The reader should compare this with the definitions of the ×, +, ⇒ operations for Kleene realizability given in the appendix. It should be remarked that the above definition can take place in classical or constructive set theory. Classically, P (A) is equivalent to a two element pre-algebra since for any inhabited X and any u ∈ X we have

A ≤^{λx.u} X.

Of course, in IZF, we cannot prove that every set is inhabited or not, so each model of IZF gives a different version of P (A). The reader may take the metatheory to be classical here if he or she so desires, however.

A simple construction allows us to interpret predicate logic in a realizability pre-algebra in a straightforward manner that strengthens the standard realizability interpretation of quantifiers in the appendix, and is more like the McCarty realizability of quantifiers in IZF.

Let X be a set, H a realizability pre-algebra. Then we define the X-indexed pre-algebra H^{X} to consist of all functions from X to H with logical operations defined pointwise:

(79)  F ∧ G(x) = F (x) ∧ G(x)
(80)  F ∨ G(x) = F (x) ∨ G(x)
(81)  F (x) → G(x) = F (x) → G(x)

top and bottom elements given by λx.⊤_{H} and λx.⊥_{H} respectively, and with the preorder given by

F ≤ G iff ⋂_{x∈X} F (x) → G(x) ≠ ∅.

The reader should note that the pre-order on functions is not given pointwise: a single realizer must work for all x ∈ X.

Definition 5.44 A member F of an indexed realizability pre-algebra H^{X} is said to be realized in H if it is uniformly realized by a term in H:

⋂_{x∈X} F (x) ≠ ∅.

this state of affairs is denoted by

H ⊧ F or H ⊧ F (x)

with the understanding that the displayed variable is uniformly quantified over (by intersection).

The preceding construction will in fact give us a Set -indexed family of realizability prealgebras H^{X}. This yields a non-topos-theoretic example of a Lawvere hyperdoctrine, which we now discuss.

Definition 5.45 An indexed category ℂ consists of

• a base category C

• a fibre category C_{A} for each object A of C

• For each arrow A ^{f} B in C a functor [f] : C_{B} → C_{A} (called the “substitution functor”) satisfying

1. [𝕀_{A}] : C_{A} → C_{A} ≃ (is naturally isomorphic to) the identity functor.

2. [g ∘ f] ≃ [g] ∘ [f]

The two properties satisfied by [] are often called pseudofunctoriality.

Definition 5.46 (Lawvere) A hyperdoctrine is an indexed category ℂ in which

• The base category is cartesian closed.

• for each arrow f in the base category, the induced functor [f] preserves cartesian structure,

and has left and right adjoints

∃_{f} ⊣ [f] ⊣ ∀_{f}

• These functors satisfy “Frobenius reciprocity” and the “Beck condition”(see lemma (5.31)), that is to say, for each pullback

[figure: A; g; B; C; p; f; D; q]

there are natural isos ∃_{p} ∘ [g] ≃ [f] ∘ ∃_{q}, and ∀_{p} ∘ [g] ≃ [f] ∘ ∀_{q}.

For a discussion of hyperdoctrines, reciprocity and Beck conditions we refer the reader to [109, 92, 77]. Suffice it to say here that the hyperdoctrine point of view defines (semantically) an abstract logic over a base category of types. One can think of each fibre category ℂ_{X} as the family of abstract predicates over the type or domain X (we will use this terminology below). The local cartesian structure on the fibres (which is often strengthened to include more logical operations) induces a propositional logic structure over each type. The global hyperdoctrine provides an extension to an abstract predicate logic, with quantification defined by the adjoints to the “substitution operation” along each arrow in C. If the resulting abstract formulas are to behave like logical formulas, they must admit commutation of quantification with substitution and addition of dummy variables. These and other fundamental properties (depending on the hyperdoctrine in question) are guaranteed by the Beck conditions.

For example, when applied to canonical projections X × Y ^{p} X and X × Y ^{f×𝕀_{Y}} X′ × Y in lieu of g, these conditions guarantee the following logical laws, for x not free in φ:

∃x(θ(x) ∧ φ) ⟺ ∃xθ(x) ∧ φ

and

∀x(θ(x) → φ) ⟺ ∀xθ(x) → φ

Observe that Freyd’s fundamental lemma (5.29) (with a proof of the corresponding Beck conditions) and lemmas(5.30) and (5.31) give us two examples of hyperdoctrines in a topos. We now consider a more general class of hyperdoctrines which can be used to build a topos out of any applicative structure.

Definition 5.47 (Hyland, Johnstone, Pitts) A tripos is a hyperdoctrine ℂ whose fibre categories ℂ_{X} are Heyting pre-algebras (C_{X} ⊢_{X}) (for each object X in the base category C) satisfying the “power object condition”: for each object A of C there is an object P A and a membership predicate ∈_{A} in ℂ_{A×P A} such that for any B in C and φ in ℂ_{A×B} there is a morphism f : B → P A in C satisfying [𝕀_{A} × f] ∈_{A}≅ φ.

A reformulation of the definition of universal relation following def. (5.23) in terms of the pullback functor induced by 1_{C} × f will help explain the “power object condition” above. We leave this as an exercise for the reader.

Theorem 5.48 If H = {H^{X}} is a Set -indexed family of realizability pre-algebras, then it is a tripos, with the functor [f] : H^{Y} → H^{X} corresponding to X ^{f} Y induced by composition.

For each set A the power object will be H^{A}, with the membership predicate just the evaluation map H^{A} × A H. Each H^{X} is clearly cartesian closed as a category. For a detailed proof see [51].

Although there is a quite general theory of realizability-style topoi based on arbitrary triposes, we will confine our attention to those generated by the Set -based realizability pre-algebras described above. The aim of the rest of the section, then, is to sketch how a model of constructive set theory can be built out of the realizability structures we have defined, one that captures much of the behavior of the realizability interpretation we saw earlier. The reader should note the similarity between the way Eff_{H} is built out of a realizability pre-algebra H and the way Ω-sets and Ω-interpretations are built out of a cHa (see section (5.2)).

Definition 5.49 Let A be a PCA. The effective topos over A, or Eff_{A}, is the category whose objects are PA -valued PERs, that is to say, pairs ⟨X, [[· ≅_{X} ·]]⟩ where X is a set and [[· ≅_{X} ·]] a partial map X × X PA satisfying

(82)  PA ⊧ [[x ≅ y]] → [[y ≅ x]]
(83)  PA ⊧ [[x ≅ y]] ∧ [[y ≅ z]] → [[x ≅ z]]

In other words PA realizes the fact that [[· ≅_{X} ·]] is symmetric and transitive. For x ∈ X we define Ex, the extent of x , to be [[x ≅ x]].

A morphism ⟨X, ≅_{X}⟩ ^{[F]} ⟨Y, ≅_{Y} ⟩ in Eff_{A} is an equivalence class of PA -valued functional relations, that is to say a (Set ) function F : X × Y → PA such that

(84)  F is relational  PA ⊧ F (x, y) ∧ [[x ≅ u]] ∧ [[y ≅ v]] → F (u, v)
(85)  F is strict  PA ⊧ F (x, y) → Ex ∧ Ey
(86)  F is single − valued  PA ⊧ F (x, y) ∧ F (x, z) → [[y ≅ z]]
(87)  F is total  PA ⊧ Ex → ⋃_{y∈Y} Ey ∧ F (x, y)

where two functional relations F, G are equivalent if

PA ⊧ F (x, y) = G(x, y)

One must now show that Eff_{A} is a category, i.e. that a composition operation can be defined which is independent of the choice of representative of morphisms. The definition of composition of functional relations

⟨X, ≅_{X}⟩ ^{F} ⟨Y, ≅_{Y} ⟩ ^{G} ⟨Z, ≅_{Z}⟩

is given by

(G ∘ F)(x, z) = ⋃_{y∈Y} Ey ∧ F (x, y) ∧ G(y, z)

With this definition we obtain not only that Eff_{A} is a category, but much more.

Theorem 5.50 (Hyland, Johnstone, Pitts) Eff_{A} is a topos.

The terminal object of Eff_{A} is ⟨{0}, ≅_{1}⟩ where

[[0 ≅_{1} 0 ]] = |A |.

Products ⟨A, ≅_{A}⟩ × ⟨B, ≅_{B}⟩ are given by ⟨A × B, ≅_{A×B}⟩ where

[[⟨x, y⟩ ≅_{A×B} ⟨x′, y′⟩]] = [[x ≅_{A} y]] ∧ [[x′ ≅_{B} y′]]

The subobject classifier is ⟨PA , ≅_{Ω}⟩ with

[[U ≅_{Ω} V ]] = U → V ∧ V → U.

We refer the reader to [51] for the details, and for a proof of a much stronger fact, namely that any category built from a tripos along the lines pursued above for realizability algebras is a topos. In said reference, and in [52, 92] it is shown that Eff_{A}, and in particular Eff_{ω}, are topos-theoretic formulations of the realizability “universe”. Many principles we saw validated in the McCarty interpretation which make sense in local set theory, are true when suitably translated in the internal logic of Eff_{A}. For example the set of Kleene-realizable sentences (over the standard PCA ω) in the first-order language of HA (see appendix) are precisely those sentences true of the natural number object (⟨N, ≅_{N}⟩ where [[n ≅ m]] = {x ∈ {n} : n = m}). Hyland shows in [52] that analysis in Eff_{ω} is essentially contsructive recursive analysis (see e.g. [8] for a discussion of this area). The real numbers in Eff_{ω} are the recursive Cauchy sequences. Church’s thesis and Brouwer’s continuity principle for the reals are true in Eff_{ω}.

Hyland and others (Scedrov) have proposed Eff_{A} as the suitable framework for carrying out recursive mathematics in the spirit of the Russian constructivist school or of the effective algebra results of Nerode, Metakides and others. Furthermore Eff_{A}and its subcategories (e.g. Modest Sets, see [92]) has offered a framework for giving a natural constructive set-theoretic interpretation of polymorphism [94].

The constructions sketched out above are the starting point for a rich theory that has provided semantics for the ontologies of greatest interest in computer science, e.g. dependent type theories, Constructions, linear and modal logics. Both the syntax and semantical analysis of new programming languages is being shaped by these semantic frameworks. The reader is urged to consult the work in e.g. [33, 101, 100, 4, 78, 54, 52, 51, 111, 112, 74, 86, 110, 91] and others cited in the appendix, for further details.

The author would like to thank Anil Nerode for introducing him to the realizability interpretation of IZF, and encouraging further study of the field, and Peter Freyd for many insights about topoi and PERs. Many thanks also to Robert Lubarsky and George Odifreddi for countless helpful discussions, and to Paul Taylor for careful reading and helpful comments, as well as his diagram macros. Thanks also to Ramesh Subrahmanyam and Thomas Streicher for helpful suggestions.

A A sketch of Kleene’s 1952 realizability interpretation

A.1 Realizability for HA

We define realizability formulas in one free variable |φ|(e) associated to each arithmetic sentence φ over the language L :

|φ|(e)  is φ  for atomic φ
|¬φ|(e)  is ∀f¬|φ|(f)
|φ^{&} ψ|(e)  is |φ|(e_{0})^{&} |ψ|(e_{1})
|φ ∨ ψ|(e)  is [e_{0} = 0^{&} |φ|(e_{1})] ∨ [e_{0} = 1^{&} |ψ|(e_{1})]
|φ → ψ|(e) is (∀f)[|φ|(f) → ∃uvT (e, f, u)^{&} U(u) = v^{&} |ψ(v)|]
|∃x φ(x)|(e) is |φ(e_{1})|(e_{0})
|∀x φ(x)|(e) is ∀n[∃uv(T (e, n, u)^{&} U(u) = v^{&} |φ(n)|(v)]

where e = ⟨e_{0}, e_{1}⟩ via the standard primitive recursive pairing and unpairing. Formally, any assertion of the form e.g. A(e_{0}) is given by (∃uv) (Pair(u, v, e) ^{&} A(u)), where Pair(u, v, e) is (u+v)(u+v+1) = 2(e−v), the standard diagonal coding predicate. Alternatively, we can (conservatively) make a definitional extension of HA, introducing the function symbols ( )_{0} , ( )_{1} and ⟨, ⟩ for unpairing and pairing. We follow the latter convention informally and leave the formalization to the reader’s taste. We will adopt the following notation, for formulas A, B in one free variable :

(A × B)(x) ≡ A(x_{0})^{&} B(x_{1})
(A + B)(x) ≡ (x_{0} = 0^{&} A(x_{1})) ∨ (x_{0} = 1^{&} B(x_{1}))
(A ⇒ B)(x) ≡ ∀n[A(n) → ∃uv(T (x, n, u)^{&} U(u) = v^{&} B(v)]

For formulas S(x, y) in two free variables (over L) we define

(∑S)(z) ≡ S(z_{1}, z_{0})
(∏S)(z) ≡ ∀x[∃uv(T (z, x, u)^{&} U(u) = v^{&} S(x, v)]

which formalizes “z is a choice function on x in the collection {S(x, y)}”. With this notation, we can abbreviate the definitions of realizability formulas:

|φ^{&} ψ| ≡ |φ| × |ψ|
|φ ∨ ψ| ≡ |φ| + |ψ|
|φ → ψ| ≡ |φ| ⇒ |ψ|

and if φ is a formula with one variable free and φ̂(x, y) is the formula in two free variables given by |φ(x)|(y) then

|∃xφ| ≡ (∑φ̂)
|∀xφ| ≡ (∏φ̂)

We can similarly define abstract realizability for Feferman’s theory APP (defined in appendix B).

Definition A.1 Let A, B be sentences over the language of APP. Then we define inductively the realizability formulas |A| in one free variable as follows:

If A is prime |A|(x) is A^{&} x ↓

|A^{&} B|(x) ≡ (|A| × |B|)(x) ≡^{def} |A|(π_{0}x)^{&} |B|(π_{1}x)
|A ∨ B|(x) ≡ (|A| + |B|)(x) ≡^{def} N(π_{0}x)^{&} (π_{0}x = 0 → |A|(π_{1}x))^{&}
(π_{0}x ≠ 0 → |B|(π_{1}x))
|A → B|(x) ≡ (|A| ⇒ |B|)(x) ≡^{def} ∀y[|A|(y) → xy ↓ ^{&} |B|(xy)]
|∃yA(y)|(x) ≡ (∑|A|)(x) ≡^{def} |A(π_{0}x)|(π_{1}x)
|∀yA(y)|(x) ≡ (∏|A|)(x) ≡^{def} ∀y[(xy) ↓ ^{&} |A(y)|(xy)]

|A|(x) is usually written x r ∼ A. Note that if A is a formula in n variables over APP then the above clauses defined an associated realizability formula in n + 1 variables.

B APP and the logic of partial terms

(There are many formulations, e.g., Troelstra–Van Dalen’s E^{+} logic ([118]), Fourman and Scott’s treatment in [32] Feferman’s formalism, Beeson’s EON [8]). We follow the lines of Beeson’s EON. A detailed formulation of abstract applicative structures within IZF is carried out in McCarty’s [83]. We need: First order language

• A partial binary function Ap( , ) ^{22}

• variables x_{1}, … y_{1}, …

• equality =

• distinguished constants s, k, π_{0}, π_{1}, p, d, 0

• unary relation symbol ↓ “convergence”

• binary relation symbol ≈ (here, following Beeson and others,one may take it to be defined: t ≈ s ≡ t ↓ ∨s ↓→ t = s)

• A unary predicate N(x) (standing for the natural number sort). Note: we need to agree on how to deal with partiality in our logic. Beeson, Troesltra-van Dalen, McCarty op.cit. take slightly different approaches, as does Scott in [106]. The most important point is that quantifier laws have to be modified to deal with partiality, e.g. we require axioms

∀xA^{&} t ↓→ A[t/x] A[t/x]^{&} t ↓→ ∃xA

in lieu of the conventional laws, and strict atomic relations

R(t_{1}, ..., t_{n}) → t_{1} ↓ ^{&} ⋯ t_{n} ↓

for atomic formulas R. The constants satisfy the axioms:

1. kxy = x (kx ↓)

2. sxy ↓ & sxyz ≈ xz(yz)

3. k ≠ s which suffice to give combinatory completeness:.

22(Ap(f, x) is usually written fx)

Theorem B.1 (Curry) For each term t and variable x, one can construct a term λx · t such that λx · t ↓ (λx · t)x ≃ t (λx · t)u ≃ t[u/x] u, t terms

See e.g. Beeson or Troesltra and Van Dalen (op.cit.) for a proof.

We also have the axioms:

• pairing:

pxy ↓ ^{&} π_{0}(pxy) = x π_{1}(pxy) = y

• conditional:

N(a)^{&} N(b)^{&} a = b → dxyab = x
N(a)^{&} N(b)^{&} a ≠ b → dxyab = y

• natural number sort

∀x(N(x) → N(s_{N}(x))^{&} p_{N}(s_{N}(x)) = x^{&} s_{N}(x) ≠ 0)

and

∀x(N(x)^{&} x ≠ 0 → N(p_{N}x)^{&} s_{N}(p_{N}(x)) = x),

as well as the induction schema for N

φ(0) ∧ ∀x(N(x) ∧ φ(x) → φ(s_{N}(x))) → ∀x(N(x) → φ(x)).

The above system and most variants in the literature satisfy two important properties:

Theorem B.2

Recursion Theorem

∃R AP P ⊢ Rf ↓ &[g = Rf → ∀x(fx ≃ fgx)]
i.e., (Rf)x ≃ (f(Rf)x)

Term Existence (AP P ⊢ ∃xA(x)) ⇒ There is a term t, such that (AP P ⊢ A(t)&t ↓)

References

[1] Aczel, P. [1977] The Strength of Martin-Löf’s Type Theory with One Universe, in: Mietissen, S. and Väänänen, J., (eds), The proceedings of the symposiums on Mathematical Logic Helsinki 1975 , University of Helsinki, 1977.

[2] Allen, S. [1987], A Non-Type-Theoretic Semantics for Type-Theoretic languages Ph. D. Dissertation, Cornell University, Ithaca, N.Y.

[3] Asperti, A. and Longo, G., [1991], Categories, Types and Structures, MIT.

[4] Barr, M., and Wells, C.[1985], Toposes, Triples and Theories, Springer, New York.

[5] Barwise, Jon, [1975], Admissible sets and structures : an approach to definability theory, Berlin ; New York : Springer-Verlag, 1975.

[6] Barwise, J; Keisler, J. eds. [1977] Handbook of Mathematical Logic, Amsterdam ; New York : North-Holland Pub. Co., 1977.

[7] Beeson, M. J. [1988], “Towards a computation system based on set theory”, Theoretical Computer Science 60, 1988, North-Holland.

[8] Beeson, M. J. [1985a], Foundations of Constructive Mathematics, Springer-Verlag, Berlin.

[9] Beeson, M. J. [1982], “Recursive models of constructive set theories”, Annals of Mathematical Logic 23, 127-178.

[10] Beeson, M. J. [1978], “A type-free Gödel interpretation”, Journal of Symbolic Logic 43, 213-227.

[11] Beeson, M. J. [1977], “Continuity and comprehension in intuitionistic formal systems”, Pacific Journal of Mathematics,.68, 29-30.

[12] Bell, J. [1985], Boolean-Valued Models and Independence Proofs in Set Theory, Clarendon Press, Oxford.

[13] Bell, J. [1989] Local Set Theory and Toposes, Cambridge University Press.

[14] Bunge, M. [1974], “Topos Theory and Souslin’s Hypothesis”, in The Journal of Pure and Applied Algebra, North-Holland.

[15] Chang, C.C., and Keisler, J. [1977], Model Theory, North Holland, Amsterdam.

[16] Cohen, P. J. [1966], Set Theory and the Continuum Hypothesis, W. A. Benjamin Inc., New York.

[17] Cohen, P. J. [1963], “The independence of continuum hypothesis”, Proceedings of the National Academy of Science, USA 50, 1143-1148.

[18] Constable, R. [1985] The Semantics of Evidence, manuscript.

[19] Constable, R. L. and Howe, D. J., [1990], “Implementing Metamathematics as an Approach to Automatic Theorem Proving”, in Formal Techniques in Artificial Intelligence, R. Banerji, ed., North-Holland.

[20] Constable, R. L., et al [1986], Implementing Mathematics with the NUPRL Development System, Prentice-Hall, N.J.

[21] Coquand, T. and G. Huet [1985a], “Constructions: A higher order proof system for mechanizing mathematics”, EUROCAL 85, Linz, Austria.

[22] Crossley, J. (ed.) [1985], “Aspects of Recursive Algebra”, The Upside Down A, Melbourne.

[23] Van Dalen, D. [1986] “Intuitionistic Logic”, in The Handbook of Philosophical Logic, vol.III , D. Reidel, Dordrecht.

[24] Devlin, K. [1984] Constructibility, North-Holland, Amsterdam.

[25] Dragalin, A. G. [1987], Mathematical Intuitionism: Introduction to Proof Theory, Translations of Mathematical Monographs 67, AMS, Providence, R. I.

[26] Dummett, M. [1977],Elements of Intuitionism, Oxford University Press, Oxford.

[27] Feferman, S. [1975] “A language and axioms for explicit mathematics”, in: Algebra and Logic, Lecture Notes in Mathematics No. 450, pp. 87-139, Springer, Berlin.

[28] Feferman, S. [1977], “Theories of Finite Type”, in: Barwise, J. (ed.), Handbook of Mathematical Logic, pp. 913-972, North-Holland, Amsterdam.

[29] Feferman, S. [1979], “Constructive theories of functions and classes”, in Boffa, M., D. van Dalen and K. McAloon (eds.), Logic Colloquium ’78: Proceedings of the Logic Colloquium at Mons, 1978, pp.159-224, North-Holland, Amsterdam.

[30] Finkelstein, S. [1994], Ph. D. Dissertation, University of Pennsylvania, to appear.

[31] Fourman, M.P. [1980], “Sheaf Models for Set Theory” in The Journal of Pure and Applied Algebra 19, North-Holland.

[32] Fourman, M. P. and D. S. Scott [1979], “Sheaves and logic”, in: Fourman, Mulvey and Scott, (eds.), Applications of Sheaves, Mathematical Lecture Notes 753, pp.302-401, Springer-Verlag, Berlin.

[33] Freyd, P. and Scedrov, A. [1990], Categories, Allegories, North-Holland, Amsterdam.

[34] Freyd, P., [1980], “The Axiom of Choice”, in The Journal of Pure and Applied Algebra, vol. 19, North-Holland, Amsterdam.

[35] Freyd, P., Mulry, P., Rosolini, G., Scott, D. [1990], “Extensional PERs”, in LICS 1990, and in TCS 1993.

[36] Friedman, H. [1973], “Some applications of Kleene’s methods for intuitionistic systems”, in: Mathias, A. and H. Rogers (eds.), Cambridge Summer School in Mathematical Logic, pp. 113-170, Lecture Notes in Mathematics No. 337, Springer, Berlin.

[37] Friedman, H. [1978], “Classically and intuitionistically provably recursive functions”, in: Müller, G.H. and D. S. Scott (eds.), Higher Set Theory, Proceedings, Oberwolfach, 1977, pp. 21-27, Lecture Notes in Mathematics No. 669, Springer, Berlin.

[38] Friedman, H. and A. Scedrov [1985], ”The lack of definable witnesses and provably recursive functions intuitionistic set theories”, in Advances in Math 57.

[39] Friedman, H. [1986?], Functional Realizability, Manuscript.

[40] Goldblatt, R. [1984], Topoi, revised ed., North-Holland, Amsterdam.

[41] Goodman, N. [1978], “Relativized realizability in intuitionistic arithmetic of all finite types”, Journal of Symbolic Logic 43, 23-44.

[42] Grayson, R. J. [1983], “Forcing in intuitionistic systems without power set”, Journal of Symbolic Logic 48, 670-682.

[43] Grayson, R. J. [1984], “Heyting-valued semantics”, in: F. Lolli, G. Longo and G. Marcja (eds.), Logic Colloquium ’82, North-Holland, Amsterdam.

[44] Grayson, R. J. [1979], “Heyting-valued models for intuitionistic set theory”, in: M. P. Fourman, D.J. Mulvey and D. S. Scott (eds.), Application of Sheaves, Springer Verlag, Berlin.

[45] Grayson, R. J. [1975], “A sheaf approach to models of set theory”, M.Sc. thesis, Oxford.

[46] Hatcher, W. S. [1982] The Logical Foundations of Mathematics, Pergamon Press, Oxford.

[47] Hayashi, S. [1980] “On set theories and toposes”, in the Proceedings of the Logic Conference, Hakone, Lecture Notes in Mathematics 891, Springer.

[48] Hayashi, S.and H. Nakano [1989], PX: A Computational Logic, The MIT Press, Cambridge.

[49] van Heijenoort, J. (ed.) [1967], From Frege to Gödel: A Source Book in Mathematical Logic, Harvard University Press.

[50] Heyting, A. [1971] Intuitionism; an introduction, 3rd.ed., Amsterdam, North-Holland.

[51] Hyland, J. M. E., P. T. Johnstone and A. M. Pitts [1980], “Tripos Theory”, Math. Proceedings of the Cambridge Phil. Society 88, 205-252.

[52] Hyland, M. [1982], “The Effective Topos”, in The L.E.J. Brouwer Centenary Symposium, North Holland.

[53] Hyland, M. and Pitts A., [1989], “The Theory of Constructions: Categorical Semantics and Topos-Theoretic Models”, in Categories in computer science and logic, American Math Society, Providence.

[54] Jacobs, B. [1991], Categorical Type Theory, Ph. D. dissertation, Nijmegen.

[55] Jech, T. [1978], Set Theory, Academic Press, San Diego.

[56] Johnstone, P. T., [1987], Notes on logic and set theory, Cambridge; New York : Cambridge University Press.

[57] Johnstone, P. T., [1982], Stone Spaces, Cambridge University Press.

[58] Johnstone, P. T. [1977], Topos Theory, Academic Press, New York.

[59] Kleene, S. C. [1945], “On the interpretation of intuitionistic number theory”, JSL 10, pp.109-124.

[60] Kleene, S. C. [1952], “Recursive Functions and Intuitionistic Mathematics”, Proc. ICM, Cambridge, 1952.

[61] Kleene, S. C. [1952], Introduction to Metamathematics, North-Holland (1971 edition), Amsterdam.

[62] Kleene, S. C. [1957], “Realizability”, Summaries of talks at the Cornell University summer school.

[63] Kleene, S. C. [1969], Formalized recursive functionals and formalized realizability, memoirs AMS, 89.

[64] Kleene, S. C. [1973], “Realizability: a retrospective survey” in [81].

[65] Kreisel, G., Troelstra, A.S. [1970]“Formal systems for some branches of intuitionistic analysis”, Annals of Math Logic I,229-387.

[66] Kripke, S. [1965], “Semantical analysis of intuitionistic logic I”, in: Crossley, J. N. and M. Dummett (eds.), Formal Systems and Recursive Functions, Proceedings of the Eighth Logic Colloquium, Oxford, 1963, North-Holland, Amsterdam, 92-130.

[67] Kunen, K. [1983], Set Theory, North-Holland, Amsterdam.

[68] Lambek, J. and P. J. Scott [1986], Introduction to higher order categorical logic, Cambridge Studies in Advanced Mathematics 7, Cambridge.

[69] Läuchli, H. [1970], “An abstract notion of realizability for which predicate calculus is complete”, in: Myhill, J., A. Kino, and R. E. Vesley (eds.), Intuitionism and Proof Theory, North-Holland, Amsterdam, 227-234.

[70] Lawvere, W. [1975], “Continuously Variable Sets; algebraic geometry = geometric logic”, in Logic Colloquium ’73 , Rose and Sheperdson, eds., North-Holland, Amsterdam.

[71] Lawvere, W. [1969], “Adjointness in Foundations”, Dialectica,23.

[72] Lawvere, W. [1964], “An elementary theory of the category of sets”, Proc.Nat.Acad.Sci.USA, 52.

[73] Lipton, J., [1990], “Constructive Kripke Semantics and Realizability”, in the proceedings of the Logic for Computer Science conference held at the Math. Sci. Research Institute, Berkeley, Nov. 1989.

[74] Longo, G. and E. Moggi [1988], “Constructive natural deduction and its modest interpretation”, CMU Report CS-88-131, Lecture delivered at the workshop on “The semantics of natural and programming languages”, Stanford, March 1987, M.I.T. Press.

[75] Lubarsky, R., [1994], “V=L in Intuitionistic L”, Manuscript, (to appear).

[76] Mac Lane, S. [1971], Categories for the working mathematician, Springer, Berlin.

[77] Mac Lane, S. and Moerdijk, I., [1992], Sheaves in Geometry and Logic: A First Introduction to Topos Theory, Springer, Berlin.

[78] Makkai, M. and G. Reyes [1977], “First order categorical logic”, Lecture Notes in Mathematics 611, Springer-Verlag, Berlin.

[79] Martin -Löf, P. [1982], “Constructive Mathematics and Computer Programming”, in Logic, Methodology and Philosophy of Science IV, North Holland, Amsterdam.

[80] Martin-Löf, P. [1984], Intuitionistic Type Theory, Studies in Proof Theory Lecture Notes, BIB-LIOPOLIS, Napoli, Italy.

[81] Mathias, A. and Rogers, H., [1973], Proceedings of the Cambridge Summer School in Mathematical Logic, LNM 337, Springer-Verlag, Berlin.

[82] McCarty, D. C. [1986], “Realizability and recursive set theory”, Annals of Pure and Applied Logic 32, 11-194.

[83] McCarty, D. C. [1984], “Realizability and recursive mathematics”, Doctoral Dissertation, Computer Science Department, Carnegie-Mellon University.

[84] McLarty, C. [1993] Elementary Categories, Elementary Toposes, Oxford University Press.

[85] McKinsey and Tarski, [1948], “Some theorems on the sentential calculi of Lewis and Heyting”, JSL 13, 1-15.

[86] Moggi, E., [1991] “Notions of Computation and Monads”, Information and Computation, 93(1).

[87] Mulry, P. [1980], The Recursive Topos, Ph. D. Dissertation, SUNY Buffalo, Buffalo, NY.

[88] Myhill, J. [1970], “Constructive set theory”, in Intuitionism and Proof Theory, Kino, Myhill, Vesley (eds.), North-Holland, Amsterdam.

[89] Myhill, J. [1973], “Some properties of Intuitionistic Zermelo-Fraenkel set theory”, in: Mathias, A. and H. Rogers (eds.), Cambridge Summer School in Mathematical Logic, pp. 113-170, Lecture Notes in Mathematics No. 337, Springer, Berlin.

[90] Odifreddi, P. [1989], Classical Recursion Theory, North-Holland, Amsterdam.

[91] van Oosten, J. [1990], Exercises in Realizability, Ph.D. Dissertation, Amsterdam.

[92] Phoa, W., [1990] An Introduction to fibration, topos theory, the effective topos, and modest sets,

    from theory.ic.ac.uk .

[93] Pitts, A. M., [1981], The Theory of Triposes, Ph. D. Thesis, Cambridge.

[94] Pitts, A. M., [1987], “Polymorphism is Set Theoretic, constructively”, in Category Theory and Computer Science, LNCS 283, Springer.

[95] Plotkin, G. and Reynolds, J. [1987] “On functors expressible in the polymorphic lambda calculus”, in Logical Foundations of Functional Programming, 1990, Addison-Wesley, Reading, MA.

[96] Powell, W. [1976], “A Completeness Theorem for Zermelo-Fraenkel Set Theory”, JSL 41.

[97] Powell, W. [1975], “Extending Gödel’s Negative Interpretation to ZF”, JSL 40.

[98] Powell, W. [1975], Unpublished manuscript.

[99] Prawitz, D. [1965] Natural Deduction: A Proof-Theoretical Study, Almquist and Wiskell, Stockholm.

[100] Rosolini, G. [1986] Continuity and Effectiveness in Topoi, Ph. D. Dissertation, Oxford.

[101] Scedrov, A. and Mitchell, J., [1993] “Notes on Sconing and Relators”, CSL ’92, Springer.

[102] Scedrov, A. [1985], “Intuitionistic Set Theory”, in Harvey Friedman’s Research on the Foundations of Mathematics, North-Holland, Amsterdam.

[103] Scedrov, A. [1984], Forcing and Classifying Topoi, Memoirs of the American Mathematical Society 295, Providence , R.I.

[104] Scedrov, A. [1981], “Consistency and independence results in intuitionistic set theory”, in: F. Richman (ed.), Constructive Mathematics, Proceedings , New Mexico, 1980, pp. 54-86, Lecture Notes in Mathematics 873, Springer-Verlag, Berlin.

[105] Scedrov, A. [1979], “’Every continuous function f : [0, 1] → R is uniformly continuous’ is Independent of intuitionistic ZF”, Preliminary Report, AMS Notices, October, 1979, A-525.

[106] Scott, D. S. [1979], “Identity and existence in intuitionistic logic”, in: Fourman, M. P., Mulvey, C. J. and D. S. Scott (eds.), Applications of Sheaves, Lecture Notes in Mathematics 753, pp. 660-696, Springer, Berlin/Heidelberg/New York

[107] Shoenfield, [1967], Mathematical Logic, Addison-Wesley.

[108] Shoenfield, [1971], “Unramified Forcing” in Axiomatic Set Theory, V. 1, Proc.Sym. Pure Math., Vol. 13, AMS, Providence, R.I.

[109] Seely, R. [1983], “Hyperdoctrines, Natural Deduction and the Beck Condition”, ZML 29.

[110] Seely, R. [1984], “Locally Cartesian Closed Categories and Type Theory”, Math. Proc. Camb. Phil. Soc. 95.

[111] Streicher, T. [1989], Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions, Ph. D. dissertation,Univ. Passau.

[112] Streicher, T. [1992], “Independence of the induction principle and the axiom of choice in the pure calculus of constructions”, TCS 103, pp. 395-408.

[113] Takeuti, G. and Titani, G. [1980], “Heyting-valued universes of intuitionistic set theory” in Logic Symposia, Hakone, 79-80, Lecture Notes in Mathematics 891, Springer.

[114] Tait, W. W. [1975], “A realizability interpretation of the theory of species”, Logic Colloquium (Boston, Mass., 1972/73), Lecture Notes in Mathematics, V. 453, Springer-Verlag, 240-251.

[115] Tennison, B. R. [1975] Sheaf Theory, Cambridge University Press.

[116] Tierney, M. [1972], “Sheaf Theory and Continuum hypothesis”, in: F. W. Lawvere (ed.), Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, pp. 13-42, Springer-Verlag, Berlin.

[117] Troelstra, A. [1978], Choice Sequences, Oxford Logic Guides, Oxford University Press.

[118] Troelstra, A. S. and D. van Dalen [1988], Constructivism in Mathematics: An Introduction, Vol. II, Studies in Logic and the Foundations of Mathematics, Vol. 123, North-Holland, Amsterdam.