# On the Compatibility of Constructive Predicative Mathematics with Weyl’s
Classical Predicativity

Michele Contente
Czech Academy of Sciences, Prague, Czechia
Maria Emilia Maietti
Department of Mathematics, University of Padova, Italy

###### Abstract

It is well known that most foundations for Bishop’s constructive mathematics
are incompatible with a classical predicative development of analysis as put
forward by Weyl in his Das Kontinuum.

Here, we first recall how this incompatibility arises from the possibility,
present in most constructive foundations, to define sets by quantifying over
(the exponentiation of) functional relations. This possibility is not allowed
in modern formulations of Weyl’s logical system.

Then, we argue how a possible way out is offered by foundations, such as the
Minimalist Foundation, where exponentiation is limited to a primitive notion
of function defined by $\lambda$-terms as in dependent type theory.

The price to pay is to renounce the so-called rule of unique choice
identifying functional relations with $\lambda$-terms, and to number-theoretic
choice principles, characteristic of foundations aimed to formalize Bishop’s
constructive analysis. This restriction calls for a point-free constructive
development of topology as advocated by P. Martin-Löf and G. Sambin with the
introduction of Formal Topology.

Hence, we conclude that the Minimalist Foundation promises to be a natural
crossroads between Bishop’s constructivism and Weyl’s classical predicativity
provided that a point-free reformulation of classical analysis is viable.

###### Contents

  1. 1 Introduction
  2. 2 Weyl’s Classical Predicativity
  3. 3 Constructive Predicative Theories
    1. 3.1 Aczel’s Constructive Zermelo-Fraenkel set theory
    2. 3.2 Martin-Löf’s type theory
    3. 3.3 Homotopy Type Theory
  4. 4 The incompatibility of ${\bf HA}^{\omega}+{\bf iRC!}_{\mathbf{N},\mathbf{N}}$ with Weyl’s predicativity
  5. 5 The incompatibility of MLTT, HoTT and CZF with Weyl’s predicativity
  6. 6 A possible way out: the Minimalist Foundation
  7. 7 Conclusion

##  1 Introduction

The book Das Kontinuum [55, 56] is a milestone in the foundations of
mathematics and, in particular, of classical predicative mathematics. Weyl’s
monograph is mainly devoted to the predicative reformulation of real analysis.

Another major reformulation of real analysis within a foundation weaker than
the usual classical one was given by Bishop in [6]. While Bishop followed
Brouwer in adopting intuitionistic logic, he refrained in his approach from
including Brouwer’s continuity principles that are inconsistent with classical
mathematics. Bishop’s aim was to develop constructive mathematics not in
opposition to classical mathematics but as a generalization of the latter.

After the publication of Bishop’s book, there was a flourishing of foundations
for constructive mathematics aimed at formally capturing Bishop’s approach. A
relevant example in axiomatic set theory is Aczel’s constructive set theory
CZF [1], and in type theory Martin-Löf Type Theory MLTT [38, 39] and the more
recent Homotopy Type Theory HoTT in [53] inspired by Voevodsky’s Univalent
Foundations. In particular, HoTT gained a lot of attention for its application
to the formalization of synthetic homotopy theory and higher category theory.
However, these systems are sometimes not even mutually compatible and this
consideration led the second author in joint work with G. Sambin to conceive
the Minimalist Foundation (for short MF) in [33], later fully worked out as a
two-level system in [24]. The two-level structure of MF in [24], which
includes an intensional level, an extensional level, and an interpretation of
the latter into the first, was introduced to better accomplish the
compatibility of MF with constructive and classical foundations including the
mentioned ones (see [24, 9]) and internal theories of categorical universes
such as that of elementary topoi in [22, 23].

It is also well known that, among all the foundations of constructive and
predicative mathematics, at least the mentioned ones, CZF, MLTT and HoTT, are
incompatible with a classical predicative development of mathematics as
advocated by Weyl in Das Kontinuum, since they become impredicative when
extended with the law of excluded middle.

Here we first discuss the source of this incompatibility. The reason lies in
their possibility of defining sets by quantifying over (the exponentiation of)
functional relations. Such a possibility is not allowed in modern formulations
of Weyl’s system [5, 4, 3, 16].

Then, we argue that it is not necessary to sacrifice exponentiation altogether
to reconcile Bishop’s mathematics with Weyl’s approach if we adopt a
foundation like the Minimalist Foundation and this for a number of reasons.

First of all, the intuitionistic version of the subsystem of second-order
arithmetic known as ACA [48] can be interpreted in the extensional level of MF
by preserving the meaning of all the logical operators, as well as the
classical ACA can be analogously interpreted in the classical extension of MF.
Therefore, Weyl’s reconstruction of analysis can be performed in the classical
version of MF, since it is known from results of reverse mathematics in [16,
17, 48] that the formalization of Weyl’s analysis can be performed at least in
ACA, whilst the proof-theoretic strength of Weyl’s original logical system
exceeds it, see [5, 4, 3, 16].

Second, the classical version of MF is equi-consistent, as shown in [27, 44],
with the original constructive MF, whose proof-theoretic strength is strictly
predicative a’ la Feferman being interpretable in first-order Martin-Löf’s
type theory [24] and directly in Feferman’s $\widehat{ID_{1}}$ (see [20]).

Third, in both levels of MF, whilst the exponentiation of functional relations
does not necessarily form a set, it does so the exponentiation of a primitive
notion of function defined by $\lambda$-terms. This is possible since, in both
levels of MF, the logic is many-sorted with sorts given by dependent types
equipped with elements defined by $\lambda$-terms as in Martin-Löf’s type
theory.

The price to be paid in MF is to renounce the so-called rule of unique choice
identifying functional relations with $\lambda$-terms. In this way
exponentiation of type-theoretic functions does not entail exponentiation of
functional relations as it happens instead in Martin-Löf’s type theory and in
Homotopy Type Theory, whose logics are also sorted on a dependent type theory.
Accordingly, dropping the rule of unique choice entails dropping all the
number-theoretic choice principles characteristic of Bishop’s mathematics as
well as the fact that real numbers a’ la Dedekind or Cauchy form a set.

As a consequence, these limitations call for a point-free constructive
development of topology as advocated by Martin-Löf and Sambin with the
introduction of Formal Topology [45] to avoid the use of Brouwer’s Fan theorem
as explained in [34]. Evidence that such an approach can be successfully
developed is provided by the point-free results in [7, 41, 42, 7, 8, 21, 47].

Given that the point-free topology of Dedekind real numbers and that of Cantor
space are definable in MF, if a point-free reformulation of classical analysis
is fully viable, then MF would become a natural crossroads between Bishop’s
constructivism and Weyl’s classical predicativity.

In the future, besides determining the exact proof-theoretic strength of MF,
which is currently an open problem, we intend to investigate whether the
extensions of MF with inductive and coinductive definitions in [28, 29, 32] is
still predicative, or even still equi-consistent with their classical
counterparts as established for MF in [27, 44]. A positive answer to one of
these questions would provide a foundation more expressive than MF and capable
of formalizing a whole development of point-free topology, including for
example the results in [36, 15, 10, 47], while still maintaining compatibility
with both Bishop’s constructive mathematics and Weyl’s classical predicative
mathematics.

The structure of the paper is the following: first, we give a short overview
of Weyl’s classical predicative conception in Das Kontinuum and highlight the
points of convergence with some ideas underlying the Minimalist Foundation. In
Section 3 we present some well-known examples of constructive predicative
foundations. Then, in Section 4 we show that already Heyting Arithmetic in all
finite types is incompatible with classical predicativity if it is extended
with classical logic and the (number-theoretic) internal rule of unique
choice. In Section 5 we extend this argument to other systems and analyze the
incompatibility of MLTT, HoTT and CZF with classical predicativity. Finally,
in Section 6 we introduce the Minimalist Foundation and we argue that it might
represent a natural solution to the issues discussed in the previous sections.

##  2 Weyl’s Classical Predicativity

Das Kontinuum [55, 56] can be regarded as the first systematic attempt to
develop predicative mathematics. The main focus of the book is the foundation
of analysis and, moreover, the reconstruction of many fundamental results in
this area without resorting to impredicative principles. Examples of theorems
shown by Weyl in his framework include the Fundamental Theorem of the
Calculus, Uniform continuity for continuous functions over a closed interval
and existence of a maximum and a minimum for them as well as sequential
versions of the Heine-Borel Theorem and the Least Upper Bound principle.
Therefore, the main merit of Das Kontinuum was to show that predicative
mathematics was a viable project. Feferman has shown that the above mentioned
results can be formalized in the subsystem of second-order arithmetic known as
ACA0 and further evidence in support of this claim has been provided by the
Reverse Mathematics program [48]. In this section, we review some basic tenets
of Weyl’s approach in relation to the Minimalist Foundation, which will be
introduced later in Section 6.

Weyl acknowledged - in agreement with Poincaré- the absolutely primitive
character of the natural numbers and the associated notion of iteration.
According to Weyl, every attempt to understand natural numbers in terms of
more fundamental notions – as it happens in Zermelo’s set theory or in the
logicist program of developing arithmetic on the basis of purely logical
notions– was doomed to failure because it necessarily presupposes this very
notion:

