A Constructive Examination of a Russell-style Ramified Type Theory

TL;DR

This paper explores a predicative, constructive interpretation of Russell's ramified type theory within Martin-Löf type theory, showing its usefulness for constructive mathematics and suggesting a related notion of predicative elementary topos.

Contribution

It provides a constructive, predicative version of Russell's ramified type theory compatible with Martin-Löf type theory, avoiding impredicativity.

Findings

Functional reducibility holds in the interpretation.

The type hierarchy supports constructive mathematics.

Suggests a natural notion of predicative elementary topos.

Abstract

In this paper we examine the natural interpretation of a ramified type hierarchy into Martin-L\"of type theory with an infinite sequence of universes. It is shown that under this predicative interpretation some useful special cases of Russell's reducibility axiom are valid, namely functional reducibility. This is sufficient to make the type hierarchy usable for development of constructive mathematics. We present a ramified type theory suitable for this purpose. One may regard the results of this paper as an alternative solution to the problems of Russell's theory, which avoids impredicativity, but instead imposes constructive logic. The intuitionistic ramified type theory introduced here, also suggests that there is a natural associated notion of predicative elementary topos.

Equations

$${\mathbf{P}}_0(S)\subseteq {\mathbf{P}}_1(S)\subseteq {\mathbf{P}}_2(S)\subseteq \cdots$$

$$\{x:A|\phi (x)\}:{\mathbf{P}}_k(A)$$

$$(\forall X:{\mathbf{P}}_r(S))(\exists Y:{\mathbf{P}}_0(S))(\forall z:S)(zϵX\iff zϵY).$$

$$|1|$$

$$|A\times B|$$

$$|{\mathbf{P}}_n(A)|$$

$$||1||$$

$$||A\times B||$$

$$||{\mathbf{P}}_n(A)||$$

$$\{x:A|\phi \}\in \mathrm{Term}({\mathbf{P}}_k(A))$$

$$\mathrm{Form}(0)\subseteq \mathrm{Form}(1)\subseteq \mathrm{Form}(2)\subseteq \cdots$$

$$z$$

$${\pi }_1(⟨x,y⟩)$$

$${\pi }_2(⟨x,y⟩)$$

$$⟨{\pi }_1(z),{\pi }_2(z)⟩$$

$$(\forall X,Y:{\mathbf{P}}_k(A))((\forall z:A)(zϵX\iff zϵY)\Rightarrow X{=}_{{\mathbf{P}}_k(A)}Y)$$

$$(\forall z:A)(zϵ\{x:A|\phi \}\iff \phi [z/x]).$$

$$x{=}_{A}y⟺{\phi }_A(x,y).$$

$${\phi }_{{\mathbf{P}}_n(A)}(x,y)\equiv (\forall z:A)(zϵx\iff zϵy).$$

$$\mathbb{N}=(\mathbf{N},\{x:\mathbf{N}|\top \},0).$$

$$(\forall x:A)(\forall y:B)(⟨x,y⟩ϵR⟹xϵX\wedge yϵY).$$

$$(\forall x:A)(\forall y,z:B)(⟨x,y⟩ϵR\wedge ⟨x,z⟩ϵR⟹y{=}_{B}z),$$

$$(\forall x:A)(xϵX\Rightarrow (\exists y:B)(yϵY\wedge ⟨x,y⟩ϵR)).$$

$$(\forall X:{\mathbf{P}}_m(A))(\forall Y:{\mathbf{P}}_n(B))(\forall F:{\mathbf{P}}_r(A\times B))$$

$$aϵD\wedge (\forall x:A)(xϵD\Rightarrow (\exists y:A)(yϵD\wedge ⟨x,y⟩ϵR))$$

$$[0^0{]}^R$$

$$[(t_1^{n_1},\dots ,t_k^{n_k}{)}^m{]}^R$$

$$|A\times B|=|A|\times |B|$$

$$(x,y){=}_{A\times B}(u,v)⟺(x{=}_{A}u)\wedge (y{=}_{B}v).$$

$$|B^A|{=}_{\mathrm{def}}(\Sigma f:|A|\to |B|)(\forall x,y:|A|)(x{=}_{A}y\Rightarrow f(x){=}_{B}f(y))$$

$$(f,p){=}_{B^A}(g,q){⟺}_{\mathrm{def}}(\forall x:|A|)(f(x){=}_{B}g(x))$$

$$(\forall x:A)(\exists !y:B)R(x,y)⟹(\exists !f:B^A)(\forall x:A)R(x,f(x)).\text{qed}$$

$$x{=}_{A}y⟹(R(x)\iff R(y)).$$

$$R(⟨f(n),f(n+1)⟩).\text{qed}$$

Full text

Mathematics Subject Classification (2010):

03B15, 03F35, 03F50

The author was supported by a grant from the Swedish Research Council (VR). Author’s address: Department of Mathematics, Stockholm University, 106 91 Stockholm. Email: palmgren[at]math.su.se.

Russell introduced with his ramified type theory a distinction between different levels of propositions in order to solve logical paradoxes, notably the Liar Paradox and the paradox he discovered in Frege’s system (Russell 1908). To be able to carry out certain mathematical constructions, e.g. the real number system, he was then compelled to introduce the reducibility axiom. This had however the effect of collapsing the ramification, from an extensional point of view, and thus making the system impredicative. The original Russell theory is not quite up to modern standards of presentation of a formal system: a treatment of substitution is lacking. In the article by Kamareddine, Laan and Nederpelt (2002) however a modern reconstruction of Russell’s type theory using lambda-calculus notation is presented. We refer to their article for further background and history.

