††thanks: Projects EU-MSCA-RISE project 731143 ”Computing with Infinite Data”
(CID), MIUR-PRIN 2010-2011 and Correctness by Construction (EU 7th framework
programme, grant no. PIRSES-GA-2013-612638) provided support for the research
presented in the paper.

# A realizability semantics for inductive formal topologies, Church’s Thesis
and Axiom of Choice

Maria Emilia Maietti  Dipartimento di Matematica “Tullio Levi Civita”,
Università di Padova, Italy<EMAIL_ADDRESS>Samuele Maschio
Dipartimento di Matematica “Tullio Levi Civita”, Università di Padova, Italy
<EMAIL_ADDRESS>Michael Rathjen  School of Mathematics, University of
Leeds, UK<EMAIL_ADDRESS>
###### Abstract

We present a Kleene realizability semantics for the intensional level of the
Minimalist Foundation, for short mTT, extended with inductively generated
formal topologies, the formal Church’s thesis and axiom of choice.

This semantics is an extension of the one used to show the consistency of the
intensional level of the Minimalist Foundation with the axiom of choice and
the formal Church’s thesis in the work by Ishihara, Maietti, Maschio,
Streicher [Arch.Math.Logic,57(7-8):873-888,2018].

A main novelty here is that such a semantics is formalized in a constructive
theory as Aczel’s constructive set theory CZF extended with the regular
extension axiom.

###### keywords:

Realizability, Axiom of Choice, Church’s thesis, Pointfree topology

##  1 Introduction

A main motivation for introducing the Minimalist Foundation, for short MF, in
[MS05, Mai09] was the desire to provide a foundation where to formalize
constructive point-free topology in a way compatible with most relevant
constructive foundations. In particular, MF was designed with the purpose of
formalizing the topological results developed by adopting the approach of
Formal Topology by P. Martin-Löf and G. Sambin introduced in [Sam87]. This
approach was further enriched with the introduction of Positive Topology by
Sambin in [Sam03]. A remarkable novelty of this approach to constructive
topology was the advent of inductive topological methods (see [CSSV03, CMS13])
to represent the point-free topologies of the real number line, of Cantor
space and of Baire space.

However, while the basic notions of Formal Topology can be formalized in the
Minimalist Foundation in [Mai09], not all the constructions of inductively
generated formal topologies are formalizable there. For instance, the formal
topology of Cantor space and that of the real line are formalizable in MF
thanks to some characterizations given in [Val07], but the formal topology of
the Baire space is not thanks to results in [CR12].

In any case this limitation is not a surprise since MF was introduced to be a
minimalist foundation compatible with the most relevant constructive and
classical foundations for mathematics in the literature in the sense of being
interpretable in them by preserving the meaning of logical and set-theoretic
onstructors.

To better fulfill this requirement MF was ideated in [MS05] as a two level
system which was completed in [Mai09]. More precisely the two-level structure
of MF consists of an intensional level, called mTT and based on an intensional
type theory à la Martin-Löf, aimed at exhibiting the computational contents of
mathematical proofs, and an extensional level formulated in a language as
close as possible to that of present day mathematics which is interpreted in
the intensional level by means of a quotient model (see [Mai09]). In
particular, the intensional level mTT is quite weak in proof-theoretic
strength because it can be interpreted in the fragment of Martin-Löf’s type
theory with one universe, or directly in Feferman’s theory of non-iterative
fixpoints $\widehat{ID}_{1}$ as first shown in [MM16].

The authors in [MS05] were led to propose a two-level system as a notion of
constructive foundation for the following reason. They wanted to found
constructive mathematics in a system interpretable in an extension of Kleene
realizability semantics of intuitionistic arithmetics with finite types. The
reason is that such a semantics makes evident the extraction of witnesses from
existential statements in a computable way thanks to the validity of the axiom
of choice (AC) and the formal Church’s thesis (CT). In more detail, AC states
that from any total relation we can extract a type-theoretic function as
follows:

$({\bf AC})\;(\forall x\in A)\,(\exists y\in B)\,R(x,y)\rightarrow(\exists
f\in A\rightarrow B)\,(\forall x\in A)\,R(x,\mathsf{Ap}(f,x))$

with $A$ and $B$ generic collections and $R(x,y)$ any relation, while CT (see
also [Tv88]) states that from any total relation on natural numbers we can
extract a (code of a) recursive function by using the Kleene predicate $T$ and
the extracting function $U$

$({\bf CT})\;(\forall f\in\mathsf{N}\rightarrow\mathsf{N})(\exists
e\in\mathsf{N})\,(\forall x\in\mathsf{N})\,(\exists
z\in\mathsf{N})\,(T(e,x,z)\wedge\mathsf{Ap}(f,x)=_{\mathsf{N}}U(z)).$

As a consequence, their desired constructive foundation should have been
consistent with AC and CT. But this consistency requirement is a very strong
property since it rules out the validity of extensional principles used in
everyday practice of mathematics, including the extensional equality of
functions, beside not being satisfied by most constructive foundations in the
literature. Therefore, the authors of [MS05] ended up in defining a
constructive foundation as a two-level system consisting of an extensional
level, formulated in a language close to that of informal mathematics and
validating all the desired extensional properties, and of an intensional level
consistent with the axiom of choice AC and CT where the extensional level is
interpreted via a quotient model. The system MF is an example of this notion
of two-level constructive foundation. The proof that its intensional level is
consistent with AC and CT was given only recently in [IMMS18].

The purpose of this paper is two-fold. First we present an extension MFind of
MF with the inductive definitions sufficient to inductively generate formal
topologies and necessary to define inductively generated basic covers which
constitute a predicative presentation of suplattices (see [BS06, CMS13]). This
is motivated by the fact that in [CSSV03] the problem of generating formal
topologies inductively is reduced to that of generating suplattices in an
inductive way. As MF also MFind is presented as a two-level system obtained by
extending each level of MF with rules generating basic covers inductively. In
particular, the rules of inductively generated basic covers added to mTT to
form the intensional level mTTind are driven by those of well-founded sets in
Martin-Löf’s type theory in [NPS90] without assuming generic well-founded sets
or ordinals as done for the formalization of such covers within type theory in
[CSSV03, Val07].

Then our main purpose is to show that the extension MFind of MF is also an
example of the mentioned notion of two-level constructive foundation in
[MS05]. To this aim the key result shown here is that its intensional level
mTTind is consistent with AC and CT.

In order to meet our goal we produce a realizability semantics for mTTind by
extending the one used to show the consistency of the intensional level of MF
with AC+CT in [IMMS18], which in turn extends Kleene realizability
interpretation of intuitionistic arithmetic.

A main novelty of the semantics in this paper is that it is formalized in a
constructive theory as the (generalized) predicative set theory CZF+REA,
namely Aczel’s constructive Zermelo-Fraenkel set theory extended with the
regular extension axiom REA.

To this purpose it is crucial to modify the realizability interpretation in
[IMMS18] in the line of the realizability interpretations of Martin-Löf type
theories in extensions of Kripke-Platek set theory introduced in [Ra93]
(published as [GR94]).

Therefore, contrary to the semantics in [IMMS18], which was formalized in a
classical theory as Feferman’s theory of non-iterative fixpoints
$\widehat{ID}_{1}$, here we produce a proof that mTTind, and hence mTT, is
constructively consistent with AC+CT.

As in [IMMS18], we actually build a realizability model for a fragment of
Martin-Löf’s type theory [NPS90], called MLttind, where mTTind extended with
the axiom of choice can be easily interpreted.

As it turns out, $\mathbf{CZF}+\mathbf{REA}$ and MLttind possess the same
proof-theoretic strength.

In the future we intend to further extend our realizability to model mTTind
enriched with coinductive definitions to represent Sambin’s generated Positive
Topologies. Another possible line of investigation would be to employ our
realizability semantics to establish the consistency strength of mTTind or of
the extension of mTT with particular inductively generated topologies, like
that of the Baire space.

##  2 The extension MFind with inductively generated formal topologies

Here we describe the extension MFind of MF capable of formalizing all the
examples of formal topologies defined by inductive methods introduced in
[CSSV03].

In that paper, the problem of generating the minimal formal topology which
satisfies some given axioms is reduced to show how to generate a complete
suplattice in terms of an infinitary relation called basic cover relation

$a\lhd V$

between elements $a$ of a set $A$, thought of as basic opens, and subsets $V$
of $A$, meaning that the basic open $a$ is covered by the union of basic opens
in the subset $V$.

Then the elements of the generated suplattice would be fixpoints of the
associated closure operator

$\lhd(-):\mathcal{P}(A)\ \longrightarrow\ \mathcal{P}(A)$

defined by putting

$\lhd(V)\,\equiv\,\\{\ x\in A\ \mid\ x\lhd V\ \\}$

These suplattices are complete with respect to families of subsets indexed
over a set.

Furthermore, a formal topology is defined as a basic cover relation satisfying
a convergence property and a positivity predicate (see [CSSV03, MV04, BS06,
CMS13]). Indeed in this case the resulting complete suplattice of
$\lhd$-fixpoints actually forms a predicative locale which is overt (or open
in the original terminology by Joyal and Tierney) for the presence of the
positivity predicate.

The tool of basic covers appears to be the only one available in the
literature to represent complete suplattices in most-relevant predicative
constructive foundations including Aczel’s CZF, Martin-Löf’s type theory and
also MF.

The reason is that there exist no non-trivial examples of complete suplattices
that form a set in such predicative foundations (see [Cur10]). As a
consequence, there exist no non-trivial examples of locales which form a set
and the approach of formal topology based on a cover relation seems to be
compulsory (see also [MS13]) when developing topology in a constructive
predicative foundation, especially in MF.

In [CSSV03] it was introduced a method for generating basic covers inductively
starting from an indexed set of axioms, called axiom set. Such a method allows
to generate a formal topology inductively when the basic cover relation $\lhd$
is defined on a preordered set $(A,\leq)$ and it is generated by an axiom set
satisfying a so called localization condition which refers to the preorder
defined on $A$. A general study of the relation between basic covers and
formal covers including their inductive generation is given in [CMS13].

In the following we describe a suitable extension of MF capable of
representing inductively generated basic covers, and hence also formal
topologies.

We start by describing how to enrich the extensional level emTT of MF in
[Mai09] with such inductive basic covers. The reason is that the language of
emTT is more apt to represent the topological axioms given that it is very
close to that of everyday mathematical practice (with proof-irrelevance of
propositions and an encoding of the usual language of first-order arithmetic
and of subsets of a set, see [Mai09]).

We recall that in emTT we have four kinds of types, namely collections, sets,
propositions and small propositions according to the following subtyping
relations:

small propositionssetspropositionscollections

where collections include the power-collection ${\mathcal{P}}(A)$ (which is
not in general a set!) of any set $A$ and small propositions are defined as
those propositions closed under intuitionistic connectives, propositional
equality and quantifiers restricted to sets.

We first extend emTT with new primitive small propositions

$a\triangleleft_{I,C}V\ prop_{s}$

expressing that the basic open $a$ is covered by the union of basic opens in
$V$ for any $a$ element of a set $A$, $V$ subset of $A$, assuming that the
basic cover is generated by a family of (open) subsets of $A$ indexed on a
family of sets $I(x)\ set\ [x\in A]$ and represented by

$C(x,j)\in{\mathcal{P}}(A)\ [x\in A,j\in I(x)].$

Recall from [Mai09] that in emTT we can define a subset membership

$a\,\epsilon\,V$

between a subset $V\in{\mathcal{P}}(A)$ and an element $a$ of a set $A$. Note
that while the membership $a\in A$ is primitive in emTT and expresses that $A$
is the type of $a$, the membership $\epsilon$ essentially expresses a relation
between subsets of $A$ and its elements.