> ‘And I became firmly convinced (in agreement with Poincaré, whose
> philosophical position I share in so few other respects) that the idea of
> iteration, i.e., of the sequence of natural numbers, is an ultimate
> foundation of mathematical thought \- in spite of Dedekind’s “theory of
> chains” which seeks to give a logical foundation for definition and
> inference by complete induction without employing our intuition of the
> natural numbers. For if it is true that the basic concepts of set theory can
> be grasped only through this “pure” intuition, it is unnecessary and
> deceptive to turn around them and offer a set-theoretic foundation for the
> concept of “natural number”.’ (ibid., p.48)

Weyl’s conception of set bears some resemblance to the way sets are understood
in Martin-Löf’s type theory (MLTT) and also in both levels of the Minimalist
Foundation (MF), which will be presented in the next sections. In such
theories, a set is determined by rules for forming its elements equipped with
an induction principle to prove properties on it and a recursive definition to
define a function by recursion from it to another set, see [39].

Furthermore, Weyl considered the notion of set (and function) underlying the
classical foundation of analysis to be irremediably circular. Weyl noted that
many basic definitions of analysis (e.g. that of least upper bound) were
actually circular, and decided to reformulate analysis by avoiding such
viciously circular definitions in favour of a predicative development. In
particular, such a circularity clearly shows up in Dedekind’s construction of
the real numbers: real numbers defined in this way do not form an
extensionally determinate collection111See [5, 14] for a detailed analysis of
this concept.. Weyl elaborates on this point in a letter to Hölder, published
as appendix in [56]:

> ‘If $A$ is a property of properties, then one may form the property $P_{A}$
> which belongs to an object $x$ if and only if there is a property
> constructed by means of these principles which belongs to $x$ and itself
> possesses the property $A$. That would be a blatant circulus vitiosus; yet
> our current version of analysis commits this error and I consider it ground
> for censure.’ ([56], p.113)

In particular, it follows from this quotation that the power of a set is not a
set according to Weyl. Thus we cannot define a new set by quantifying over the
powerset to which it should belong. The subtle point is that this does not
mean that the power of a set does not exist, but simply that it is not a set
but a collection that is not inductively generated. In the Minimalist
Foundation, this distinction between sets and collections is explicitly
assumed. Accordingly, in Weyl’s work collections exceed the power-collection
of a set, as shown in [4, 3, 5], but they are not allowed to enter into the
definition of new sets.

A major distinction between sets and collections in the Minimalist Foundation
is that, whilst both entities are generated by rules forming their canonical
elements as sets in Martin-Löf’s type theory, sets distinguish from
collections for being equipped with an induction principle and a recursive
definition of functions from them toward any other entity. Collections instead
do not enjoy any induction principle or recursive definition from them, since
inductive or recursive definitions acting on them would not be invariant under
extensions of the theory with new sets. This approach aligns closely with the
idea that predicative sets should be invariant, which traces back to Poincaré
and has been carefully analyzed in [13].

Both in Das Kontinuum and in the Minimalist Foundation real numbers provide an
example of a collection which is not a set. In particular, Weyl introduced
real numbers as Dedekind cuts of rationals and are formalized as quadruples of
natural numbers. The fact that the resulting collection $\mathbb{R}$ of real
numbers is not extensionally determinate in Weyl’s terminology, means that we
cannot define new sets by quantification over $\mathbb{R}$, in sharp contrast
with the case of natural numbers. This implies, for instance, that the least
upper bound principle for sets of real numbers is not predicatively provable,
while the principle is provable for sequences of real numbers, since the
latter do not involve quantification over $\mathbb{R}$.

Finally, we want to point out that Weyl in Das Kontinuum places a significant
emphasis on his notion of function and contrasts it with the set-theoretical
definition. To this purpose, Avron writes in [5]:

> ‘Weyl totally rejected the modern view of a function as any set of pairs
> that satisfies the functionality condition. He insists that (like sets)
> functions can be determined only by a rule’.

With reference to this, it might be intriguing to attribute to Weyl a kind of
computational understanding of what a function is. Indeed, Weyl works in a
classical framework and assumes that functions are extensional objects just as
sets in his system. However, Weyl’s quotation is in line with the fact that in
the Minimalist Foundation we distinguish between functions as functional
relations and functions as primitive operations defined by $\lambda$-terms.
The distinct character of these two notions of functions is a peculiarity of
MF among foundations for constructive predicative mathematics. While it might
be argued that Weyl foreshadowed this distinction, nevertheless his technical
treatment of the notion of function is not exactly the same. Therefore, we can
only highlight the significance of the insight of viewing functions as rule-
based objects. Moreover, this resembles the notion of Brouwer lawlike
sequence, which we will identify with a $\lambda$-term in the Minimalist
foundation (see [46]).

There have been various attempts in the literature to formalize Weyl’s system
in a modern fashion, since Weyl’s original presentation presents some
ambiguities. An influential reconstruction of Weyl’s system has been offered
by Feferman in several works [16, 17, 18]. Feferman has extensively argued
that Weyl’s system should correspond to the theory $\mathbf{ACA}_{0}$ or, if
the full induction scheme is accepted, to $\mathbf{ACA}$, which are well-known
subsystems of second-order arithmetic [48]. However, Feferman’s proposal has
been criticized by Adams and Luo in [4, 3] and more recently by Avron in [5].
They observed that in certain sections of Das Kontinuum, Weyl introduces non-
arithmetical sets and makes use of induction for non-arithmetical formulas.
Therefore, they concluded that Weyl’s system should be stronger than what
thought by Feferman, even if ${\bf ACA}_{0}$ should be sufficient to
reconstruct predicative analysis as developed in Das Kontinuum.

The systems introduced in these papers are many-sorted logics axiomatized over
a dependent type theory, in a way similar to both levels of the Minimalist
Foundation. But they differ between them and with MF for what regards
exponentiation of functions. Indeed, Adams and Luo’s system in [4, 3] includes
some exponentiation of $\lambda$-functions in the form of function types,
which are treated as large types in the sense that they are not contained in
the universe of small types, that in turn can be thought of as the universe of
sets. Then, Avron in [5] restricts the possibility to form exponentials by
assuming that only certain types might serve as codomains. However, in his
system we cannot define a set by quantifying over functions. Instead, in MF
there is no exponentiation of functions between collections but only sets
exponentiating $\lambda$-functions between sets.

##  3 Constructive Predicative Theories

Among the most popular frameworks introduced as foundations for Bishop’s
constructive mathematics there are Constructive Zermelo-Fraenkel set theory
$\mathbf{CZF}$ [1] and Martin-Löf Type Theory MLTT [39]. More recently, an
extension of the latter called Homotopy Type Theory HoTT [53] has gained much
attention, especially for its applications to synthetic homotopy theory and
higher categories. All these systems are examples of constructive and
predicative theories. However, the predicativity of these theories is closely
tied to the adoption of a constructive logic. Indeed, whenever they are
extended with the law of excluded middle or equivalent classical principles,
they become impredicative and thus they are not compatible with classical
predicativity a lá Weyl. Briefly, the issue is that such theories are closed
under the exponentiation of functional relations and the two-element set that,
when classical logic is added, are strong enough to allow for impredicative
constructions. Therefore, we cannot establish the predicativity of their
classical counterparts, as it happens instead in the case of Heyting
arithmetic or of the Minimalist Foundation, which we will introduce in detail
in Section 6.

###  3.1 Aczel’s Constructive Zermelo-Fraenkel set theory

CZF [1] is a theory formulated in the same language of classical ZF and based
on intuitionistic logic. The theory includes the following axioms:
extensionality, pairing, union, restricted separation, infinity,
$\in$-induction, strong collection, and subset collection.

The predicative nature of the theory is reflected in the restriction of
separation to $\Delta_{0}$-formulas, which means that the defining formula
$\phi$ might quantify only over sets that have already been introduced, and in
the rejection of the full powerset axiom. The powerset axiom is replaced by
the weaker axiom of subset collection, which in turn implies the
exponentiation axiom for functions. Functions are defined as functional
relations in the standard set-theoretic manner.

We recall that the Axiom of Choice in the form

