1 Introduction
In this paper, we prove that extensional generic realizability [Reference Frittaion and Rathjen17] validates the natural extension of $\mathsf { AC}_{\mathsf {FT}}$ (the axiom of choice in finite types) and $\mathsf {RDC}_{\mathsf {FT}}$ (relativized dependent choice in finite types) to transfinite dependent types. By routinely combining extensional generic realizability with a Beeson-style forcing construction, along the lines of [Reference Friedman and Ščedrov15, Section 5], we also show that T augmented with such choice principles is conservative over T for arithmetic sentences, for a host of intuitionistic set theories T. In particular, we extend Friedman and Ščedrov’s result [Reference Friedman and Ščedrov15] that $\mathsf {IZF}$ augmented with $\mathsf {CAC}_{\mathsf {FT}}$ (finite type countable choice) and $\mathsf {DC}_{\mathsf {FT}}$ (finite type dependent choice) is arithmetically conservative over $\mathsf {IZF}$ .Footnote 1
Generic realizabilityFootnote 2 is distinguished by its treatment of unbounded quantifiers: a realizer of $\forall x\, \varphi (x)$ (resp. $\exists x\, \varphi (x)$ ) must be a realizer of $\varphi (x)$ for every x (resp. some x). This strain of realizability goes back to Kreisel and Troelstra’s realizability for theories of elementary analysis with species variables [Reference Kreisel and Troelstra21, Section 3.7]. A direct descendant of Kreisel and Troelstra’s realizability was applied to nonextensional theories of higher order arithmetic and set theory by Friedman [Reference Friedman14] and Beeson [Reference Beeson5, Reference Beeson7]. McCarty [Reference McCarty22, Reference McCarty23] developed a version of generic realizability that applies directly to the extensional set theory $\mathsf {IZF}$ . He also employed, inspired by Feferman [Reference Feferman12], arbitrary partial combinatory algebras, rather than just natural numbers. Whereas McCarty’s approach is geared towards $\mathsf {IZF}$ , it was shown in [Reference Rathjen30] that $\mathsf {CZF}$ suffices for a formalization of generic realizability, thus providing a self-validating semantics for $\mathsf {CZF}$ and other fragments of $\mathsf {IZF}$ .
In [Reference Frittaion and Rathjen17], we added an extra layer of extensionality to McCarty’s generic realizability, and thus obtained inner models of both $\mathsf {CZF}$ and $\mathsf {IZF}$ that further validate $\mathsf {AC}_{\mathsf {FT}}$ .Footnote 3 In the present paper, we show that extensional generic realizability yields an interpretation of
-
• $T+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ in T, and
-
• $T+\mathsf {REA}+ {\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}^{\dagger } +{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ in $T+\mathsf {REA}$ ,
where T can be either $\mathsf {CZF}$ , $\mathsf {IZF}$ or an extension thereof with other choice axioms. We will introduce this family of choice principles for dependent types in Section 2. Suffice it to say here that ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf { AC}^{\dagger }$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}^{\dagger }$ are closely related to, and in fact follow from, Aczel’s ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}$ . The latter are validated by the type-theoretic interpretations of $\mathsf {CZF}$ [Reference Aczel1, Reference Aczel2] and $\mathsf {CZF}+\mathsf {REA}$ [Reference Aczel3], respectively. Our interpretation does not appear to validate ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}$ and relatives, even if we assume it in the background theory. We will see in Section 4.4 that extensional generic realizability refutes the statement that every set is an image of a ${\Pi }{\Sigma }\mathrm {I}$ -set ( ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -set), which instead holds true in Aczel’s type-theoretic interpretation of $\mathsf {CZF}$ ( $\mathsf {CZF}+\mathsf {REA}$ ).
The basic plan for interpreting choice via extensional generic realizability can be easily described as follows. Consider the ${\Pi }{\Sigma }\mathrm {I}$ case. We start out with a realizability universe $\mathrm {V_{ext}}(A)$ , which is built on top of a given partial combinatory algebra A. We then construct an extensional type structure on A (Definition 4.3). In particular, types are elements of A. Next, we single out nice sets of $\mathrm {V_{ext}}(A)$ of the form $X_{\sigma }$ , where $\sigma $ runs over all types (Definition 4.9). We think of these sets as the extensions of the corresponding types. With this identification in mind, we show that $\mathsf {AC}_{\sigma ,\tau }$ and $\mathsf {RDC}_{\sigma }$ hold in $\mathrm {V_{ext}}(A)$ (Theorems 4.17 and 4.18). Finally, we prove that every ${\Pi }{\Sigma }\mathrm {I}$ -set of $\mathrm {V_{ext}}(A)$ is nicely represented (Theorems 4.14 and 4.16). Niceness is captured by a suitable notion of being injectively presented in $\mathrm {V_{ext}}(A)$ (similar notions can be encountered in [Reference Aczel2, Reference Aczel3, Reference Rathjen27–Reference Rathjen29]). It will be crucial to work with extensional type structures.
2 Preliminaries
2.1 $\mathsf {CZF}$ and $\mathsf {IZF}$
In this paper, we will be concerned with (extensions of) $\mathsf {CZF}$ (constructive Zermelo–Fraenkel set theory) and $\mathsf {IZF}$ (intuitionistic Zermelo–Fraenkel set theory). The logic is intuitionistic first order logic with equality in the language of classical $\mathsf {ZF}$ . As usual, a formula is bounded, or $\Delta _0$ , if all quantifiers appear in the form $\forall x\in y$ and $\exists x\in y$ .
The theory $\mathsf {CZF}$ consists of the following axioms:
$^{\ast} $ Let $x=0$ be $\forall y\in x\, (y\notin x)$ and $x=y\cup \{y\}$ be $\forall z\kern-1pt \in\kern-1pt x\, (z\kern-1pt \in\kern-1pt y\lor z\kern-1pt =\kern-1pt y)\land \forall z\kern-1pt \in\kern-1pt y\, (z\in x)\land y\kern-1pt \in\kern-1pt x$ .
The theory $\mathsf {IZF}$ consists of extensionality, pairing, union, infinity, induction,
Thus $\mathsf {IZF}$ is $\mathsf {CZF}$ with bounded separation replaced by full separation and subset collection replaced by powerset. Note that powerset implies subset collection, and strong collection follows from separation and collection. It is well known that $\mathsf { CZF}$ with classical logic, and hence $\mathsf {IZF}$ with classical logic, is equivalent to $\mathsf {ZF}$ .
2.2 Countable and dependent choice
The full axiom of choice $\mathsf {AC}$ is known to imply forms of excluded middle [Reference Diaconescu11]. For example, $\mathsf {CZF}+\mathsf {AC}+\text { separation}=\mathsf {IZF}+\mathsf {AC}=\mathsf {ZFC}$ (cf. [Reference Aczel and Rathjen4]). Nevertheless, countable choice and several forms of dependent choice are deemed constructively acceptable. Note that $\mathsf {RDC}$ is an axiom of Myhill’s $\mathsf {CST}$ (constructive set theory) [Reference Myhill24], which provides a standard set-theoretical framework for Bishop-style constructive mathematics [Reference Bishop9]. Dependent choice also features in Brouwer’s intuitionistic analysis (cf. [Reference Troelstra and van Dalen34]).
Countable choice ( $\mathsf {AC}_{\omega }$ ): if $\forall n\in \omega \, \exists y\, \varphi (n,y)$ , then there exists a function f with $\operatorname {{\mathrm {dom}}}(f)=\omega $ such that $\forall n\in \omega \, \varphi (n,f(n))$ , for all formulae $\varphi $ .
Dependent choice ( $\mathsf {DC}$ ): if $\forall x\, \exists y\, \varphi (x,y)$ , then for every x there is a function f with $\operatorname {{\mathrm {dom}}}(f)=\omega $ such that $f(0)=x$ and $\forall n\in \omega \, \varphi (f(n),f(n+1))$ , for all formulae $\varphi $ .
Limited dependent choice ( $\mathsf {DC}^{\dagger }$ ): if X is a set and $\forall x\in X\, \exists y\in X\, \varphi (x,y)$ , then for every $x\in X$ there is a function $f\colon \omega \to X$ such that $f(0)=x$ and $\forall n\in \omega \, \varphi (f(n),f(n+1))$ , for all formulae $\varphi $ .
Relativized dependent choice ( $\mathsf {RDC}$ ): if $\forall x\, (\psi (x)\rightarrow \exists y\, (\psi (y)\land \varphi (x,y)))$ , then for every x such that $\psi (x)$ , there is a function f with $\operatorname {{\mathrm {dom}}}(f)=\omega $ such that $f(0)=x$ and $\forall n\in \omega \, \varphi (f(n),f(n+1))$ , for all formulae $\psi $ and $\varphi $ .
Limited relativized dependent choice ( $\mathsf {RDC}^{\dagger }$ ): if X is a set and $\forall x\in X\, (\psi (x)\rightarrow \exists y\in X\, (\psi (y)\land \varphi (x,y)))$ , then for every $x\in X$ such that $\psi (x)$ , there is a function $f\colon \omega \to X$ such that $f(0)=x$ and $\forall n\in \omega \, \varphi (f(n),f(n+1))$ , for all formulae $\psi $ and $\varphi $ .
Note that classically, say over $\mathsf {ZF}$ , the above forms of dependent choice are all equivalent to one another. Over $\mathsf {CZF}$ , $\mathsf {RDC}\rightarrow \mathsf {DC}$ and $\mathsf {RDC}\rightarrow \mathsf {RDC}^{\dagger }\rightarrow \mathsf {DC}^{\dagger }\rightarrow \mathsf { AC}_{\omega }$ . Over $\mathsf {IZF}$ , due to separation, $\mathsf {RDC}^{\dagger }\leftrightarrow \mathsf {DC}^{\dagger }$ .
2.3 Inductive definitions and the regular extension axiom
The theory $\mathsf {CZF}$ allows for a smooth treatment of inductively defined classes [Reference Aczel3, Reference Aczel and Rathjen4].
Definition 2.1. An inductive definition is a class $\Phi $ of ordered pairs. In other words, any formula $\Phi (X,x)$ is an inductive definition. We write
or simply $(X,x)\in \Phi $ , in place of $\Phi (X,x)$ . A class I is closed under $\Phi $ if, whenever $(X,x)\in \Phi $ and $X\subseteq I$ , we have $x\in I$ .
Theorem 2.2. Given an inductive definition $\Phi $ , there exists a class $I(\Phi )$ such that $\mathsf {CZF}$ proves that $I(\Phi )$ is closed under $\Phi $ , and for every class J, $\mathsf {CZF}$ proves that if J is closed under $\Phi $ , then $I\subseteq J$ . We say that $I(\Phi )$ is inductively defined by $\Phi $ .
Proof See, e.g., [Reference Aczel and Rathjen4] for details. The class $I(\Phi )$ is defined as follows. A set of ordered pairs Z is called an iteration set for $\Phi $ if for every $\langle {u,x}\rangle \in Z$ there exists $(X,x)\in \Phi $ such that $X\subseteq \bigcup _{v\in u}\{z\mid \langle {v,z}\rangle \in Z\}$ . Let
To prove that $I(\Phi )$ is closed under $\Phi $ we invoke strong collection. The fact that $I(\Phi )$ is the smallest class closed under $\Phi $ is proved by induction.
Theorem 2.3 (Induction on the inductive definition $\Phi $ ).
$\mathsf {CZF}$ proves
for every formula $\varphi $ .
Proof Obvious.
In the presence of Aczel’s $\mathsf {REA}$ (regular extension axiom), one can show that many inductively defined classes exist as sets.
Definition 2.4 (Regular).
A set X is regular if it is transitive and, whenever $x\in X$ and R is a set such that $\forall u\in x\, \exists v\in X\, (\langle {u,v}\rangle \in R)$ , then there is a $y\in X$ such that
In particular, if $R\colon x\to X$ is a function, then $\operatorname {{\mathrm {ran}}}(R)\in X$ .
Regular extension axiom ( $\mathsf {REA}$ ): every set is a subset of a regular set.
Definition 2.5. An inductive definition $\Phi $ is bounded if:
-
• the class $\{x\mid (X,x)\in \Phi \}$ is a set for every set X;
-
• there is a set B such that whenever $(X,x)\in \Phi $ , then X is an image of a set in B, that is, there is a function f from Y onto X for some $Y\in B$ . The set B is called a bound for $\Phi $ .
Theorem 2.6 ( $\mathsf {CZF}+\mathsf {REA}$ ).
If $\Phi $ is a bounded inductive definition, then the class $I(\Phi )$ is a set.
Proof See [Reference Aczel3, Theorem 5.2].
2.4 Dependent type constructions
The usual type constructors ${\Pi }$ (dependent product), ${\Sigma }$ (dependent sum), $\mathrm {I}$ (identity), and $\mathrm {W}$ have obvious set-theoretic analogues.
Definition 2.7 ( $\mathsf {CZF}$ ).
Let F be a function with $\operatorname {{\mathrm {dom}}}(F)=X$ . Let
For x, y sets, let $\mathrm {I}(x,y)=\{z\in \{0\}\mid x=y\}$ .
Remark 2.8. Set exponentiation $X\to Y$ and the binary Cartesian product $X\times Y$ are special instances of ${\Pi }(X,F)$ and ${\Sigma }(X,F)$ respectively, with $F(x)=Y$ .
Definition 2.9 ( $\mathsf {CZF}$ ).
If F is a function with $\operatorname {{\mathrm {dom}}}(F)=X$ , then $\mathrm {W}(X,F)$ is the smallest class W such that
-
• if $x\in X$ and $f\colon F(x)\to W$ , then $\langle {x,f}\rangle \in W$ .
Remark 2.10. $\mathrm {W}(X,F)$ is the class of well-founded rooted trees with labels in X such that the arity of a node with label x is the set $F(x)$ .
Theorem 2.11 ( $\mathsf {CZF}+\mathsf {REA}$ ).
The class $\mathrm {W}(X,F)$ is a set.
Proof By Theorem 2.6, since $\mathrm {W}(X,F)$ is bounded inductively definable.
Definition 2.12 ( $\mathsf {CZF}$ ).
The class $I={\Pi }{\Sigma }$ is inductively defined by clauses:
-
(i) $n\in I$ for every $n\in \omega $ ;
-
(ii) $\omega \in I$ ;
-
(iii) if $X\in I$ and $F\colon X\to I$ , then ${\Pi }(X,F),{\Sigma }(X,F)\in I$ .
The class $I={\Pi }{\Sigma }\mathrm {I}$ is inductively defined by clauses (i), (ii), (iii), and
-
(iv) if $X\in I$ and $x,y\in X$ , then $\mathrm {I}(x,y)\in I$ .
Definition 2.13 ( $\mathsf {CZF}+\mathsf {REA}$ ).
The class $I={\Pi }{\Sigma }\mathrm {W}$ is inductively defined by clauses (i), (ii), (iii), and
-
(v) if $X\in I$ and $F\colon X\to I$ , then $\mathrm {W}(X,F)\in I$ .
The class $I={\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ is inductively defined by clauses (i)–(v).
Given a class I, we say that x is an I-set if x belongs to I.
2.5 Choice for dependent types
Definition 2.14 (Base).
A set X is a base if for every relation R such that $\forall x\in X\, \exists y\, (\langle {x,y}\rangle \in R)$ , there exists a function f with domain X such that $\forall x\in X\, (\langle {x,f(x)}\rangle \in R)$ .Footnote 4
Presentation axiom ( $\mathsf {PAx}$ ): every set is an image of a base.
${\Pi }{\Sigma }$ axiom of choice ( ${\Pi }{\Sigma }\text {-}\mathsf {AC}$ ): every ${\Pi }{\Sigma }$ -set is a base.
${\Pi }{\Sigma }$ presentation axiom ( ${\Pi }{\Sigma }\text {-}\mathsf {PAx}$ ): every set is an image of a ${\Pi }{\Sigma }$ -set and every ${\Pi }{\Sigma }$ -set is a base.
We have analogue axioms for ${\Pi }{\Sigma }\mathrm {I}$ and relatives. A simple argument shows that $\mathsf {CZF}+\mathsf {PAx}\vdash \mathsf { DC}^{\dagger }$ (cf. [Reference Aczel1, p. 65] and [Reference Aczel2, p. 27]). Aczel’s interpretation of $\mathsf {CZF}$ in type theory [Reference Aczel1] validates $\mathsf {RDC}$ [Reference Aczel1, Theorem 7.1], [Reference Aczel2, Theorem 5.7] and ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {PAx}$ [Reference Aczel2, Theorem 7.4]. In [Reference Aczel3], the type-theoretic interpretation of $\mathsf {CZF}+\mathsf {REA}$ (by using $\mathrm {W}$ -types) is shown to validate $\mathsf {RDC}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {PAx}$ [Reference Aczel3, Theorem 5.6].Footnote 5 Similarly, Rathjen’s formulae-as-classes interpretation provides a model of $\mathsf {CZF}+\mathsf { RDC}+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}$ in $\mathsf {CZF}_{\mathsf {exp}}$ [Reference Rathjen29, Theorem 4.13] and of $\mathsf {CZF}+\mathsf {REA}+\mathsf {RDC}+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}$ in $\mathsf {CZF}_{\mathsf { exp}}+\mathsf {REA}$ [Reference Rathjen29, Theorem 4.33], where $\mathsf {CZF}_{\mathsf {exp}}$ is $\mathsf {CZF}$ with exponentiation in lieu of subset collection.
We introduce the following natural extensions of $\mathsf {AC}_{\mathsf {FT}}$ and $\mathsf {RDC}_{\mathsf {FT}}$ .
${\Pi }{\Sigma }$ limited axiom of choice ( ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ ): if X and Y are ${\Pi }{\Sigma }$ -sets and $\forall x\in X\, \exists y\in Y\, \varphi (x,y)$ , then there is a function $f\colon X\to Y$ such that $\forall x\in X\, \varphi (x,f(x))$ , for all formulae $\varphi $ .
${\Pi }{\Sigma }$ limited relativized dependent choice ( ${\Pi }{\Sigma }\text {-}\mathsf {RDC}^{\dagger }$ ): this is just $\mathsf { RDC}^{\dagger }$ restricted to ${\Pi }{\Sigma }$ -sets.
We have similar axioms for ${\Pi }{\Sigma }\mathrm {I}$ and relatives. Each schema can be replaced by a single axiom over say $\mathsf { IZF}+\mathsf {REA}$ . This is just an upper bound. For example, over $\mathsf {CZF}$ , ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ is equivalent to:
If X and Y are ${\Pi }{\Sigma }$ -sets, then for every relation R such that $\forall x\in X\, \exists y\in Y\, (\langle {x,y}\rangle \in R)$ , there is a function $f\colon X\to Y$ such that $\forall x\in X\, (\langle {x,f(x)}\rangle \in R)$ .
Clearly, ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ follows from ${\Pi }{\Sigma }\text {-}\mathsf {AC}$ , and similarly for ${\Pi }{\Sigma }\mathrm {I}$ and the like. Note that ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ already includes the axiom of choice for all finite types.
Theorem 2.15. Over $\mathsf {CZF}$ , ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}\leftrightarrow {\Pi }{\Sigma }\text {-}\mathsf {AC}$ and ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {PAx} \ \leftrightarrow {\Pi }{\Sigma }\text {-}\mathsf {PAx}$ .
Over $\mathsf {CZF}+\mathsf {REA}$ , ${\Pi }{\Sigma }\mathrm {W}\text {-}\mathsf {AC}\leftrightarrow {\Pi }{\Sigma }\text {-}\mathsf {AC}$ and ${\Pi }{\Sigma }\mathrm {W}\text {-}\mathsf {PAx}\leftrightarrow {\Pi }{\Sigma }\text {-}\mathsf {PAx}$ .
Proof See [Reference Aczel3, Theorems 3.7 and 5.9].
Theorem 2.15 does not translate to ${\Pi }{\Sigma }\text {-}\mathsf {AC}^{\dagger }$ and relatives. For example, the proof of [Reference Aczel3, Theorem 3.7] consists in showing, under ${\Pi }{\Sigma }\text {-}\mathsf {AC}$ , that every set in ${\Pi }{\Sigma }\mathrm {I}$ is in bijection with a set in ${\Pi }{\Sigma }$ . The use of ${\Pi }{\Sigma }\text {-}\mathsf {AC}$ is essential. The proof of the following is trivial.
Theorem 2.16. Over $\mathsf {CZF} +$ “every set is an image of a ${\Pi }{\Sigma }\mathrm {I}$ -set,” $ {\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC} \leftrightarrow {\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }$ . Similarly for $\mathsf {CZF}+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ in place of $\mathsf {CZF}$ and ${\Pi }{\Sigma }\mathrm {I}$ respectively.
3 Extensional generic realizability
3.1 Partial combinatory algebras
Generic realizability is based on the notion of partial combinatory algebra. Let us review some basic facts. For more information, we refer the reader to [Reference Beeson7, Reference Feferman12, Reference Feferman13, Reference van Oosten26].
Definition 3.1. Application terms, or simply terms, over a set A are defined by clauses:
-
(i) variables $x_1,x_2,\ldots $ are terms;
-
(ii) elements of A are terms;
-
(iii) if t and s are terms, $(ts)$ is also a term.
Definition 3.2. A partial algebra is a set A together with a partial binary operation $\cdot $ on A.
Every partial algebra A induces a partial interpretation of closed applications terms over A by elements of A in the obvious way.
Notation 3.3. Let $a,b,c\in A$ and $t,s$ be closed terms over A. Instead of $a\cdot b$ we just write $ab$ . We also employ the association to the left convention, meaning that $abc$ stands for $(ab)c$ . The relation $t\downarrow a$ is defined by clauses: (i) $a\downarrow a$ and (ii) $(ts)\downarrow a$ if $t\downarrow b$ , $s\downarrow c$ , and $bc=a$ for some $b,c\in A$ . We write $t\downarrow $ for $\exists a\, (t\downarrow a)$ . We use Kleene equality $t\simeq s$ to express that either both sides are undefined, or else they are both defined and equal. In the second case, we write $t=s$ .
Definition 3.4. A partial algebra $(A,\cdot )$ with at least two elements is a partial combinatory algebra (pca) if there are elements $\mathbf k$ and $\mathbf s$ in A such that for all $a,b,c\in A$ :
-
• $\mathbf ka b\simeq a$ ;
-
• $\mathbf sab\downarrow $ and $\mathbf sabc\simeq ac(bc)$ .
The combinators $\mathbf k$ and $\mathbf s$ are due to Schönfinkel [Reference Schönfinkel31] and the defining equations, although formulated just in the total case, are due to Curry [Reference Curry10]. The name combinatory stems from the property known as combinatory completeness. Informally, this means that we can form $\lambda $ -terms.
Lemma 3.5 ( $\lambda $ -abstraction).
Let A be a pca. For every term $t(x,x_1,\ldots ,x_n)$ , one can find (in an effective way) a new term $s(x_1,\ldots ,x_n)$ , denoted $\lambda x.t$ , such that for all $a_1,\ldots ,a_n\in A$ :
-
• $s(a_1,\ldots ,a_n)\downarrow $ ;
-
• $s(a_1,\ldots ,a_n)a\simeq t(a,a_1,\ldots ,a_n)$ .
Remark 3.6. The term $\lambda x.t$ is built solely with the aid of $\mathbf k$ , $\mathbf s$ , and symbols occurring in t. Also, the construction of this term is uniform in the given pca.
An immediate consequence of $\lambda $ -abstraction is the existence of pairing and unpairing combinators $\mathbf p$ , $\mathbf {p_0}$ , and $\mathbf {p_1}$ such that $\mathbf pab\downarrow $ and $\mathbf {p_i}(\mathbf pa_0a_1)\simeq a_i$ .Footnote 6 A more remarkable application of $\lambda $ -abstraction is the recursion theorem for pca’s.
Lemma 3.7 (Recursion theorem).
There exists a closed term $\mathbf f$ such that for all $a,b\in A$ we have $\mathbf f a\downarrow $ and $\mathbf f ab\simeq a(\mathbf fa) b$ .
It is worth considering some additional structure (see however Remark 3.9).
Definition 3.8. We say that A is a pca over $\omega $ if there are combinators $\mathbf {succ}, \mathbf {pred}$ (successor and predecessor combinators), $\mathbf d$ (definition by cases combinator), and a map $n\mapsto \bar n$ from $\omega $ to A such that for all $n\in \omega $
One then defines $\mathbf 0=_{\mathrm {def}}\bar 0$ and ${\mathbf 1}=_{\mathrm {def}}\bar 1$ .
For the rest of the paper, by a pca we really mean a pca over $\omega $ . The only closed terms we ever need are built up by using the combinators $\mathbf k$ , $\mathbf s$ , $\mathbf p$ , $\mathbf {p_0}$ , $\mathbf {p_1}$ , $\mathbf 0$ , ${\mathbf 1}$ , $\mathbf {succ}$ , $\mathbf {pred}$ , and $\mathbf d$ .
Note that one can do without $\mathbf k$ by letting $\mathbf k=_{\mathrm {def}}\mathbf d\mathbf 0\mathbf 0$ . The existence of $\mathbf d$ implies that the map $n\mapsto \bar n$ is one-to-one. In fact, suppose $\bar n=\bar m$ but $n\neq m$ . Then $\mathbf d\bar n\bar n\simeq \mathbf d\bar n\bar m$ . It then follows that $a\simeq \mathbf d\bar n\bar nab\simeq \mathbf d\bar n\bar mab\simeq b$ for all $a,b$ . On the other hand, by our definition, every pca contains at least two elements.
Remark 3.9. Every pca can be turned into a pca over $\omega $ . For example, one can define Curry numerals and construct by $\lambda $ -abstraction a combinator $\mathbf d$ for this representation of natural numbers. In practice, however, all natural examples of pca come already equipped with a canonical copy of the natural numbers and pertaining combinators.
3.2 Defining realizability
Definition 3.10 ( $\mathsf {CZF}$ ).
Given a pca A, the class $\mathrm {V_{ext}}(A)$ is inductively defined by the clause:
-
• if $x\subseteq A\times A\times \mathrm {V_{ext}}(A)$ , then $x\in \mathrm {V_{ext}}(A)$ .
The inductive definition of $\mathrm {V_{ext}}(A)$ within $\mathsf {CZF}$ is on par with that of $\mathrm {V}(A)$ [Reference Rathjen30,Lemma 3.4].
Notation 3.11. We use $(a)_i$ or simply $a_i$ for $\mathbf {p_i}a$ . Whenever we write a term t, we assume that it is defined. In other words, a formula $\varphi (t)$ stands for $\exists a\, (t\downarrow a\land \varphi (a))$ .
Definition 3.12 (Extensional realizability).
We define the relation $a=b\Vdash \varphi $ , where $a,b\in A$ and $\varphi $ is a realizability formula with parameters in $\mathrm {V_{ext}}(A)$ . The atomic cases fall under the scope of definitions by transfinite recursion.
Notation 3.13. We write $\Vdash \varphi $ in place of $\exists a,b\in A\, (a=b\Vdash \varphi )$ and $a\Vdash \varphi $ for $a=a\Vdash \varphi $ .
We will repeatedly use the following internal pairing function $\langle {x,y}\rangle _{\!A}$ in $\mathrm {V_{ext}}(A)$ .
Definition 3.14 (Pairing).
For $x,y\in \mathrm {V_{ext}}(A)$ , let
Note that all these sets are in $\mathrm {V_{ext}}(A)$ .
We use $\operatorname {{\mathrm {OP}}}(z,x,y)$ as abbreviation for the set-theoretic formula expressing that z is the ordered pair of x and y. In standard notation, $z=\langle {x,y}\rangle $ . Ordered pairs can be defined as usual as $\langle {x,y}\rangle =_{\mathrm {def}}\{\{x\},\{x,y\}\}$ .
Lemma 3.15. There are closed terms ${\mathbf u}_i$ such that $\mathsf {CZF}$ proves
Proof This is similar to [Reference McCarty22, Lemmas 3.2 and 3.4].
Theorem 3.16 [Reference Frittaion and Rathjen17].
For every theorem $\varphi $ of $\mathsf {CZF}+\mathsf {AC}_{\mathsf {FT}}$ , there is a closed term ${\mathbf t}$ such that $\mathsf { CZF}$ proves ${\mathbf t}\Vdash \varphi $ . The same for $\mathsf {IZF}$ .
Remark 3.17. The realizability relation $\Vdash $ uses A as a parameter. We should then write $\Vdash _A$ . The soundness theorem claims that for every theorem $\varphi $ of T there is a closed term ${\mathbf t}$ such that $T\vdash \forall A\, (A\text { is a pca}\rightarrow {\mathbf t}\Vdash _A \varphi )$ . For special cases, where the pca A is definable as a set in T and $T\vdash A \text { is a pca}$ , we obtain $T\vdash {\mathbf t}\Vdash _A \varphi $ . For instance, in the case of Kleene’s first algebra, we have that for every theorem $\varphi $ , there is a closed term ${\mathbf t}$ such that $T\vdash \exists n\in \omega \, ({\mathbf t}\downarrow n\land n\Vdash \varphi )$ .
Definition 3.18. Write $T\models \varphi $ for $T\vdash \exists a,b\in A\, (a=b\Vdash \varphi )$ . In general, we write $T\models S$ if $T\models \varphi $ for every sentence $\varphi $ of S. We say that T is self-validating if $T\models T$ .
Theorem 3.19. Let T be any of the theories obtained by appending to either $\mathsf {CZF}$ or $\mathsf {IZF}$ some or all of the axioms $\mathsf { REA}$ , $\mathsf {AC}_{\omega }$ , $\mathsf {DC}$ , $\mathsf {DC}^{\dagger }$ , $\mathsf {RDC}$ , $\mathsf {RDC}^{\dagger }$ , and $\mathsf {PAx}$ . Then T is self-validating.
Proof This holds in the case of generic realizability. See [Reference Rathjen30, Theorem 6.2] for $\mathsf {REA}$ and [Reference Rathjen30, Theorem 10.1] for $\mathsf {DC}^{\dagger }$ (there called $\mathsf {DC}$ ), $\mathsf {RDC}$ , and $\mathsf { PAx}$ . The other axioms are treated in a similar way. In the case of extensional generic realizability, the proof is a nearly verbatim copy of that for generic realizability.
Let us sketch a proof for $\mathsf {PAx}$ . We wish to find a closed term ${\mathbf e}$ such that, over $\mathsf {CZF}+\mathsf {PAx}$ ,
By definition, this means that for every $y\in \mathrm {V_{ext}}(A)$ there are $x,f\in \mathrm {V_{ext}}(A)$ such that
Let $y\in \mathrm {V_{ext}}(A)$ . By $\mathsf {PAx}$ in the background universe, there exists a base B and a function F from B onto y. Say $F(u)=\langle {a_u,b_u,z_u}\rangle \in y$ for $u\in B$ . By transfinite recursion, define
Then for every set u, $\check u\in \mathrm {V_{ext}}(A)$ . Moreover, by induction, one can show that these names are absolute, namely,
Let
where $\langle {u,v}\rangle _{\!A}$ is the internal pair in $\mathrm {V_{ext}}(A)$ from Definition 3.14. One can find a closed term $\mathbf f$ such that $\mathbf f \Vdash \operatorname {{\mathrm {Fun}}}(f)$ thanks to the absoluteness of $\check {}$ names. It is not difficult to build a closed term ${\mathbf t}$ such that ${\mathbf t} \Vdash f\colon x\twoheadrightarrow y$ . Finally, it is straightforward to cook up a closed term $\mathbf b$ and show that $\mathbf b\Vdash x \text { is a base}$ , by using the fact that B is a base.
In view of Definition 3.18, our goal is to show that:
-
• $T\models T+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ ,
-
• $T+\mathsf {REA}\models T+\mathsf {REA}+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf { AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ ,
where T is as in Theorem 3.19.
4 Realizing choice for dependent types
4.1 Dependent types over partial combinatory algebras
Given a pca A, we wish to define extensional type structures on A, that is, structures of the form
where $\sim $ is a partial equivalence relation on A and $\sim _{\sigma }$ is a partial equivalence relation on A for every $\sigma $ such that $\sigma \sim \sigma $ . Then $\mathbb {T}=\{\sigma \in A\mid \sigma \sim \sigma \}$ and $A_{\sigma }=\{a\in A\mid a\sim _{\sigma } a\}$ for every $\sigma \in \mathbb {T}$ . Clearly, we want equivalent types to have the same elements. We must then ensure that if $\sigma \sim \tau $ , then $a\sim _{\sigma } b$ iff $a\sim _{\tau } b$ .
Definition 4.1. We say that $\sigma $ is a type if $\sigma \in \mathbb {T}$ . We say that $a\in A$ has type $\sigma $ if $a\in A_{\sigma }$ .
From now on, definitions and theorems take place in $\mathsf {CZF}$ , unless we are dealing with $\mathrm {W}$ -types, in which case we work in $\mathsf {CZF}+\mathsf {REA}$ .
Notation 4.2. Given a pca A, $a,b,c\in A$ , and $n\in \omega $ , we write:
This ensures unique readability. For example, $\mathsf {N}\neq {\Pi }_a b$ , and ${\Pi }_ab={\Pi }_cd$ implies $a=b$ and $c=d$ .
Definition 4.3 ( ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -types).
Given a pca A, we inductively define the ${\Pi }{\Sigma }$ type structure by clauses:
-
(i) $\mathsf {N}_n\sim \mathsf {N}_n$ and $a\sim _{\mathsf {N}_n} b$ iff $a=b=\bar m$ for some $m<n$ ;
-
(ii) $\mathsf {N}\sim \mathsf {N}$ and $a\sim _{\mathsf {N}} b$ iff $a=b=\bar n$ for some $n\in \omega $ ;
-
(iii) if $\sigma \sim \tau $ , and $a\sim _{\sigma } b$ implies $ia\sim jb$ , then:
-
• $\alpha ={\Pi }_{\sigma } i\sim {\Pi }_{\tau } j$ ;
-
• $f\sim _{\alpha } g$ iff $fa\sim _{ia} gb$ whenever $a\sim _{\sigma } b$ ; and
-
• $\beta ={\Sigma }_{\sigma } i\sim {\Sigma }_{\tau } j$ ;
-
• $a\sim _{\beta } b$ iff $a_0\sim _{\sigma } b_0$ and $a_1\sim _{ia_0} b_1$ .
-
The $\Pi {\Sigma }\mathrm {I}$ type structure is inductively defined by adding the clause:
-
(iv) if $\sigma \sim \tau $ , $a\sim _{\sigma } \breve a$ , and $b\sim _{\sigma } \breve b$ , then:
-
• $\gamma =\mathrm {I}_{\sigma }(a,b)\sim \mathrm {I}_{\tau }(\breve a,\breve b)$ ;
-
• $c\sim _{\gamma } d$ iff $c=d=\mathbf 0$ and $a\sim _{\sigma } b$ .
-
The ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ type structure is inductively defined by clauses (i), (ii), (iii), (iv), and
-
(v) if $\sigma \sim \tau $ , and $a\sim _{\sigma } b$ implies $ia\sim jb$ , then:
-
• $\delta =\mathrm {W}_{\sigma } i\sim \mathrm {W}_{\tau } j$ ;
-
• $c\sim _{\delta } d$ iff $c_0\sim _{\sigma } d_0$ and $c_1p\sim _{\delta } d_1q$ whenever $p\sim _{ic_0} q$ .
-
Remark 4.4. To be precise, each type structure from Definition 4.3 is an inductively defined class I of triples $\langle {\sigma ,\tau ,B}\rangle $ . The intended meaning is $\sigma \sim \tau $ and $a\sim _{\sigma } b$ iff $\langle {a,b}\rangle \in B$ . For instance, the rules for the introduction of ${\Pi }$ -types and $\mathrm {W}$ -types are
where $\sigma ,\tau ,i,j\in A$ , and for some set $B\subseteq A\times A$ and some function F with $\operatorname {{\mathrm {dom}}}(F)=B$ , we have:
-
• $\{\langle {\sigma ,\tau ,B}\rangle \}\cup \{\langle {ia,jb,F(a,b)}\rangle \mid \langle {a,b}\rangle \in B\}\subseteq X$ ,
-
• $C=\{\langle {f,g}\rangle \in A\times A\mid \forall \langle {a,b}\rangle \in B\, (\langle {fa,gb}\rangle \in F(a,b))\}$ ,
-
• $D=\{\langle {c,d}\rangle \in A\times A\mid \langle {c_0,d_0}\rangle \in B\land \forall \langle {p,q}\rangle \in F(c_0,d_0)\, \langle {c_1p,d_1p}\rangle \in D\}$ .
It is not difficult to see that D has a bounded inductive definition, and therefore by Theorem 2.6 is a set in $\mathsf { CZF}+\mathsf {REA}$ .
By induction on the inductive definition of I, one may show that if $\langle {\sigma ,\tau _0,B_0}\rangle \in I$ and $\langle {\sigma ,\tau _1,B_1}\rangle \in I$ , then $B_0=B_1$ . Hence, by letting
we obtain in particular that if $\langle {\sigma ,\tau ,B}\rangle \in I$ , then $B=\bigcup \{B\mid \exists \tau \, \langle {\sigma ,\tau ,B}\rangle \in I\}$ is a set, and so $\sim _{\sigma }$ is a set as well.
Lemma 4.5. Suppose $\sigma \sim \tau $ and $\tau \sim \rho $ . Then:
-
(i) $\sigma \sim \sigma $ , $\tau \sim \sigma $ , and $\sigma \sim \rho $ ;
-
(ii) $a\sim _{\sigma } b$ iff $a\sim _{\tau } b$ ;
-
(iii) $a\sim _{\sigma } b$ and $b\sim _{\sigma } c$ implies $a\sim _{\sigma } a$ , $b\sim _{\sigma } a$ , and $a\sim _{\sigma } c$ .
In other words, $\sim $ and $\sim _{\sigma }$ are partial equivalence relations on A.
Proof By induction on the (inductive definition of the) type structure. The case of $\mathrm {W}_{\sigma } i$ is dealt with a further induction on the given $\mathrm {W}$ -type.
4.2 Representing ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$
Definition 4.6. Given a type structure on A and a type $\sigma $ , we say that $i\in A$ is a family of types over $\sigma $ if $ia\sim ib$ whenever $a\sim _{\sigma } b$ . If $\sigma $ is a type and $ia\sim jb$ whenever $a\sim _{\sigma } b$ , we write $i\approx _{\sigma } j$ .
Note that in any of the type structures here considered, if i is a family of types over $\sigma $ , then ${\Pi }_{\sigma } i$ and ${\Sigma }_{\sigma } i$ are types. Moreover, if $\sigma \sim \tau $ and $i\approx _{\sigma } j$ , then $i\approx _{\tau } j$ .
Definition 4.7 (Mapping typed elements of A in $\mathrm {V_{ext}}(A)$ ).
For $n\in \omega $ , let
For every ${\Pi }{\Sigma }\mathrm {I}$ -type $\sigma $ , we inductively define $a^{\sigma }\in \mathrm {V_{ext}}(A)$ for every a of type $\sigma $ by:
-
• if $\sigma =\mathsf {N}_n$ or $\sigma =\mathsf {N}$ , let $a^{\sigma }=\dot m$ , where $a=\bar m$ ;
-
• if $\alpha ={\Pi }_{\sigma } i$ , let $ f^{\alpha }=\{\langle {a,b,\langle {a^{\sigma },(fa)^{\tau }}\rangle _{\!A}}\rangle \mid a\sim _{\sigma } b\land ia=\tau \}$ ;
-
• if $\beta ={\Sigma }_{\sigma } i$ , let $ a^{\beta }=\langle {(a_0)^{\sigma },(a_1)^{\tau }}\rangle _{\!A}$ , where $ia_0= \tau $ ;
-
• if $\gamma =\mathrm {I}_{\sigma }(a,b)$ , let $ c^{\gamma }=0 $ .
For ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -types, we add the clause:
-
• if $\delta =\mathrm {W}_{\sigma } i$ , let $c^{\delta }=\langle {a^{\sigma },\{\langle {p,q,\langle {p^{ia},(c_1p)^{\delta }}\rangle _{\!A}}\rangle \mid p\sim _{ia} q\}}\rangle _{\!A}$ , where $a=c_0$ .
Remark 4.8. A comment on the above definition may be in order. The class function $(\sigma ,a)\mapsto a^{\sigma }$ is obtained by defining a class E of pairs $\langle {\sigma ,e_{\sigma }}\rangle $ , the intended meaning of which is $e_{\sigma }=\{\langle {a,a^{\sigma }}\rangle \mid a\in A_{\sigma }\}$ , where $A_{\sigma }=\{a\in A\mid a\text { has type } \sigma \}$ . Note that $A_{\sigma }$ is a set. Hence, $a^{\sigma }$ is really $e_{\sigma }(a)$ . For example, the rules for ${\Sigma }$ -types and $\mathrm {W}$ -types are
where $\sigma $ is type, i is a family of types over $\sigma $ , and there exist functions $e_{\sigma }$ and f on $A_{\sigma }$ such that:
-
• $\operatorname {{\mathrm {Fun}}}(f(a))\land \operatorname {{\mathrm {dom}}}(f(a))=A_{ia}$ , for every $a\in A_{\sigma }$ ,
-
• $X=\{\langle {\sigma ,e_{\sigma }}\rangle \}\cup \{\langle {ia,f(a)}\rangle \mid a\in A_{\sigma }\}$ ,
-
• $e_{\beta }=\{\langle {a,\langle {e_{\sigma }(a_0),f(a_0,a_1)}\rangle _{\!A}}\rangle \mid a\text { has type } {\Sigma }_{\sigma } i\}$ ,
and $e_{\delta }$ is inductively defined by the clause:
-
• if c has type $\mathrm {W}_{\sigma } i$ and there exists a function k with $\operatorname {{\mathrm {dom}}}(k)=A_{ic_0}$ such that $\langle {c_1p,k(p)}\rangle \in e_{\delta }$ for every $p\in \operatorname {{\mathrm {dom}}}(k)$ , then
$$\begin{align*}\langle{c,\langle{e_{\sigma}(c_0),\{\langle{p,q,\langle{f(c_0,p), k(p)}\rangle_{\!A}}\rangle\mid p\sim_{ic_0} q\}}\rangle_{\!A}}\rangle \in e_{\delta}. \end{align*}$$
By induction on the inductive definition of E, one shows that E is a class function on $\mathbb {T}$ , and $E(\sigma )=e_{\sigma }\colon A_{\sigma }\to \mathrm {V_{ext}}(A)$ , for every type $\sigma $ . Note that $e_{\delta }$ has a bounded inductive definition and so is a set in $\mathsf {CZF}+\mathsf {REA}$ .
Definition 4.9 (Canonical ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -sets in $\mathrm {V_{ext}}(A)$ ).
Given a type $\sigma $ and a family i of types over $\sigma $ , we define sets $X_{\sigma }, F_{\sigma ,i}\in \mathrm {V_{ext}}(A)$ by:
-
• $X_{\sigma }=\{\langle {a,b,a^{\sigma }}\rangle \mid a \sim _{\sigma } b\}$ ;
-
• $F_{\sigma ,i}=\{\langle {a,b,\langle {a^{\sigma },X_{\tau }}\rangle _{\!A}}\rangle \mid a\sim _{\sigma } b\land ia= \tau \}$ .
Remark 4.10. The set $X_{\mathsf {N}_n}=\dot n$ is the canonical name for $n\in \omega $ , and $X_{\mathsf {N}}=\dot \omega =\{\langle {\bar n,\bar n, \dot n}\rangle \mid n\in \omega \}$ is the canonical name for $\omega $ .
Lemma 4.11 (Absoluteness and uniqueness up to extensional equality).
Let $\sigma \sim \tau $ and $a,b$ of type $\sigma $ . Then:
-
• $\Vdash a^{\sigma }=b^{\tau }$ implies $a\sim _{\sigma } b$ ;
-
• $a\sim _{\sigma } b$ implies $a^{\sigma }=b^{\tau }$ .
Proof By induction on the (inductive definition of the) type structure. The cases $\sigma =\tau =\mathsf {N}_n$ and $\sigma =\tau =\mathsf {N}$ are straightforward.
Let $\alpha ={\Pi }_{\sigma } i\sim {\Pi }_{\tau } j=\gamma $ and $f,g\in A_{\alpha }$ . Recall that:
Suppose $\Vdash f^{\alpha }=g^{\gamma }$ . Let us show that $f\sim _{\alpha } g$ . Let $a\sim _{\sigma } b$ . We want to prove $fa\sim _{\rho } gb$ , where $\rho =ia$ . By definition of realizability, we have that
for some $\breve {a}\in A_{\tau }$ , where $\eta =j\breve {a}$ . Then $\Vdash a^{\sigma }=\breve a^{\tau }$ and $\Vdash (fa)^{\rho }=(g\breve a)^{\eta }$ . By induction, $a\sim _{\sigma } \breve a$ and $fa\sim _{\rho } g\breve a$ . By Lemma 4.5, $\breve a\sim _{\sigma } b$ . Hence, $\breve a\sim _{\tau } b$ , and therefore $g\breve a\sim _{\eta } gb$ . Since $i\approx _{\sigma } j$ , it also follows from $a\sim _{\sigma } \breve a$ that $\rho \sim \eta $ . Thus $g\breve a\sim _{\rho } gb$ . By transitivity, $fa\sim _{\rho } gb$ .
Now suppose $f\sim _{\alpha } g$ . We wish to show that $f^{\alpha }=g^{\gamma }$ . Since $\sigma \sim \tau $ , it suffices to show that if $a\in A_{\sigma }$ , then $a^{\sigma }=a^{\tau }$ and $(fa)^{ia}=(ga)^{ja}$ . This follows by induction since $\sigma \sim \tau $ , $a\sim _{\sigma } a$ , $ia\sim ja$ , and $fa\sim _{ia} ga$ .
The cases ${\Sigma }_{\sigma } i$ , $\mathrm {I}_{\sigma }(a,b)$ and $\mathrm {W}_{\sigma } i$ are left as an exercise.
By virtue of Lemmas 4.5 and 4.11, every $X_{\sigma }$ is injectively presented in the following sense.
Definition 4.12. A set $x\in \mathrm {V_{ext}}(A)$ is injectively presented if
where $\sim $ is a partial equivalence relation on A and f is a (definable) function from the domain of $\sim $ to $\mathrm {V_{ext}}(A)$ such that:
-
• $\Vdash f(a)=f(b)$ implies $a\sim b$ ;
-
• $a\sim b$ implies $f(a)=f(b)$ .
This property will ensure the validity of choice for names of the form $X_{\sigma }$ (see Theorem 4.17).
Lemma 4.13. Let $\sigma \sim \tau $ and $i\approx _{\sigma } j$ . Then $X_{\sigma }=X_{\tau }$ and $F_{\sigma ,i}=F_{\tau ,j}$ .
Proof By Lemma 4.11.
Theorem 4.14. There are closed terms such that:
where $\sigma $ is a type, i is a family of types over $\sigma $ , and $a,b$ have type $\sigma $ .
Remark 4.15. $\mathsf {CZF}$ proves (i)–(v) for ${\Pi }{\Sigma }\mathrm {I}$ -types. $\mathsf {CZF}+\mathsf {REA}$ proves (i)–(vi) for ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -types.
Theorem 4.16. There are closed terms $\mathbf i$ and ${\mathbf e}$ such that:
for every $X\in \mathrm {V_{ext}}(A)$ . The same for ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ .
4.3 Realizing choice
Theorem 4.17 ( $\mathsf {AC}_{\sigma ,\tau }$ ).
There is a closed term ${\mathbf e}$ such that $\mathsf {CZF}$ proves
for all ${\Pi }{\Sigma }\mathrm {I}$ -types $\sigma ,\tau $ and for every formula $\varphi $ . The same for $\mathsf {CZF}+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -types.
Proof Suppose $c=d\Vdash \forall x\in X_{\sigma }\, \exists y\in X_{\tau }\, \varphi (x,y)$ . Then, whenever $a\sim _{\sigma } b$ , we have $(ca)_0\sim _{\tau } (db)_0$ and $(ca)_1=(db)_1\Vdash \varphi (a^{\sigma },e^{\tau })$ , where $e=(ca)_0$ . Let
Then $f\in \mathrm {V_{ext}}(A)$ . We wish to find ${\mathbf e}$ such that
It suffices to look for closed terms $\mathbf {r},\mathbf {c},\mathbf {f}$ such that:
where $f\subseteq X_{\sigma }\times X_{\tau }$ stands for $\forall z\in f\, \exists x\in X_{\sigma }\, \exists y\in X_{\tau }\, \operatorname {{\mathrm {OP}}}(z,x,y)$ , and f is functional stands for
(1) and (2) are straightforward. (3) Let $a\sim _{\sigma } b$ and $\breve a\sim _{\sigma } \breve b$ . We want
for all $x,y_0,y_1\in \mathrm {V_{ext}}(A)$ , where $e=(ca)_0$ and $\breve e=(c\breve a)_0$ . Suppose
In particular, $\Vdash a^{\sigma }=\breve a^{\sigma }$ . By Lemma 4.11, $a\sim _{\sigma } \breve a$ . By Lemma 4.5, since $(ca)_0\sim _{\tau } (da)_0$ and $(c\breve a)_0\sim _{\tau } (da)_0$ , it follows that $(ca)_0\sim _{\tau } (c\breve a)_0$ . That is, $e\sim _{\tau } \breve e$ . By Lemma 4.11 again, we get $e^{\tau }=\breve e^{\tau }$ . By the properties of equality, there is a closed term $\mathbf q$ such that $\mathbf q\breve c=\mathbf q\breve d\Vdash y_0=y_1$ . We may let $\mathbf f=_{\mathrm {def}}\lambda ca\breve a\breve c. \mathbf q\breve c$ .
Theorem 4.18 ( $\mathsf {RDC}_{\sigma }$ ).
There is a closed term ${\mathbf e}$ such that $\mathsf {CZF}$ proves
for every ${\Pi }{\Sigma }\mathrm {I}$ -type $\sigma $ and for every formula $\varphi $ . The same for $\mathsf {CZF}+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -types.
Proof Suppose
$\mathring a\sim _{\sigma } \mathring b$ and $\mathring c=\mathring d\Vdash \psi (a^{\sigma })$ . We search for ${\mathbf e}$ such that
By (1), whenever $a\sim _{\sigma } b$ and $\breve c=\breve d\Vdash \psi (a^{\sigma })$ , we have
In every pca one can simulate primitive recursion. We thus have a closed term $\mathbf r$ satisfying the following equations, where r is an abbreviation for $\mathbf rc\mathring a\mathring c$ :
By induction, owing to (2) and (3), one can verify that for every $n\in \omega $ ,
Note that $\mathring a=(\mathbf rc\mathring a\mathring c \mathbf 0)_0\sim _{\sigma } (\mathbf rd\mathring b\mathring d \mathbf 0)_0=\mathring b$ , and $\mathring c=(\mathbf rc\mathring a\mathring c \mathbf 0)_{10}= (\mathbf rd\mathring b\mathring d \bar 0)_{10}=\mathring d \Vdash \psi (\mathring a^{\sigma })$ . Let
Then $f\in \mathrm {V_{ext}}(A)$ . By using $\mathbf r$ , it is not difficult to build ${\mathbf e}$ such that
Theorem 4.19. There is a closed term $\mathbf c$ such that $\mathsf {CZF}$ proves $\mathbf c\Vdash \chi $ , for every instance $\chi $ of ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }$ . The same for ${\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ . Similarly, there is a closed term $\mathbf c$ such that $\mathsf {CZF}+\mathsf {REA}$ proves $\mathbf c\Vdash \chi $ , for every instance $\chi $ of ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}^{\dagger }$ . The same for ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ .
Corollary 4.20. It thus follows by Theorem 3.19 that:
-
(i) $T\models T+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf { RDC}^{\dagger }$ ,
-
(ii) $T+\mathsf {REA}\models T+\mathsf {REA}+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf { AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ ,
for every theory T obtained by appending to either $\mathsf {CZF}$ or $\mathsf {IZF}$ some or all of the axioms $\mathsf { AC}_{\omega }$ , $\mathsf {DC}$ , $\mathsf {DC}^{\dagger }$ , $\mathsf {RDC}$ , $\mathsf {RDC}^{\dagger }$ , and $\mathsf {PAx}$ .
4.4 Failure of presentation
The interpretations of $\mathsf {CZF}$ and $\mathsf {CZF}+\mathsf {REA}$ in type theory validate strong presentation axioms (see Section 2.5). It is natural to ask whether extensional generic realizability validates the statement that every set is an image of a ${\Pi }{\Sigma }\mathrm {I}$ -set, even under the assumption that this holds in the background universe. If it did, in view of Theorems 2.16 and 4.19, we would obtain that $T+\text {every set is an image of a } {\Pi }{\Sigma }\mathrm {I}\text {-set} \models {\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {PAx}$ , and similarly for $T+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -sets. However, the answer is negative.
Theorem 4.21. The following holds.
Similarly for $\mathsf {CZF}+\mathsf {REA}$ and ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -sets.
Proof Let $y=\{\langle {\mathbf 0,\mathbf 0,\dot 0}\rangle ,\langle {\mathbf 0,\mathbf 0,\dot 1}\rangle \}\in \mathrm {V_{ext}}(A)$ . Although y is in bijection with $2=\{0,1\}$ , this fact is not realizable. The proof is the same in both cases. Let us consider the ${\Pi }{\Sigma }\mathrm {I}$ case and show that
Towards a contradiction, suppose $\Vdash X\in {\Pi }{\Sigma }\mathrm {I}\land f\colon X \twoheadrightarrow y$ , for some $X,f\in \mathrm {V_{ext}}(A)$ . By soundness and Theorem 4.16, there is a ${\Pi }{\Sigma }\mathrm {I}$ -type $\sigma $ such that $\Vdash f\colon X_{\sigma } \twoheadrightarrow y$ . In particular, there are $a,b$ such that
By unpacking the definition, we must have $\breve a= (a\mathbf 0)_0\sim _{\sigma }(b\mathbf 0)_0=\breve b$ and
where $x=\breve a^{\sigma }$ . From $\Vdash \operatorname {{\mathrm {Fun}}}(f)$ , we then obtain $\Vdash \dot 0=\dot 1$ , which implies $0=1$ , for the desired contradiction.
5 Far beyond Goodman’s theorem
Goodman [Reference Goodman18, Reference Goodman19] proved that intuitionistic finite type arithmetic $\mathsf {HA}^{\omega }$ augmented with the axiom of choice in all finite types $\mathsf {AC}_{\mathsf {FT}}$ is conservative over $\mathsf {HA}$ . This still holds in the presence of extensionality, that is, $\mathsf {HA}^{\omega }+\mathsf {EXT}+\mathsf {AC_{\mathsf {FT}}}$ is conservative over $\mathsf {HA}$ (cf. [Reference Beeson6, Reference Beeson7]). Since $\mathsf {HA}^{\omega }$ and $\mathsf {HA}^{\omega } +\mathsf {EXT}$ are easily seen to be conservative over $\mathsf{HA}$ (via the models ${\mathsf{HRO}}$ and $\mathsf {HEO}$ respectively; cf. [Reference Troelstra32]), Goodman’s theorem is the prototypical example of arithmetical conservativity of (some) choice over a given theory T. Goodman-type results have been proved for a variety of set theories and choice principles at finite types. Write $T=_{arith}S$ to convey that T and S prove the same arithmetic sentences.
Theorem 5.1. This much (as a minimum) is known:
-
• $T =_{arith}T+\mathsf {CAC}_{\mathsf {FT}}+{\mathsf {DC}}_{\mathsf {FT}}$ for $T=\mathsf {IZF}$ and extensions of $\mathsf {IZF}$ by large set axioms; see [Reference Friedman and Ščedrov15, Theorem 5.1];
-
• $T =_{arith}T+\mathsf {AC}_{\mathsf {FT}}$ for $T=\mathsf {CZF}$ and fragments thereof; see [Reference Gordeev20, p. 25].
We are going to further extend such results and in particular make good on the claim in [Reference Frittaion and Rathjen17] that extensional realizability may be used to show arithmetical conservativity of $\mathsf {AC}_{\mathsf {FT}}$ over $\mathsf {IZF}$ (as well as $\mathsf {CZF}$ ).
Theorem 5.2. Let T be any of the theories obtained by appending to either $\mathsf {CZF}$ or $\mathsf {IZF}$ some or all of the axioms $\mathsf { AC}_{\omega }$ , $\mathsf {DC}$ , $\mathsf {DC}^{\dagger }$ , $\mathsf {RDC}$ , $\mathsf {RDC}^{\dagger }$ , and $\mathsf {PAx}$ . Then:
-
• $T =_{arith}T+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {RDC}^{\dagger } $ ;
-
• $T +\mathsf {REA} =_{arith}T+\mathsf {REA}+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}^{\dagger }+ {\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ .
One can allow type $1$ parameters. Namely, we have conservativity for sentences of the form
where $\varphi $ is arithmetic (relative to $f_1,\ldots ,f_n$ ).
Remark 5.3. Of course, some of the theories to the left reduce to $T+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }$ and $T+\mathsf { REA}+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}^{\dagger }$ respectively.
Friedman and Ščedrov’s [Reference Friedman and Ščedrov15] versions of generic realizability and forcing only work for set theories without extensionality. We show how to adapt the argument to an extensional setting. Definition 5.4 fully specifies our forcing relation. It is a routine although tedious matter to check all the details. By the way, one should also prove that every theory T as above is self-validating with respect to forcing. This is not difficult to see.
It is convenient to work in a conservative extension S of T obtained by adding the constant symbol $\omega $ and an axiom saying that $\omega $ is the set of natural numbers.Footnote 7 Now, we can clearly identify number quantifiers with bounded quantifiers of the form $\forall x\in \omega $ and $\exists x\in \omega $ . On the other hand, every primitive recursive number-theoretic function and hence relation is canonically definable by a $\Sigma $ formula in the language of set theory (with just $\in $ as primitive).Footnote 8 We call such formulas primitive recursive. Kleene’s T-predicate $T(e,x,z)$ and the function $U(z)$ are among them. We then say that a formula is arithmetic if it is built up from primitive recursive formulas by using $\land $ , $\lor $ , $\neg $ , $\rightarrow $ , and number quantifiers $\forall x\in \omega $ and $\exists x\in \omega $ .
Proof of Theorem 5.2
We first consider the case without parameters. The goal is to show that for every arithmetic sentence $\varphi $ of S,
-
• if $S+\Phi \vdash \varphi $ , then $S\vdash \varphi $ ,
-
• if $S+\mathsf {REA}+\Psi \vdash \varphi $ , then $S+\mathsf {REA}\vdash \varphi $ ,
where $\Phi ={\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {I}\text {-}\mathsf {RDC}^{\dagger }$ and $\Psi ={\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf {AC}^{\dagger }+{\Pi }{\Sigma }\mathrm {W}\mathrm {I}\text {-}\mathsf { RDC}^{\dagger }$ .
Step 1. Let $S^g$ be the theory obtained from S by adjoining a new constant symbol g and an axiom saying the g is a partial function from $\omega $ to $\omega $ . Within $S^g$ , one can define extensional generic realizability $a=b\Vdash _{\omega } \varphi $ , where $a,b\in \omega $ and $\varphi $ is a formula of T with parameters in $\mathrm {V_{ext}}(\omega )$ , by using partial recursive application relative to the generic oracle g. To be precise, we use Kleene’s relativized T-predicate $T(e,x,z,f)$ , where f is a partial function from $\omega $ to $\omega $ . So, for example, the clause for implication reads as follows:
For $\land $ and $\lor $ , we may use a primitive recursive pairing function $(n,m)$ on natural numbers with primitive recursive projections $(n)_0$ and $(n)_1$ . So, for example, we let
One can lift the realizability interpretation to every formula $\varphi $ of S by interpreting $\omega $ with $\dot \omega \in \mathrm {V_{ext}}(\omega )$ . Here, $\dot \omega =\{\langle {n,n,\dot n}\rangle \mid n\in \omega \}$ , where $\dot n=\{\langle {m,m,\dot m}\rangle \mid m\in n\}$ .
One proves that
Similarly for $S+\mathsf {REA}+\Psi $ and $(S+\mathsf {REA})^g$ . This concludes the realizability part.
Step 2. Next, within S, given any definable set $\mathbb {P}$ of partial functions from $\omega $ to $\omega $ such that $0\in \mathbb {P}$ , one defines a forcing interpretation $p\Vdash _{\mathbb {P}} \varphi $ , where $p\in \mathbb {P}$ and $\varphi $ is a formula of T with parameters in $\mathrm {V}(\mathbb {P})$ . The universe $\mathrm {V}(\mathbb {P})$ is inductively defined by the clause:
-
• if $x\subseteq \mathbb {P}\times \mathrm {V}(\mathbb {P})$ and $\langle {q,z}\rangle \in x$ whenever $\langle {p,z}\rangle \in x$ with $q\supseteq p$ , then $x\in \mathrm {V}(\mathbb {P})$ .
In $\mathrm {V}(\mathbb {P})$ , we have a canonical name $\mathring g$ for the generic g defined as
where $\check n=\{\langle {p,\check m}\rangle \mid p\in \mathbb {P}\land m\in n\}$ , and $\langle {x,y}\rangle _{\mathbb {P}}$ is some suitable pairing function in $\mathrm {V}(\mathbb {P})$ . In particular, every natural number $n\in \omega $ has a canonical name $\check n$ in $\mathrm {V}(\mathbb {P})$ . A canonical name $\check \omega $ for $\omega $ is given by $ \check \omega =\{\langle {p,\check n}\rangle \mid p\in \mathbb {P}\land n\in \omega \}$ .
One can then extend the forcing interpretation $p\Vdash _{\mathbb {P}} \varphi $ to formulas of $S^g$ by interpreting g with $\mathring g$ and $\omega $ with $\check \omega $ . The basic idea however is that $p\Vdash _{\mathbb {P}} g(\check n)=\check m$ iff $\langle {n,m}\rangle \in p$ . Moreover,
-
• if $\{e\}^p(a)\simeq b$ , then $p\Vdash \{\check e\}^g(\check a)\simeq \check b$ ,
-
• if $p\Vdash \{\check e\}^g(\check a)\simeq \check b$ , then for every $q\supseteq p$ , there is an $r\supseteq q$ such that $\{e\}^r(a)\simeq b$ .
Then one shows that
Similarly for $S^g+\mathsf {REA}$ and $S+\mathsf {REA}$ . In particular, we must have that
Moreover, forcing is absolute for arithmetic sentences, namely,
for every arithmetic sentence $\varphi $ of S. This is the forcing part.
Finally, one shows that if $\varphi $ is an arithmetic sentence, then there exists a forcing notion $\mathbb {P}$ such that
Step 3. By putting all together, the arguments run as follows. If $S+\Phi \vdash \varphi $ , with $\varphi $ arithmetic, let $\mathbb {P}$ be as in (4). By (1), $S^g\vdash \exists e\in \omega \, (e\Vdash _{\omega }\varphi )$ . By (2), $S\vdash \forall p\, \exists q\supseteq p\, (q\Vdash _{\mathbb {P}} \exists e\in \omega \, (e\Vdash _{\omega }\varphi ))$ . We now reason in S. By the soundness of forcing and (4), we can find $p\in \mathbb {P}$ such that $p\Vdash _{\mathbb {P}} \varphi $ . By (3), we finally obtain $\varphi $ .
Definition 5.4 (Forcing).
We define the relation $p\Vdash _{\mathbb {P}} \varphi $ , where $p\in \mathbb {P}$ and $\varphi $ is a formula of T with parameters in $\mathrm {V}(\mathbb {P})$ . The atomic cases are defined by transfinite recursion.
Forcing is monotone, that is, if $p\Vdash _{\mathbb {P}} \varphi $ and $q\supseteq p$ , then $q\Vdash _{\mathbb {P}} \varphi $ .
All the ingredients are in place to carry out a proof of (1)–(4). Here we give some clues.
On absoluteness
For every set x, define by transfinite recursion the name $\check x\in \mathrm {V}(\mathbb {P})$ by $\check x=\{\langle {p,\check y}\rangle \mid p\in \mathbb {P} \land y\in x\}$ . We set out to prove that for every arithmetic formula $\varphi (x_1,\ldots ,x_n)$ ,
The absoluteness of arithmetic sentences in the sense of (3) then follows.
It is an easy exercise to show that (5) is preserved under logical connectives and number quantifiers. It is thus sufficient to show that for every primitive recursive function $f(x_1,\ldots ,x_n)$ , the primitive recursive formula $\varphi _f(x_1,\ldots ,x_n,y)$ defining f satisfies (5). This is proved by (an external) induction on the generation of f.
For example, suppose $f(x_1,\ldots ,x_n,x)$ is defined by primitive recursion from $g(x_1,\ldots ,x_n)$ and $h(x_1,\ldots ,x_n,x,y)$ , namely,
Define $\varphi _f(x_1,\ldots ,x_n,x,y)$ as $\exists z\, (\psi (z) \land z(x)=y)$ , where $\psi (z)$ is
(Note that $\varphi _f$ is equivalent to a $\Sigma $ formula if $\varphi _g$ and $\varphi _h$ are also $\Sigma $ definable.) One shows that (5) holds for $\varphi _f(x_1,\ldots ,x_n,x,y)$ , by assuming that it holds for $\varphi _g$ and $\varphi _h$ . The left-to-right direction of (5) requires some standard absoluteness arguments. For the right-to-left direction, one also uses the fact that, for every primitive recursive function $f(x_1,\ldots ,x_n)$ ,
and thereby this is forced in S.
On forcing self-realizability
To obtain (4), one shows that for every arithmetic formula $\varphi (x_1,\ldots ,x_n)$ there is a $\mathbb {P}$ such that S proves:
-
(i) there is $e\in \omega $ such that for every p there is a $q\supseteq p$ forcing
$$ \begin{align*} & \forall a_1\in\omega\cdots\forall a_n\in\omega\, (\varphi(a_1,\ldots,a_n)\rightarrow \\ & \qquad\qquad\qquad \exists b\in\omega\, (\{\check e\}^g(a_1,\ldots,a_n,0)=b\land b\Vdash_{\omega} \varphi(\dot a_1,\ldots,\dot a_n))); \end{align*} $$ -
(ii) for every p there is a $q\supseteq p$ forcing
$$\begin{align*}\forall a_1\in\omega\cdots\forall a_n\in\omega\, \forall a,b\in\omega\, ((a=b\Vdash_{\omega} \varphi(\dot a_1,\ldots,\dot a_n))\rightarrow \varphi(a_1,\ldots,a_n)). \end{align*}$$
Here, $\{e\}^f(a,b)$ stands for $\{\{e\}^f(a)\}^f(b)$ , and so on and so forth. On a technical note, the dummy argument for $0$ is used to handle the case where $\varphi $ is closed.
Now, let $\varphi (x_1,\ldots ,x_n)$ be arithmetic. We define $\mathbb {P}$ as follows. First, let $\mathbb {Q}$ be the set of partial functions p from $\omega $ to $\omega $ such that $\operatorname {{\mathrm {dom}}}(p)$ is an image of a natural number. The point of this definition is just to make sure that, within $\mathsf {CZF}$ , the class $\mathbb {Q}$ exists as a set and the domain of every $p\in \mathbb {Q}$ is decidable, in the sense that
Note that if we are working in $\mathsf {IZF}$ , we can directly define the set $\mathbb {Q}$ of all partial functions from $\omega $ to $\omega $ with decidable domain. Enumerate all subformulas $\varphi _1,\ldots ,\varphi _k$ of $\varphi $ starting from the primitive recursive ones. Let $\mathbb {P}$ be the set of $p\in \mathbb {Q}$ such that for every subformula $\varphi _i(y_1,\ldots , y_{j}) $ of the form $\psi _0\lor \psi _1$ , for every $a_1,\ldots ,a_j\in \omega $ , if $a=(i,a_1,\ldots ,a_j)\in \operatorname {{\mathrm {dom}}}(p)$ , then $p(a)=0\land \psi _0(a_1,\ldots ,a_j)$ or $p(a)=1\land \psi _0(a_1,\ldots ,a_j)$ , and for every subformula $\varphi _i(y_1,\ldots ,y_j)$ of the form $\exists x\, \psi (x,y_1,\ldots ,y_j)$ , for every $a_1,\ldots ,a_j\in \omega $ , if $a=(i,a_1,\ldots ,a_j)\in \operatorname {{\mathrm {dom}}}(p)$ , then $\psi (p(a),a_1,\ldots ,a_j)$ .
One can write down a formula defining $\mathbb {P}$ as there are standard finitely many subformulas of $\varphi $ . Here, $(a_1,\ldots ,a_j)$ is a primitive recursive coding of sequences of natural numbers. One then shows (i) and (ii) for every subformula of $\varphi $ .
If $\varphi $ is primitive recursive, then one can find a number e such that
where we identify e with the corresponding numeral. This fact can be gleaned from [Reference McCarty22, Chapter 4, Theorem 2.6] in the case of $\mathsf {IZF}$ . The same holds for $\mathsf {CZF}$ [Reference Rathjen30, Proposition 8.5]. We can then use the soundness of forcing to get (i) and (ii).
The index of complex subformulas is computed according to the following table. Let i be the number of the given subformula according to our enumeration. Write $\vec {a}$ for the tuple $a_1,\ldots ,a_j$ .
By way of example, let us illustrate how to obtain (i) in the existential case. For simplicity, suppose we have a subformula of the form $\exists y\in \omega \, \varphi (x,y)$ . We work in S. We have already found an index $e_{\varphi }$ for $\varphi $ . So, let e be such that
Let $p\in \mathbb {P}$ . We search for a $q\supseteq p$ such that
Notice that, within $S^g$ ,
and thereby this is forced in S. It is then enough to find an extension $q\supseteq p$ such that
We claim that p already satisfies (1). Let $a\in \omega $ , $q\supseteq p$ , and suppose $q\Vdash _{\mathbb {P}} \exists y\in \omega \, \varphi (\check a,y)$ . We are clear if we find $r\supseteq q$ such that
where the formula $i(x,y)$ expresses that $y=\dot x$ for $x\in \omega $ . By definition, there is a $b\in \omega $ such that $q\Vdash _{\mathbb {P}} \varphi (\check a,\check b)$ . By absoluteness, $\varphi (a,b)$ holds. Now, we can decide whether $(i,a)\in \operatorname {{\mathrm {dom}}}(q)$ . If not, we can take $q'=q\cup \{\langle {(i,a),b}\rangle \}$ . By the assumption on $e_{\varphi }$ , there is an $s\supseteq q'$ such that
One can see that $s\Vdash _{\mathbb {P}} \{\check e\}^g(\check a,0)\simeq (\check b,\{\check e_{\varphi }\}^g(\check a,\check b,0))$ . By (3) and soundness, one can finally find an $r\supseteq s$ satisfying (2), as desired.
Adding parameters
We briefly discuss how to generalize such conservation result to arithmetic formulas with type $1$ parameters. For example, suppose $S+\Phi \vdash \forall f\in \omega ^{\omega }\, \varphi (f)$ . Then $(S+\Phi )_f\vdash \varphi (f)$ , where, in general, $T_f$ is obtained from T by adjoining a constant symbol f and an axiom saying that f is a function from $\omega $ to $\omega $ . It clearly suffices to show that $S_f\vdash \varphi (f)$ . If we do so, then $S\vdash \forall f\in \omega ^{\omega }\, \varphi (f)$
Now consider the theory $(S_f)^g$ obtained from $S_f$ by further extending the language with a constant symbol g and an axiom saying that g is a partial function from $\omega $ to $\omega $ . Within $(S_f)^g$ , consider extensional generic realizability $a=b\Vdash _{\omega } \varphi $ , where $a,b\in \omega $ and $\varphi $ is a formula of $S_f$ , by using partial recursive application relative to the oracle $f\oplus g=\{\langle {2n,f(n)}\rangle \mid n\in \omega \}\cup \{\langle {2n+1,g(n)}\rangle \mid n\in \operatorname {{\mathrm {dom}}}(g)\}$ . Use the name $\dot f=\{\langle {n,n,\langle {\dot n,\dot m}\rangle _{\omega }}\rangle \mid f(n)=m\}\in \mathrm {V_{ext}}(\omega )$ to define realizability on formulas containing f. Note that we could extend the interpretation to every formula of $(S_f)^g$ by interpreting g with $\dot g$ , which is defined in a similar way as $\dot f$ . Show that
Similarly for $(S+\mathsf {REA}+\Psi )_f$ and $(S_f+\mathsf {REA})^g$ . In particular, we must have
This is the realizability part.
In $S_f$ , given any definable set $\mathbb {P}$ of partial functions from $\omega $ to $\omega $ , where now we can use the parameter f in defining $\mathbb {P}$ , we extend the forcing interpretation $p\Vdash _{\mathbb {P}} \varphi $ of Definition 5.4 to formulas of $(S_f)^g$ by interpreting g with $\mathring g$ , like before, and f with $\check f$ . Note that $\check f=\{\langle {p,\check z}\rangle \mid p\in \mathbb {P}\land z\in f\}=\{\langle {p,\langle {\check n,\check m}\rangle _{\mathbb {P}}}\rangle \mid p\in \mathbb {P}\land f(n)=m\}$ . The rest of the argument is roughly as before, but with everything relativized to the parameter f. In particular, one must show that arithmetic (in f) formulas are absolute for forcing. Finally, given $\varphi (f)$ , one defines $\mathbb {P}$ as before, but relative to f, and show that in $\mathrm {V}(\mathbb {P})$ , $\varphi (f)$ is self-realizing.⊣
6 Appendix
The proofs of Theorems 4.14 and 4.16 will rely on the following two facts.
Theorem 6.1 ( $\mathsf {CZF}$ ).
There is a formula $\vartheta (u,Y)$ , such that
where
with $\psi (u,X,F)$ being a shorthand for
Similarly, there is a formula $\vartheta ^*(u,Y)$ , such that
where $\vartheta ^*_i$ for $i=0,\ldots ,4$ is defined in a similar fashion as $\vartheta _i$ , and
Theorem 6.2 ( $\mathsf {CZF}+\mathsf {REA}$ ).
If F is a function with domain X, then for every set Y,
Proof of Theorem 4.14
From now on, let
(i) A closed term $\mathbf o$ such that $\mathbf o\Vdash X_{\mathsf {N}}=\omega $ is given in the proof of Theorem 3.16. In fact, the set $X_{\mathsf {N}}=\dot \omega $ is the canonical name for $\omega $ used to realize infinity.
(ii) We aim for $\mathbf {fun}\Vdash \operatorname {{\mathrm {Fun}}}(F)\land \operatorname {{\mathrm {dom}}}(F) = X_{\sigma }$ . It suffices to look for closed terms $\mathbf r,\mathbf f, {\mathbf t}$ such that:
We can easily arrange for $\mathbf r$ and ${\mathbf t}$ . Let us find $\mathbf f$ . By unraveling the definition, we want $\mathbf f$ such that, if $a\sim _{\sigma } b $ , $\breve a\sim _{\sigma } \breve b$ and
where $ia=\tau $ and $i\breve a=\breve \tau $ , then $\mathbf fa\breve ac=\mathbf fb\breve bd\Vdash y_0=y_1$ . By the properties of pairing, from c and d as above we get $\Vdash a^{\sigma }=\breve a^{\sigma }$ . By Lemma 4.11, we must have $a\sim _{\sigma } \breve a$ . Since i is a family of types over $\sigma $ , $ia\sim i\breve a$ . That is, $\tau \sim \breve \tau $ . By Lemma 4.13, $X_{\tau }=X_{\breve \tau }$ . As in the proof of Theorem 4.17, by the properties of equality, there is a closed term $\mathbf q$ such that $\mathbf q c=\mathbf q d\Vdash y_0=y_1$ . We may let $\mathbf f=_{\mathrm {def}}\lambda a\breve ac. \mathbf q c$ .
(iii) We aim for $\mathbf {prod}\Vdash X_{{\Pi }_{\sigma } i}={\Pi }(X_{\sigma }, F)$ . We abbreviate
Let $\alpha ={\Pi }_{\sigma } i$ . For the direction left to right, it suffices to look for closed terms $\mathbf r$ , ${\mathbf t}$ , and $\mathbf f$ such that whenever $f\sim _{\alpha } g$ , then
For the direction right to left, we look for a closed term $\mathbf c$ such that, for every $h\in \mathrm {V_{ext}}(A)$ , if $c=d\Vdash \vartheta _r(h,X_{\sigma },F)\land \vartheta _t(X_{\sigma },h)\land \vartheta _f(h)$ , then $\mathbf c c=\mathbf c d\Vdash h\in X_{{\Pi }_{\sigma } i}$ .
Let us start with the forward direction.
(1) Let $f\sim _{\alpha } g$ , $a\sim _{\sigma } b$ , $ia=\tau $ , and $fa=e$ . We want
We let $(\mathbf rfa)_0=a$ and set out for
We let $(\mathbf rfa)_{10}=a$ , $Y=X_{\tau }$ and set out for
Let $(\mathbf rfa)_{110}=(\mathbf rfa)_{1110}={\mathbf v}$ , where ${\mathbf v}\Vdash \operatorname {{\mathrm {OP}}}(\langle {x,y}\rangle _{\!A},x,y)$ exists by Lemma 3.15. Let $(\mathbf rfa)_{1111}=\mathbf p(ca)\mathbf i$ , where $\mathbf i\Vdash \forall x\, (x=x)$ . Then $\langle {fa,gb,e^{\tau }}\rangle \in X_{\tau }$ and
is as desired.
(2) Exercise.
(3) Let $f\sim _{\alpha } g$ . Let $a_j\sim _{\sigma } b_j$ , $ia_j=\tau _j$ , and $fa_j=e_j$ for $j=0,1$ . We wish to find $\mathbf f$ such that, if $c=d\Vdash \operatorname {{\mathrm {OP}}}(\langle {a_0^{\sigma },e_0^{\tau _0}}\rangle _{\!A},x,y_0)\land \operatorname {{\mathrm {OP}}}(\langle {a_1^{\sigma },e_1^{\tau _1}}\rangle _{\!A},x,y_1)$ , then $\mathbf ffa_0a_1c=\mathbf fgb_0b_1d\Vdash y_0=y_1$ , for all $x,y_0,y_1\in \mathrm {V_{ext}}(A)$ . Suppose we have c and d as above. Then in particular $\Vdash a_0^{\sigma }=a_1^{\sigma }$ . By Lemma 4.11, it follows that $a_0\sim _{\sigma } a_1$ , and hence $\tau _0\sim \tau _1$ and $e_0\sim _{\tau _0} e_1$ . Thus by Lemma 4.11 again, $y=e_0^{\tau _0}=e_1^{\tau _1}$ . Then $c=d\Vdash \operatorname {{\mathrm {OP}}}(\langle {a_0^{\sigma },y}\rangle _{\!A},x,y_0)\land \operatorname {{\mathrm {OP}}}(\langle {a_1^{\sigma },y}\rangle _{\!A},x,y_1)$ . By soundness and the properties of pairing, $\mathbf q c=\mathbf qd\Vdash y_0=y_1$ , for some closed term $\mathbf q$ . Thus $\mathbf f=_{\mathrm {def}}\lambda f\lambda a_0\lambda a_1\lambda c. \mathbf qc$ is as desired.
Conversely, let $h\in \mathrm {V_{ext}}(A)$ and suppose
We wish to find $\mathbf c$ such that $\mathbf c c=\mathbf c d\Vdash h\in X_{{\Pi }_{\sigma } i}$ . We thus aim for $f=(\mathbf cc)_0\sim _{\alpha } (\mathbf cd)_0=g$ and $(\mathbf cc)_1=(\mathbf cd)_1\Vdash h=f^{\alpha }$ . Let us first find f and g. If $a\sim _{\sigma } b$ , then by (5) there are $z,y\in \mathrm {V_{ext}}(A)$ such that
From (4) and (7), it follows that
and for some $\breve {y},Y\in \mathrm {V_{ext}}(A)$ ,
where $\tilde \tau =i \tilde {a}$ . Now, by (8) and (9) we obtain $\Vdash a^{\sigma }=\breve {a}^{\sigma }$ and $\Vdash \tilde {a}^{\sigma }=\breve {a}^{\sigma }$ , and hence by Lemma 4.11 we have $a\sim _{\sigma } \breve {a}\sim _{\sigma } \tilde {a}$ . Therefore, $a^{\sigma }=\breve a^{\sigma }$ , $\tau =ia\sim i\breve {a}=\breve {\tau }$ , and $X_{\tau }=X_{\breve {\tau }}$ . By the properties of pairing and equality, from (8) and (9) we obtain $\mathbf q ca=\mathbf q db\Vdash y\in X_{\tau }$ , for some closed term $\mathbf q$ . Hence
Therefore, by (10), by letting $(\mathbf c c)_0=\lambda a.(\mathbf qca)_0$ , we have
It remains to show $(\mathbf c c)_1=(\mathbf c d)_1\Vdash h=f^{\alpha }$ .
For the right to left inclusion, let $a\sim _{\sigma } b$ , $e=fa$ , and $\tau =ia$ . We want
By the foregoing discussion, we have that (7), (8), and (11) hold true for some $z,y\in \mathrm {V_{ext}}(A)$ . By the properties of pairing and equality, it follows from (8) and (11) that $\mathbf rca=\mathbf rdb\Vdash \langle {a^{\sigma },e^{\tau }}\rangle _{\!A}=z$ , for some closed term $\mathbf r$ . We may then let $((\mathbf c c)_1a)_{1}=\mathbf p (c_{10}a)_0 (\mathbf rca)$ .
The left to right inclusion is treated in a similar manner. Suppose $\langle {\breve c,\breve d,\breve z}\rangle \in h$ . By (4), $a=(c_0\breve c)_0\sim _{\sigma } (d_0\breve d)_0=b$ , and for some $\breve y\in \mathrm {V_{ext}}(A)$ , $(c_0\breve c)_{110}= (d_0\breve d)_{110}\Vdash \operatorname {{\mathrm {OP}}}(\breve z,a^{\sigma },\breve y)$ . As before, there are $z,y\in \mathrm {V_{ext}}(A)$ such that (7), (8), and (11) hold true of a and b. On account of (6), it follows from (7), (8), and (11) that $\mathbf l c\breve c=\mathbf ld\breve d\Vdash \breve z=\langle {a^{\sigma },(fa)^{\tau }}\rangle _{\!A}$ , for some closed term $\mathbf l$ . Then $\mathbf c$ such that $((\mathbf c c)_1\breve c)_0=\mathbf p (c_0\breve c)_0 (\mathbf lc\breve c)$ does the job.
(iv) We aim for $\mathbf {sum}\Vdash X_{{\Sigma }_{\sigma } i}={\Sigma }(X_{\sigma }, F)$ . Let $\beta ={\Sigma }_{\sigma } i$ . For the direction from left to right, we ask for a closed term $\mathbf l$ such that
Let $a\sim _{\beta } b$ . We want
where $\tau =ia_0$ . By definition, $a_0\sim _{\sigma } b_0$ . Let $(\mathbf l a)_0=a_0$ . Then we aim for
for some $y,Y\in \mathrm {V_{ext}}(A)$ . Let $y=a_1^{\tau }$ , and $Y=X_{\tau }$ . Note that $\langle {a_0,b_0,\langle {a_0^{\sigma },X_{\tau }}\rangle _{\!A}}\rangle \in F$ . Set $(\mathbf la)_{10}=a_0$ . We thus want
By the properties of pairing, we just need to worry about the last conjunct. Now, $a_1\sim _{\tau } b_1$ , and thereby $\langle {a_1,b_1,a_1^{\tau }}\rangle \in X_{\tau }$ . Therefore, $\mathbf p a_1\mathbf i=\mathbf p b_1\mathbf i\Vdash a_1^{\tau }\in X_{\tau }$ , where $\mathbf i\Vdash \forall x\, (x=x)$ .
We now consider the converse direction. We look for a closed term $\mathbf r$ such that
Let $z,y\in \mathrm {V_{ext}}(A)$ and $\breve a\sim _{\sigma }\breve b$ . We want
Let $a\sim _{\sigma } b$ and $\tau =ia$ . We set out for
for every $Y\in \mathrm {V_{ext}}(A)$ . Fix a $Y\in \mathrm {V_{ext}}(A)$ and suppose
By the properties of pairing and equality, we have $\Vdash a^{\sigma }=\breve a^{\sigma }$ and
for some closed term $\mathbf q$ . By Lemma 4.11, we then obtain $a^{\sigma }=\breve a^{\sigma }$ . Therefore,
By the usual properties of pairing and equality, we have $\mathbf z c=\mathbf z d\Vdash z=\langle {a^{\sigma },\mathring c^{\tau }}\rangle _{\!A}$ , for some closed term $\mathbf z$ . Now, $\mathbf p a\mathring c\sim _{\beta }\mathbf p b\mathring d$ , and so $\langle {\mathbf p a\mathring c,\mathbf p b\mathring d, \langle {a^{\sigma },\mathring c^{\tau }}\rangle _{\!A}}\rangle \in X_{{\Sigma }_{\sigma } i}$ . Therefore,
Then $\mathbf r$ such that $\mathbf r\breve a ac=\mathbf p(\mathbf p a(\mathbf q c)_{10})(\mathbf z c)$ does the job.
(v) We aim for $\mathbf {id}\Vdash X_{\mathrm {I}_{\sigma }(a,b)}=\mathrm {I}(a^{\sigma },b^{\sigma })$ . For the left to right direction, we want a closed term $\mathbf l$ such that whenever $\langle {c,d,z}\rangle \in X_{\mathrm {I}_{\sigma }(a,b)}$ , then $\mathbf {l}c=\mathbf ld\Vdash \nu (z)\land a^{\sigma }=b^{\sigma }$ , where $\nu (z)$ expresses that $z=0$ . Suppose $\langle {c,d,z}\rangle \in X_{\mathrm {I}_{\sigma }(a,b)}$ . By definition, $c=d=\mathbf 0$ , $z=0$ , and $a\sim _{\sigma } b$ . It is easy to find ${\mathbf t}$ such that ${\mathbf t}\Vdash \nu (0)$ . On the other hand, by Lemma 4.11, from $a\sim _{\sigma } b$ we obtain $a^{\sigma }=b^{\sigma }$ . Let $\mathbf l=_{\mathrm {def}}\lambda c.\mathbf p\mathbf q\mathbf i$ , where $\mathbf i\Vdash \forall x\, (x=x)$ .
For the right to left direction, we aim for a closed term $\mathbf r$ such that for every $z\in \mathrm {V_{ext}}(A)$ , $\mathbf r\Vdash \nu (z)\land a^{\sigma }=b^{\sigma } \rightarrow z\in X_{\mathrm {I}_{\sigma }(a,b)}$ . Note that $\Vdash \nu (z)$ implies $z=0$ . By Lemma 4.11, $\Vdash a^{\sigma }=b^{\sigma }$ implies $a\sim _{\sigma } b$ . Thus let $\mathbf r=_{\mathrm {def}}\lambda c.\mathbf p\mathbf 0\mathbf i$ , where $\mathbf i$ is as before.
(vi) We aim for $\mathbf w\Vdash X_{\mathrm {W}_{\sigma } i}=\mathrm {W}(X_{\sigma },F)$ . Set $\delta =\mathrm {W}_{\sigma } i$ . By Theorem 6.2, it suffices to find closed terms $\mathbf l$ and $\mathbf r$ such that
where $\vartheta (y,x,f) \Leftrightarrow \operatorname {{\mathrm {OP}}}(y,x,f)\land \vartheta _0(x,f)\land \vartheta _1(f)\land \vartheta _2(f)$ , with
Remember that
From left to right, note that if $c\sim _{\delta } d$ , then $c_0\sim _{\sigma } d_0$ . Let $(\mathbf lc)_0=c_0$ . We then want $(\mathbf lc)_1=(\mathbf ld)_1\Vdash \exists f\, \vartheta (c^{\delta },c_0^{\sigma },f)$ . The obvious candidate for f is $f_c$ . The details are tedious but straightforward.
Let us consider the slightly more interesting direction. Let $y\in \mathrm {V_{ext}}(A)$ and suppose
The goal is to find $\mathbf r$ such that $\mathbf ra=\mathbf rb\Vdash y\in X_{\delta }$ . By undoing (16), we obtain
for some $f\in \mathrm {V_{ext}}(A)$ . It follows from the second half of (17) that $a_{10}=b_{10}\Vdash \operatorname {{\mathrm {OP}}}(y,a_0^{\sigma },f)$ . Also, we can find closed terms $\mathbf q_0,\mathbf q_1,\mathbf q_2$ such that $\mathbf q_0a=\mathbf q_0b\Vdash \vartheta _0(a_0^{\sigma },f)$ and $\mathbf q_ia=\mathbf q_ib\Vdash \vartheta _i(f)$ for $i=1,2$ . Because $a_0\sim _{\sigma } b_0$ by the first half of (17), we can apply $\mathbf q_0$ and obtain
where
By the properties of pairing with $X=X_{ia_0}$ , it follows from (18) that
for some closed term ${\mathbf t}$ . Suppose $p\sim _{ia_0} q$ . By (19), $(\mathbf ta)_1p=({\mathbf t} b)_1q\Vdash \exists z\, \exists v\in f \operatorname {{\mathrm {OP}}}(v,p^{ia_0},z)$ , and hence for some $z,v\in \mathrm {V_{ext}}(A)$ ,
Write $\langle {\breve p,\breve q,v}\rangle $ for $\langle {((\mathbf ta)_1p)_0, (({\mathbf t} b)_1q)_0,v}\rangle $ . Now, $\mathbf q_2a=\mathbf q_2b\Vdash \vartheta _2(f)$ . It then follows from (20) that
By (21) and (22), we get $\mathbf q_2a\breve p((\mathbf ta)_1p)_1=\mathbf q_2b\breve q(({\mathbf t} b)_1q)_1 \Vdash z\in X_{\delta }$ , and so we can construct a closed term $\mathbf f$ such that
The foregoing discussion also shows that, if we let $(\mathbf ra)_0=\mathbf p a_0(\lambda p.(\mathbf fap)_0)$ , then $c= (\mathbf ra)_0\sim _{\delta } (\mathbf rb)_0=d$ . We then wish to find $\mathbf r$ such that $(\mathbf ra)_1=(\mathbf rb)_1\Vdash y=c^{\delta }$ . For this one needs to show that $\mathbf ha=\mathbf hb\Vdash f=f_c$ for some closed term $\mathbf h$ . Since this is similar to the proof of the right to left direction of (iii), we leave the details to the reader.
Proof of Theorem 4.16
We have to provide closed terms $\mathbf i$ and ${\mathbf e}$ such that
for every $X\in \mathrm {V_{ext}}(A)$ . The same task for ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ -sets.
Let $\vartheta (u,Y)$ be as in Theorem 6.1. Thus ${\Pi }{\Sigma }\mathrm {I}=\{Y\mid \exists u\, \vartheta (u,Y)\}$ . We want $\mathbf i$ and ${\mathbf e}$ such that for every $u,Y\in \mathrm {V_{ext}}(A)$ ,
The closed terms $\mathbf i$ and ${\mathbf e}$ are obtained by means of the recursion theorem for pca’s. The verification is done by induction on u. First, by soundness, there is a closed term $\mathbf {t}$ such that $c=d\Vdash \vartheta (u,Y)$ implies
By using the definition by cases combinator $\mathbf d$ , we can find closed terms $\mathbf {c}$ and ${\mathbf t}_i$ for $i<4$ such that if $c=d\Vdash \vartheta (u,Y)$ , then for some $i<5$ ,
Case 0. If $\mathbf c c=\mathbf 0$ , then ${\mathbf t}_0 c={\mathbf t}_0 d\Vdash Y\in \omega $ . By Theorem 4.14, we have a closed term $\mathbf o$ such that $\mathbf o\Vdash X_{\mathsf {N}}=\omega $ . By soundness, there is a closed term ${\mathbf v}_0$ such that ${\mathbf v}_0c={\mathbf v}_0d\Vdash Y\in X_{\mathsf {N}}$ . This means that, for some $n\in \omega $ , $({\mathbf v}_0c)_0=({\mathbf v}_0d)_0=\bar n$ and $({\mathbf v}_0c)_1=({\mathbf v}_0d)_1\Vdash Y=\dot n$ . Now, $\mathsf {N}_n=\mathbf p \mathbf 0\bar n$ and $X_{\mathsf {N}_n}=\dot n$ . Therefore, in this case, meaning $\mathbf c c=\mathbf 0$ , we look for $\mathbf i$ and ${\mathbf e}$ such that $\mathbf ic=\mathbf p\mathbf 0({\mathbf v}_0c)_0$ and $\mathbf ec=({\mathbf v}_0c)_1$ .
Case 1. If $\mathbf cc={\mathbf 1}$ , then ${\mathbf t}_1c={\mathbf t}_1d\Vdash Y=\omega $ . As before, by soundness, there is a closed term ${\mathbf v}_1$ such that ${\mathbf v}_1c={\mathbf v}_1d\Vdash Y=X_{\mathsf {N}}$ . Therefore, in this case, meaning $\mathbf cc={\mathbf 1}$ , we look for $\mathbf i$ and ${\mathbf e}$ such that $\mathbf ic=o$ and $\mathbf ec={\mathbf v}_1c$ .
Case 2. Suppose $\mathbf c c=\mathbf 2$ . We are in the case where
for some $X,F\in \mathrm {V_{ext}}(A)$ . By undoing (1), we get that for some $\langle {\mathring {c},\mathring {d},v}\rangle \in u$ , $({\mathbf t}_2 c)_{01}=({\mathbf t}_2 d)_{01} \Vdash \vartheta (v,X)$ . By induction, we can assume
By the properties of equality, on account of (1) and (3), we can find closed terms $\mathbf q_0,\mathbf q_1,\mathbf q_2$ such that
Suppose $a\sim _{\sigma } b$ . By using (4), we can obtain a closed term $\mathbf r$ such that
Therefore, there are $Z,\mathring {X}\in \mathrm {V_{ext}}(A)$ such that $\mathbf r\mathbf eca=\mathbf r\mathbf edb\Vdash Z\in F\land \operatorname {{\mathrm {OP}}}(Z,a^{\sigma },\mathring {X})$ . On the other hand, it follows from (5) that
In particular, for some $\langle {\mathring c,\mathring d,v}\rangle \in u$ , $(\mathbf q_1\mathbf eca)_1(\mathbf r\mathbf eca)=(\mathbf q_1\mathbf edb)_1(\mathbf r\mathbf edb)\Vdash \vartheta (v,\mathring {X})$ . To ease notation, let $r({\mathbf e},c,a)=(\mathbf q_1\mathbf eca)_1(\mathbf r\mathbf eca)$ . By induction, we can assume that $\rho =\mathbf i r({\mathbf e},c,a)\sim \mathbf i r({\mathbf e},d,b)$ and ${\mathbf e} r({\mathbf e},c,a)={\mathbf e} r({\mathbf e},d,b)\Vdash \mathring X=X_{\rho }$ . We have just shown that if $a\sim _{\sigma } b$ then $ia\sim jb$ , where $i=\lambda a.\mathbf i r({\mathbf e},c,a)$ and $j=\lambda b.\mathbf i r({\mathbf e},d,b)$ . By (2), we thus have ${\Pi }_{\sigma } i\sim {\Pi }_{\tau } j$ .
Let $\mathbf {prod}$ be as in Theorem 4.14. That is, $\mathbf {prod}\Vdash X_{{\Pi }_{\sigma } i}={\Pi }(X_{\sigma },F_{\sigma ,i})$ . We aim to show that for some closed term $\mathbf f$ , $\mathbf f \mathbf ec=\mathbf f \mathbf ed\Vdash F=F_{\sigma ,i}$ . If we do so, owing to the soundness, we can cook up, by using (6) and $\mathbf {prod}$ , a closed term ${\mathbf v}_2$ such that ${\mathbf v}_2\mathbf ec={\mathbf v}_2\mathbf ed\Vdash Y=X_{{\Pi }_{\sigma } i}$ . In this case, meaning $\mathbf c c=\mathbf 2$ , we thus want $\mathbf i$ and ${\mathbf e}$ such that
Let us show how to find $\mathbf f$ . By Theorem 4.14, $\mathbf {fun}\Vdash \operatorname {{\mathrm {Fun}}}(F_{\sigma ,i})\land \operatorname {{\mathrm {dom}}}(F)=X_{\sigma }$ . By (4), it then suffices to look for a closed term $\mathbf {h}$ such that
Let $a\sim _{\sigma } b$ . We aim for $\mathbf h \mathbf eca=\mathbf h \mathbf edb\Vdash \langle {a^{\sigma },X_{\rho }}\rangle _{\!A}\in F$ , where $\rho =i a$ . As before, we know that for some $Z,\mathring X\in \mathrm {V_{ext}}(A)$ , $\mathbf r\mathbf eca=\mathbf r\mathbf edb \Vdash Z\in F\land \operatorname {{\mathrm {OP}}}(Z,a^{\sigma },\mathring {X})$ and ${\mathbf e} r({\mathbf e},c,a)={\mathbf e} r({\mathbf e},d,b) \Vdash \mathring X=X_{\rho }$ . By the properties of equality and pairing, we can easily arrange for such $\mathbf h$ .
Case 3. The case $\mathbf c c=\mathbf 3$ is treated similarly.
Case 4. Suppose $\mathbf cc={\mathbf 4}$ . In this case,
for some $X\in \mathrm {V_{ext}}(A)$ . As in Case 2, we can assume
By the properties of equality, owing to (7) and (8), we thus have a closed term $\mathbf q$ such that $\mathbf q\mathbf ec=\mathbf q\mathbf ed\Vdash \exists x\in X_{\sigma }\, \exists y\in X_{\sigma }\, (Y=\mathrm {I}(x,y))$ . By unfolding the definition, we obtain
By using $\mathbf {id}\Vdash X_{\mathrm {I}_{\sigma }(a,b)}=\mathrm {I}(a^{\sigma },b^{\sigma })$ from Theorem 4.14, we then obtain by soundness a closed term ${\mathbf v}_4$ such that ${\mathbf v}_4\mathbf ec={\mathbf v}_4\mathbf ed\Vdash Y=X_{\mathrm {I}_{\sigma }(a,b)}$ . In this case, meaning $\mathbf c c={\mathbf 4}$ , we thus want $\mathbf i$ and ${\mathbf e}$ such that
In the ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}$ case, one considers $\vartheta ^*(u,Y)$ as in Theorem 6.1. Thus ${\Pi }{\Sigma }\mathrm {W}\mathrm {I}=\{Y\mid \exists u\, \vartheta ^*(u,Y)\}$ . The proof then proceeds exactly as before, except that now we also need to deal with $\mathrm {W}$ -types. On the other hand, the treatment of $\mathrm {W}$ -types is completely analogous to that of ${\Pi }$ -types and ${\Sigma }$ -types. The reader can easily fill in the gaps using Case 2 as template.
Acknowledgment
The author’s research was funded by the Alexander von Humboldt foundation.