The precise rules extending emTT to form a new type system emTTind are the
following:

Rules of inductively generated basic covers in emTTind

$\begin{array}[]{l}\mbox{\rm F-$\triangleleft$}\
\displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \ \ I(x)\ set\ [x\in A]\ \ \
C(x,j)\in{\mathcal{P}}(A)\ \ [x\in A,j\in I(x)]\\\ V\in{\mathcal{P}}(A)\qquad
a\in A\end{array}}{\displaystyle a\triangleleft_{I,C}V\ prop_{s}}}\\\\[20.0pt]
\mbox{\rm rf-$\triangleleft$}\displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \
\ I(x)\ set\ [x\in A]\ \ \ C(x,j)\in{\mathcal{P}}(A)\ \ [x\in A,j\in I(x)]\\\
V\in{\mathcal{P}}(A)\qquad\qquad a\,\epsilon\,V\
true\end{array}}{\displaystyle a\triangleleft_{I,C}V\ true}}\\\ \\\ \mbox{\rm
tr-$\triangleleft$}\ \displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \ \ I(x)\
set\ [x\in A]\ \ \ C(x,j)\in{\mathcal{P}}(A)\ \ [x\in A,j\in I(x)]\\\ a\in
A\qquad i\in I(a)\qquad\qquad V\in{\mathcal{P}}(A)\\\ (\forall_{y\in A})\ (\
y\,\epsilon\,C(a,i)\ \rightarrow\ y\triangleleft_{I,C}V\ )\
true\end{array}}{\displaystyle a\triangleleft_{I,C}V\ true}}\\\\[20.0pt]
\mbox{ind-$\triangleleft$}\displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \ \
I(x)\ set\ [x\in A]\ \ \ C(x,j)\ \in{\mathcal{P}}(A)\ \ [x\in A,j\in I(x)]\\\
P(x)\ prop\ [x\in A]\qquad V\in{\mathcal{P}}(A)\qquad\mathsf{cont}(V,P)\
true\\\ a\in A\qquad a\lhd_{I,C}V\ true\end{array}}{P(a)\ true\ }}\end{array}$

where

$\begin{array}[]{rl}\mathsf{cont}(V,P)\ \equiv&\forall_{x\in A}\ (\
x\,\epsilon\,V\ \rightarrow\ P(x)\ )\\\ &\qquad\wedge\ \forall_{x\in A}\ \ (\
\forall_{j\in I(x)}\ \forall_{y\in A}\ (y\,\epsilon\,C(x,j)\ \rightarrow\
P(y)\ )\ \rightarrow\ P(x)\ )\end{array}$

where above we adopted the convention of writing $\phi\ true$ for a
proposition $\phi$ instead of $\mathsf{true}\in\phi$ as in [Mai09].

The first rule expresses the formation of the small propositional function
representing a basic cover, the second one expresses a form of reflexivity
since it states that any element of a subset $V$ is covered by it, the third
one expresses a form of transitivity property applied to open subsets of the
axiom set and the fourth one is a form of induction on the generated basic
cover.

A main example of inductively generated cover formalizable in emTTind is that
of the topology of the real line, represented by Joyal’s inductive formal
cover $\lhd_{r}$ of Dedekind real numbers defined on the set
$\mathbb{Q}\,\times\,\mathbb{Q}$ (which acts as $A$ in the rules above) where
$\mathbb{Q}$ is the set of rational numbers. This formal cover is generated by
a family of open subsets $C(\langle p,q\rangle,j)$ for $\langle
p,q\rangle\in\mathbb{Q}\,\times\,\mathbb{Q}$ and $j\in I(\langle p,q\rangle)$
where $I(\langle p,q\rangle)$ is the set of indexes of the following rules:

${\displaystyle\frac{q\leq p}{\langle p,q\rangle\lhd_{r}U}}$ | ${\displaystyle\frac{p^{\prime}\leq p<q\leq q^{\prime}\qquad\langle p^{\prime},q^{\prime}\rangle\lhd_{r}U}{\langle p,q\rangle\lhd_{r}U}}$
---|---
${\displaystyle\frac{p\leq r<s\leq q\qquad\langle p,s\rangle\lhd_{r}U\quad\langle r,q\rangle\lhd_{r}U}{\langle p,q\rangle\lhd_{r}U}}$ | $\ {\displaystyle\frac{\mathsf{wc}(\langle p,q\rangle)\lhd_{r}U}{\langle p,q\rangle\lhd_{r}U}}$

where in the last axiom we have used the abbreviation

$\mathsf{wc}(\langle p,q\rangle)\equiv\\{\,\langle
p^{\prime},q^{\prime}\rangle\in\mathbb{Q}\,\times\,\mathbb{Q}\ \mid\
p<p^{\prime}<q^{\prime}<q\\}$

($\mathsf{wc}$ stands for ‘well-covered’).

Some relevant applications regarding the formal topology of the real line are
discussed for instance in [CN95, Pal05, MS13].

There exists also an alternative presentation of the formal topology of the
real line due to T. Coquand in [CN95] which makes this topology formalizable
in emTT, and hence in MF. The reason is that its cover can be defined in terms
of another inductive cover generated by a finite set of axioms and
formalizable in emTT by using a characterization of inductive formal
topologies given in [Val07] and the crucial fact that in emTT we can define
sequences of subsets by recursion on natural numbers.

Other relevant examples of inductively generated formal topologies are the
topologies of Cantor and Baire spaces. These are instances of the more general
notion of tree formal topology relative to a set $E$ represented by the cover
$\triangleleft_{tr(E)}$ on the set $\mathsf{List}(E)$ of lists of $E$
generated by a family of open subsets $C(l,j)$ for a list $l$ and $j\in I(h)$
where $I(h)$ is the set of indexes of the following rules:

$\displaystyle{\frac{s\sqsubseteq l\qquad
l\triangleleft_{tr(E)}V}{\displaystyle s\triangleleft_{tr(E)}V}}$
$\displaystyle{\frac{\forall{x\in E}\ \
[l,x]\triangleleft_{tr(E)}V}{\displaystyle l\triangleleft_{tr(E)}V}}$
---

where $s\sqsubseteq l$ means that the list $l$ is an initial segment of the
list $s$, formally defined as $s\sqsubseteq
l\,\equiv\,\exists_{t\in\mathsf{List}(E)}\,\mathsf{Id}(\mathsf{List}(E),s,[l,t])$
and $[l,t]$ is the concatenation of the list $l$ with $t$.

Then the formal topology of the Cantor space is the tree topology
$\triangleleft_{tr(\\{0,1\\})}$ when $E$ is the boolean set $\\{0,1\\}$ and
the formal topology of the Baire space is the tree topology
$\triangleleft_{tr(\mathsf{N})}$ when $E$ is the set $\mathsf{N}$ of natural
numbers.

The formal topology of the Baire space is a genuine example of inductively
generated cover definable in emTTind but not in emTT contrary to that of the
Cantor space which is definable in emTT:

######  Proposition 1.

The formal topology of the Baire space $\triangleleft_{tr(\mathsf{N})}$ is not
formalizable in emTT, and hence in MF, while the formal topology of Cantor
space $\triangleleft_{tr(\\{0,1\\})}$ is formalizable there.

######  Proof 2.1.

The formal topology of the Cantor space $\triangleleft_{tr(\\{0,1\\})}$ is
formalizable in emTT thanks to the characterization of
$\triangleleft_{tr(\\{0,1\\})}(V)$ for a subset $V$ of
$\mathsf{List}(\\{0,1\\})$ in [Val07], beside the fact that in emTT we can
define sequences of subsets of a set by recursion on natural numbers.

Instead the formal topology of the Baire space
$\triangleleft_{tr(\mathsf{N})}$ is not formalizable in emTT for the following
reason. From [Mai09] we know that emTT can be translated in $\mathbf{CZF}$ by
preserving the meaning of propositions and sets. Now if the topology
$\triangleleft_{tr(\mathsf{N})}$ were formalizable in emTT then it would be
formalizable also in $\mathbf{CZF}$ but from [CR12] we know that this is not
possible.

More generally, all the finitary topologies in [CSSV03] are definable in emTT,
and hence in MF, in a way similar to what done to formalize the formal
topology of the Cantor space.

It is worth noting that different presentations of basic covers may yield to
the same complete suplattice. For example, any complete suplattice presented
by (the collection of fixpoints associated to) a basic cover $\lhd_{I,C}$ on a
quotient set $B/R$, can be equivalently presented by a cover on the set $B$
itself which behaves like $\lhd_{I,C}$ but in addition it considers as equal
opens those elements which are related by $R$.

In order to properly show this fact, which will motivate some definitions in
the next section, we define a correspondence between subsets of $B/R$ and
subsets of $B$ as follows:

######  Definition 2.2.

In emTTind, given a quotient set $B/R$, for any subset $W\in\mathcal{P}(B/R)$
we define

$\mathsf{es}(W)\,\equiv\,\\{\ b\in B\ \mid\ [b]\,\epsilon\,W\ \\}$

and given any $V\in\mathcal{P}(B)$ we define $\mathsf{es}^{-}(V)\,\equiv\,\\{\
z\in B/R\ \mid\ \exists_{b\in B}\ (\ b\,\epsilon\,V\ \wedge\ z=_{B/R}[b]\
)\\}$.

######  Definition 2.3.

Given an axiom set represented by a set $A\,\equiv\,B/R$ with $I(x)\ set\
[x\in A]$ and $C(x,j)\in{\mathcal{P}}(A)\ \ [x\in A,j\in I(x)]$, we define a
new axiom set as follows:

$\begin{array}[]{l}A^{R}\,\equiv\,B\qquad\qquad I^{R}(x)\,\equiv\,I([x])+\
(\Sigma y\in B)\ R(x,y)\qquad\qquad\mbox{ for }x\in B\\\ \end{array}$

where $C^{R}(b,j)$ is the formalization of

$C^{R}(b,j)\,\equiv\,\begin{cases}\mathsf{es}(\,C([b],j)\,)&\mbox{ if }j\in
I([b])\\\ \\{\,\pi_{1}(j)\,\\}&\mbox{ if }j\in(\Sigma y\in B)\ R(b,y)\\\
\end{cases}$

for $b\in B$ and $j\in I^{R}(x)$.

We then call $\lhd_{I,C}^{R}$ the inductive basic cover generated from this
axiom set.

It is then easy to check that

######  Lemma 2.4.

For any axiom set in emTTind represented by a set $A\,\equiv\,B/R$ with $I(x)\
set\ [x\in A]$ and $C(x,j)\in{\mathcal{P}}(A)\ \ [x\in A,j\in I(x)]$, the
suplattice defined by $\lhd_{I,C}$ is isomorphic to that defined by
$\lhd_{I,C}^{R}$ by means of an isomorphism of suplattices.

######  Proof 2.5.

It is immediate to check that for any subset $W$ of $B/R$ which is a fixpoint
for $\lhd_{I,C}$ the subset $\mathsf{es}(W)$ is a fixpoint for
$\lhd_{I,C}^{R}$ and that, conversely, for any subset $V$ of $B$ which is a
fixpoint for $\lhd_{I,C}^{R}$ the subset $\mathsf{es}^{-}(V)$ is a fixpoint
for $\lhd_{I,C}$. Moreover, this correspondence preserves also the suprema
defined as in [CMS13]. Alternatively, one could check that the relation
$z\,F\,b\,\equiv\ \mathsf{Id}(\,B/R\,,\,z\,,\,[b]\,)$, namely the
propositional equality of $z$ with $[b]$, defines a basic cover isomorphism in
the sense of [CMS13] between the basic cover $\lhd_{I,C}$ and
$\lhd_{I,C}^{R}$.