$({\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,f(x))$

cannot be added to CZF while preserving its constructive character:

######  Theorem 3.1.

CZF \+ AC derives the law of excluded middle for $\Delta_{0}$-formulas.

###### Proof.

See [2]. ∎

######  Remark 3.2.

In [2], it is shown that this proof can be carried out in a weaker subsystem
of CZF. On the other hand, the weaker principles of countable choice and
dependent choice can be added to CZF without leading to undesirable results.

Moreover, in CZF real numbers form a set:

######  Theorem 3.3.

Real numbers both as Dedekind cuts or as Cauchy’s sequences form a set in CZF.

###### Proof.

See [2]. ∎

###  3.2 Martin-Löf’s type theory

Martin-Löf Type Theory (MLTT) [39] is a foundation for constructive
mathematics, which was explicitly introduced to formalize Bishop’s mathematics
[37]. The theory is not presented in the usual language of first-order logic,
but it is formulated in the language of dependent type theory.

Types of MLTT are introduced by means of four rules: formation, introduction,
elimination and computation. In particular, the constructors of a given type
are specified by the introduction rules, while the elimination rule states
simultaneously a principle of induction at the level of types and of
definition by recursion at the level of terms with the aid of the computation
rules. The predicative nature of the theory is related to the fact that all
the types are inductively generated by the relevant rules. Two fundamental
aspects of MLTT are the presence of a primitive notion of function, called
here $\lambda$-function to disambiguate it from the notion of functions as
functional relation, and the identification between propositions and types.
$\lambda$-functions are represented as $\lambda$-terms and this differentiates
this foundational theory from other theories such as CZF. The identification
between propositions and types makes the constructive logic of MLTT stronger
than usual intuitionistic logic. This additional strength is visible in the
case of the existential quantifier that is identified with the dependent sums
type $\Sigma$. The elimination rule for this type is enough strong to allow
for the definition of projection operators 222We recall that the canonical
elements of $\Sigma$-types given by the introduction rule are pairs.. These
projections play a fundamental role in establishing the following fact:

######  Theorem 3.4.

The type-theoretic Axiom of Choice

$({\bf AC})\ \Pi_{(x:A)}\ \Sigma_{(y:B)}\ R(x,y)\
\rightarrow\Sigma_{(f:A\rightarrow B)}\ \Pi_{(x:A)}\ R(x,f(x))$

is derivable in MLTT.

We remark that the rules for $\Sigma$-type are enough strong to derive also
the corresponding choice rule. Furthermore, the Axiom of Unique Choice AC!,
which identifies functional relations with $\lambda$-functions,

$({\bf AC!})\ \Pi_{(x:A)}\ \Sigma!_{(y:B)}\ R(x,y)\ \rightarrow\
\Sigma_{(f:A\rightarrow B)}\ \Pi_{(x:A)}\ R(x,f(x))$

(where $\Sigma!_{(y:B)}\ R(x,y)\ {\ :\equiv\ }\ \Sigma_{(y:B)}\ R(x,y)\
\times\ \Pi_{(y_{1},y_{2}:B)}\ (R(x,y_{1})\ \times\ R(x,y_{2}))\ \rightarrow\
\mathsf{Id}(B,y_{1},y_{2})$) also follows from the validity of AC.

Henceforth, we can refer in MLTT with the name function to either a functional
relation or a $\lambda$-function without ambiguity. As anticipated in section
2, the two notions of function are instead kept distinct in the Minimalist
Foundation as well as in some modern presentations of Weyl’s system as those
given in [3, 5].

Due to the absence of quotient sets in MLTT, real numbers, both à la Dedekind
or à la Cauchy, are formally represented there using setoids whose elements
are then indexed by a set. A setoid [40], called set by Bishop in ([6], p.
13), is a pair $(A,=_{A})$, consisting of a set called support equipped with a
suitable equivalence relation $a=_{A}a^{\prime}\ [a,a^{\prime}:A]$ used to
equate the elements in the same equivalence class.

For example, Bishop reals in [6] can be represented as the setoid whose
support is given by the set of Cauchy regular sequences from the set of
natural numbers to that of rational numbers equipped with the equivalence
relation $=_{\mathcal{R_{C}}}$ as in [6], pp.15-16. Bishop defined them by
using the notion of operation which we can identify in MLTT with the notion of
$\lambda$-function, i.e. with a $\lambda$-term of MLTT. Moreover, for what we
have said about the notion of function in MLTT, Cauchy reals defined as Cauchy
functional relations can be identified in MLTT with Bishop reals. For unifying
the various concepts, we name them Cauchy sequences a’ la Bishop.

Instead, in MLTT Dedekind reals can be defined only relatively to a universe
of sets $U_{k}$ (indexed by a natural number $k$) and are represented by a
setoid whose support is given by the set of Dedekind cuts on the rationals
relative to $U_{k}$ as follows:

######  Definition 3.5.

A Dedekind cut on the rationals is a pair of propositional functions
$L,U:\mathbb{Q}\rightarrow\mathcal{U}_{k}$ for some universe $U_{k}$ that
satisfy the usual conditions of being inhabited, disjoint, open, monotone, and
located, all defined as in [35].

######  Definition 3.6.

We denote with $\mathbb{R}_{D_{k}}$ the support of Dedekind cuts made of
propositional functions with values in the universe $U_{k}$ for any natural
number $k$.

Again thanks to the validity in MLTT of choice principles on natural numbers
and thanks to the exponentiation of $\lambda$-terms by means of the dependent
product type $\Pi_{(x:A)}B(x)$ of any family of types $B(x)(x:A)$, in MLTT
each real number à la Dedekind in the form of a Dedekind cut corresponds
bijectively to a Bishop real and hence to a Dedekin cut in
$\mathbb{R}_{D_{0}}$.

######  Proposition 3.7.

In MLTT, Dedekind reals $\mathbb{R}_{D_{0}}$ are in bijective correspondence
with the Cauchy reals, defined as Cauchy sequences à la Bishop.

###### Proof.

See Prop. 17 in [7] and section 4.3 of [34]. ∎

As a consequence, we deduce that:

######  Proposition 3.8.

In MLTT, Dedekind reals $\mathbb{R}_{D_{0}}$ are in bijective correspondence
with $\mathbb{R}_{D_{k}}$ for any natural number $k$.

###### Proof.

Given a Dedekind cut as in def. 3.5 in $\mathbb{R}_{D_{k}}$ for any natural
number $k$, by using the axiom of choice we can define a Bishop real given by
an operation $\lambda n.x_{n}$, usually written $(x_{n})_{n}$, as in Prop. 17
in [7] or section 4.3 in [34], whose cut $(L_{0},D_{0})$ in
$\mathbb{R}_{D_{0}}$ is defined as

$L_{0}\equiv\\{p:\mathbb{Q}\ \mid\ \Sigma_{n:\mathbb{N}}\ p\leq x_{n}-2/n\
\\}\qquad\qquad U_{0}\equiv\\{q:\mathbb{Q}\ \mid\ \Sigma_{n:\mathbb{N}}\ q\geq
x_{n}+2/n\ \\}$

and is propositionally equivalent to the starting cut $(L,U)$ in
$\mathbb{R}_{D_{k}}$ thanks to the correspondence between Dedekind cuts,
formal points of point-free topology of real numbers and Bishop reals in
section 4.3 of [34]. ∎

######  Remark 3.9.

The previous proposition shows that some instances of resizing can be derived
from choice principles constructively. In particular, this can be regarded as
the fact that special cases of Russell’s Reducibility Axiom can be derived in
the presence of choice principles provided that the logic is constructive.

###  3.3 Homotopy Type Theory

Homotopy Type Theory (HoTT) [53] is an extension of MLTT and is an instance of
Voevodsky’s Univalent Foundations. It extends MLTT with the Univalence Axiom
and Higher Inductive types, examples of which include quotients of homotopy
sets and propositional truncation. The Univalence Axiom is formulated as
follows:

$\mbox{the map}\ \mathsf{idtoeqv}:(A=_{\mathcal{U}}B)\ \rightarrow\ (A\simeq
B)\ \mbox{is an equivalence}$

where $(A\simeq B)$ is the type of equivalences between $A$ and $B$. The map
$\mathsf{idtoeqv}$ and the notion of equivalence $\simeq$ are defined as in
Section 2 of [53]. Among the consequences of this axiom, there are certain
extensional principles (e.g. function extensionality) that are not available
in intensional MLTT.

A significant feature of HoTT is allowing for a representation of logical
notions alternative to the propositions-as-types paradigm. The key notion here
is that of h-proposition, where a type $P$ is a h-proposition whenever for all
$x,y:P$, $x=_{P}y$ holds, and it is analogous to the notion of mono type in
the internal theory of topos in [23]. Further, a type $A$ is a h-set if the
associated identity type $=_{A}$ is a h-proposition.

The logic of h-propositions behaves differently from the propositions-as-types
logic and is similar to the internal logic of elementary topoi or of regular
categories as presented in [23]. In particular, the existential quantifier is
not identified with the $\Sigma$-type any longer. Rather, it is identified
with the propositional truncation of the $\Sigma$:

$\exists_{(x:A)}\ P(x)\ {\ :\equiv\ }\ ||\ \Sigma_{(x:A)}\ P(x)\ ||$

Observe that the propositional truncation of a type is always a h-proposition.
Indeed the constructors for the propositional truncation of a type $A$ are the
following: if $a:A$, then $|\ a\ |:||\ A\ ||$ and $x=_{||A||}y$ holds for all
$x,y:||\ A\ ||$. Moreover, it holds that if $P$ is a h-proposition, then it is
equivalent to its truncation.

Observe also that in HoTT, while it is obviously possible to derive the type-
theoretic AC under the identification propositions-as-types, it is not instead
possible to derive the type-theoretic AC using the identification of
propositions as h-propositions in the version:

$\Pi_{(x:A)}\ \exists_{(y:B)}\ R(x,y)\ \rightarrow\ \exists_{(f:A\rightarrow
B)}\ \Pi_{(x:A)}\ R(x,f(x))$

with $A,B$ h-sets and $R(x,y)$ h-proposition for $x:A,y:B$, as shown in [53].
Indeed, in HoTT it is only possible to derive the axom of unique choice AC!
formulated as follows

$({\bf AC!})\ \Pi_{(x:A)}\ \exists!_{(y:B)}\ R(x,y)\ \rightarrow\
\Sigma_{(f:A\rightarrow B)}\ \Pi_{(x:A)}\ R(x,f(x))$

with $A,B$ types and $R(x,y)$ h-proposition and where unique existence
$\exists!_{(y:B)}R(x,y)$ amounts to the following condition:

$\exists_{(y:B)}\ R(x,y)\ \times\ \Pi_{(y_{1},y_{2}:A)}\ R(x,y_{1})\ \land\
R(x,y_{2})\ \rightarrow\ y_{1}=_{B}y_{2}.$

######  Proposition 3.10.

AC! can be derived in HoTT.

###### Proof.

See [43]. ∎

######  Remark 3.11.

Unique existence can be formulated in an equivalent way in HoTT by employing
the notion of contractible type. A type $A$ is said to be contractible if the
following type is inhabited:

$\Sigma_{(x:A)}\ \Pi_{(y:A)}\ x=_{A}y.$

Therefore, we can rewrite unique choice by requiring the contractibility of
$\Sigma_{(y:B)}\ R(x,y)$.

######  Remark 3.12.

The proof of AC! in [43] is a special case of a result that holds in the
internal dependent type theory $\mathcal{T}_{reg}$ of any regular category
[23]. Following [23], observe that the propositional truncation of a
$\Sigma$-type $\Sigma_{(x:A)}\ P(x)$ can be equivalently expressed in
$\mathcal{T}_{reg}$ as a quotient, namely the quotient $\Sigma_{(x:A)}\
P(x)/\mathbf{1}$ over the unit type identifying all the proof-terms. Then, the
proof in [43] corresponds to the argument in [23] relying on the fact that
unique existence can be written as $\Sigma_{(y:B)}\ R(x,y)$ together with the
usual uniqueness condition. In this case, $\Sigma_{(y:B)}\ R(x,y)$ is a mono
type, according to the terminology introduced in [23], and is equivalent to
its quotient over the unit type, and hence we can use $\Sigma$-projections to
prove AC!.

A crucial feature of HoTT is the presence of quotient sets as higher inductive
types. This means that Cauchy real numbers à la Bishop can be formalized as a
quotient of the type of Cauchy sequences under the equivalence relation
$=_{\mathbb{R}_{C}}$ without resorting to setoids. In particular, they form a
set in HoTT.

The case of Dedekind reals is more delicate. The notion of cut can be
formalized as a pair of propositional functions
$(L,U):\mathbb{Q}\rightarrow\mathsf{Prop}_{\mathcal{U}_{k}}$ relative to some
univalent universe of set $U_{k}$, that satisfy the conditions of Def.3.5. So
it is possible to show that the Dedekind cuts up to a given universe form a
set, but we cannot collect into a set all the Dedekind cuts varying in any
universe unless impredicativity in the form of propositional resizing is
assumed. Indeed, for the absence of dependent choice Prop.3.8 fails in HoTT,
and hence there is no reduction of Dedekind reals of level $k$ to those of the
lowest level.

This fact can be contrasted with what happens in the Minimalist Foundation,
and in particular in its extensional level where the presence of the power
collection of a set allows us to collect all Dedekind cuts together inside the
theory.

In any case, it must be noticed that in HoTT real numbers a’ la Cauchy are
defined as a higher inductive type $\mathbb{R}_{\mathsf{c}}$ ([53], see Sec.
11.3). Hence, they form a set. However, the construction is different from the
usual type-theoretic definition of Cauchy reals or Bishop reals. In
particular, the definition of $\mathbb{R}_{\mathsf{c}}$ is intended to
formalize the idea that Cauchy reals can be regarded as the free complete
metric space generated by the rationals.

##  4 The incompatibility of ${\bf HA}^{\omega}+{\bf
iRC!}_{\mathbf{N},\mathbf{N}}$ with Weyl’s predicativity