In this paper we shall present an intuitionistic version of ramified type theory IRTT. By employing a restricted form of reducibility it can be shown to be predicatively acceptable. This axiom, called the Functional Reducibility Axiom (FR), reduce type levels only of total functional relations. The axiom is enough to handle the problem of proliferation of levels of real numbers encountered in Russell’s original theory (Kamareddine et al. 2002, pp. 231 – 232). It is essential that theory is based on intuitionistic logic, as (FR) imply the full reducibility principle using classical logic. The system IRTT is demonstrated to be predicative by interpreting it in a subsystem of Martin-Löf type theory (Martin-Löf 1984), a system itself predicative in the proof-theoretic sense of Feferman and Schütte (Feferman 1982). One may regard the results of this paper as an alternative solution to the problems of Russell’s theory which avoids impredicativity, but instead imposes constructive logic.

The interpretation is carried out in Sections 2 and 3. In Section 4, we see how universal set constructions useful for e.g. formalizing real numbers can be carried out in IRTT. The intuitionistic ramified type theory introduced here, also suggests that there is a natural associated notion of predicative elementary topos, but this will have to be developed elsewhere. Adding the principle of excluded middle to IRTT makes the full reducibility axiom a theorem (Section 5).

An extended abstract of an early version of this paper has been published as [8].

1. Ramified Type Theory

Our version of the ramified type hierarchy is built from basic types ${\bf 1}$ (the unit type) and ${\bf N}$ (the type of natural number) using the product type construction $\times$, and for each $n=0,1,2,\ldots$ the restricted power set operation ${\bf P}_{n}(S)$. The latter operation assigns to each type $S$ the type of level $n$ propositional functions on $S$, or level $n$ subsets of $S$. (See Remark 1.2 below for a comparison with Russell’s ramified types.) Intuitively these power sets form an increasing sequence:

[TABLE]

To avoid impredicativity when forming a subset

[TABLE]

it is required that $\varphi(x)$ does not contain quantifiers over ${\bf P}_{n}(S)$ where $n\geq k$. A version of the full reducibility axiom says that this hierarchy collapses from an extensional point of view: for each level $r$,

[TABLE]

This has the effect of reintroducing impredicativity, as was observed by Ramsey (Ramsey 1926); see also Myhill (1979). However, a special case of the reducibility axiom is predicatively acceptable if we work against the background of intuitionistic logic. This is shown by modelling it in Martin-Löf type theory.

We now turn to the formal presentation of our theory. The set of *ramified type symbols * ${\mathcal{R}}$ is inductively defined by

• •

${\bf 1},{\bf N}\in{\mathcal{R}}$,

• •

if $A,B\in{\mathcal{R}}$, then $A\times B\in{\mathcal{R}}$,

• •

if $A\in{\mathcal{R}}$ and $n\in{\mathbb{N}}$, then ${\bf P}_{n}(A)\in{\mathcal{R}}$.

The level of a type symbol $A$, $|A|$, is defined recursively

[TABLE]

For instance, the level of the type expression ${\bf P}_{3}({\bf N})\times{\bf P}_{1}({\bf N}\times{\bf P}_{1}({\bf 1}))$ is 4. Let ${\mathcal{R}}_{n}=\{A\in{\mathcal{R}}\>:\>|A|\leq n\}$. We also define the equality level $||A||$ of a type $A$ recursively by

[TABLE]

(The significance of this measure is seen in Lemma 1.1.) Below we often write $n_{1}\lor\cdots\lor n_{k}$ for $\max(n_{1},\ldots,n_{k})$.

Our system IRTT of intuitionistic ramified type theory will be based on many-sorted intuitionistic logic. The sorts will be the types in ${\mathcal{R}}$. We define simultaneously the set of terms ${\rm Term}(A)$ of type $A\in{\mathcal{R}}$ and the set of formulas of level $k\in{\mathbb{N}}$, denoted ${\rm Form}(k)$.

• •

For each $A\in{\mathcal{R}}$ there is a countable sequence of variables of sort $A$: ${\sf v}_{0}^{A},{\sf v}_{1}^{A},{\sf v}_{2}^{A},\ldots$ in ${\rm Term}(A)$;

• •

$\star\in{\rm Term}({\bf 1})$;

• •

$0\in{\rm Term}({\bf N})$;

• •

If $a\in{\rm Term}({\bf N})$, then ${\sf S}(a)\in{\rm Term}({\bf N})$;

• •

If $a,b\in{\rm Term}({\bf N})$, then $a+b,a\cdot b\in{\rm Term}({\bf N})$;

• •

If $a\in{\rm Term}(A)$, $b\in{\rm Term}(B)$, then $\langle a,b\rangle\in{\rm Term}(A\times B)$;

• •

If $c\in{\rm Term}(A\times B)$, then $\pi_{1}(c)\in{\rm Term}(A)$ and $\pi_{2}(c)\in{\rm Term}(B)$,

• •

If $\varphi\in{\rm Form}(k)$ and $x$ is a variable in ${\rm Term}(A)$, then

[TABLE]

(This is the set-abstraction term and $x$ is considered to be a bound variable in this term.)

• •

If $|A|\leq k$ and $a,b\in{\rm Term}(A)$, then $(a=_{A}b)\in{\rm Form}(k)$;

• •

If $a\in{\rm Term}(A)$ and $b\in{\rm Term}({\bf P}_{n}(A))$, then $(a\;\epsilon\;b)\in{\rm Form}(k)$ for any $k\geq n$;