###  2.1 The intensional level mTTind

Here we describe the extension mTTind of the intensional level mTT of MF
capable of interpreting the extension emTTind.

We recall that in mTT we have the same four kinds of types as in emTT with the
difference that in mTT power-collections of sets are replaced by the existence
of a collection of small propositions $\mathsf{prop_{s}}$ and function
collections $A\rightarrow\mathsf{prop_{s}}$ for any set $A$. Such collections
are enough to interpret power-collections of sets in emTT within a quotient
model of dependent extensional types built over mTT, as explained in [Mai09].

In order to complete emTTind into a two-level foundation according to the
requirements in [MS05], we need to define an extension of mTT with a proof-
relevant version of the inductively generated basic covers of emTTind.

To this purpose we defined the extension mTTind by extending mTT in [Mai09]
with new small propositions

$a\triangleleft_{I,C}V\ prop_{s}$

and corresponding new proof-term constructors associated to them so that
judgements asserting that some proposition is true in emTTind are turned into
judgements of mTTind producing a proof-term of the corresponding proposition.

We recall that in mTTind as in mTT in [Mai09] the universe of small
propositions is defined in the version à la Russell. A version of mTT with the
universe of small propositions à la Tarski can be found in [MM16].

It is worth noting that the equality rules of the inductive basic covers are
driven by those of well-founded sets in Martin-Löf’s type theory in [NPS90]
without assuming generic well-founded sets or ordinals as in the
representations given in [CSSV03, Val07]. However, in accordance with the idea
that proof-terms of propositions of mTT represent just a constructive
rendering of the proofs of propositions in emTT, we do restrict the
elimination rules of inductive basic covers to act toward propositions which
do not depend on their proof-terms, since these proof-terms do not appear at
the extension level emTT.

When expressing the rules of inductive basic covers we use the abbreviation

$a\,\epsilon\,V\qquad\mbox{ to mean }\qquad\mathsf{Ap}(\,V\,,\,a\,)$

for any set $A$, any small propositional function $V\in
A\rightarrow\mathsf{prop_{s}}$ and any element $a\in A$.

The precise rules of inductive basic covers extending mTT to form a new type
system mTTind are the following:

Rules of inductively generated basic covers in mTTind

$\begin{array}[]{l}\mbox{\rm F-$\triangleleft$}\
\displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \ \ I(x)\ set\ [x\in A]\ \ \
C(x,j)\in A\rightarrow\mathsf{prop_{s}}\ [x\in A,j\in I(x)]\\\ V\in
A\rightarrow\mathsf{prop_{s}}\qquad a\in A\end{array}}{\displaystyle
a\triangleleft_{I,C}V\ prop_{s}}}\\\\[20.0pt] \mbox{\rm rf-$\triangleleft$}\
\displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \ \ I(x)\ set\ [x\in A]\ \ \
C(x,j)\in A\rightarrow\mathsf{prop_{s}}\ \ [x\in A,j\in I(x)]\\\ V\in
A\rightarrow\mathsf{prop_{s}}\qquad a\in A\qquad r\in
a\,\epsilon\,V\end{array}}{\displaystyle\mathsf{rf}(a,r)\in
a\triangleleft_{I,C}V}}\\\\[20.0pt] \end{array}$ $\begin{array}[]{l}\mbox{\rm
tr-$\triangleleft$}\ \displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \ \ I(x)\
set\ [x\in A]\ \ \ C(x,j)\in A\rightarrow\mathsf{prop_{s}}\ [x\in A,j\in
I(x)]\\\ V\in A\rightarrow\mathsf{prop_{s}}\qquad\ \ a\in A\qquad i\in I(a)\\\
r\in\forall_{x\in A}\ (\ x\,\epsilon\,C(a,i)\rightarrow x\triangleleft_{I,C}V\
)\end{array}}{\displaystyle\mathsf{tr}(a,i,r)\in a\triangleleft_{I,C}V\
}}\\\\[20.0pt]
\mbox{ind-$\triangleleft$}\displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \ \
I(x)\ set\ [x\in A]\ \ \ C(x,j)\ \in A\ \rightarrow\mathsf{prop_{s}}\ \ [x\in
A,j\in I(x)]\\\\[5.0pt] P(x)\ prop\ [x\in A]\qquad V\in A\ \rightarrow\
\mathsf{prop_{s}}\\\\[5.0pt] a\in A\qquad m\in a\lhd_{I,C}V\\\\[5.0pt]
q_{1}(x,z)\in P(x)\ [x\in A,z\in x\,\epsilon\,V]\\\\[5.0pt] q_{2}(y,j,f)\in
P(y)\ [y\in A,j\in I(y),f\in\forall_{z\in A}\ (\ z\,\epsilon\,C(y,j)\
\rightarrow\ P(z)\ )]\end{array}}{\mathsf{ind}(m,q_{1},q_{2})\in
P(a)}}\\\\[20.0pt] \end{array}$
$\begin{array}[]{l}\mbox{C${}_{1}$-ind}\displaystyle{\frac{\begin{array}[]{l}A\
set\ \ \ \ I(x)\ set\ [x\in A]\ \ \ C(x,j)\ \in A\ \rightarrow\
\mathsf{prop_{s}}\ \ [x\in A,j\in I(x)]\\\\[5.0pt] P(x)\ prop\ [x\in A]\qquad
V\in A\ \rightarrow\mathsf{prop_{s}}\\\\[5.0pt] a\in A\qquad r\in
a\,\epsilon\,V\\\\[5.0pt] q_{1}(x,z)\in P(x)\ [x\in A,z\in
x\,\epsilon\,V]\\\\[5.0pt] q_{2}(y,j,f)\in P(y)\ [y\in A,j\in
I(y),f\in\forall_{z\in A}\ (\ z\,\epsilon\,C(y,j)\ \rightarrow\ P(z)\
)]\end{array}}{\mathsf{ind}(\mathsf{rf}(a,r),q_{1},q_{2})=q_{1}(a,r)\in
P(a)}}\\\\[20.0pt]
\mbox{C${}_{2}$-ind}\displaystyle{\frac{\begin{array}[]{l}A\ set\ \ \ \ I(x)\
set\ [x\in A]\ \ \ C(x,j)\ \in A\ \rightarrow\ \mathsf{prop_{s}}\ \ [x\in
A,j\in I(x)]\\\\[5.0pt] P(x)\ prop\ [x\in A]\qquad V\in A\
\rightarrow\mathsf{prop_{s}}\\\\[5.0pt] a\in A\qquad i\in I(a)\qquad
r\in\forall_{x\in A}\ (\ x\,\epsilon\,C(a,i)\ \rightarrow\
x\triangleleft_{I,C}V\ )\\\\[5.0pt] q_{1}(x,z)\in P(x)\ [x\in A,z\in
x\,\epsilon\,V]\\\\[5.0pt] q_{2}(y,j,f)\in P(y)\ [y\in A,j\in
I(y),f\in\forall_{z\in A}\ (\ z\,\epsilon\,C(y,j)\ \rightarrow\ P(z)\
)]\end{array}}{\mathsf{ind}(\mathsf{tr}(a,i,r),q_{1},q_{2})=q_{2}(\,a\,,i\,,\,\lambda
z.\lambda
w.\,\mathsf{ind}(\,\mathsf{Ap}(\mathsf{Ap}(r,z),w)\,,q_{1},q_{2})\,)\in
P(a)}}\end{array}$

Note that the cover relation preserves extensional equality of subsets
represented as small propositional functions thanks to the induction
principle:

######  Lemma 2.6.

For any axiom set in mTTind on a set $A$ with $I(x)\ set\ [x\in A]$ and
$C(x,j)\in A\ \rightarrow\mathsf{prop_{s}}\ \ [x\in A,j\in I(x)]$ and for any
propositional functions $V_{1}\in A\ \rightarrow\mathsf{prop_{s}}$ and
$V_{2}\in A\ \rightarrow\mathsf{prop_{s}}$, there exists a proof-term

$q\in V_{1}=_{ext}V_{2}\ \rightarrow\
a\triangleleft_{I,C}V_{1}=_{ext}a\triangleleft_{I,C}V_{2}$

where for any small propositional functions $W_{1}$ and $W_{2}$ on a set $A$
we use the following abbreviation

$W_{1}=_{ext}W_{2}\,\equiv\,\forall_{x\in A}\ (\ W_{1}(x)\ \leftrightarrow\
W_{2}(x)\ )$

Recall that the interpretation of emTT in mTT in [Mai09] interprets a set $A$
as an extensional quotient defined in mTT as a set $A^{J}$ of mTT, called
support, equipped with an equivalence relation $=_{A^{J}}$ over $A^{J}$, as
well as families of sets are interpreted as families of extensional sets
preserving the equivalence relations in their telescopic contexts. Now, lemma
2.4 suggests that we can interpret an inductive basic cover on a set $A$ of
emTTind within mTTind as an inductive cover of mTTind on the support $A^{J}$
by enriching the interpretation of the axiom-set in mTTind with the
equivalence relation $=^{A^{J}}$ in a similar way to definition 2.3 as
follows:

######  Definition 2.7.

For any axiom set in mTTind represented by a set $A$ with $I(x)\ set\ [x\in
A]$ and $C(x,j)\in A\ \rightarrow\mathsf{prop_{s}}\ \ [x\in A,j\in I(x)]$ and
for any given equivalence relation $x=_{A}y\in\mathsf{prop_{s}}\ [x\in A,y\in
A]$ turning $A$ into an extensional set as well as the family of set $I(x)\
set\ [x\in A]$ and propositional functions $C(x,j)\in A\
\rightarrow\mathsf{prop_{s}}\ \ [x\in A,j\in I(x)]$ into an extensional family
of sets and extensional propositional functions preserving $=_{A}$ according
to the definitions in [Mai09], we define a new axiom set as follows

$\begin{array}[]{l}A^{=_{A}}\,\equiv\,A\qquad\qquad
I^{=_{A}}(x)\,\equiv\,I(x)+(\Sigma y\in A)(x=_{A}y)\qquad\qquad\mbox{ for
}x\in A\\\ \end{array}$

where $C^{=_{A}}(a,j)$ is the formalization of

$C^{=_{A}}(a,j)\,\equiv\,\begin{cases}C(a,j)\,&\mbox{ if }j\in I(a)\\\
\\{\,\pi_{1}(j)\,\\}&\mbox{ if }j\in(\Sigma y\in A)(a=_{A}y)\\\ \end{cases}$

for $a\in A$ and $j\in I^{=_{A}}(x)$.

We then call $\lhd_{I,C}^{=_{A}}$ the inductive basic cover generated from
this axiom set.

We are now ready to interpret emTTind in the quotient model over mTTind built
as in [Mai09]:

######  Proposition 2.

The interpretation of emTT in mTT in [Mai09] extends to an interpretation of
emTTind in mTTind by interpreting an inductive basic cover $a\lhd_{I,C}V$ for
$a\in A$ and $V\in{\mathcal{P}}(A)$ as the inductive basic cover
$\lhd_{I^{J},C^{J}}^{=_{A^{J}}}$ in mTTind over the support $A^{J}$ of the
interpretation of $A$.

######  Proof 2.8.

It follows from the proof given in [Mai09] after checking that the inductive
basic cover $\lhd_{I^{J},C^{J}}^{=_{A^{J}}}$ is an extensional proposition
over the extensional set interpreting $A$ and over the interpretation of
${\mathcal{P}}(A)$ in the sense of [Mai09].

##  3 The fragment MLttind of intensional Martin-Löf’s type theory with
inductive basic covers