In this section, we want to show that already the weaker system of Heyting
Arithmetic in all finite types (${\bf HA^{\omega}}$), when extended with the
internal rule of unique choice and the law of excluded middle, becomes
impredicative. Since the most common constructive and predicative foundations
interpret this system, then the result can be easily extended to these more
expressive theories.

For the presentation of ${\bf HA^{\omega}}$, we refer to the standard
reference [52].

The finite type structure $\mathrm{T}$ is defined as follows: $\mathbf{N}$ is
a finite type and if $\sigma,\tau$ are finite types, then so are
$\sigma\rightarrow\tau$ and $\sigma\times\tau$.

The language of ${\bf HA^{\omega}}$ includes countably infinite variables
$x^{\sigma},y^{\sigma},z^{\sigma},\ldots$ for each type symbol
$\sigma\in\mathrm{T}$. A binary predicate for equality $=_{\sigma}$ at each
type $\sigma\in\mathrm{T}$ and an application operator
$\mathsf{Ap}_{\sigma,\tau}$ for all $\sigma,\tau\in\mathrm{T}$. Furthermore,
the language comprehends constants for zero and successor, recursor, pairing
and projections and the combinators ${\bf k}$ and ${\bf s}$.

The axioms of ${\bf HA^{\omega}}$ include the axioms of many-sorted
intuitionistic predicate logic with equality, congruence rules for equality,
the usual axioms for zero and successor with the induction scheme, and the
defining conditions for the constants.

We recall two fundamental results about ${\bf HA^{\omega}}$. It is immediate
to realize that Heyting Arithmetic (HA) is a subsystem of ${\bf HA^{\omega}}$.
Furthermore, if we extend ${\bf HA^{\omega}}$ with the Axiom of Choice for all
finite types

$({\bf AC}_{\sigma,\tau})\ \forall x^{\sigma}\ \exists y^{\tau}\ \phi(x,y)\
\supset\ \exists f^{\sigma\rightarrow\tau}\ \forall x^{\sigma}\ \phi(x,fx)$

the resulting theory is conservative over HA. This result is known as
Goodman’s Theorem [19].

Another significant fact is that ${\bf HA^{\omega}}$ is equi-consistent with
its classical version by a double negation translation. This result can be
found in [51]. However, this result does not apply to the case of ${\bf
HA^{\omega}}+{\bf AC}_{\sigma,\tau}$. Indeed, it is possible to show that
${\bf HA^{\omega}}+{\bf AC}_{\sigma,\tau}+{\bf LEM}$ is enough strong to
derive the second-order comprehension axiom and thus to interpret full second-
order classical arithmetic ${\bf PA^{2}}$, which is an impredicative theory.
The first to observe that ${\bf HA^{\omega}}$ extended with the Axiom of
Choice and classical logic allows to derive the second-order comprehension
principle was Spector in [49]. We remark that already the internal rule of
unique choice (${\bf iRC!}_{\sigma,\tau}$) is sufficient to carry out the
proof.

######  Definition 4.1.

The internal rule of unique choice for ${\bf HA^{\omega}}$ is formulated as
follows:

$\mbox{if}\ \ {\bf HA^{\omega}}\vdash\forall x^{\sigma}\ \exists!y^{\tau}\
\phi(x,y)\qquad\mbox{then}\ \ {\bf HA^{\omega}}\vdash\exists
f^{\sigma\rightarrow\tau}\ \forall x^{\sigma}\ \phi(x,fx)$

where $\exists!y^{\tau}\ \phi(x,y)\ {\ :\equiv\ }\ \exists y^{\tau}\
\phi(x,y)\land\forall y_{1}^{\tau}\ \forall y_{2}^{\tau}\ (\ \phi(x,y_{1})\
\land\ \phi(x,y_{2})\ \supset\ y_{1}=_{\tau}y_{2})$.

######  Remark 4.2.

We call the rule displayed above internal rule of unique choice to contrast it
with the following rule of unique choice: if ${\bf HA^{\omega}}\ \vdash\
\forall x^{\sigma}\ \exists!y^{\tau}\ \phi(x,y)$, then there exists a function
$f^{\sigma\ \rightarrow\ \tau}$ such that ${\bf HA^{\omega}}\ \vdash\ \forall
x^{\sigma}\ \phi(x,fx)$, where the existence of the choice function is stated
externally. Admittedly, in ${\bf HA^{\omega}}$ the two rules are equivalent by
the results in [51]. In general, this equivalence holds for all the systems
that satisfy the existence property, but it cannot be stated in general. For
instance, it does not hold for classical systems.