• •

$\bot\in{\rm Form}(k)$;

• •

If $\varphi,\psi\in{\rm Form}(k)$, then $(\varphi\lor\psi),(\varphi\land\psi),(\varphi\Rightarrow\psi)\in{\rm Form}(k)$;

• •

If $\varphi\in{\rm Form}(k)$ and $x$ is a variable in ${\rm Term}(A)$ where $|A|\leq k$, then $(\forall x:A)\varphi,(\exists x:A)\varphi\in{\rm Form}(k)$.

It is clear that

[TABLE]

The axioms of ramified type theory are the following. First there are standard axioms for equality stating that each $=_{A}$ is an equivalence relation and that operations and predicates respect these equivalence relations. Axioms for unit type and product type

[TABLE]

The arithmetical axioms are the standard Peano axioms for [math], $S$, $+$ and $\cdot$, together with the induction scheme.

For subsets we have the following axioms

• Axiom of Extensionality:

[TABLE]

• Defining Axiom for Restricted Comprehension:

[TABLE]

The extensionality axiom gives the following

Lemma 1.1**.**

For any type symbol $A$, there is a formula $\varphi_{A}(x,y)$ in ${\rm Form}(||A||)$ such that

[TABLE]

Proof.

Let $\varphi_{A}(x,y)\equiv(x=_{A}y)$ for $A={\bf 1},{\bf N}$, and $\varphi_{B\times C}(x,y)\equiv(\pi_{1}(x)=_{B}\pi_{1}(y)\land\pi_{2}(x)=_{C}\pi_{2}(y))$. Further, define

[TABLE]

The righthand side formula has level $\max(n,|A|)=||{\bf P}_{n}(A)||$, and is by the extensionality axiom equivalent to $x=_{{\bf P}_{n}(A)}y$. It is now easy prove the properties of the other types by induction. ∎

To state the Functional Reducibility Axiom, which is the final axiom, we need to introduce some terminology. Inspired by the terminology in (Bell 1988) of the syntactic counterpart to toposes as local set theories, we define a local set to be a type $A$ together with an element $X$ of ${\bf P}_{n}(A)$, for some $n$. It is thus specified by a triple $(A,X,n)$, where $A$ is the underlying type, $X$ is the propositional function defining the subset of $A$ and $n$ the level of the propositional function. A basic example is the natural numbers as a local set given by

[TABLE]

A relation $R$ between $(A,X,n)$ and $(B,Y,m)$ is some $R:{\bf P}_{k}(A\times B)$ such that

[TABLE]

Such a relation is functional if

[TABLE]

and is total if

[TABLE]

A functional, total relation is simply called a map.

Now the central axiom is the following:

Functional Reducibility Axiom: For $A,B\in{\mathcal{R}}$, $m,n\in{\mathbb{N}}$, we have for $k=||B||\lor m\lor n$ that for any $r\in{\mathbb{N}}$

[TABLE]

Note: $G$ is necessarily unique by the extensionality axiom.

These are the axioms of the basic theory IRTT. To make the system useful for developing Bishop style constructive analysis, we may also extend it by the Relativized Dependent Choice (RDC) axiom scheme, which is the following:

RDC: Let $A$ be any sort and $m,n\geq 0$. Then we have the axiom: for any $D:{\bf P}_{m}(A)$, any $R:{\bf P}_{n}(A\times A)$, and any $a:A$ satisfying

[TABLE]

there is $F:{\bf P}_{k}({\bf N}\times A)$ a map from ${\mathbb{N}}$ to $(A,D,m)$, satisfying

• (a)

$\langle 0,a\rangle\;\epsilon\;F$,

• (b)

$(\forall i:{\bf N})(\forall y,z:A)(\langle i,y\rangle\;\epsilon\;F\land\langle i+1,z\rangle\;\epsilon\;F\Rightarrow\langle y,z\rangle\;\epsilon\;R)$.

Here $k=|A|$.

Remark 1.2**.**

The ramified types of Russell are — according to the modern elaboration of Laan and Nederpelt (1996) — given by the following inductive definition. Each ramified type has the form $t^{n}$ where $n$ is a natural number indicating the order of the type. These are generated as follows

• (a)

$0^{0}$ is a ramified type (the type of individuals)

• (b)

if $t_{1}^{n_{1}},\ldots,t_{k}^{n_{k}}$ are ramified types, and $m>n_{1},\ldots,n_{k}$, then $(t_{1}^{n_{1}},\ldots,t_{k}^{n_{k}})^{m}$ is a ramified type.

A ramified type is minimal (or predicative) if in each application of (b) in its construction, one takes $m=1+\max(n_{1},\ldots,n_{k})$. The reducibility axiom then states that an element of a type $t^{n}$ is extensional equivalent to some element of a corresponding minimal type (Kamareddine et al. 2002, p. 233).

These ramified types can be interpreted into the types ${\mathcal{R}}$ as follows, assuming the type individuals is interpreted as the type of natural numbers:

[TABLE]

Here $A_{1}\times\cdots\times A_{k}=(\cdots(A_{1}\times A_{2})\times\cdots)\times A_{k}$, which in case $k=0$ is just the unit type ${\bf 1}$. The types of ${\mathcal{R}}$ are thus richer than Russell’s, but still have a predicative interpretation as is demonstrated in the following sections.

2. Setoids