We here briefly describe the theory MLttind obtained by adding the rules of
inductive basic covers to the first order fragment of intensional Martin-Löf’s
type theory in [NPS90] with one universe.

This theory interprets mTTind as soon as propositions are identified with sets
following the Curry-Howard correspondence in [NPS90]. In accordance with this
propositions as sets interpretation, which is a pecularity of Martin-Löf’s
type theory, contrary to mTTind in MLttind we strengthen the elimination rule
of inductive basic covers to act towards sets depending on their proof-terms
according to inductive generation of types in Martin-Löf’s type theory.

As a consequence the interpretation of mTTind into MLttind also validates the
axiom of choice AC as formulated in the introduction.

Therefore in order to show the consistency of mTTind with AC+CT (with CT
formulated as in the introduction) it is enough to show the consistency of
MLttind extended with (the translation of) CT.

Here we adopt the notation of types and terms within the first order fragment
MLtt1 of intensional Martin-Löf’s type theory with one universe $U_{0}$ à la
Tarski in [IMMS18] and we just describe the rule of inductive basic covers
added to it.

To this purpose we add to MLtt1 the code

$a\,\widehat{\triangleleft}_{s,i,c}\,v\in U_{0}\qquad\mbox{ for
}a\in\mathsf{T}(s)\mbox{ and }v\in\mathsf{T}(s)\ \rightarrow\ U_{0}$

meaning that the element $a$ of a small set $\mathsf{T}(s)$ represented by the
code $s\in U_{0}$ is covered by the subset $v$ represented by a small
propositional function from $\mathsf{T}(s)$ to the (large) set of small
propositions identified with $U_{0}$ by the propositions-as-sets
correspondence.

Moreover, we use the abbreviations

$a\triangleleft_{s,i,c}v\,\equiv\,\mathsf{T}(a\,\widehat{\triangleleft}_{s,i,c}\,v)\qquad\qquad
x\,\epsilon\,y\,\equiv\,\mathsf{T}(\mathsf{Ap}(y,x))$

and the notation

$\mathsf{axcov}(s,i,c)$

to abbreviate the following judgements

$s\in U_{0}\ \ \ \ i(x)\in U_{0}\ [x\in\mathsf{T}(s)]\ \ \
c(x,y)\in\mathsf{T}(s)\rightarrow U_{0}\
[x\in\mathsf{T}(s),y\in\mathsf{T}(i(x))]$

Then, the precise rules of inductive basic covers extending MLtt1 to form a
new type system MLttind are the following:

Rules of inductively generated basic covers in MLttind

$\begin{array}[]{l}\mbox{\rm F-$\triangleleft$}\
\displaystyle{\frac{\begin{array}[]{l}\mathsf{axcov}(s,i,c)\qquad
a\in\mathsf{T}(s)\qquad v\in\mathsf{T}(s)\rightarrow
U_{0}\end{array}}{\displaystyle a\,\widehat{\triangleleft}_{s,i,c}\,v\in
U_{0}}}\\\ \\\\[20.0pt] \end{array}$ $\begin{array}[]{l}\mbox{\rm
rf-$\triangleleft$}\
\displaystyle{\frac{\begin{array}[]{l}\mathsf{axcov}(s,i,c)\qquad
a\in\mathsf{T}(s)\qquad v\in\mathsf{T}(s)\rightarrow U_{0}\qquad\ r\in
a\,\epsilon\,v\end{array}}{\displaystyle\mathsf{rf}(a,r)\in
a\triangleleft_{s,i,c}v}}\\\ \\\\[20.0pt] \end{array}$
$\begin{array}[]{l}\mbox{\rm tr-$\triangleleft$}\
\displaystyle{\frac{\begin{array}[]{l}\mathsf{axcov}(s,i,c)\qquad
a\in\mathsf{T}(s)\qquad j\in\mathsf{T}(i(a))\qquad
v\in\mathsf{T}(s)\rightarrow U_{0}\\\ r\in(\Pi
z\in\mathsf{T}(s))(z\,\epsilon\,c(a,j)\rightarrow
z\triangleleft_{s,i,c}v)\end{array}}{\displaystyle\mathsf{tr}(a,j,r)\in
a\triangleleft_{s,i,c}v}}\\\ \\\\[10.0pt] \end{array}$
$\begin{array}[]{l}\mbox{ind-$\triangleleft$}\displaystyle{\frac{\begin{array}[]{l}\mathsf{axcov}(s,i,c)\\\
v\in\mathsf{T}(s)\rightarrow U_{0}\qquad P(x,u)\ type\ [x\in\mathsf{T}(s),u\in
x\triangleleft_{s,i,c}v]\\\ a\in\mathsf{T}(s)\qquad m\in
a\triangleleft_{s,i,c}v\\\ q_{1}(x,w)\in P(x,\mathsf{rf}(x,w))\
[x\in\mathsf{T}(s),w\in x\,\epsilon\,v]\\\\[3.0pt] q_{2}(x,h,k,f)\in
P(x,\mathsf{tr}(x,h,k))\\\
\quad\qquad[x\in\mathsf{T}(s),h\in\mathsf{T}(i(x)),\\\ \qquad\qquad k\in(\Pi
z\in\mathsf{T}(s))(z\,\epsilon\,c(x,h)\rightarrow z\triangleleft_{s,i,c}v),\\\
\qquad\qquad\qquad f\in(\Pi z\in\mathsf{T}(s))(\Pi u\in
z\,\epsilon\,c(x,h))\,P(z,\mathsf{Ap}(\mathsf{Ap}(k,z),u))]\end{array}}{\mathsf{ind}(m,q_{1},q_{2})\in
P(a,m)}}\\\\[20.0pt] \end{array}$
$\begin{array}[]{l}\mbox{C${}_{1}$-ind-$\triangleleft$}\displaystyle{\frac{\begin{array}[]{l}\mathsf{axcov}(s,i,c)\\\
v\in\mathsf{T}(s)\rightarrow U_{0}\qquad P(x,u)\ type\ [x\in\mathsf{T}(s),u\in
x\triangleleft_{s,i,c}v]\\\ a\in\mathsf{T}(s)\qquad r\in a\,\epsilon\,v\\\
q_{1}(x,w)\in P(x,\mathsf{rf}(x,w))\ [x\in\mathsf{T}(s),w\in
x\,\epsilon\,v]\\\\[5.0pt] q_{2}(x,h,k,f)\in P(x,\mathsf{tr}(x,h,k))\\\
\quad\qquad[x\in\mathsf{T}(s),h\in\mathsf{T}(i(x)),\\\ \qquad\qquad k\in(\Pi
z\in\mathsf{T}(s))(z\,\epsilon\,c(x,h)\rightarrow x\triangleleft_{s,i,c}v),\\\
\qquad\qquad\qquad f\in(\Pi z\in\mathsf{T}(s))(\Pi u\in
z\,\epsilon\,c(x,h))\,P(z,\mathsf{Ap}(\mathsf{Ap}(k,z),u))]\end{array}}{\mathsf{ind}(\mathsf{rf}(a,r),q_{1},q_{2})=q_{1}(a,r)\in
P(a,\mathsf{rf}(a,r))}}\\\\[20.0pt] \end{array}$
$\begin{array}[]{l}\mbox{C${}_{2}$-ind-$\triangleleft$}\displaystyle{\frac{\begin{array}[]{l}\mathsf{axcov}(s,i,c)\\\
v\in\mathsf{T}(s)\rightarrow U_{0}\qquad P(x,u)\ type\ [x\in\mathsf{T}(s),u\in
x\triangleleft_{s,i,c}v]\\\ a\in\mathsf{T}(s)\qquad j\in\mathsf{T}(i(a))\qquad
r\in(\Pi z\in\mathsf{T}(s))(z\,\epsilon\,c(a,j)\rightarrow
z\triangleleft_{s,i,c}v)\\\ q_{1}(x,w)\in P(x,\mathsf{rf}(x,w))\
[x\in\mathsf{T}(s),w\in x\,\epsilon\,v]\\\\[5.0pt] q_{2}(x,h,k,f)\in
P(x,\mathsf{tr}(x,h,k))\\\
\quad\qquad[x\in\mathsf{T}(s),h\in\mathsf{T}(i(x)),\\\ \qquad\qquad k\in(\Pi
z\in\mathsf{T}(s))(z\,\epsilon\,c(x,h)\rightarrow z\triangleleft_{s,i,c}v),\\\
\qquad\qquad\qquad f\in(\Pi z\in\mathsf{T}(s))(\Pi u\in
z\,\epsilon\,c(x,h))P(z,\mathsf{Ap}(\mathsf{Ap}(k,z),u))]\end{array}}{\mathsf{ind}(\mathsf{tr}(a,j,r),q_{1},q_{2})=q_{2}(a,j,r,\lambda
z.\lambda u.\mathsf{ind}(\mathsf{Ap}(\mathsf{Ap}(r,z),u),q_{1},q_{2}))\in
P(a,\mathsf{tr}(a,j,r))}}\\\\[20.0pt] \end{array}$

A crucial difference from the ordinary versions of Martin-Löf’s type theory is
that for MLttind we postulate just the replacement rule repl)

$\begin{array}[]{l}\mbox{repl)}\ \
\displaystyle{\frac{\displaystyle\begin{array}[]{l}c(x_{1},\dots,x_{n})\in
C(x_{1},\dots,x_{n})\ \ [\,x_{1}\in A_{1},\,\dots,\,x_{n}\in
A_{n}(x_{1},\dots,x_{n-1})\,]\\\\[2.0pt] a_{1}=b_{1}\in A_{1}\ \dots\
a_{n}=b_{n}\in A_{n}(a_{1},\dots,a_{n-1})\end{array}}{\displaystyle
c(a_{1},\dots,a_{n})=c(b_{1},\dots,b_{n})\in
C(a_{1},\dots,a_{n})}}\end{array}$

in place of the usual congruence rules which would include the $\xi$-rule in
accordance with the rules of mTT in [Mai09], and hence of mTTind.

The motivation for this restriction in mTTind and in MLttind is due to the
fact that the realizability semantics we present in the next sections, based
on that in [IMMS18] and hence on the original Kleene realizability in [Tv88],
does not validate the $\xi$-rule111Notice that a trivial instance of the
$\xi$-rule is derivable from repl) when $c$ and $c^{\prime}$ don’t depend on
$x^{B}$. of lambda-terms

$\mbox{ $\xi$}\ \displaystyle{\frac{\displaystyle c=c^{\prime}\in C\ [x\in
B]}{\displaystyle\lambda x^{B}.c=\lambda x^{B}.c^{\prime}\in(\Pi x\in B)C}}$

which is instead valid in [NPS90].

It is indeed an open problem whether the original intensional version of
Martin-Löf’s type theory in [NPS90], including the $\xi$-rule of lambda terms,
is consistent with CT.

It is worth noting that the lack of the $\xi$-rule does not affect the
possibility of adopting mTT as the intensional level of a two-level
constructive foundation as intended in [MS05], since its term equality rules
suffice to interpret an extensional level including extensionality of
functions, as that represented by emTT, by means of the quotient model as
introduced in [Mai09] and studied abstractly in [MR13a, MR13b, MR15].

Furthermore our realizability semantics interprets terms as applicative terms
in the first Kleene algebra and their equality as numerical equality turning
into an extensional equality in the context-dependent case. Hence we need a
suitable encoding of lambda-terms which validates the replacement rule under
the interpretation. As observed in [IMMS18] not each translation of pure
lambda calculus in the first Kleene algebra satisfies this requirement (see
pp.881-882 in [IMMS18]).