The theory ${\bf PA}^{2}$ is usually formulated as an extension of the
language of ${\bf PA}$ by a second sort of variables $X,Y,Z\ldots$ standing
for subsets of natural numbers and a membership symbol $\in$, where $t\in X$
is a new atomic formula for $t$ first-order term. The axioms include the
second-order induction axiom and the full scheme of comprehension for sets of
natural numbers. However, the theory can be equally formulated in a language
with typed primitive function symbols. Then first-order variables are
interpreted as variables of type $\mathbf{N}$, second-order variables are
interpreted by their characteristic functions with type
$\mathbf{N}\rightarrow\mathbf{N}$ and the atomic formulas $t\in X$ are
interpreted by $X(t)=1$. In particular, the comprehension axiom is formulated
as follows:

$({\bf CA})\ \ \exists f^{\mathbf{N}\ \rightarrow\ \mathbf{N}}\ \forall
x^{\mathbf{N}}\ \ (\ fx=1\ \Leftrightarrow\ \phi(x)\ )$

where $\phi(x)$ is an arbitrary formula of the language provided that $f$ does
not occur free in $\phi$.

Now, we show that in ${\bf HA^{\omega}}+{\bf
iRC!_{\mathbf{N},\mathbf{N}}}+{\bf LEM}$ this comprehension principle is
derivable.

######  Proposition 4.3.

The theory ${\bf HA^{\omega}}+{\bf iRC!_{\mathbf{N},\mathbf{N}}}+{\bf LEM}$
derives the second-order comprehension principle ${\bf CA}$.

###### Proof.

Let us consider a formula $\phi(x)$ with $x$ of type $\mathbf{N}$. Then, we
can define the following relation

$\chi_{\phi}(x,y)\ {\ :\equiv\ }\ (\phi(x)\ \land\ y^{\mathbf{N}}=1)\ \lor\
(\neg\phi(x)\ \land\ y^{\mathbf{N}}=0)$

By the validity of LEM, we can argue by cases:

  * –

if $\phi(x)$ holds, then $\chi_{\phi}(x,1)$ holds.

  * –

if $\neg\phi(x)$ holds, then $\chi_{\phi}(x,0)$ holds.

We recall that $0\neq 1$ follows from the axioms of ${\bf HA^{\omega}}$. Thus
we obtain $\forall x^{\mathbf{N}}\ \exists!y^{\mathbf{N}}\ \chi_{\phi}(x,y)$,
that is a functional relation.

Therefore, we can apply ${\bf iRC!}_{\sigma,\tau}$ (for
$\sigma,\tau=\mathbf{N}$) and we obtain that

$\exists f^{\mathbf{N}\rightarrow\mathbf{N}}\ \forall x^{\mathbf{N}}\
\chi_{\phi}(x,fx)$

which, unfolding the definition of $\chi_{\phi}$, amounts to

$\exists f^{\mathbf{N}\rightarrow\mathbf{N}}\ \forall x^{\mathbf{N}}\
((\phi(x)\ \land\ fx=1)\ \lor\ (\neg\phi(x)\ \land\ fx=0))$

From which CA follows. ∎

######  Corollary 4.4.

The theory ${\bf PA}^{2}$ can be interpreted within ${\bf HA^{\omega}}+{\bf
iRC!_{\mathbf{N},\mathbf{N}}}+{\bf LEM}$, which is then impredicative and
incompatible with Weyl’s predicativity.

##  5 The incompatibility of MLTT, HoTT and CZF with Weyl’s predicativity

In this section, we show that the classical extensions of the systems
presented in Section 3 are not compatible with classical predicativity.

By compatibility of a theory $\mathsf{T}_{1}$ with another theory
$\mathsf{T}_{2}$ we mean that there exists a translation from $\mathsf{T}_{1}$
to $\mathsf{T}_{2}$ preserving the meaning of logical and set-theoretical
constructors. In this manner, a proof of a theorem in $\mathsf{T}_{1}$ can be
transported into $\mathsf{T}_{2}$ with the same meaning.

It is easy to see that ${\bf HA^{\omega}}$ extended with ${\bf
iRC!_{\mathbf{N},\mathbf{N}}}$ is compatible both with MLTT and HoTT since
these are essentially extensions of ${\bf HA^{\omega}}$ validating ${\bf
iRC!_{\mathbf{N},\mathbf{N}}}$.

######  Definition 5.1.

A compatible translation from ${\bf HA}^{\omega}+{\bf
iRC!_{\mathbf{N},\mathbf{N}}}$ to MLTT can be defined as follows:

  * -

$(\mathbf{N})^{\ast}\ {\ :\equiv\ }\ \mathbb{N}$, while
$(\sigma\rightarrow\tau)^{\ast}\ {\ :\equiv\ }\
\sigma^{\ast}\rightarrow\tau^{\ast}$ and $(\sigma\times\tau)^{\ast}\ {\
:\equiv\ }\ \sigma^{\ast}\times\tau^{\ast}$.

  * -

variables $x:\sigma$ are translated as variables $x:\sigma^{\ast}$ and
application terms as application terms in MLTT.

  * -

constants of ${\bf HA}^{\omega}$ are translated as the corresponding terms in
MLTT: e.g., $(\textbf{k})^{\ast}{\ :\equiv\ }\lambda x.\lambda
y.x:\sigma^{\ast}\rightarrow(\tau^{\ast}\rightarrow\sigma^{\ast})$.

  * -

the formulas of many-sorted intuitionistic logic are sent to the corresponding
types according to the propositions-as-types principle: e.g., $(\exists
x^{\sigma}\ \phi(x))^{\ast}\ {\ :\equiv\ }\ \Sigma_{(x:\sigma^{\ast})}\
\phi^{\ast}(x)$.

######  Proposition 5.2.

The translation $(-)^{\ast}$ is a compatible translation of ${\bf
HA}^{\omega}+{\bf iRC!_{\mathbf{N},\mathbf{N}}}$ in MLTT.

###### Proof.

The proof is by induction over the structure of derivations. In particular,
the interpretation of the number-theoretic internal rule of unique choice
follows from the validity of the more general rule of choice in MLTT. ∎

Therefore, when MLTT is extended with the law of excluded middle, we can
reproduce the argument showing the incompatibility of HAω with Weyl’s
predicativity:

######  Corollary 5.3.

MLTT with the addition of the law of excluded middle becomes impredicative.

###### Proof.

It follows from Prop. 5.2 and Cor. 4.4. ∎

######  Remark 5.4.

In general, in MLTT with classical logic we can use the type of booleans 2 as
a classifier, however we do not get a (strong) power object. For instance, the
type $\mathbb{N}\rightarrow{\bf 2}$ behaves more like a weak power object,
because MLTT lacks of the relevant extensionality principles.

The translation of ${\bf HA}^{\omega}$ into MLTT defined above can be refined
in the case of HoTT. A finite type $\sigma$ is translated as a pair
$\sigma^{\ast}\ \equiv\ (\sigma^{\star},p_{\sigma^{\star}})$, where the second
component is a proof that $\sigma^{\star}$ is a h-set in HoTT. Similarly,
formulas of ${\bf HA}^{\omega}$ can be translated as h-propositions in HoTT,
while the rest of the translation is defined as in the case of MLTT.
Therefore, the following fact holds:

######  Proposition 5.5.

The translation $(-)^{\ast}$ is a compatible translation of ${\bf
HA}^{\omega}+{\bf iRC!_{\mathbf{N},\mathbf{N}}}$ in HoTT.

As in the case of MLTT, we can reproduce the same proof of Prop.4.3 but with a
significant difference. The law of excluded middle cannot be formulated
according to the propositions-as-types identifications for all types in HoTT,
because this would yield a contradiction in presence of Univalence (see Ch.3
[53]). However, it is still possible to formulate ${\bf LEM}$ for all those
types that are h-propositions. This formulation serves our purposes and is
consistent with Univalence.

######  Corollary 5.6.

HoTT with the addition of the law of excluded middle for h-propositions
becomes impredicative.

###### Proof.

It follows from Prop. 5.5 and Cor. 4.4. ∎

######  Remark 5.7.

When HoTT is extended with LEM for h-propositions, it is possible to show that
the type of h-propositions within any universe $\mathcal{U}$, that is
$\mathsf{Prop}_{\mathcal{U}}$, is equivalent (and hence equal by Univalence)
to the type of Booleans 2 in $\mathcal{U}$. Therefore, 2 behaves like a
subobject classifier and we can prove that the category of h-sets, as defined
in [53], is an elementary topos.

######  Definition 5.8.

A compatible translation from ${\bf HA}^{\omega}+{\bf
iRC!_{\mathbf{N},\mathbf{N}}}$ to CZF can be defined as follows:

  * -

$(\mathbf{N})^{\ast}\ {\ :\equiv\ }\ \omega$, while
$(\sigma\rightarrow\tau)^{\ast}\ {\ :\equiv\ }\
\sigma^{\ast}\rightarrow\tau^{\ast}$, which is the set of functional relations
from $\sigma^{\ast}$ to $\tau^{\ast}$, and $(\sigma\times\tau)^{\ast}\ {\
:\equiv\ }\ \sigma^{\ast}\times\tau^{\ast}$, which is the usual cartesian
product of sets.

  * -

terms of $\mathbf{HA}^{\omega}$ are interpreted by the corresponding definable
terms of CZF.

  * -