As interpreting theory we consider Martin-Löf type theory with an infinite sequence of universes ${\rm U}_{0},{\rm U}_{1},{\rm U}_{2},\ldots$. Each universe ${\rm U}_{n}$ is closed under the standard type constructions $\Pi$, $\Sigma$, $+$ and ${\rm Id}$. ${\rm U}_{0}$ contains basic types such as the type $N$ of natural numbers, empty type and unit type. Moreover if $A:{\rm U}_{n}$ then $A$ is a type and $A:{\rm U}_{n+1}$. Finally ${\rm U}_{n}:{\rm U}_{n+1}$. This is as presented in (Martin-Löf 1984) although we assume that the identity type ${\rm Id}$ is intensional instead of extensional. This theory is considered predicative in the strict sense of Feferman and Schütte and its proof-theoretic ordinal is $\Gamma_{0}$ (Feferman 1982) On the propositions-as-types interpretation, the universe $U_{n}$ can be regarded as the type of propositions of level $n$.

A setoid $A=(|A|,=_{A})$* is of index $(m,n)$* if $|A|:{\rm U}_{m}$ and $=_{A}:|A|\to|A|\to{\rm U}_{n}$. We also say that $A$ is an $(m,n)$-setoid. Since any type of ${\rm U}_{k}$ is a type of ${\rm U}_{k^{\prime}}$ for any $k^{\prime}\geq k$, it follows that any $(m,n)$-setoid is an $(m^{\prime},n^{\prime})$-setoid whenever $m^{\prime}\geq m$ and $n^{\prime}\geq n$.

$A$ is said to be an $n$-setoid if it is an $(n,n)$-setoid. It is an $n$-classoid if it is an $(n+1,n)$-setoid.

Examples 2.1**.**

• (a)

$(N,{\rm Id}(N,\cdot,\cdot))$ is a 0-setoid.

• (b)

Aczel’s model of CZF $(V,=_{V})$ is a 0-classoid if $V$ is built from the universe $U_{0}$.

• (c)

$\Omega_{n}=(U_{n},\leftrightarrow)$ is an $n$-classoid, when $\leftrightarrow$ is logical equivalence.

For setoids $A$ and $B$, the product construction $A\times B$ is provided by

[TABLE]

and

[TABLE]

Whereas the exponent construction $B^{A}$ is given by

[TABLE]

and

[TABLE]

Thus an element $g=(|g|,{\rm ext}_{g})$ of $|B^{A}|$ consists of a function $|g|$ and a proof ${\rm ext}_{g}$ of its extensionality.

Lemma 2.2**.**

If $A$ is an $(m,n)$-setoid and $B$ is a $(k,\ell)$-setoid then $A\times B$ is a $(m\lor k,n\lor\ell)$-setoid and $B^{A}$ is a $(m\lor n\lor k\lor\ell,m\lor\ell)$-setoid. ∎

To simplify notation in the sequel, we usually write $x:A$ for $x:|A|$ when $A$ is a setoid. Moreover, we write $g(x)$ for $|g|(x)$ when $g:[A\to B]$. We have the principle of unique choice that gives a one-to-one correspondence between functions and total, functional relations:

Theorem 2.3**.**

Let $A$ and $B$ be setoids. Suppose that $R(x,y)$ is an extensional property depending on $x:A$, $y:B$.

[TABLE]

For any setoid $A$, note that an element $R=(|R|,{\rm ext}_{R}):[A\to\Omega_{n}]$ consists of a predicate $|R|:|A|\to U_{n}$ and proof of its extensionality, i.e. that if for all $x,y:|A|$

[TABLE]

We call this an extensional propositional function on $A$ of level $n$. The set $[A\to\Omega_{n}]$ will be the interpretation of ${\bf P}_{n}(A)$.

We finally recall that the following form of dependent choice is valid for setoids.

Theorem 2.4**.**

Let $A$ be a setoid and let $R$ be an extensional predicate on $A\times A$. Suppose that $(\forall x:A)(\exists y:A)R(\langle x,y\rangle)$. Then for any $x:A$ there is $f:[{\mathbb{N}}\to A]$ so that $f(0)=_{A}x$ and for all $n:{\mathbb{N}}$:

[TABLE]

3. A model of ramified type theory

The type symbols of ${\mathcal{R}}$ interpret naturally as an extensional hierarchy of setoids in the background theory. Define setoids ${S}^{*}$ by recursion on the structure of $S\in{\mathcal{R}}$.

[TABLE]

Lemma 3.1**.**

If $S\in{\mathcal{R}}$ , then ${S}^{*}$ is an $(|S|,||S||)$-setoid and $|S|\geq||S||$.

Proof.

By induction on the structure of $S$. If $S$ is ${\bf 1}$ or ${\bf N}$, then ${S}^{*}$ is an $(0,0)$-setoid, and $|S|=||S||=0$. If $S=S_{1}\times S_{2}$, then $|S|=|S_{1}|\lor|S_{2}|$ and $||S||=||S_{1}||\lor||S_{2}||$. Now ${S}^{*}={S_{1}}^{*}\times{S_{2}}^{*}$. By Lemma 2.2 , and the induction hypothesis, we have that ${S_{1}}^{*}\times{S_{2}}^{*}$, is a $(|S_{1}|\lor|S_{2}|,||S_{1}||\lor||S_{2}||)$-setoid, and thus by definition of levels, an $(|S|,||S||)$-setoid. By inductive hypothesis also $|S|\geq||S||$. For the case $|S|={\bf P}_{n}(A)$, we have that

[TABLE]