Now note that we can interpret mTTind within MLttind by first interpreting
mTTind in the version of MLttind with the universe $U_{0}$ à la Russell which
is then interpreted into the original version MLttind with the first universe
à la Tarski.

In more detail, we call MLtt${}_{1}^{r}$ the first order fragment of
intensional Martin-Löf’s type theory in [NPS90] with the first universe
$U_{0}$ formulated à la Russell. Then, we call MLtt${}_{ind}^{r}$ the version
of MLttind with the universe $U_{0}$ and the rules of inductively generated
basic covers à la Russell which are obtained from those of MLttind by
identifying the code of a set in the first universe $U_{0}$ with the set
itself. In particular in MLtt${}_{ind}^{r}$ we must have a new set in $U_{0}$
expressing the basic cover

$a\,\triangleleft_{I,C}V\qquad\mbox{ for a set $A$ in $U_{0}$ }\mbox{ and
}V\in A\ \rightarrow\ U_{0}$

for any axiom set given by a set family $I(a)$ in $U_{0}$ for $a\in A$ and
$C(a,j)\in A\ \rightarrow\ U_{0}$ for $a\in A$ and $j\in I(a)$.

######  Theorem 3.1.

The interpretation of mTT into MLtt${}_{1}^{r}$ given in [Mai09] extends to
that of mTTind by interpreting each basic cover $\lhd_{I,C}$ of mTTind
associated to an axiom set $I(-)$ and $C(-,-)$ in the corresponding basic
cover of MLtt${}_{ind}^{r}$ associated to the interpreted axiom set.

######  Proof 3.2.

Note that small propositions are encoded in the universe $U_{0}$ as well as
axiom sets generating a basic cover in mTTind.

Observe that the version à la Russell MLtt${}_{ind}^{r}$ can be interpreted in
that à la Tarski MLttind by preserving the meaning of sets and of their
elements:

######  Proposition 3.

MLtt${}_{ind}^{r}$ can be interpreted into MLttind in such a way that any set
$A$ (under a context) in the first universe is interpreted as a set
$\mathsf{T}(c)$ for some code $c$ and each basic cover $a\lhd_{I,C}V$ of
MLtt${}_{ind}^{r}$ for $a\in A$ and $V\in A\rightarrow U_{0}$ associated to an
axiom set $I(-)$ and $C(-,-)$ is interpreted as the set with code
$a\,\widehat{\triangleleft}_{s,i,c}\,v\in U_{0}\mbox{ for
}a\in\mathsf{T}(s)\mbox{ and }v\in\mathsf{T}(s)\ \rightarrow\ U_{0}$ where $s$
is the code of the set interpreting $A$, $v$ is the interpretation of $V$ and
$i(x)\in U_{0}\ [x\in\mathsf{T}(s)]$ and $c(x,y)\in\mathsf{T}(s)\rightarrow
U_{0}\ [x\in\mathsf{T}(s),y\in\mathsf{T}(i(x))]$ are the interpretation of the
axiom-set.

######  Proof 3.3.

We first give a definition of pre-terms and pre-types associated to the syntax
of terms and types of MLttind after observing that a set in the first universe
à la Russell may appear both as a preterm and as a pretype. Then we define a
partial interpretation of preterms and pretypes respectively as preterms and
pretypes of MLttind with the warning of interpreting a set in the first
universe $U_{0}$ used as a preterm as its corresponding code à la Tarski in
MLttind.

######  Corollary 4.

mTTind can be interpreted in MLttind by composing the interpretations in
theorem 3.1 and proposition 3.

##  4 A realizability interpretation of MLttind with the formal Church’s
Thesis

Here we are going to describe a realizability model of MLttind with CT
extending that of MLtt1 in [IMMS18].

A main novelty here is that we formalize such a model in the (generalized)
predicative and constructive theory $\mathbf{CZF+REA}$ where $\mathbf{CZF}$
stands for Constructive Zermelo-Fraenkel Set Theory and $\mathbf{REA}$ stands
for the regular extension axiom (for details see [Acz86, AR01, AR10]).

Since the interpretation in [IMMS18] is performed in $\widehat{ID_{1}}$ which
is a classical theory of fixed points, we cannot follow the proof technique in
[IMMS18] to fulfill our purpose. Moreover $\widehat{ID_{1}}$ is a too weak
theory to accommodate inductively defined topologies as it can be gleaned from
[CR12]. The solution is to adopt the proof-technique in [Ra93, GR94] to
fulfill our goal.

As usual in set theory we identify the natural numbers with the finite
ordinals, i.e. $\mathbb{N}:=\omega$. To simplify the treatment we will assume
that $\mathbf{CZF}$ has names for all (meta) natural numbers. Let
$\overline{n}$ be the constant designating the $n^{th}$ natural number. We
also assume that $\mathbf{CZF}$ has function symbols for addition and
multiplication on $\mathbb{N}$ as well as for a primitive recursive bijective
pairing function
$\mathfrak{p}:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ and its
primitive recursive inverses $\mathfrak{p}_{0}$ and $\mathfrak{p}_{1}$, that
satisfy $\mathfrak{p}_{0}(\mathfrak{p}(n,m))=n$ and
$\mathfrak{p}_{1}(\mathfrak{p}(n,m))=m$. We also assume that $\mathbf{CZF}$ is
endowed with symbols for a primitive recursive length function
$\ell:\mathbb{N}\rightarrow\mathbb{N}$ and a primitive recursive component
function $(-)_{-}:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ determining
a bijective encoding of finite lists of natural numbers by means of natural
numbers. $\mathbf{CZF}$ should also have a symbol $T$ for Kleene’s
$T$-predicate and the result extracting function $U$. Let $P(\\{e\\}(n))$ be a
shorthand for $\exists m(T(e,n,m)\wedge P(U(m)))$. Further, let
$\mathfrak{p}(n,m,k):=\mathfrak{p}(\mathfrak{p}(n,m),k)$,
$\mathfrak{p}(n,m,k,h):=\mathfrak{p}(\mathfrak{p}(n,m,k),h)$, etc. A similar
convention will be adopted for application of partial recursive functions: Let
$\\{e\\}(a,b):=\\{\\{e\\}(a)\\}(b)$, $\\{e\\}(a,b,c):=\\{\\{e\\}(a,b)\\}(c)$
etc. We use $a,b,c,d,e,f,n,m,l,k,q,r,s,v,j,i$ as metavariables for natural
numbers.

We first need to introduce some abbreviations:

  1. 1.

$\mathsf{n}_{0}$ is $\mathfrak{p}(0,0)$, $\mathsf{n}_{1}$ is
$\mathfrak{p}(0,1)$ and $\mathsf{n}$ is $\mathfrak{p}(0,2)$.

  2. 2.

$\widetilde{\Sigma}(a,b)$ is $\mathfrak{p}(1,\mathfrak{p}(a,b))$,
$\widetilde{\Pi}(a,b)$ is $\mathfrak{p}(2,\mathfrak{p}(a,b))$ and $+(a,b)$ is
$\mathfrak{p}(3,\mathfrak{p}(a,b))$.

  3. 3.

$\mathsf{list}(a)$ is $\mathfrak{p}(4,a)$ and $\mathsf{id}(a,b,c)$ is
$\mathfrak{p}(5,\mathfrak{p}(a,b,c))$.

  4. 4.

$a\widetilde{\triangleleft}_{c,d,e}b$ is
$\mathfrak{p}(6,\mathfrak{p}(a,b,c,d,e))$.

  5. 5.

$\widetilde{\mathsf{rf}}(a,r)$ is $\mathfrak{p}(7,\mathfrak{p}(a,r))$.

  6. 6.

$\widetilde{\mathsf{tr}}(a,j,r)$ is $\mathfrak{p}(8,\mathfrak{p}(a,j,r))$.

Recall that in intuitionistic set theories ordinals are defined as transitive
sets all of whose members are transitive sets, too. Unlike in the classical
case, one cannot prove that they are linearly ordered but they are perfectly
good as a scale along which one can iterate various processes. The trichotomy
of $0$, successor, and limit ordinal, of course, has to be jettisoned. We use
lowercase greek letters as metavariables for ordinals.

######  Definition 4.1.

By transfinite recursion on ordinals (cf. [AR10], Proposition 9.4.4) we define
simultaneously two relations $\mathsf{Set}_{\alpha}(n)$ and
$n\,\varepsilon_{\alpha}\,m$ on $\mathbb{N}$ in $\mathbf{CZF+REA}$.

In the following definition we use the shorthand $\mathsf{Fam}_{\alpha}(e,k)$
to convey that $\mathsf{Set}_{\alpha}(k)$ and $\forall
j(j\,\varepsilon_{\alpha}\,k\rightarrow\mathsf{Set}_{\alpha}(\\{e\\}(j)))$ and
we shall write $\mathsf{Set}_{\in\alpha}(n)$ for
$\exists\beta\in\alpha(\mathsf{Set}_{\beta}(n))$,
$n\,\varepsilon_{\in\alpha}\,m$ for
$\exists\beta\in\alpha(n\,\varepsilon_{\beta}\,m)$ and
$\mathsf{Fam}_{\in\alpha}(e,k)$ for
$\exists\beta\in\alpha(\mathsf{Fam}_{\beta}(e,k))$.

  1.   2. 1.

$\mathsf{Set}_{\alpha}(\mathsf{n}_{j})$ if $j=0$ or $j=1$, and
$m\,\varepsilon_{\alpha}\,\mathsf{n}_{j}$ if $m<j$;

  3. 2.

$\mathsf{Set}_{\alpha}(\mathsf{n})$ holds, and
$m\,\varepsilon_{\alpha}\,\mathsf{n}$ if $m\in\mathbb{N}$.

  4.   5. 3.

If $\mathsf{Fam}_{\in\alpha}(e,k)$, then
$\mathsf{Set}_{\alpha}(\widetilde{\Pi}(k,e))$ and
$\mathsf{Set}_{\alpha}(\widetilde{\Sigma}(k,e))$;

  6. if $\mathsf{Fam}_{\in\alpha}(e,k)$, then

    1. (a)

$n\,\varepsilon_{\alpha}\,\widetilde{\Pi}(k,e)$ if there exists
$\beta\in\alpha$ such that $\mathsf{Fam}_{\beta}(e,k)$ and $(\forall
i\,\varepsilon_{\beta}\,k)\,\\{n\\}(i)\,\varepsilon_{\beta}\,\\{e\\}(i)$.222We
use the obvious shorthand $(\forall i\,\varepsilon_{\beta}\,k)\ldots$ for
$\forall i[i\,\varepsilon_{\beta}\,k\rightarrow\ldots]$; also employed
henceforth.

    2. (b)

$n\,\varepsilon_{\alpha}\,\widetilde{\Sigma}(k,e)$ if there exists
$\beta\in\alpha$ such that $\mathsf{Fam}_{\beta}(e,k)$ as well as
$\mathfrak{p}_{0}(n)\,\varepsilon_{\beta}\,k$ and
$\mathfrak{p}_{1}(n)\,\varepsilon_{\beta}\,\\{e\\}(\mathfrak{p}_{0}(n))$.

  7.   8. 4.

If there exists $\beta\in\alpha$ such that $\mathsf{Set}_{\beta}(n)$ and
$\mathsf{Set}_{\beta}(m)$, then $\mathsf{Set}_{\alpha}(+(n,m))$, and

  9. $i\,\varepsilon_{\alpha}{+}(n,m)$ if there exists $\beta\in\alpha$ such that $\mathsf{Set}_{\beta}(n)$, $\mathsf{Set}_{\beta}(m)$ and