the formulas of many-sorted intutionistic logic are interpreted by the
corresponding formulas of intuitionistic logic, with sorts interpreted as
predicates: e.g., $(\forall x^{\sigma}\ \phi(x))^{\ast}{\ :\equiv\ }\forall x\
(x\in\sigma^{\ast}\ \rightarrow\ \phi^{\ast}(x))$.

######  Proposition 5.9.

The translation $(-)^{\ast}$ is a compatible translation of ${\bf
HA}^{\omega}+{\bf iRC!_{\mathbf{N},\mathbf{N}}}$ in CZF.

######  Corollary 5.10.

CZF with the addition of the law of excluded middle becomes impredicative.

###### Proof.

It follows from Prop. 5.9 and Cor. 4.4. ∎

It is worth noting that in the case of CZF, the incompatibility with classical
predicativity can be shown by a very direct and simple argument proved by
Aczel in [1]:

######  Proposition 5.11.

The axiom of exponentiation and the law of excluded middle for
$\Delta_{0}$-formulas imply the powerset axiom.

###### Proof.

It is enough to show that $\mathcal{P}(1)$ is a set. This follows from an
application of LEM. The rest follows from the fact that the powerset axiom is
equivalent to exponentiation plus the existence of the powerset of the
singleton set. ∎

Moreover, since the powerset axiom implies subset collection, which in turn
implies exponentiation, it follows:

######  Proposition 5.12.

CZF with classical logic and ZF prove the same set of theorems.

###### Proof.

See [1]. ∎

##  6 A possible way out: the Minimalist Foundation

In this section, we want to show that there exists a constructive predicative
system that does not present the same incompatibility with classical
predicativity as the other systems previously considered and, at the same
time, is enough expressive to allow for the development of non-trivial
mathematics by keeping a form of exponentiation for a primitive notion of
functions defined by $\lambda$-terms. This system is the Minimalist Foundation
MF.

MF is a two-level foundation for constructive mathematics, that was first
conceived in [33] and then fully developed in [24]. It consists of an
intensional level, called mTT, and an extensional one, called emTT, together
with an interpretation of the latter into the first, as defined in [24].

The two-level structure facilitates the compatibility of MF with the most
relevant constructive and classical foundations as shown in [24]: the
intensional level mTT is compatible with MLTT and Coquand-Paulin’s Calculus of
Inductive Constructions [11], while the extensional level is compatible with
CZF, HoTT and the internal theory of elementary topoi in [22, 23]. It is a
remarkable property that both levels of MF are compatible with HoTT as shown
in [9].

Moreover, both levels of MF extend a version of Martin-Löf’s type theory with
a primitive notion of proposition: mTT extends the intensional type theory in
[39], while emTT extends the extensional version presented in [38].

In MF there are four primitive distinct sorts: small propositions,
propositions, sets and collections. The following diagram shows the relations
between these primitive sorts

small propositionssetspropositionscollections

The basic forms of judgement in MF include:

$A\ set\ [\Gamma]\qquad B\ coll\ [\Gamma]\qquad\phi\ prop\ [\Gamma]\qquad\psi\
prop_{s}\ [\Gamma]$

to which we add the meta-judgement

$A\ {\it type}\ [\Gamma]$

where ‘type’ is to be interpreted as a meta-variable ranging over the four
basic sorts.

The set-constructors of mTT and emTT include those of first order Martin-Löf’s
type theory, respectively as presented in [39] and [38]. Hence we have the
following set constructors: the empty set $N_{0}$, the singleton set $N_{1}$,
the set of lists $List(A)$ over a set $A$, hence the set of natural numbers
$\mathsf{N}$, the indexed sum and the dependent product of the family of sets
$B(x)\ set\ [x\in A]$ denoted respectively as $\Sigma_{x\in A}\ B(x)$ and
$\Pi_{x\in A}\ B(x)$, the disjoint sum $A+B$ of the set $A$ with the set $B$.
In the case of the extensional level emTT we have that sets are closed under
effective quotients $A/R$ over a set $A$, provided that $R$ is a small
equivalence relation $R(x,y)\ prop_{s}\ [x\in A,y\in A]$. This set
constructors is not included in the intensional level mTT. Furthermore, both
the sets of mTT and those of emTT include also their small propositions $\phi\
prop_{s}$ regarded as sets of their proofs. Small propositions are those
propositions closed under intuitionistic connectives and under quantifiers and
equalities restricted to sets.

Collections of mTT and emTT include their sets and the indexed sum
$\Sigma_{x\in A}B(x)$ of the family of collections $B(x)\ coll\ [x\in A]$
indexed over a collection $A$. Moreover, they also include propositions $\psi\
prop$ regarded as collections of their proofs. A significant distinction
between mTT-collections and emTT-collections is the following: the former
includes the proper collection of small propositions $\mathsf{prop_{s}}$ and
the collection of small propositional functions
$A\rightarrow\mathsf{prop_{s}}$ over a set $A$ (which are definitely not sets
predicatively when $A$ is not empty), while the latter includes the power-
collection of the singleton ${\cal P}(1)$, which is the quotient of the
collection of small propositions under the relation of equiprovability, and
the power-collection $A\rightarrow{\cal P}(1)$ of a set $A$, that can be
written simply as ${\cal P}(A)$.

In mTT we identify predicates over the set $A$ with propositional functions
defined as primitive $\lambda$-terms. Hence, in emTT a subset of a set $A$ is
identified with the equivalence class of propositional function up to
equiprovability. So this use of $\lambda$-terms corresponding to predicates is
a major difference with axiomatic set theory where subsets of a set $A$ are
simply defined as sets in a certain relation with $A$ and hence are identified
with functional relations into the boolean set $\\{0,1\\}$ when the logic is
classical.

Both propositions of mTT and emTT include standard connectives and
quantifiers. However, they differ in the way the rules for propositional
equality are given. Indeed, mTT-propositions include an intensional
propositional equality defined as in [39], except for the fact that the
elimination rule is restricted to propositions. While emTT-propositions
include an extensional propositional equality with an elimination rule
formulated like that in [38].

Finally, we recall that emTT-propositions are proof-irrelevant and have one
canonical element denoted as $\mathsf{true}$.

It is relevant for our discussion to remark that elimination rules for
propositions act only towards propositions and not towards collections. The
same applies to small propositions. In this way, mTT and emTT do not generally
validate choice principles. In particular, even unique choice cannot be
derived in MF, thanks to the results in [30, 31, 25] and similarly to what
happens in Coquand’s Calculus of Constructions CoC, as first proved in [50].
This is in contrast with what happens in MLTT and in HoTT, as we have seen in
Section 3. The fact that choice principles are not validated in MF is
important in connection with the notion of compatibility introduced in Section
5. In this way, MF turns out to be also compatible with theories where choice
does not generally hold, such as CoC.

Now, we discuss the status of the internal rule of unique choice in MF, in
particular in mTT.

######  Definition 6.1.

In mTT the internal rule of unique choice holds if for any derivable small
proposition

$R(x,y)\ prop_{s}\ [x\in A,y\in B]$

and for any derivable judgement of the form

$p(x)\in\exists!_{y\in B}\ R(x,y)\ [x\in A]$

there exists a proof-term $q$ such that the following judgement is derivable

$q\in\exists_{f\in A\rightarrow B}\ \forall_{x\in A}\
R(\,x,\mathsf{Ap}(f,x)\,)\ \ $

We call number-theoretic internal rule of unique choice the instance of the
internal rule of unique choice when $A$ and $B$ coincide with the set
$\mathbb{N}$ of natural numbers.

Instead, we reserve the name rule of unique choice for the version of the
above rule requiring the external existence of the choice function term $f$,
i.e. if $\exists!_{y\in B}\ R(x,y)\ [x\in A]$ holds then we can derive a term
$f\in A\rightarrow B$ such that $R(\,x,\mathsf{Ap}(f,x)\,)\ [x\in A]$ holds.

From [25] we know that the rule of unique choice is not valid in mTT:

######  Proposition 6.2.

The rule of unique choice is not valid in mTT.

###### Proof.

See proof of Th.1 of [25]. ∎

The existence property of mTT, following from normalization results, would
allow to deduce the equivalence of the rule of unique choice with its internal
version and hence the non-validity of the internal rule of unique choice in
mTT, too.

Nevertheless, it is worth pointing out that without relying on the existence
property, we can show the not validity of the internal rule of unique choice
following the same argument in [25] since this can be exported also to
extensions of mTT, not validating the existence property, such as its
classical version:

######  Proposition 6.3.

If mTT satisfies the internal rule of unique choice, then it satisfies the
axiom of unique choice.

###### Proof.

The proof of Prop.3 in [25] can be easily adapted to the case of the internal
rule of unique choice. ∎

Now, thanks to the model in [50], we deduce from Prop. 6.3 that

######  Corollary 6.4.

mTT does not validate the internal rule of unique choice.