Now by inductive hypothesis ${A}^{*}$ is an $(|A|,||A||)$-setoid. Also $\Omega_{n}$ is an $(n+1,n)$-setoid. Thus by Lemma 2.2, ${S}^{*}$ is a setoid of index

[TABLE]

Here we have used the inductive hypothesis $|A|\geq|A|$. Clearly we have $|S|\geq||S||$. ∎

The interpretation ${(-)}^{*}$ is now extended in the standard fashion for propositions-as-types interpretations of many-sorted intuitionistic logic (cf. Martin-Löf 1998). Each formula $\varphi$ is interpreted as a type ${\varphi}^{*}$. Each term $a$ of sort $A$ is interpreted as an element ${a}^{*}$ of type $|{A}^{*}|$. Moreover, if $\varphi$ is in ${\rm Form}(n)$ we shall require that ${\varphi}^{*}:{\rm U}_{n}$.

Each variable $x$ of sort $A$ is interpreted as a variable ${x}^{*}$ of type $|{A}^{*}|$. All the terms associated with the sorts ${\bf 1}$, ${\bf N}$, $A\times B$ are interpreted in the obvious way. Logical constants are interpreted as the corresponding type constructions in the familiar way. E.g. for quantifiers we define

[TABLE]

Then for atomic formulas define

[TABLE]

where $a$ and $b$ are terms of sort $A$, and $c$ is a term of sort $B$ and $d$ a term of sort ${\bf P}_{k}(B)$. If $\varphi\in{\rm Form}(n)$ and $x$ is variable of sort $A$, then define ${\{x:A\;|\;\varphi\}}^{*}=(\lambda{x}^{*}.{\varphi}^{*},e)$ where $e$ is a proof object for the extensionality of $\lambda{x}^{*}.{\varphi}^{*}:|{A}^{*}|\to{\rm U}_{n}$.

Lemma 3.2**.**

For $\varphi\in{\rm Form}(n)$, the interpretation satisfies ${\varphi}^{*}:{\rm U}_{n}$.

Proof.

By induction on the build-up of formulas. We do some interesting cases:

$\varphi=(a=_{A}b)$: if $|A|\leq n$, then since ${A}^{*}$ is an $n$-setoid, ${\varphi}^{*}:{\rm U}_{n}$.

$\varphi=(c\;\epsilon\;d)$: if $d$ has sort ${\bf P}_{k}(A)$ where $k\leq n$, then ${\varphi}^{*}=|{d}^{*}|({c}^{*}):{\rm U}_{k}$. But $k\leq n$, so indeed ${\varphi}^{*}:U_{n}$.

$\varphi=(\forall x:A)\psi$: if $|A|<n$, $\psi\in{\rm Form}(n)$, then ${\varphi}^{*}=(\Pi{x}^{*}:|{A}^{*}|){\psi}^{*}\in{\rm U}_{n}$, since ${A}^{*}$ is an $n$-setoid and ${\psi}^{*}\in{\rm U}_{n}$ according to the inductive hypothesis.

∎

Next we consider the semantic version of a local set. A pair $M=(S_{M},\chi_{M})$ consisting of $S_{M}$ an $(m,n)$-setoid and a propositional function $\chi_{M}\in[S_{M}\to\Omega_{k}]$ is called a local set. It gives rise to a setoid

[TABLE]

where

[TABLE]

This setoid has index $(m\lor k,n)$.

For two local sets $M$ and $K$, we call $F\in[S_{M}\times S_{K}\to\Omega_{r}]$ a map from $M$ to $K$ if

[TABLE]

and

[TABLE]

The following theorem implies the validity of the Functional Reducibility Axiom under the interpretation.

Theorem 3.3** (Functional reducibility).**

Let $A$ be an $(m,n)$-setoid and $B$ be an $(m^{\prime},n^{\prime})$-setoid. Suppose $X:[A\to\Omega_{k}]$ and $Y:[B\to\Omega_{k^{\prime}}]$. Let $r\in{\mathbb{N}}$. Then for every map $F:[A\times B\to\Omega_{r}]$ from $(A,X)$ to $(B,Y)$ there is $G:[A\times B\to\Omega_{\ell}]$ such that for all $a:A$ and $b:B$

[TABLE]

Here $\ell=k\lor k^{\prime}\lor n^{\prime}$.

Proof.

Construct setoids $U=\widehat{(A,X)}$ and $V=\widehat{(B,Y)}$. These are $(m\lor k,n)$- and $(m^{\prime}\lor k^{\prime},n^{\prime})$-setoids, respectively. For $f:[U\to V]$ define the relation

[TABLE]

Since $x=_{V}y$ is in $U_{n^{\prime}}$, we have that the righthand side is in $\Omega_{\ell}$ where $\ell=k\lor k^{\prime}\lor n^{\prime}$. Suppose now that $r\in{\mathbb{N}}$ and that $F:[A\times B\to\Omega_{r}]$ is a map from $(A,X)$ to $(B,Y)$. This implies that

[TABLE]

Thus

[TABLE]

By the axiom of unique choice there is a unique $f:[U\to V]$ so that

[TABLE]