$[\mathfrak{p}_{0}(i)=0\wedge\mathfrak{p}_{1}(i)\,\varepsilon_{\beta}\,n]\,\vee\,[\mathfrak{p}_{0}(i)=1\wedge\mathfrak{p}_{1}(i)\,\varepsilon_{\beta}\,m].$

  10.   11. 5.

If there exists $\beta\in\alpha$ such that $\mathsf{Set}_{\beta}(n)$, then
$\mathsf{Set}_{\alpha}(\mathsf{list}(n))$, and

  12. $i\,\varepsilon_{\alpha}\,\mathsf{list}(n)$ if there exists $\beta\in\alpha$ such that $\mathsf{Set}_{\beta}(n)$ and $\forall j\,[j<\ell(i)\rightarrow(i)_{j}\,\varepsilon_{\beta}\,n]$.

  13.   14. 6.

If $\mathsf{Set}_{\in\alpha}(n)$, then
$\mathsf{Set}_{\alpha}(\mathsf{id}(n,m,k))$, and

  15. $s\,\varepsilon_{\alpha}\,\mathsf{id}(n,m,k)$ if there exists $\beta\in\alpha$ such that $\mathsf{Set}_{\beta}(n)$, $m\,\varepsilon_{\beta}\,n$ and $s=m=k$.

  16.   17. 7.

Let $\beta\in\alpha$. Suppose that the following conditions (collectively
called $*_{\beta}$) are satisfied:

    1. (a)

$\mathsf{Set}_{\beta}(s)$,

    2. (b)

$a\,\varepsilon_{\beta}\,s$,

    3. (c)

$\mathsf{Fam}_{\beta}(v,s)$,

    4. (d)

$\mathsf{Fam}_{\beta}(i,s)$ and

    5. (e)

$\forall x\forall
y[x\,\varepsilon_{\beta}s\,\wedge\,y\,\varepsilon_{\beta}\\{i\\}(x)\rightarrow\mathsf{Fam}_{\beta}(\\{c\\}(x,y),s)]$.

Then $\mathsf{Set}_{\alpha}(a\widetilde{\triangleleft}_{s,i,c}v)$.

  18. For $\beta\in\alpha$ satisfying $*_{\beta}$, let $V_{\beta}$ be the smallest subset of $\mathbb{N}$ satisfying the following conditions:

    1. (a)

if $z\,\varepsilon_{\beta}s$ and $r\,\varepsilon_{\beta}\\{v\\}(z)$ then
$\mathfrak{p}(z,\widetilde{\mathsf{rf}}(z,r))\in V_{\beta}$;

    2. (b)

if $r\in\mathbb{N}$, $z\,\varepsilon_{\beta}\,s$,
$j\,\varepsilon_{\beta}\\{i\\}(z)$ and

$(\forall u\,\varepsilon_{\beta}s)\,(\forall
t\,\varepsilon_{\beta}\\{c\\}(z,j,u))\ \mathfrak{p}(u,\\{r\\}(u,t))\in
V_{\beta}$

then $\mathfrak{p}(z,\widetilde{\mathsf{tr}}(z,j,r))\in V_{\beta}$.

The existence of the set $V_{\beta}$ is guaranteed by the axiom
$\mathbf{REA}$.

  19. Finally we define $q\,\varepsilon_{\alpha}\,a\widetilde{\triangleleft}_{s,i,c}v$ by $\exists\beta\in\alpha\,[\,*_{\beta}\,\wedge\,\mathfrak{p}(a,q)\in V_{\beta}]$.

######  Remark 4.2.

It is perhaps worth noting that in the above definition the interpretation of
the Propositional Identity $T(\,\widehat{\mathsf{Id}}(s,a,b)\,)$ for $s\in
U_{0}$ and $a\in\mathsf{T}(s)$ and $b\in\mathsf{T}(s)$ agrees with that in
[IMMS18] which validates the rules of the extensional Propositional Identity
in [NPS90]. Hence, also our realizability semantics actually validates the
extensional version of MLttind. Therefore the elimination rule of inductive
basic covers can be equivalently weakened to act towards types which do not
depend on proof-terms of basic covers, as soon as we add a suitable
$\eta$-rule in a way similar to what happens to the rules of first-order types
(like disjoint sums or natural numbers or list types) in the extensional type
theories in [Mai05].

Here we have a crucial lemma.

######  Lemma 5.

($\mathbf{CZF}+\mathbf{REA}$)

  * •

For all $m\in\mathbb{N}$, if $\mathsf{Set}_{\alpha}(m)$ and
$\alpha\subseteq\rho$, then $\mathsf{Set}_{\rho}(m)$.

  * •

For all $m\in\mathbb{N}$, if $\mathsf{Set}_{\alpha}(m)$, then for all $\rho$
such that $\mathsf{Set}_{\rho}(m)$,

$(*)\;\;\;\;\forall i\in\mathbb{N}(i\,\varepsilon_{\alpha}\,m\leftrightarrow
i\,\varepsilon_{\rho}\,m).$

######  Proof 4.3.

The proof is similar to the one for Lemma 4.2 in [Ra93, GR94]. (i) and (ii)
are proved simultaneously by induction on $\alpha$ (cf. [AR10], Proposition
9.4.3). Suppose $\mathsf{Set}_{\alpha}(m)$ and $\mathsf{Set}_{\rho}(m)$. We
look at the forms $m$ can have.

If $m$ is $\mathsf{n}_{0}$, $\mathsf{n}_{1}$ or $\mathsf{n}$, then the claim
is immediate in view of clauses $(1)$ and $(2)$ in the previous definition.

If $m$ is of the form $\widetilde{\Pi}(k,e)$, then there exists
$\beta\in\alpha$ such that $\mathsf{Fam}_{\beta}(e,k)$. The induction
hypothesis applied to $\beta$ yields that whenever $\mathsf{Fam}_{\xi}(e,k)$,
then for all $\xi$

$\forall j\in\mathbb{N}(i\,\varepsilon_{\beta}\,m\leftrightarrow
i\,\varepsilon_{\xi}\,m)$ $\forall i\in\mathbb{N}\forall
j\in\mathbb{N}(i\,\varepsilon_{\beta}\,m\rightarrow(j\,\varepsilon_{\beta}\,\\{e\\}(i)\leftrightarrow
j\,\varepsilon_{\xi}\,\\{e\\}(i)))$

The claim $(*)$ follows from the foregoing. If $m$ is either
$\widetilde{\Sigma}(k,e)$, $+(a,b)$, $\mathsf{list}(a)$ or
$\mathsf{id}(a,b,c)$ the argument proceeds as in the previous case.

If $m$ is of the form $a\widetilde{\triangleleft}_{s,i,c}v$, the proof is
similar, although more involved.

######  Definition 4.4.

We define in $\mathbf{CZF}+\mathbf{REA}$ the formula $\mathsf{Set}(n)$ as
$\exists\alpha(\mathsf{Set}_{\alpha}(n))$ and $x\,\varepsilon\,y$ as
$\exists\alpha(x\,\varepsilon_{\alpha}\,y)$.

######  Theorem 4.5.

Consistency of the theory $\mathbf{CZF}+\mathbf{REA}$ implies the consistency
of the theory MLttind extended with the formal Church thesis CT.

######  Proof 4.6.

We outline a realizability semantics in CZF+$\mathbf{REA}$. Let $\mathbf{p}$
be a code for the primitive recursive pairing function $\mathfrak{p}$
introduced just before Definition 4.1, i.e.
$\\{\mathbf{p}\\}(n,m)=\mathfrak{p}(n,m)$.333Recall that when we write
$\\{b\\}(a_{1},\ldots,a_{n})$, we mean
$\\{\ldots\\{\\{b\\}(a_{1})\\}(a_{2})\ldots\\}(a_{n})$.

Every preterm is interpreted as a $\mathcal{K}_{1}$-applicative term (that is,
a term built with numerals, variables and Kleene application) as it is done in
[IMMS18] with the only difference that here we do not identify $\mathsf{N}$
with $\mathsf{List}(\mathsf{N}_{1})$ but we consider it as a primitive type
interpreted as the set of natural numbers $\mathbb{N}$; zero and successor
terms are interpreted in the obvious way while the eliminator relative to
$\mathsf{N}$ is interpreted using a numeral encoding a recursor.

We must notice that in introducing codes for sets in the universe in
Definition 4.1 we took account of dependencies by means of natural numbers
representing recursive functions; however every preterm depending on variables
will be interpreted as a $\mathcal{K}_{1}$-applicative term having the same
free variables (we identify the variables of MLttind with those in
CZF+$\mathbf{REA}$). For these reasons, whenever a term $s$ in MLttind depends
on terms $t_{1},\ldots,t_{n}$ in context, its interpretation will depend on
the interpretations of $t_{1},\ldots,t_{n}$ bounded with adequate $\Lambda$
operators. The variables which will be bounded by these $\Lambda$s will be the
ones used in the rule where the term $s$ is introduced. This abuse of notation
allows us to avoid heavy fully-annotated terms in the syntax.

We only need to interpret the new preterms of MLttind as follows.

  1. 1.

$(a\widehat{\triangleleft}_{s,i,c}v)^{I}$ is defined as
$\\{\mathbf{p}\\}(6,\\{\mathbf{p}_{5}\\}(a^{I},v^{I},s^{I},\Lambda
x.i^{I},\Lambda x.\Lambda y.c^{I}))$
($=a^{I}\;\widetilde{\triangleleft}_{s^{I},\Lambda x.i^{I},\Lambda x.\Lambda
y.c^{I}}\;v^{I}$),444$(=\ldots)$ is meant to convey that the preceding term
evaluates to same number as the one indicated by $\ldots$. where $\mathbf{p}$
and $\mathbf{p}_{5}$ are numerals representing the encoding of pairs of
natural numbers and of $5$-tuples of natural numbers, respectively.

  2. 2.

$(\mathsf{rf}(a,r))^{I}:=\\{\mathbf{p}\\}(7,\\{\mathbf{p}\\}(a^{I},r^{I}))$
($=\widetilde{\mathsf{rf}}(a^{I},r^{I})$).

  3. 3.

$(\mathsf{tr}(a,j,r))^{I}:=\\{\mathbf{p}\\}(8,\\{\mathbf{p}_{3}\\}(a^{I},j^{I},r^{I}))$
($=\widetilde{\mathsf{tr}}(a^{I},j^{I},r^{I})$), where $\mathbf{p}_{3}$ is a
numeral representing the encoding of triples of natural numbers.

  4. 4.

$(\mathsf{ind}(m,q_{1},q_{2}))^{I}$ is
$\\{\mathbf{ind}_{q_{1},q_{2}}\\}(m^{I})$ where $\mathbf{ind}_{q_{1},q_{2}}$
is the code of a recursive function555Actually depending primitive recursively
on the parameters, i.e. free variables, occuring in $q_{1}$ and $q_{2}$. such
that

    1. (a)

$\mathbf{ind}_{q_{1},q_{2}}(\widetilde{\mathsf{rf}}(z,r))\simeq\\{\Lambda
x.\Lambda w.q_{1}^{I}\\}(z,r)~{}$666 $t\simeq s$ to mean that the applicative
term $t$ converges if and only if $s$ converges, and in this case $t=s$. ,

    2. (b)

$\mathbf{ind}_{q_{1},q_{2}}(\widetilde{\mathsf{tr}}(a,i,r))\simeq\\{\Lambda
x.\Lambda h.\Lambda k.\Lambda f.q_{2}^{I}\\}(a,i,r,\Lambda z.\Lambda
u.\mathbf{ind}_{q_{1},q_{2}}(\ \\{r\\}(z,u)))$.

For the existence of such a code one appeals to the recursion theorem.