It is important to remark that already the intensional level mTT can be
regarded as an extension of ${\bf HA}^{\omega}$. Indeed, it is possible to
show that there is a compatible translation of this theory into mTT following
a similar translation of Section 5 for MLTT by interpreting ${\bf
HA}^{\omega}$-propositions as mTT-propositions. What is most interesting is
that MF extends ${\bf HA}^{\omega}$ while preserving the fundamental property
of equi-consistency with its classical counterpart. Indeed, recently it has
been shown that both levels of MF are equi-consistent with their classical
counterparts (collapsed to the extension of the extensional level emTT with
the law of excluded middle), unlike theories such as MLTT, HoTT and CZF:

######  Proposition 6.5.

Both levels of MF are equi-consistent with emTT with the addition of the law
of excluded middle.

###### Proof.

For a proof, we refer to [27, 44]. ∎

Therefore, the extension of MF with the law of excluded middle is still
predicative. From this, knowing that HAω can be embedding in mTT and emTT in a
compatible way, we can deduce the non-derivability of unique choice on natural
numbers in their classical version:

######  Corollary 6.6.

The classical version of emTT and of mTT do not validate the number-theoretic
internal rule of choice and hence the number-theoretic axiom of unique choice:

$({\bf AC!_{\mathbb{N},\mathbb{N}}})\ \forall_{x\in\mathsf{N}}\
\exists!_{y\in\mathbb{N}}\ R(x,y)\ \rightarrow\
\exists_{f\in\mathbb{N}\rightarrow\mathbb{N}}\ \forall_{x\in\mathbb{N}}\
R(x,f(x))$

###### Proof.

First, observe that $\bf AC!_{\mathbb{N},\mathbb{N}}$ implies the number-
theoretic internal rule of unique choice. Then, the claim follows from Prop.
6.5 and Cor. 4.4. ∎

Since the validity of the axiom of unique choice in a theory can be
transferred to its extensions, contrary to the rule of unique choice, from
Cor. 6.6 we can immediately deduce the non-validity of ${\bf
AC!_{\mathbb{N},\mathbb{N}}}$ in mTT and emTT themselves:

######  Corollary 6.7.

Both emTT and of mTT do not validate the number-theoretic axiom of unique
choice.

It is worth noting that in the extensional level emTT of MF we can also
interpret the intuitionistic version of ACA in a way that preserves the
meaning of all logical operators:

######  Proposition 6.8.

The intuitionistic version of ACA is interpretable in the extensional level
emTT of MF. Hence, ACA can be interpreted in its classical version.

###### Proof.

It is sufficient to define a translation from ACA to emTT as follows. First-
order variables of ACA are translated as variables of type $\mathbb{N}$ in
emTT. The constants for zero and the successor are interpreted by the
corresponding constructors of type $\mathbb{N}$ in emTT. Second-order
variables for sets of natural numbers are interpreted as propositional
functions $X\in\mathbb{N}\rightarrow\mathcal{P}(1)$ in emTT and the atomic
formulas of the form $t\in X$ are translated as applications of these
functions $X(t)$.

In general, first-order formulas of ACA are interpreted as small propositions
of emTT with quantifiers and equalities restricted to $\mathbb{N}$. While
second-order formulas are interpreted by propositions of emTT quantifying over
collections.

Peano axioms can be derived from the rules for natural numbers in emTT and the
presence of power-collections, see [24]. The induction scheme of ACA follows
from the elimination rule for $\mathsf{N}$ which acts towards all types
including all propositions. Finally, the arithmetical comprehension axiom is
validated as follows: given an arithmetical formula $\phi(x)$ in ACA, we know
that it is interpreted as a small proposition in emTT. Then we can introduce
$[\phi](x)\in[x\in\mathsf{N}]$ in $\mathcal{P}(1)$ and we get $X\ {\ :\equiv\
}\lambda x.\phi(x)\in\mathsf{N}\rightarrow\mathcal{P}(1)$. Therefore, it
follows that there exists $X$ such that for all $n\in\mathsf{N}$,
$X(x)\leftrightarrow\phi$. ∎

Hence, from prop. 6.8 it follows that the classical version of MF can
formalize Weyl’s classical predicative reformulation of analysis in Das
Kontinuum following Feferman’s analysis in [17, 18].

Furthermore, from [24, 20] we know a proof-theoretic upper bound for MF:

######  Proposition 6.9.

The proof-theoretic strength of both levels of MF are bounded by Feferman’s
theory $\widehat{ID_{1}}$ of non-iterative fixpoints.

######  Corollary 6.10.

The proof-theoretic strength of the classical extension of MF is bounded by
Feferman’s theory $\widehat{ID_{1}}$ of non-iterative fixpoints.

###### Proof.

It follows from Prop.6.5 and Prop.6.9.

∎

Another significant feature of MF which makes it compatible with Weyl’s
classical predicativity, is that real numbers do not form a set in its
extensional level emTT (and this holds also for their intensional
representation in the quotient model over mTT). This reflects Weyl’s idea that
the collection of real numbers is not an extensionally determinate collection.

######  Proposition 6.11.

In the extensional level emTT of MF real numbers à la Dedekind or Cauchy do
not form a set as well as in their classical version.

###### Proof.

A direct proof of this was given [26] but it follows also from the
predicativity of the classical version of MF. If real numbers form a set in MF
then this is so in the classical version of MF and every interval of real
numbers form a set too. Since classically, the power-collection of natural
numbers can be put in bijection with an interval of real numbers, then it
would follow that impredicative definitions can be employed in the classical
version of MF contrary to its predicativity established thanks in prop.6.10. ∎

Despite the absence of choice principles and quantification over all real
numbers to form new sets, a development of mathematics, and in particular of
topology and analysis, within emTT is possible if point-free methods are
adopted as advocated by Martin-Löf and Sambin with the introduction of Formal
Topology in [45]. Indeed, in emTT the following point-free topologies are
definable:

######  Proposition 6.12.

In the extensional level emTT of MF the point-free topology of Dedekind real
numbers and Cantor space are definable.

###### Proof.

The formalization of the point-free topology of the Cantor space can be
carried on in emTT as in section 2.1 of [54]. Then, observe that the point-
free topology of real numbers can be defined as in Def.3 of [7] in terms of
another cover generated by a finite set of axioms that can be represented in
emTT with a completely analogous proof to that just mentioned for the point-
free topology of Cantor space. ∎

Therefore, one can carry on in MF the development of analysis initiated by
Palmgren in [7, 41, 42] (see also [21]) and that of Positive Topology in [47]
and loc.cit..

##  7 Conclusion

We have discussed the incompatibility with Weyl’s classical predicativity of
some foundations for Bishop mathematics like Aczel’s constructive set theory
CZF, Martin-Löf Type Theory MLTT and Homotopy Type Theory HoTT. We have
observed that this incompatibility reduces to the fact that these theories
interpret Heyting arithmetic in all finite types ${\bf HA^{\omega}}$, which is
a many-sorted theory where sorts include finite types, with the addition of
the internal rule of number-theoretic unique choice iRC!N,N, identifying
functional relations over natural numbers with a primitive notion of function
as $\lambda$-terms. Indeed, HAω \+ iRC!N,N with the further addition of the
law of excluded middle becomes impredicative since it interprets second-order
Peano arithmetic.

Whilst Weyl’s foundational system does not contain quantification over
exponentiation of functions as observed by [5], we have argued that it is not
necessary to sacrifice exponentiation altogether to reconcile Bishop’s
mathematics with Weyl’s approach if we adopt a foundation like the Minimalist
Foundation.

Given that the Minimalist Foundation interprets HAω, the price to pay is to
renounce the rule of unique choice as well as all the number-theoretic choice
principles characteristic of Bishop’s mathematics and furthermore that real
numbers à la Dedekind or Cauchy form a set. All these facts together call for
a point-free development of analysis by adopting the topological methods
advocated by Martin-Löf and Sambin with the introduction of Formal Topology
[45].

Hence, provided that a point-free reformulation of classical analysis is
viable, as hinted in [7, 41, 42, 21], MF promises to be a natural crossroads
between Bishop’s constructivism and Weyl’s classical predicativity.

In the future, besides establishing the exact proof-theoretic strength of MF,
which is currently an open problem, we will explore whether the extension of
MF with inductive and coinductive definitions in [28, 29, 32] is still
predicative, or even is still equiconsistent with its classical counterpart,
as established for MF in [27, 44]. A positive answer to either of these
questions would provide a foundation capable of formalizing general results of
point-free mathematics as those presented in [12, 36, 15, 47], and still
compatible with both Bishop’s constructivism and Weyl’s classical
predicativity, as in the case of MF.

