arXiv reader

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

Michele Contente and Maria Emilia Maietti

arXiv
2407.04161v4 · PDF · 4 December 2025
Categories
math.LO
Licence
CC BY 4.0 The site shows the text.

Abstract

It is well known that most constructive and predicative foundations aiming to develop Bishop’s constructive analysis are incompatible with a classical predicative development of analysis as put forward by Weyl in his \textit{Das Kontinuum}. Here, we show how this incompatibility arises from the possibility to define sets by quantifying over (the exponentiation of) functional relations. Such a possibility is present in most constructive foundations but it is not allowed in modern reformulations of Weyl’s logical system. In particular, we show how in Aczel’s Constructive Set Theory, Martin-Löf’s type theory and Homotopy Type Theory, the incompatibility with classical predicativity à la Weyl reduces to the fact of being able to interpret Heyting arithmetic in all finite types with the addition of the internal rule of number-theoretic unique choice, identifying functional relations over natural numbers with a primitive notion of function defined as \lambda-terms of type theory. Then, we argue that a possible way out is offered by constructive foundations, such as the Minimalist Foundation, where exponentiation is limited to functions defined as \lambda-terms of (dependent) type theory. The price to pay is to renounce number-theoretic choice principles, including the rule of unique choice, typical of most foundations formalizing Bishop’s constructive mathematics. 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. We then 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 constructive reformulation of analysis is viable.

Items 55

Theorem

Theorem 3.1

8OH4

CZF + AC derives the law of excluded middle \phi \vee \neg \phi for \Delta_0-formulas \phi.

Proof of Theorem 3.1

See [AczelRath].

Remark

Remark 3.2

GX1W

In [AczelRath], 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.

Theorem

Theorem 3.3

L8VH

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

Proof of Theorem 3.3

See [AczelRath].

Theorem

Theorem 3.4

C0HT

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))

where A and B are sets (i.e. types) and R any relation on them, is derivable in MLTT.

Definition

Definition 3.5

Q00N

A Dedekind cut on the rationals is a pair (L,U) of subsets L,U \subseteq \mathbb{Q} that satisfy the usual conditions of being inhabited, disjoint, open, monotone, and located, all defined as in [maiettisambinhand].

Definition

Definition 3.6

JWHB

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.

Proposition

Proposition 3.7

QX2D

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

Proof of Proposition 3.7

See Prop.17 in [CN95] and section 4.3 of [MSpointfree].

Proposition

Proposition 3.8

GV73

In MLTT, the set \mathbb{R}_{D_{0}} of Dedekind reals is in bijective correspondence with the set of Dedekind reals \mathbb{R}_{D_{k}} for any natural number k.

Proof of Proposition 3.8

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 [CN95] or section 4.3 in [MSpointfree], 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 [MSpointfree].

Remark

Remark 3.9

YURM

The previous proposition resembles a special case of Russell’s Reducibility Axiom which constructively requires a choice principle to be derived. If the law of excluded middle were valid the full Reducibility axiom would follow as shown in section 5.

Proposition

Proposition 3.10

XV9P

AC! can be derived in HoTT.

Proof of Proposition 3.10

See [rijke2015sets].

Remark

Remark 3.11

0LEI

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

Remark 3.12

SZ2P

The proof of AC! in [rijke2015sets] is a special case of a result that holds in the internal dependent type theory \mathcal{T}_{reg} of any regular category [Maietti05]. Following [Maietti05], 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 [rijke2015sets] corresponds to the argument in [Maietti05] 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 [Maietti05], and is equivalent to its quotient over the unit type, and hence we can use \Sigma-projections to prove AC!.

Definition

Definition 4.1

S1A4

The internal rule of unique choice, called {\bf iRC!}, is formulated for {\bf HA^\omega} 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).

The special case when {\bf iRC!} acts only on natural numbers, namely both \sigma and \tau coincide with the type \mathbf{N} of natural numbers, is called internal number-theoretic rule of unique choice and it is denoted with the symbol {\bf iRC!_{\mathbf{N},\mathbf{N}}}.

Used by Proof
Remark

Remark 4.2

O6O8

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 [troelstra1973]. 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.

Proposition

Proposition 4.3

19GJ

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

Proof of Proposition 4.3

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!}_{\mathbf{N}, \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

Corollary 4.4

21SF

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.

Used by Proof, Proof, Proof
Definition

Definition 5.1

YEQ1

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

Proposition 5.2

GVD3

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

Used by Proof
Proof of Proposition 5.2

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.

Uses Definition 4.1
Remark

Remark 5.4

G6DN

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.

Proposition

Proposition 5.5

NTKB

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

Used by Proof
Remark

Remark 5.7

WF08

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 [hottbook], is an elementary topos.

Definition

Definition 5.8

WCXN

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)).