Suppose that $F(\langle a,b\rangle)$ for $a:A$ and $b:B$. By strictness of $F$ there is $p:X(a)$. Let $u=\langle a,p\rangle$. By (2) we have $F(\langle a,\pi_{1}(f(u))\rangle)$. Thus $\pi_{1}(f(u))=_{B}b$. Let $q=\pi_{2}(f(u))$. Thus $f(\langle a,p\rangle)=_{V}\langle b,q\rangle$, i.e. $G_{f}(\langle a,b\rangle)$. Conversely, suppose $G_{f}(\langle a,b\rangle)$, so that $f(\langle a,p\rangle)=_{V}\langle b,q\rangle$ for some $p:X(a)$ and $q:Y(b)$. By (2) we have $F(\langle\pi_{1}(\langle a,p\rangle),\pi_{1}(f(\langle a,p\rangle))\rangle)$. Thus since $F$ is extensional, $F(\langle a,b\rangle)$. This proves

[TABLE]

∎

We verify the Functional Reducibility Axiom. Suppose $A,B\in{\mathcal{R}}$, $m,n\in{\mathbb{N}}$ and let $k=||B||\lor m\lor n$. By Lemma 3.1 ${B}^{*}$, is a $(|B|,||B||)$-setoid. Suppose ${X}^{*}:{{\bf P}_{m}(A)}^{*}$, ${Y}^{*}:{{\bf P}_{n}(B)}^{*}$, ${F}^{*}:{{\bf P}_{r}(A\times B)}^{*}$ and that

[TABLE]

is true. This says that ${F}^{*}$ is a map from $({A}^{*},{X}^{*})$ to $({B}^{*},{Y}^{*})$. By Theorem 3.3 above we get for $\ell=m\lor n\lor||B||$ some $G:[{A}^{*}\times{B}^{*}\to\Omega_{\ell}]$ such that for all $a:{A}^{*}$ and $b:{B}^{*}$

[TABLE]

The axiom RDC is verified as follows. Let $A\in{\mathcal{R}}$ and $m,n\geq 0$. Let $k=|A|$. Suppose ${D}^{*}:{{\bf P}_{m}(A)}^{*}$, ${R}^{*}:{{\bf P}_{n}(A\times A)}^{*}$ and $x:{A}^{*}$ are such that ${D}^{*}(x)$ and

[TABLE]

are true. Setting $E=({A}^{*},{D}^{*})$ the assumption (3) implies that

[TABLE]

We have $t:{D}^{*}(x)$ for some $t$, so $w=\langle x,t\rangle:\hat{E}$. By Theorem 2.4 there is $f:[{\mathbb{N}}\to E]$ so that $f(0)=_{E}w$ and for all $i:{\mathbb{N}}$

[TABLE]

Define

[TABLE]

Now $F(\langle i,a\rangle)$ is in ${\rm U_{k}}$, so it is easy to see that $F$ satisfies the requirements.

We thus conclude:

Theorem 3.4**.**

IRTT + RDC can be interpreted in Martin-Löf type theory with an infinite sequence of universes. ∎

4. Constructions using local sets in IRTT

The system IRTT is not primarily intended to be practical for formalization, but a theoretical exhibit to clarify the relation between Russell’s type theory and modern type theories. IRTT can straightforwardly be embedded into modern proof assistants based on Martin-Löf type theory. The notation of IRTT is undeniably quite cumbersome to handle because of the levels associated to types, a property it inherits from Russell’s system. To simplify its use we can formulate the abstract properties of the local sets in category-theoretic terms as in (Bell 1988).

The category of local sets

The objects of the category are the local sets of IRTT. A morphism between locals set ${\bf X}=(A,X,m)$ and ${\bf Y}=(B,Y,n)$ is a pair ${\bf F}=(F,k)$ such that $F:{\bf P}_{k}(A\times B)$ is a map from ${\bf X}$ to ${\bf Y}$. We write ${\bf F}:{\bf X}\to{\bf Y}$. Two such morphisms $(F,k)$ and $(F^{\prime},k^{\prime})$ are equal if they have extensionally equal graphs:

[TABLE]

Suppose that ${\bf F}:{\bf X}\to{\bf Y}$ and ${\bf G}=(G,\ell):{\bf Y}\to{\bf Z}=(C,Z,p)$ are morphisms. The composition ${\bf G}\circ{\bf F}=(G\circ F,q)$ is then given by

[TABLE]

and since $G\circ F:{\bf P}_{|B|\lor k\lor\ell}(A\times C)$, we can take $q=|B|\lor k\lor\ell$. Hence

[TABLE]

For a local set ${\bf X}=(A,X,m)$ its identity map $1_{\bf X}:{\bf X}\to{\bf X}$ is given by $1_{\bf X}=(1_{X},m\lor||A||)$ where

[TABLE]

It is easily verified that the local sets form a category using extensional equality of maps.

Real numbers

Note that by the Functional Reducibility Axiom, every

[TABLE]

is extensionally equal to some $(F^{\prime},||B||\lor m\lor n):(A,X,m)\to(B,Y,n)$, so hom-sets are ”small”, in the sense that they are limited by the level of the domains and codomains. In particular, for $(A,X,m)=(B,Y,m)={\mathbb{N}}=({\bf N},\{x:{\bf N}\;|\;\top\},0)$ and any $(F,k)$ as above is equal to some $(F^{\prime},0):{\mathbb{N}}\to{\mathbb{N}}$. By this we may conclude that (Cauchy) real numbers of IRTT + RDC all live on the first level of functions.

Quotient sets

The quotient sets construction is similar to that in simple type theory or topos logic, but we need to keep track of the levels of the power sets involved. Let ${\bf X}=(A,X,m)$ be a local set and suppose ${\bf E}=(A\times A,E,n)$ is a local set that represents an equivalence relation on ${\bf X}$, i.e.  it satisfies

[TABLE]