If $\tau$ is a $\mathcal{K}_{1}$-applicative term and $A=\\{x|\,\phi\\}$ is a
class, we will define $\tau\,\in\,A$ as an abbreviation for $\phi[\tau/x]$.

We will interpret pretypes into the language of set theory (with
$\mathbf{CZF}+\mathbf{REA}$ being the interpreting theory) as definable
subclasses of $\mathbb{N}$ as follows.

  1. 1.

$\mathsf{N}_{0}^{I}:=\\{x\in\mathbb{N}|\,\bot\\}$.

  2. 2.

$\mathsf{N}_{1}^{I}:=\\{x\in\mathbb{N}|\,x=0\\}$.

  3. 3.

$\mathsf{N}^{I}:=\\{x\in\mathbb{N}|\,x=x\\}=\mathbb{N}$.

  4. 4.

$((\Sigma y\in A)B)^{I}:=\\{x\in\mathbb{N}|\,\mathfrak{p}_{0}(x)\in
A^{I}\wedge\mathfrak{p}_{1}(x)\in B^{I}[\mathfrak{p}_{0}(x)/y]\\}$.

  5. 5.

$((\Pi y\in A)B)^{I}:=\\{x\in\mathbb{N}|\,\forall y\in\mathbb{N}\,[y\in
A^{I}\rightarrow\\{x\\}(y)\in B^{I}]\\}$.

  6. 6.

$(A+B)^{I}:=\\{x\in\mathbb{N}|\,[\mathfrak{p}_{0}(x)=0\wedge\mathfrak{p}_{1}(x)\in
A^{I}]\,\vee\,[\mathfrak{p}_{0}(x)=1\wedge\mathfrak{p}_{1}(x)\in B^{I}]\\}$.

  7. 7.

$(\mathsf{List}(A))^{I}:=\\{x\in\mathbb{N}|\,\forall
i\in\mathbb{N}\,[i<\ell(x)\rightarrow(x)_{i}\in A^{I}]\\}$.

  8. 8.

$(\mathsf{Id}(A,a,b))^{I}:=\\{x\in\mathbb{N}|\,x=a^{I}\wedge
a^{I}=b^{I}\,\wedge\,a^{I}\in A^{I}\\}$.

  9. 9.

$U_{0}^{I}:=\\{x|\,\mathsf{Set}(x)\\}$.

  10. 10.

$\mathsf{T}(a)^{I}:=\\{x|\,x\,\varepsilon\,a^{I}\\}$.

Precontexts are interpreted as conjunctions of set-theoretic formulas as
follows.

  1. 1.

$[\;]^{I}$ is the formula $\top$;

  2. 2.

$[\Gamma,x\in A]^{I}$ is the formula $\Gamma^{I}\,\wedge\,x\in A^{I}$.

Validity of judgements $J$ in $\mathbf{CZF}+\mathbf{REA}$ under the foregoing
interpretation is defined as follows:

  1. 1.

$A\,type\,[\Gamma]$ holds if
$\mathbf{CZF}+\mathbf{REA}\vdash\Gamma^{I}\to\forall x\,(x\in A^{I}\rightarrow
x\in\mathbb{N})$

  2. 2.

$A=B\,type\,[\Gamma]$ holds if
$\mathbf{CZF}+\mathbf{REA}\vdash\Gamma^{I}\to\forall x\,(x\in
A^{I}\leftrightarrow x\in B^{I})$

  3. 3.

$a\in A\,\,[\Gamma]$ holds if $\mathbf{CZF}+\mathbf{REA}\vdash\Gamma^{I}\to
a^{I}\in A^{I}$

  4. 4.

$a=b\in A\,\,[\Gamma]$ holds if $\mathbf{CZF}+\mathbf{REA}\vdash\Gamma^{I}\to
a^{I}\in A^{I}\wedge a^{I}=b^{I}$,

where $x$ is a fresh variable.

The encoding of lambda-abstraction in terms of $\mathcal{K}_{1}$-applicative
terms can be chosen (see [IMMS18]) in such a way that if $a$ and $b$ are terms
and $x$ is a variable which is not bounded in $a$, then the terms
$(\,a[b/x]\,)^{I}$ and $a^{I}[\,b^{I}/x]$ coincide.

The proof that for every judgement if $\mbox{\bf MLtt${}_{ind}$}\vdash J$,
then $J$ holds in the realizability model is a long verification. Serving as a
generic example, we will prove that the rules for the inductively generated
covers (rf-$\triangleleft$) and (tr-$\triangleleft$) preserve the validity of
judgments in the model. In doing so we will tacitly be assuming that the
interpretation of the context $\Gamma^{I}$ holds true.

  1. (rf-$\triangleleft$)

Suppose the premisses of the following rule are valid in the model.

$\mbox{\rm rf-$\triangleleft$}\ \displaystyle{\frac{\begin{array}[]{l}s\in
U_{0}\qquad i(x)\in U_{0}\ [x\in\mathsf{T}(s)]\ \ \
c(x,y)\in\mathsf{T}(s)\rightarrow U_{0}\ \
[x\in\mathsf{T}(s),y\in\mathsf{T}(i(x))]\\\ a\in\mathsf{T}(s)\qquad
v\in\mathsf{T}(s)\rightarrow U_{0}\qquad\qquad r\in
a\,\epsilon\,v\end{array}}{\displaystyle\mathsf{rf}(a,r)\in
a\triangleleft_{s,i,c}v}}$

Then, the following hold true:

    1. (a)

$\mathsf{Set}(s^{I})$

    2. (b)

$\forall
x\in\mathbb{N}\,(x\,\varepsilon\,s^{I}\rightarrow\mathsf{Set}((i(x))^{I}))$

    3. (c)

$\forall x,y,z\in\mathbb{N}\,(x\,\varepsilon\,s^{I}\wedge
y\,\varepsilon\,(i(x))^{I}\wedge
x\,\varepsilon\,s^{I}\rightarrow\mathsf{Set}(\\{(c(x,y))^{I}\\}(z)))$

    4. (d)

$a^{I}\,\varepsilon\,s^{I}$

    5. (e)

$\forall
x\in\mathbb{N}\,(x\,\varepsilon\,s^{I}\rightarrow\mathsf{Set}(\\{v^{I}\\}(x)))$

    6. (f)

$r^{I}\,\varepsilon\,\\{v^{I}\\}(a^{I})$

(a) entails that there exists an ordinal $\alpha$ such that

$\displaystyle\mathsf{Set}_{\alpha}(s^{I})$ (1)

and by (b) we have $\forall
x\in\mathbb{N}\,(x\,\varepsilon_{\alpha}\,s^{I}\rightarrow\exists\beta\,\mathsf{Set}_{\beta}((i(x))^{I}))$.
Using strong collection in our background theory, the latter yields the
existence of a set of ordinals $b_{1}$ such that

$\displaystyle\forall
x\in\mathbb{N}\,(x\,\varepsilon_{\alpha}\,s^{I}\rightarrow\exists\beta\in
b_{1}\,\mathsf{Set}_{\beta}((i(x))^{I})).$ (2)

Let $\gamma$ be $\alpha\cup b_{1}\cup\bigcup b_{1}$. One then determines that
$\gamma$ is an ordinal. From (c) it follows by strong collection that there
exists a set of ordinals $b_{2}$ such that

$\displaystyle\forall
x,y,z\in\mathbb{N}\,(x\,\varepsilon_{\gamma}\,s^{I}\wedge
y\,\varepsilon_{\gamma}\,(i(x))^{I}\wedge
x\,\varepsilon_{\gamma}\,s^{I}\rightarrow\exists\xi\in
b_{2}\,\mathsf{Set}_{\xi}(\\{(c(x,y))^{I}\\}(z))).$ (3)

Likewise, (e) yields the existence of a set of ordinals $b_{3}$ such that

$\displaystyle\forall
x\in\mathbb{N}\,(x\,\varepsilon_{\gamma}\,s^{I}\rightarrow\exists\zeta\in
b_{3}\,\mathsf{Set}_{\zeta}(\\{v^{I}\\}(x))).$ (4)

Finally, let $\delta$ be the ordinal $\gamma\cup b_{2}\cup\bigcup b_{2}\cup
b_{3}\cup\bigcup b_{3}$. In light of Lemma 5, we can infer from the above (1,
2, 3 and 4) collectively that

     * (i)

$\mathsf{Set}_{\delta}(s^{I})$

     * (ii)

$\forall
x\in\mathbb{N}\,(x\,\varepsilon_{\delta}\,s^{I}\rightarrow\mathsf{Set}_{\delta}((i(x))^{I}))$

     * (iii)

$\forall x,y,z\in\mathbb{N}\,(x\,\varepsilon_{\delta}\,s^{I}\wedge
y\,\varepsilon_{\delta}\,(i(x))^{I}\wedge
x\,\varepsilon_{\delta}\,s^{I}\rightarrow\mathsf{Set}_{\delta}(\\{(c(x,y))^{I}\\}(z)))$

     * (iv)

$a^{I}\,\varepsilon_{\delta}\,s^{I}$

     * (v)

$\forall
x\in\mathbb{N}\,(x\,\varepsilon_{\delta}\,s^{I}\rightarrow\mathsf{Set}_{\delta}(\\{v^{I}\\}(x)))$

     * (vi)

$r^{I}\,\varepsilon_{\delta}\,\\{v^{I}\\}(a^{I})$

Let $\theta$ be any ordinal such that $\delta\in\theta$. By Definition 4.1(7),
we then have
$\mathsf{Set}_{\theta}(a^{I}\;\widetilde{\triangleleft}_{s^{I},i^{I},c^{I}}\;v^{I})$
and
$\mathsf{rf}(a,r)^{I}=\widetilde{\mathsf{rf}}(a^{I},r^{I})\,\varepsilon\,a^{I}\;\widetilde{\triangleleft}_{s^{I},i^{I},c^{I}}\,v^{I}$.
So the validity of the judgement $\mathsf{rf}(a,r)\in a\triangleleft_{s,i,c}v$
in the model is established.

  2. (tr-$\triangleleft$)

Suppose the premisses of the following rule are valid in the model.

$\mbox{\rm tr-$\triangleleft$}\displaystyle{\frac{\begin{array}[]{l}s\in
U_{0}\ \ \ \ i(x)\in U_{0}\ [x\in\mathsf{T}(s)]\ \ \
c(x,y)\in\mathsf{T}(s)\rightarrow U_{0}\ \
[x\in\mathsf{T}(s),y\in\mathsf{T}(i(x))]\\\ a\in\mathsf{T}(s)\qquad
j\in\mathsf{T}(i(a))\qquad v\in\mathsf{T}(s)\rightarrow U_{0}\\\ r\in(\Pi
x\in\mathsf{T}(s))(x\,\epsilon\,c(a,j)\rightarrow
x\triangleleft_{s,i,c}v)\end{array}}{\displaystyle\mathsf{tr}(a,j,r)\in
a\triangleleft_{s,i,c}v}}$

Then, in addition to (a)-(e) of the previous case,
$j^{I}\,\varepsilon\,\\{i^{I}\\}(a^{I})$ and

$\forall x\in\mathbb{N}\,\forall y\in\mathbb{N}\,[x\,\varepsilon\,s^{I}\wedge
y\,\varepsilon\,\\{c^{I}(a^{I},j^{I})\\}(x)\rightarrow\\{r^{I}\\}(x,y)\,\varepsilon\,x\,\widetilde{\triangleleft}_{s^{I},i^{I},c^{I}}\,v^{I}]$