Used by Proposition 5.9, Corollary 5.10, Proposition 5.12
Proposition

Proposition 5.11

U2GI

The axiom of exponentiation and the law of excluded middle for \Delta_0-formulas imply the powerset axiom.

Proof of Proposition 5.11

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.

Definition

Definition 6.1

52DE

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 \mathsf{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.

Used by Proposition 6.2, Proposition 6.3, Proof, Corollary 6.4, Proof
Proposition

Proposition 6.3

H73O

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

Uses Definition 6.1
Proof of Proposition 6.3

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

Uses Definition 6.1
Proposition

Proposition 6.5

HTH7

Both levels of MF are equiconsistent with emTT extended the addition of the law of excluded middle \phi \vee \neg \phi for all propositions \phi.

Used by Proof
Proof of Proposition 6.5

For a proof, we refer to [MSdoubleneg].

Proposition

Proposition 6.6

URO6

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

Used by Proof
Corollary

Corollary 6.7

RSHU

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

Used by Proof
Proof of Corollary 6.7

It follows from Prop.6.5 and Prop.6.6.

From this, knowing that HA^\omega can be embedded 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.

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

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

First, observe that \bf AC!_{\mathsf{N},\mathsf{N}} implies the number-theoretic internal rule of unique choice. The claim then follows from Proposition 6.7 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. Proof we can immediately deduce the non-validity of {\bf AC!_{\mathsf{N},\mathsf{N}}} in mTT and emTT themselves:

Corollary.

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.

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

Proof.

It is sufficient to define a translation from ACA to emTT as follows. Numerical variables of ACA are translated as variables of type \mathsf{N} in emTT. Set variables of ACA are translated as terms of type \mathcal{P}(\mathsf{N}). The symbols for zero and the successor in ACA are interpreted by the corresponding constructors for \mathsf{N} in emTT. Atomic formulas of the form s = t are translated as propositional equalities over \mathsf{N} and those of the form t \in X as small propositions t\ \varepsilon\ X(This notation can be defined in emTT. Given X \in \mathcal{P}(A) and t \in A, we define t\ \varepsilon\ X as \mathsf{Eq}(\mathcal{P}(1), X(t), [ \top]). Moreover, it holds that t\ \varepsilon\ \{x \in A \mid \phi(x) \} \leftrightarrow \phi(t) is true. ). In general, first-order formulas of ACA are translated as small propositions with quantifiers ranging over \mathsf{N}, while second-order formulas are translated as propositions with quantifiers ranging over the collection \mathcal{P}(\mathsf{N}).

Peano axioms can be derived in emTT thanks to the rules for \mathsf{N} and the presence of \mathcal{P}(1). In particular, the induction scheme of ACA follows from the elimination rule for \mathsf{N}, which acts towards all collections, including propositions.

Finally, the arithmetical comprehension axiom is validated as follows: given a small proposition \phi(x)\ [x \in \mathsf{N}], we can introduce [\phi(x)]\in \mathcal{P}(1)\ [x \in \mathsf{N}] and then form \{ x \in \mathsf{N}\ \mid\ \phi(x)\} \in \mathcal{P}(\mathsf{N}). Then, it follows that there is an X \in \mathcal{P}(\mathsf{N}) such that for all x \in \mathsf{N}, x\ \varepsilon\ X\ \leftrightarrow\ \phi(x) holds.

Hence, from prop. ? 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 [feferman1998light, feferman2000significance].

Uses Proposition 6.5, Proposition 6.6, Definition 6.1
Proposition

Proposition 6.11

3RR2

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 of Proposition 6.11

A direct proof of this was given in [ober2020] but it follows also from the predicativity of the classical version of MF (see also [MSdoubleneg]). If real numbers form a set in MF then this is so in the classical version of MFand 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.7.

Uses Corollary 6.7
Proposition

Proposition 6.12

2HSK

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

Proof of Proposition 6.12

The formalization of the point-free topology of the Cantor space can be carried on in emTT as in section 2.1 of [Valentini-bar]. Then, observe that the point-free topology of real numbers can be defined as in Def.3 of [CN95] 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.

Source and licence

The text on this page is from arXiv:2407.04161v4 by Michele Contente and Maria Emilia Maietti, under the licence CC BY 4.0. The corpus made these changes: it read the items out of the LaTeX source, it expanded the macros of the paper, it put each proof after its statement, and it converted the text to HTML. The formulas are the TeX of the paper, and KaTeX renders them. A formula or a reference can look different from the PDF. The page is published under CC BY 4.0.

The record of each item is in analysis/objects/2407/2407.04161.jsonl.