Define the quotient $X/E:{\bf P}_{\ell}({\bf P}_{\ell}(A))$ by

[TABLE]

Here $\ell=m\lor n\lor|A|$. Write $B={\bf P}_{\ell}(A)$. Thus we have a local set ${\bf X}/{\bf E}=(B,X/E,\ell)$, that we shall see is the quotient set of ${\bf X}$ by ${\bf E}$. Define the quotient map $(Q,\ell)$ from ${\bf X}$ to ${\bf X}/{\bf E}$ by

[TABLE]

We show that $(Q,\ell)$ satisfies the universal property for a quotient. Suppose that $(F,k):{\bf X}\to{\bf Z}=(C,Z,p)$ is a map that respects the equivalence relation $E$, i.e.

[TABLE]

Define a map ${\bf H}=(H,r):{\bf X}/{\bf E}\to{\bf Z}$ by

[TABLE]

Here $r=\ell\lor k\lor p$. We have that $\langle x,z\rangle\;\epsilon\;(H\circ Q)$ is equivalent to

[TABLE]

From this and (4) it follows that $\langle x,z\rangle\;\epsilon\;F$. Conversely, suppose $\langle x,z\rangle\;\epsilon\;F$. For $S:B$ we may take $S=\{y:A\;|\;\langle x,y\rangle\;\epsilon\;E\}$, as $n\leq\ell$. It follows immediately that $\langle x,z\rangle\;\epsilon\;(H\circ Q)$. Thus $F$ is extensionally equal to $H\circ Q$.

Now suppose that ${\bf H^{\prime}}=(H^{\prime},s):{\bf X}/{\bf E}\to{\bf Z}$ is another map such that $H^{\prime}\circ Q$ is extensionally equal to $F$. We show that $H^{\prime}$ is extensionally equal to $H$: suppose $\langle S,z\rangle\in H^{\prime}$. Then $S\;\epsilon\;X/E$, so there is some $x\;\epsilon\;X$ with $x\;\epsilon\;S$. Hence $\langle x,S\rangle\;\epsilon\;Q$, and so $\langle x,z\rangle\;\epsilon\;(H^{\prime}\circ Q)$. Thus $\langle x,z\rangle\;\epsilon\;F$. By definition of $H$ we get $\langle S,z\rangle\;\epsilon\;H$. For the converse, suppose $\langle S,z\rangle\;\epsilon\;H$. Then there is some $u\;\epsilon\;X$ with $u\;\epsilon\;S$ and $\langle u,z\rangle\;\epsilon\;F$. Thus by assumption $\langle u,z\rangle\;\epsilon\;(H^{\prime}\circ Q)$. Then there is some $T$ with $\langle u,T\rangle\in Q$ and $\langle T,z\rangle\;\epsilon\;H^{\prime}$. Then $u\;\epsilon\;T$, so in fact we have $S=T$ as $T\;\epsilon\;X/E$. Hence $\langle S,z\rangle\;\epsilon\;H^{\prime}$ as required.

Products

For two local sets ${\bf X}_{1}=(A_{1},X_{1},m_{1})$ and ${\bf X}_{2}=(A_{2},X_{2},m_{2})$, define their binary product to be

[TABLE]

This gives a local set ${\bf X}_{1}\times{\bf X}_{2}=(A_{1}\times A_{2},X_{1}\times X_{2},m_{1}\lor m_{2})$. The projection maps are

[TABLE]

for $i=1,2$. Then $p_{i}:{\bf P}_{r_{i}}((A_{1}\times A_{2})\times A_{i})$, where $r_{i}=m_{1}\lor m_{2}\lor||A_{i}||$, and

[TABLE]

For maps ${\bf F}=(F,p):{\bf Z}\to{\bf X}_{1}$ and ${\bf G}=(G,q):{\bf Z}\to{\bf X}_{2}$, where ${\bf Z}=(C,Z,k)$, define

[TABLE]

We have $\langle{\bf F},{\bf G}\rangle=(\langle F,G\rangle,p\lor q):{\bf Z}\to{\bf X}_{1}\times{\bf X}_{2}$. It is straightforward to check that these constructions make up a category-theoretic product of the local sets ${\bf X}_{1}$ and ${\bf X}_{2}$.

The terminal object (0-ary product) is given by the local set $\tilde{\bf 1}=({\bf 1},\{x:{\bf 1}\;|\;\top\},0)$.

Exponential sets

Again this construction is similar to the construction in simple type theory. Let ${\bf X}=(A,X,m)$ and ${\bf Y}=(B,Y,n)$ be local sets and let $k=||B||\lor m\lor n$ be as in the Functional Reducibility Axiom. Define

[TABLE]

Then by examining the type level involved in the definition of amap one sees that $Y^{X}:{\bf P}_{s}({\bf P}_{k}(A\times B))$ where $s=|A|\lor||A||\lor|B|\lor||B||\lor m\lor n=|A|\lor|B|\lor m\lor n$, giving the local set

[TABLE]

We have that the product

[TABLE]

The evaluation map ${\bf ev}=({\rm ev},s):{\bf Y}^{\bf X}\times{\bf X}\to{\bf Y}$ is given by

[TABLE]

Consider an arbitrary local set ${\bf Z}=(C,Z,p)$ and an arbitrary map ${\bf G}=(G,q)$ from ${\bf Z}\times{\bf X}$ to ${\bf Y}$. Define a map ${\bf H}=(H,k):{\bf Z}\to{\bf Y}^{\bf X}$ by

[TABLE]