## References

  * [1] P. Aczel.  The type theoretic interpretation of constructive set theory.  In Studies in Logic and the Foundations of Mathematics, volume 96, pages 55–66. Elsevier, 1978.
  * [2] P. Aczel and M. Rathjen.  CST Book Draft.  unpublished manuscript, 2010.
  * [3] R. Adams and Z. Luo.  Classical predicative logic-enriched type theories.  Ann. Pure Appl. Log., 161(11):1315–1345, 2010.
  * [4] R. Adams and Z. Luo.  Weyl’s predicative classical mathematics as a logic-enriched type theory.  ACM Transactions on Computational Logic (TOCL), 11(2):1–29, 2010\.
  * [5] A. Avron.  Weyl Reexamined: “Das Kontinuum” 100 Years Later.  Bull. Symb. Log., 26(1):26–79, 2020.
  * [6] E. Bishop.  Foundations of constructive analysis, volume 60.  McGraw-Hill, 1967.
  * [7] 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.
  * [8] F. Ciraulo and G. Sambin.  Reducibility, a constructive dual of spatiality.  Journal of Logic and Analysis, 11, 2019.
  * [9] M. Contente and M. E. Maietti.  The compatibility of the minimalist foundation with homotopy type theory.  Theoretical Computer Science, 991:114421, 2024.
  * [10] T. Coquand, E. Palmgren, and B. Spitters.  Metric complements of overt closed sets.  Math. Log. Q., 57(4):373–378, 2011.
  * [11] T. Coquand and C. Paulin.  Inductively defined types.  In P. Martin-Löf and G. Mints, editors, COLOG-88, International Conference on Computer Logic, Tallinn, USSR, December 1988, Proceedings, volume 417 of Lecture Notes in Computer Science, pages 50–66. Springer, 1988.
  * [12] T. Coquand, G. Sambin, J. Smith, and S. Valentini.  Inductively generated formal topologies.  Ann. Pure Appl. Log., 124(1-3):71–106, 2003.
  * [13] L. Crosilla.  Predicativity and Constructive Mathematics.  In G. Oliveri, C. Ternullo, and S. Boscolo, editors, Objects, Structures and Logics. Springer Cham, 2022.
  * [14] L. Crosilla and Ø. Linnebo.  Weyl and two kinds of potential domains.  Noûs, 2023.
  * [15] G. Curi.  Abstract Inductive and Co-Inductive Definitions.  J. Symb. Log., 83(2):598–616, 2018.
  * [16] S. Feferman.  Weyl Vindicated: Das Kontinuum, 70 Years Later.  In Proceedings of the Cesena Conference on Logic and Philosophy of Science, 1988.
  * [17] S. Feferman.  In the Light of Logic.  Oxford University Press, 1998.
  * [18] S. Feferman.  The significance of Weyl’s Das Kontinuum.  In Proof Theory- History and Philosophical Significance, pages 179–194. Springer, 2000.
  * [19] N. D. Goodman.  Relativized realizability in intuitionistic arithmetic of all finite types.  The Journal of Symbolic Logic, 43(1):23–44, 1978.
  * [20] 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.
  * [21] T. Kawai.  Bishop Metric Spaces in Formal Topology.  In M. R. Douglas Bridges, Hajime Ishihara and H. Schwichtenberg, editors, Handbook of Constructive Mathematics, pages 395–425. Cambridge University Press, 2023.
  * [22] J. Lambek and P. J. Scott.  Introduction to Higher Order Categorical Logic.  Cambridge University Press, 1986.
  * [23] M. E. Maietti.  Modular correspondence between dependent type theories and categories including pretopoi and topoi.  Math. Struct. Comput. Sci., 15(6):1089–1149, 2005.
  * [24] M. E. Maietti.  A minimalist two-level foundation for constructive mathematics.  Annals of Pure and Applied Logic, 160(3):319–354, 2009.
  * [25] M. E. Maietti.  On choice rules in dependent type theory.  In TAMC, volume 10185 of Lecture Notes in Computer Science, pages 12–23, 2017.
  * [26] M. E. Maietti.  On minimality of the Minimalist Foundation.  In Mathematisches Forschungsinstitut Oberwolfach Report No. 34/2020, Mathematical Logic: Proof Theory, Constructive Mathematics (hybrid meeting). MFO, 2020.
  * [27] M. E. Maietti.  Equiconsistency of the Minimalist Foundation with its classical version.  In Mathematisches Forschungsinstitut Oberwolfach Report n.50/2023- Mathematical Logic: Proof Theory, Constructive Mathematics. MFO, 2024\.
  * [28] M. E. Maietti, S. Maschio, and M. Rathjen.  A realizability semantics for inductive formal topologies, Church’s Thesis and Axiom of Choice.  Logical Methods in Computer Science, 17(2), 2021.
  * [29] M. E. Maietti, S. Maschio, and M. Rathjen.  Inductive and Coinductive Topological Generation with Church’s thesis and the Axiom of Choice.  Log. Methods Comput. Sci., 18(4), 2022.
  * [30] M. E. Maietti and G. Rosolini.  Quotient completion for the foundation of constructive mathematics.  Logica Universalis, 7(3):371–402, 2013.
  * [31] M. E. Maietti and G. Rosolini.  Relating quotient completions via categorical logic.  In D. Probst and P. Schuster, editors, Concepts of Proof in Mathematics, Philosophy, and Computer Science, pages 229–250, 2016.
  * [32] M. E. Maietti and P. Sabelli.  A topological counterpart of well-founded trees in dependent type theory.  In M. Kerjean and P. B. Levy, editors, Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, MFPS XXXIX, Indiana University, Bloomington, IN, USA, June 21-23, 2023, volume 3 of EPTICS. EpiSciences, 2023.
  * [33] M. E. Maietti and G. Sambin.  Toward a Minimalist Foundation for Constructive Mathematics.  In From sets and types to topology and analysis, volume 48 of Oxford logic guides. Oxford University Press, 2005.
  * [34] M. E. Maietti and G. Sambin.  Why Topology in the Minimalist Foundation Must Be Pointfree.  Logic and Logical Philosophy, 22(2):167–199, 2013.
  * [35] M. E. Maietti and G. Sambin.  The Minimalist Foundation and Bishop’s Constructive Mathematics.  In M. R. Douglas Bridges, Hajime Ishihara and H. Schwichtenberg, editors, Handbook of Constructive Mathematics, pages 525–563. Cambridge University Press, 2023.
  * [36] 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.
  * [37] P. Martin-Löf.  An intuitionistic theory of types: Predicative part.  In Studies in Logic and the Foundations of Mathematics, volume 80, pages 73–118. Elsevier, 1975.
  * [38] P. Martin-Löf.  Intuitionistic type theory, volume 1 of Studies in Proof Theory.  Bibliopolis, 1984.
  * [39] B. Nordström, K. Petersson, and J. M. Smith.  Programming in Martin-Löf’s type theory, volume 200.  Oxford University Press Oxford, 1990.
  * [40] E. Palmgren.  Bishop’s set theory, 2005.  Slides for lecture at the TYPES summer school.
  * [41] E. Palmgren.  Continuity on the real line and in formal spaces.  In L. Crosilla and P. M. Schuster, editors, From Sets and Types to Topology and Analysis, volume 48 of Oxford Logic Guides. Oxford University Press, 2005.
  * [42] E. Palmgren.  A constructive and functorial embedding of locally compact metric spaces into locales.  Topology and its Applications, 154(9):1854–1880, 2007.
  * [43] E. Rijke and B. Spitters.  Sets in homotopy type theory.  Mathematical Structures in Computer Science, 25(5):1172–1202, 2015\.
  * [44] P. Sabelli.  Around the Minimalist Foundation: (co)-induction and equiconsistency.  PhD thesis, Department of Mathematics, University of Padova, 2024.  to appear.
  * [45] G. Sambin.  Intuitionistic formal spaces - a first communication.  In D. G. Skordev, editor, Mathematical logic and its Applications, pages 187–204. Springer, 1987.
  * [46] G. Sambin.  Two applications of dynamic constructivism: Brouwer’s continuity principle and choice sequences in formal topology.  In M. B. Mark Van Atten, Pascal Boldini and G. Heinzmann, editors, One Hundred Years of Intuitionism (1907–2007) The Cerisy Conference, pages 301–315. Springer, 2008.
  * [47] G. Sambin.  Positive Topology: A New Practice in Constructive Mathematics.  Oxford University Press, 2024.
  * [48] S. G. Simpson.  Subsystems of Second Order Arithmetic, volume 1.  Cambridge University Press, 2009.
  * [49] C. Spector.  Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics.  In F. Dekker, editor, Recursive function theory: Proceedings of Symposia in Pure Mathematics, volume 5, pages 1–27. American Mathematical Society, 1962.
  * [50] T. Streicher.  Independence of the induction principle ad the axiom of choice in the pure calculus of constructions.  Theoretical computer science, 103(2):395–408, 1992.
  * [51] A. S. Troelstra.  Metamathematical investigation of intuitionistic arithmetic and analysis.  Springer, 1973.
  * [52] A. S. Troelstra and D. van Dalen.  Constructivism in Mathematics : An Introduction.  Studies in logic and the foundations of mathematics 121/123. North Holland, Amsterdam, 1988.
  * [53] Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.  https://homotopytypetheory.org/book, Institute for Advanced Study, 2013\.
  * [54] S. Valentini.  Constructive characterizations of bar subsets.  Ann. Pure Appl. Logic, 145(3):368–378, 2007.
  * [55] H. Weyl.  Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis.  De Gruyter, Berlin, Boston, 1918.
  * [56] H. Weyl.  The Continuum: a critical examination of the foundation of analysis.  Courier Corporation, 1994.