hold. Thus just as in the previous case, we have to find sufficiently large
ordinals in which all the relevant coded sets “live”. However, we will not
repeat this procedure. Following it, we have, by Definition 4.1(7),
$(\mathsf{tr}(a,j,r))^{I}=\widetilde{\mathsf{tr}}(a^{I},j^{I},r^{I})\,\varepsilon\,a^{I}\;\widetilde{\triangleleft}_{s^{I},i^{I},c^{I}}\,v^{I}$,
which means that $\mathsf{tr}(a,j,r)\in a\triangleleft_{s,i,c}v$ is valid in
the model.

To conclude, one can show in $\mathbf{CZF}+\mathbf{REA}$ that the
interpretation of $\mathbf{CT}$ is inhabited by some numeral $\mathbf{n}$.
This numeral is “almost” a Turing machine code for the identity function,
however, it also depends on the Kleene normal form predicate $T$ and the
result extracting function $U$.

######  Corollary 6.

Consistency of the theory $\mathbf{CZF}+\mathbf{REA}$ implies the consistency
of the theory mTTind$+\mathbf{AC}+\mathbf{CT}$.

######  Proof 4.7.

This follows from corollary 4 and theorem 4.5.

######  Corollary 7.

The theory mTTind$+\mathbf{AC}+\mathbf{CT}$ has an interpretation in the
intensional version of the type theory $\mathbf{ML}_{\mathrm{1W}}\mathbf{V}$
in Definition 5.1 of [Ra93] or [GR94].

######  Proof 4.8.

This is a consequence of corollary 4 together with the proof of the above
Theorem 4.5 and Proposition 5.3 in [Ra93, GR94], namely the interpretability
of $\mathbf{CZF}+\mathbf{REA}$ in $\mathbf{ML}_{\mathrm{1W}}\mathbf{V}$.

######  Remark 4.9.

In a certain sense there is nothing special about inductively generated basic
covers in that the interpretation of MLttind in $\mathbf{CZF}+\mathbf{REA}$
would also work if one added further inductive types such as generic well
founded sets to MLttind. In the same vein one could add more universes or even
superuniverses (see [Pal98, Ra01]) after beefing up the interpreting set
theory by adding large set axioms. As a consequence one can conclude that
intensional Martin-Löf type theory with some or all these type constructors
added, but crucially missing the $\xi$-rule, is consistent with the formal
Church’s thesis.

######  Theorem 4.10.

MLttind and $\mathbf{CZF}+\mathbf{REA}$ have the same proof-theoretic
strength.

######  Proof 4.11.

It follows from [Ra93], Theorem 5.13, Theorem 6.9, Theorem 6.13 (or the same
theorems in [GR94]) together with our theorem 4.5 and the observation that the
theory $\mathbf{IARI}$ of [Ra93] in Definition 6.2 can already be interpreted
in MLttind using the interpretation of [Ra93] in Definition 6.5.

We just recall that $\mathbf{IARI}$ is a subsystem of second order
intuitionistic number theory. It has a replacement schema and an axiom of
inductive generation asserting that for every binary set relation $R$ on the
naturals the well-founded part of this relation is a set. The interpretation
for the second order variables are the propositions on the naturals with truth
conditions in $U_{0}$.

The crucial step is to interpret the axiom of inductive generation of
$\mathbf{IARI}$ in MLttind. To this purpose one has to show that if $s\in
U_{0}$ and $R\in\mathsf{T}(s)\times\mathsf{T}(s)\to U_{0}$ then the well-
founded part of $R$, $\mathsf{WP}(R)$, can be given as a predicate
$\mathsf{WP}(R)\in\mathsf{T}(s)\to U_{0}$. To this end define
$i\in\mathsf{T}(s)\to U_{0}$ by $i(x):=s$, $v\in\mathsf{T}(s)\to U_{0}$ by
$v(p):=\mathsf{n}_{0}$, $c(x,y)\in\mathsf{T}(s)\to U_{0}$ by
$c(x,y)(z):=R(z,x)$ (so $y$ is dummy) for $x\in\mathsf{T}(s)$ and
$y\in\mathsf{T}(s)$. Now let $\mathsf{WP}(R)(a):=a\triangleleft_{s,i,c}v$ for
$a\in\mathsf{T}(s)$. Then it follows that $a$ is in the well-founded part
exactly when $\mathsf{WP}(R)(a)$ is inhabited. To see this, suppose we have a
truth maker $r$ for $(\Pi x\in\mathsf{T}(s))(R(x,a)\to\mathsf{WP}(R)(x))$.
Then $r\in(\Pi x\in\mathsf{T}(s))(x\,\epsilon\,c(a,a)\to
x\triangleleft_{s,i,c}v)$, hence $\mathsf{tr}(a,a,r)\in
a\triangleleft_{s,i,c}v$ by ($\mathrm{tr}\mbox{-}\triangleleft)$, whence
$\mathsf{tr}(a,a,r)\in\mathsf{WP}(R)(a)$. Thus $\mathsf{WP}(R)$ satisfies the
appropriate closure properties characterizing the well-founded part of $R$.
The pertaining induction principle is then a consequence of
$(\mathrm{ind}\mbox{-}\triangleleft)$.

######  Remark 4.12.

The proof of theorem 4.10 does not work if we substitute MLttind with mTTind.
The reason is that the axiom of replacement in $\mathbf{IARI}$ does not appear
to be interpretable in mTTind and to establish the exact proof theoretic
strength of mTTind is left to future work.

### Conclusions

In the future we aim to further extend the realizability semantics presented
here to model MFind enriched with coinductive definitions capable of
representing generated Positive Topologies in [Sam03].

Further goals would be to study the consistency strength of mTTind or of mTT
extended with specific inductive formal topologies such as that of the Baire
space.

### Acknowledgments

We would like to thank the anonymous referees very much for their keenly
perceptive comments. The first author acknowledges very helpful discussions
with F. Ciraulo, P. Martin-Löf, G. Sambin and T. Streicher. The third author
was supported by a grant from the John Templeton Foundation (“A new dawn of
intuitionism: mathematical and philosophical advances,” ID 60842) and a grant
from the University of Padova for a research sojourn at its Department of
Mathematics.

## References

  * [Acz86] P. Aczel.  The type theoretic interpretation of constructive set theory: inductive definitions.  In Logic, methodology and philosophy of science, VII (Salzburg, 1983), volume 114 of Stud. Logic Foundations Math., Amsterdam-New York, 1986. North-Holland.
  * [AR01] P. Aczel and M. Rathjen.  Notes on constructive set theory.  Mittag-Leffler Technical Report No.40, 2001.
  * [AR10] P. Aczel and M. Rathjen.  Notes on constructive set theory.  Available at http://www1.maths.leeds.ac.uk/$\sim$rathjen/book.pdf, 2010\.
  * [BS06] G. Battilotti and G. Sambin.  Pretopologies and a uniform presentation of sup-lattices, quantales and frames.  In Special Issue: Papers presented at the 2nd Workshop on Formal Topology (2WFTop 2002), volume 137 of Annals of Pure and Applied Logic, pages 30–61, (2006).
  * [CMS13] F. Ciraulo, M. E. Maietti, and G. Sambin.  Convergence in formal topology: a unifying notion.  J. Logic & Analysis, 5, 2013.
  * [CN95] J. Cederquist and S. Negri.  A constructive proof of the Heine-Borel covering theorem for formal reals.  In S. Berardi and M. Coppo, editors, Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers, volume 1158 of Lecture Notes in Computer Science, pages 62–75. Springer, 1995.
  * [CR12] G. Curi. and M. Rathjen.  Formal Baire space in constructive set theory.  In Logic, construction, computation, volume 3 of Ontos Math. Log., pages 123–135. Ontos Verlag, Heusenstamm, 2012.
  * [CSSV03] T. Coquand, G. Sambin, J. Smith, and S. Valentini.  Inductively generated formal topologies.  Annals of Pure and Applied Logic, 124(1-3):71–106, 2003.
  * [Cur10] G. Curi.  On some peculiar aspects of the constructive theory of point-free spaces.  Mathematical Logic Quarterly, 56(4):375–387, (2010).
  * [GR94] E. Griffor and M. Rathjen.  The strength of some Martin-Löf type theories.  Archive for Mathematical Logic, 33(5):347–385, 1994.
  * [IMMS18] H. Ishihara, M.E. Maietti, S. Maschio, and T. Streicher.  Consistency of the intensional level of the Minimalist Foundation with Church’s thesis and axiom of choice.  Archive for Mathematical Logic, 57(7-8):873–888, 2018.
  * [Mai05] M.E. Maietti.  Modular correspondence between dependent type theories and categories including pretopoi and topoi.  Mathematical Structures in Computer Science, 15(6):1089–1149, 2005\.
  * [Mai09] M. E. Maietti.  A minimalist two-level foundation for constructive mathematics.  Annals of Pure and Applied Logic, 160(3):319–354, 2009.
  * [MM16] M.E. Maietti and S. Maschio.  A predicative variant of a realizability tripos for the Minimalist Foundation.  IfCoLog Journal of Logics and their applications, 3(4):595–668, 2016.
  * [MR13a] M. E. Maietti and G. Rosolini.  Elementary quotient completion.  Theory and Applications of Categories, 27(17):445–463, 2013.
  * [MR13b] M.E. Maietti and G. Rosolini.  Quotient completion for the foundation of constructive mathematics.  Logica Universalis, 7(3):371–402, 2013.
  * [MR15] M. E. Maietti and G. Rosolini.  Unifying exact completions.  Applied Categorical Structures, 23(1):43–52, 2015.
  * [MS05] M. E. Maietti and G. Sambin.  Toward a minimalist foundation for constructive mathematics.  In L. Crosilla and P. Schuster, editor, From Sets and Types to Topology and Analysis: Practicable Foundations for Constructive Mathematics, number 48 in Oxford Logic Guides, pages 91–114. Oxford University Press, 2005\.
  * [MS13] M. E. Maietti and G. Sambin.  Why topology in the Minimalist Foundation must be pointfree.  Logic and Logical Philosophy, 22(2):167–199, 2013.
  * [MV04] M. E. Maietti and S. Valentini.  A structural investigation on formal topology: coreflection of formal covers and exponentiability.  Journal of Symbolic Logic, 69:967–1005, 2004.
  * [NPS90] B. Nordström, K. Petersson, and J. Smith.  Programming in Martin Löf’s Type Theory. Clarendon Press, Oxford, 1990.
  * [Pal98] E. Palmgren.  On universes in type theory.  In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 191–204. Oxford Univ. Press, New York, 1998.
  * [Pal05] E. Palmgren.  Continuity on the real line and in formal spaces.  In From Sets and Types to Topology and Analysis: Towards Practicable Foundations of Constructive Mathematics, Oxford Logic Guides, University Press, pages 165–175, 2005.
  * [Ra93] M. Rathjen.  The strength of some Martin-Löf type theories.  Preprint, Department of Mathematics, Ohio State University,available at http://www1.maths.leeds.ac.uk/$\sim$rathjen/typeOHIO.pdf, 1993.
  * [Ra01] M. Rathjen.  The strength of Martin-Löf type theory with a superuniverse. II.  Archive for Mathematical Logic, 40(3):207–233, 2001.
  * [Sam87] G. Sambin.  Intuitionistic formal spaces - a first communication.  Mathematical logic and its applications, pages 187–204, 1987.
  * [Sam03] G. Sambin.  Some points in formal topology.  Theoretical Computer Science, 305(1-3):347–408, 2003.
  * [Tv88] A. S. Troelstra and D. van Dalen.  Constructivism in mathematics, an introduction, vol. I.  In Studies in logic and the foundations of mathematics. North-Holland, 1988.
  * [Val07] S. Valentini.  Constructive characterizations of bar subsets.  Annals of Pure and Applied Logic, 145:368–378, 2007.