Here $t=|A|\lor|B|\lor|C|\lor m\lor n\lor p\lor q$. For $z:C$, $x:A$ and $y:B$ we have

[TABLE]

if, and only if, there are $S:{\bf P}_{k}(A\times B)$ and $u:A$ with

[TABLE]

which is equivalent to

[TABLE]

and spelling this out we get

[TABLE]

Clearly this implies $\langle\langle z,x\rangle,y\rangle\;\epsilon\;G$. Thus we have shown the implication

[TABLE]

To show the converse, we assume $\langle\langle z,x\rangle,y\rangle\;\epsilon\;G$. Let

[TABLE]

This is a map from ${\bf X}$ to ${\bf Y}$. By the Functional Reducibility Axiom there is $S:{\bf P}_{k}(A\times B)$ so that

[TABLE]

But $\langle x,y\rangle\;\epsilon\;L\Leftrightarrow\langle\langle z,x\rangle,y\rangle\;\epsilon\;G$, and hence $\langle x,y\rangle\;\epsilon\;S$, so we have indeed $\langle\langle z,x\rangle,y\rangle\;\epsilon\;{\rm ev}\circ(H\times{\rm id})$. Thus ${\rm ev}\circ(H\times{\rm id})$ and $G$ are extensionally equal.

Finally, we check uniqueness of $H$. Suppose $H^{\prime}$ is another map from ${\bf Z}$ to ${\bf Y}^{\bf X}$ such that ${\rm ev}\circ(H^{\prime}\times{\rm id})$ and $G$ are extensionally equal. Thus we have

[TABLE]

We check that $H$ and $H^{\prime}$ are equal maps. Suppose $\langle z,S\rangle\;\epsilon\;H$ and $\langle z,S^{\prime}\rangle\;\epsilon\;H^{\prime}$. To prove: $S=_{{\bf P}_{k}(A\times B)}S^{\prime}$. By definition of $H$ the equivalence

[TABLE]

Now since $H^{\prime}$ is functional, the $S^{\prime\prime}$ in (5) can only be $S^{\prime}$. Putting (5) and (6) together we have

[TABLE]

as required.

Equalizer set

Let ${\bf X}=(A,X,m)$ and ${\bf Y}=(B,Y,n)$ be local sets. Assume that $(F,k),(G,\ell):{\bf X}\to{\bf Y}$ are two maps. Define a local set ${\bf E}=(A,E,r)$ by

[TABLE]

here $r=|B|\lor k\lor\ell$. Define the inclusion ${\bf I}=(I,p):{\bf E}\to{\bf X}$ by

[TABLE]

where $p=r\lor||A||$.

Characteristic functions

The local set

[TABLE]

may be considered as the collection of possible truth values of level $k$, where the maximal subset

[TABLE]

is the value true. Note that for $u:{\bf P}_{k}({\bf 1})$, we have $u\;\epsilon\;\Omega_{k}$ and $u={\bf t}_{k}$ if, and only if, $\star\;\epsilon\;u$.

Let ${\bf X}=(A,X,m)$ be an arbitrary local set, and suppose that $Y:{\bf P}_{m\lor k}(A)$ satisfies $Y\subseteq X$. We define the relation

[TABLE]

Then $K_{Y}:{\bf P}_{m\lor k}(A\times{\bf P}_{k}({\bf 1}))$, and this gives a map

[TABLE]

Now for $u:A$ with $u\;\epsilon\;X$,

[TABLE]

For ${\bf F}=(F,n):{\bf X}\to\Omega_{k}$ and $u:A$ with $u\;\epsilon\;X$,

[TABLE]

is a formula of level $n$. By the Functional Reducibility Axiom, $(F,n)$ is extensionally equal to some $(F^{\prime},||{\bf P}_{k}({\bf 1})||\lor m\lor 0)=(F^{\prime},k\lor m)$. Thus (7) can be at most of level $m\lor k$.

For the special case where $m\leq k$, we have that characteristic functions $(A,X,m)\to\Omega_{k}$ correspond exactly to local sets $(A,Y,k)$ with $Y\subseteq X$. In particular, characteristic functions ${\mathbb{N}}\to\Omega_{k}$ corresponds to subsets $Y:{\bf P}_{k}({\bf N})$.

Remark 4.1**.**

It is to be expected that IRTT gives rise to a natural notion of predicative topos, but we leave the detailed investigation of this for future work. **

5. Adding classical logic to IRTT

Adding classical logic to IRTT we arrive at a version of Russell’s theory with the full reducibility axiom.

For a type $A$, let $\tilde{A}=(A,\{x:A\;|\;\top\},0)$ be the corresponding local set. Thus $\tilde{N}={\mathbb{N}}$. A particular case of the Functional Reducibility Axiom for $\tilde{A}$ and $\tilde{N}$ is that for any $r$:

[TABLE]

The Full Reducibility Axiom (1) follows from the Principle of Excluded Middle (PEM):

Theorem 5.1**.**

Assume (PEM). Then for any type $A$ and level $k$:

[TABLE]

Proof.

Let $X:{\bf P}_{k}(A)$. Define a relation

[TABLE]

Then $F:{\bf P}_{k}(A\times N)$. Now $F$ can be seen to be a map from $\tilde{A}$ to $\tilde{N}$, where (PEM) is used to prove totality. By (8) above we get $G:{\bf P}_{0}(A\times N)$ such that

[TABLE]

Let

[TABLE]

Then $Y:{\bf P}_{0}(A)$ and clearly

[TABLE]

∎