2.1 The restricted process

It is also possible to outline a restricted version of the logico-mathematical process, which prevents the introduction of higher-level sets. This weaker procedure can be connected to the interpretation of Das Kontinuum advocated by Feferman and to certain subsystems of second-order arithmetic. We know from [Reference Simpson21] that non-trivial mathematical results can be established within these systems.

The restriction imposed on the logico-mathematical process takes the following form: the only formulas from which we can construct sets are those containing quantifiers ranging only over natural numbers (and not over sets of them). Such formulas are known as arithmetical formulasFootnote ⁵ in the literature. In practice, the restriction amounts to accepting the comprehension principle in the following form: given $z : \mathbb {N}$

$$ \begin{align*}z\ \varepsilon\ [x : \mathbb{N}\ \vert\ P] \leftrightarrow P [z/x],\end{align*} $$

where P is arithmetical.

Therefore, the restricted process can be described as follows: we take the type of natural numbers as ground type and we apply the logical process building new propositions; then we introduce the type of arithmetical sets $\mathsf {Set}_0(\mathbb {N})$ . Arithmetical propositions are closed under quantification over natural numbers and a term of type $\mathsf {Set}_0(\mathbb {N})$ is well-formed whenever the proposition P is arithmetical.

The restricted process imposes a constraint on set-formation principles but not on the rules for forming propositions. We can still introduce propositions containing quantification over sets of natural numbers. However, the mathematical process cannot be applied to these and, as a result, they do not give rise to sets. Hence, all the conventions about levels are superfluous in the case of the restricted process, since only arithmetical sets are taken into account.

The core of Feferman’s reading of Das Kontinuum is that Weyl’s aim was to develop a kind of arithmetical mathematics. Weyl’s insight was that the definable sets of the first level of the ramified hierarchy are sufficient to develop significant parts of analysis. Such sets correspond to the arithmetical ones. Without entering into the debate about the interpretation of Das Kontinuum here,Footnote ⁶ it is worth mentioning that Avron has put forward a detailed criticism of Feferman’s interpretation in [Reference Avron4]. In particular, Avron challenges the idea that Weyl was committed to a form of arithmetical mathematics and argues that the extent of predicative mathematics as outlined in Das Kontinuum was significantly broader. Nevertheless, at least for the case of predicative analysis, it seems to be correct the claim that this can be developed in arithmetical systems in the sense of Feferman. The system proposed by Feferman in [Reference Feferman, Cellucci and Sambin10, Reference Feferman11] as a faithful formalization of Weyl’s theory is equivalent to the subsystem of second-order arithmetic known as ACA $_0$ ,Footnote ⁷ which is conservative over PA. In the following, we will show that the theory resulting from the restricted process is conservative over ACA $_0$ .

2.2 The logic of the process

A natural question is which logic the Weylian predicativist should adopt when iterating the Mathematical Process. Weyl in Das Kontinuum opted for classical logic. He believed that every quantified proposition expressible in the language of the system of Das Kontinuum has a determinate truth value. The motivations supporting this belief are articulated more clearly in a letter to Hölder (published as Appendix in [Reference Weyl24]). There, Weyl introduces the notion of extensionally determinate concept:

An extensionally determinate concept C is one whose extension forms a ‘closed aggregate which is intrinsically determined and demarcated’. In a more down to earth language, we can say that a concept C is extensionally determinate just if the domain determined by C has a fixed extension. Therefore, we call a domain extensionally determinate if it is determined by an extensionally determinate concept. Such domains can be regarded as forming closed totalities. According to Weyl, the concept ‘natural number’ or any concept having a finite extension is certainly extensionally determinate. Whereas the concept ‘real number’ as conceived in classical analysis or the general concept of ‘property’ are not. It follows that the domains determined by these concepts cannot be taken to form closed totalities.

While this is sufficient to establish a distinction between open and closed totalities, it is still not an argument in support of classical logic. Classical reasoning is supported by the second half of the quotation above. If a is an object belonging to the extension of the concept C and P is a predicate that applies to objects in the extension of C, then not only the sentence $P(a)\ \lor \neg P(a)$ possesses a definite truth value, but also the existential sentence $\exists (x: C) P(x)\ \lor \neg \exists (x:C) P(x)$ does. According to Weyl, this is a defining property of extensionally determinate concepts.

Then, what characterizes domains given by extensionally determinate concepts is that bivalence continues to hold when quantified sentences are considered.Footnote ⁸

Classical logic is warranted because we are quantifying over domains having a fixed extension. The members of a finite domain can be exhaustively enumerated and for certain infinite domains like $\mathbb {N}$ , the extension is fixed because we have a procedure that allows us to generate all the members.

By contrast, we lack enumerations or procedures capable of exhaustively describing all the members of a domain that is not extensionally determinate. Therefore, bivalence ceases to hold for sentences quantifying over these domains. Weyl’s idea in Das Kontinuum seems to consider only those domains that are extensionally determinate.

It is interesting to assess the consequences of these views whenever the iteration of the Mathematical Process is considered. In particular, they should provide arguments in support of the classical system $\mathcal {LM}$ , that we will introduce in the next section.

If we want to adopt classical logic while iterating the mathematical process, we need to justify the claim that all entities generated through this iteration are extensionally determinate. In particular, the constructions that we apply to the types must preserve extensional determinateness at higher levels in the hierarchy.

For the type of propositions of a given level, we can argue as follows: we start from a primitive collection of propositions and we form new propositions by combining them by means of the logical operations. Since we can provide an exhaustive enumeration of all the propositions that are generated by this method, we can introduce a type that stands for the collection of all these propositions. Thanks to the level-restriction over quantification, it is not possible to introduce a proposition in $\Omega _0$ , which refers to higher levels. In this sense, the domain can be regarded as a closed collection. Then, we can extend the argument to levels greater than zero. At each step, a proposition is introduced only on the basis of entities that have been already constructed. Since we have a procedure to generate all the propositions of a given level and since the type of propositions of a given level cannot be ‘disordered’ by introducing propositions referring to later stages, it seems legitimate to conclude that $\Omega _n$ is extensionally determinate for each n.

To justify the claim that the type-forming operation $\mathsf {Set}_n(-)$ , which, given a type $\alpha $ , allows us to form the subsets of $\alpha $ of level n, preserves extensional determinateness, we can proceed as follows: first, we remark that the level of the type $\mathsf {Set}_n$ is always strictly greater than n; secondly, we observe that all such types should be enumerable. Set-like terms of type $\mathsf {Set}_n (\alpha )$ are introduced by abstraction: given $x: \alpha $ and a proposition $P: \Omega _n$ , we can form $[ x: \alpha \ \vert \ P]$ . The constraints on levels guarantee that each set of this form is introduced by quantifying only over objects that have been constructed at earlier levels and, in particular, the type of all these sets of level n is introduced at the level $n + 1$ . Therefore, the extension of all the subsets is always fixed locally—relatively to a level n—and we possess a procedure to generate exhaustively all these objects. In particular, for each level n and each type $\alpha $ , we can form the set $V_{n, \alpha }$ containing all the X’s in $\mathsf {Set}_n (\alpha )$ . This set is of type with level necessarily greater than n. Having access to this construction supports the claim that we have a completed collection of subsets with level n and hence that the operation $\mathsf {Set}_n (-)$ preserves extensional determinateness. In particular, all higher-level predicative sets can be taken to be extensionally determinate.

There are compelling reasons, however, to consider the iteration of the process with intuitionistic logic as well. The main motivation being that adopting intuitionistic logic allows for a more generous notion of predicativity. In the next section, we will also consider the constructive system $\mathcal {LM}^i$ .

In the realm of constructive foundations of mathematics, one can find many examples of predicative theories. Among the most well-known are Constructive Zermelo–Fraenkel set theory CZF [Reference Aczel, MacIntyre, Pacholski and Paris1] and various versions of Martin-Löf Type Theory [Reference Martin-Löf, Rose and Sheperdson16, Reference Martin-Löf17], including Homotopy Type Theory [22].

A first caveat is that predicativity here is understood in a generalized sense. These systems support constructions which make them stronger than predicative systems in the sense of Feferman–Schütte proof-theoretic analysis.Footnote ⁹

Working within a constructive setting permits some extensions of the predicative point of view that are hard to justify classically. Two such extensions are briefly discussed here: one by the inclusion of various forms of inductive definitions, and the other by function exponentiation.

The extension by generalized inductive definitions such as the type of well-founded trees makes Martin-Löf Type Theory stronger proof-theoretically. Furthermore, such extensions are also important for a smoother formalization of many notions appearing in the mathematical practice. The system $\mathcal {LM}^i$ is justified by an interpretation within (a fragment of) Homotopy Type Theory, as we will show later. It is worth noting that this system is very close to the theory introduced by Palmgren in [Reference Palmgren19], that is, a version of intuitionistic ramified type theory (IRTT). Palmgren also justifies his system by designing an interpretation within Martin-Löf Type Theory. Although the two interpretations are different, they suggest that it would be possible to extend the ramified systems with generalized inductive definitions, which are in fact validated by both models.

The other extension is by function exponentiation. One of CZF axioms is the axiom of exponentiation saying that, given two sets $A,B$ , the collection of all functions from A to B forms a set. It is easy to prove that this axiom is equivalent to the powerset axiom whenever classical logic is adopted [Reference Aczel, MacIntyre, Pacholski and Paris1]. However, exponentiation is strictly weaker than the powerset within a constructive setting.

Similarly, in Martin-Löf Type Theory we can form the type of functions from a type A to a type B,Footnote ¹⁰ where a primitive notion of function is considered.

These constructions are usually considered to be predicatively justified. In systems like $\mathcal {LM}^i$ as well as Palmgren’s IRTT, there is no primitive notion of function. However, functions can be introduced by adapting the usual set-theoretic definition. Prima facie, the introduction of an exponentiation axiom in ramified type theories like $\mathcal {LM}^i$ or Palmgren’s system does not seem to be justified. In fact, levels do not seem to be closed under functional exponentiation. Let us consider a simple example. Given the ground type $\mathbb {N}$ , we can define the following arithmetical set:

$$ \begin{align*} \mathrm{Nat}\ =\ [ x: \mathbb{N}\ \mid\ x =_{\mathbb{N}} x]: \mathsf{Set}_0 (\mathbb{N}). \end{align*} $$

A function from $\mathrm {Nat}$ to $\mathrm {Nat}$ is a total functional relation, hence a term of type $\mathsf {Set}_k (\mathbb {N} \times \mathbb {N})$ . While it is clear that the level of $\mathrm {Nat}$ is 1, we cannot conclude that the same is true for the function. In general, we could have functions over $\mathrm {Nat}$ of many different levels. Moreover, the levels of such functions are not bounded from the levels of the domain and codomain. Furthermore, whenever we could form the set of functions $\mathtt {Func}(A,B)$ , where $A, B: \mathsf {Set}_n (\alpha )$ , this set will be necessarily of a level greater than n.

In general, it is not only true that levels are not closed under functional exponentiation, but also that we cannot show that functions with the same domain and codomain possess the same level. It would be tempting to say that whenever F is a function of arbitrary level k, there is an equivalent function $F'$ whose level is ‘minimal’. However, this sounds suspiciously similar to the Axiom of Reducibility and in fact the previous statement can be derived from Russell’s axiom. The most interesting aspect of Palmgren’s work [Reference Palmgren19] consists precisely in the introduction of a similar axiom without destroying the predicative character of the theory. This axiom of Functional Reducibility can also be formulated in our system. Roughly, the axiom is the following: given a function F from A to B with arbitrary level, there is a function G from A to B that is extensionally equal to F and whose level is bounded by the levels of A and B.

Palmgren defines a setoid model of his system within Martin-Löf Type Theory which validates Functional Reducibility, thereby showing that this axiom can be predicatively acceptable. We will see later that the axiom is also made valid under a different interpretation in type theory.

The crucial fact is that Palmgren’s FRA is predicatively acceptable just in case the underlying logic is intuitionistic as proved by Palmgren himself in [Reference Palmgren19]. Indeed, whenever we extend the logic with classical principles, then we can show that this is equivalent to the full Axiom of Reducibility. This fact seems to confirm that the extent of the notion of predicativity is sensitive to the underlying logic by providing further insight into the status of the Axiom of Reducibility.

Finally, there is a third option that we will not pursue here. Restricting classical logic to natural numbers, while employing intuitionistic logic for sets of natural numbers. This leads to semiconstructive systems [Reference Coquand and Palmgren7, Reference Feferman, Berger, Diener, Schuster and Seisenberger14]. Technically, such idea is implemented by including some version of bounded omniscience principles, that are weaker than the full law of excluded middle.

3.1 The arithmetical theory and ACA $_0$

In this section, we turn our attention to the (classical) theory resulting from the restricted process. As we have seen in §2.1, the restricted process consists in limiting the comprehension axiom to arithmetical propositions. Thus, it prevents the introduction of higher-level sets, thereby blocking the iteration of the mathematical process. It follows that we need only the type of natural numbers and the type of arithmetical sets $\mathsf {Set}_0 (\mathbb {N})$ . Furthermore, there is no need to introduce a type of arithmetical propositions: they are defined simultaneously with the terms, but are not treated as terms themselves. We will only distinguish between arithmetical propositions and arbitrary propositions, which might contain quantifiers ranging over the type of arithmetical sets, but do not enter into the definition of set-like abstraction terms. Therefore, all the conventions about levels, set out in Definition 3.2, are superfluous in this context and the type structure is drastically simplified.

The main interest in studying the system resulting from the restricted process is that it can be compared to the system considered by Feferman in [Reference Feferman, Cellucci and Sambin10] as faithful formalization of Weyl’s ideas in Das Kontinuum. As we remarked above, Feferman’s proposal has been criticized for being a too restrictive formalization of Weyl’s conception of predicativity. However, there seems to be a general agreement on the fact that predicative analysis as conceived by Weyl can be formalized in systems of this strength.

Among the systems introduced in [Reference Feferman, Cellucci and Sambin10], the system $K^{(\alpha )}$ is of interest to us. As already observed by Feferman, such a system can be drastically simplified and turns out to be equivalent to the second-order system known as ACA $\!\! _0$ . This system is formulated in the two-sorted language $L_2$ .

The non-logical axioms of ACA $_0$ are the universal closures of the following formulas in $L_2$ :

• – Basic axioms:

  $$ \begin{align*} & n + 1 \neq 0 & m + 1 = n + 1 \rightarrow m = n \\ & m + 0 = m & m + (n +1) = (m + n) + 1 \\ & m \cdot 0 = 0 & m \cdot (n + 1) = (m \cdot n) + m. \end{align*} $$

• – Induction axiom:

  $$ \begin{align*} (0 \in X \land \forall n (n \in X \rightarrow n + 1 \in X)) \rightarrow \forall n (n \in X). \end{align*} $$

• – Arithmetical comprehension axiom:

  $$ \begin{align*} \exists X \forall n (n \in X \leftrightarrow \phi(n)), \end{align*} $$
  where $\phi (n)$ is arithmetical and X does not occur free in $\phi $ .

This concludes the presentation of ACA $_0$ . Next, we introduce the system $\mathcal {LM}_0$ , that is meant to provide an axiomatization of the restricted process. The type structure of $\mathcal {LM}_0$ is defined as follows.

Definition 3.19. The types of $\mathcal {LM}_0$ are the following:

$$ \begin{align*} \mathbb{N}\ \quad\quad \mathsf{Set}_0(\mathbb{N}).\ \end{align*} $$

While we cannot introduce higher-level sets in $\mathcal {LM}_0$ , we can still form non-arithmetical propositions. Therefore, we are going to introduce a definition for such a class of propositions, which must also be considered for interpreting arbitrary formulas in the language of $\mathbf {ACA}_0$ . We call these simply propositions and they extend the arithmetical ones.

We assume any standard axiomatisation for many-sorted classical logic and Peano axioms for zero, successor, addition and multiplication. The other axioms of $\mathcal {LM}_0$ are the following:

• – Induction axiom: For every $X: \mathsf {Set}_0(\mathbb {N})$ ,

  $$ \begin{align*} (0\ \varepsilon\ X \land \forall n : \mathbb{N}\ (n\ \varepsilon\ X \rightarrow \mathsf{succ}(n)\ \varepsilon\ X)) \rightarrow \forall n: \mathbb{N}\ ( n\ \varepsilon\ X). \end{align*} $$

• – Extensionality axiom: For every $X, Y: \mathsf {Set}_0 (\mathbb {N})$ ,

  $$ \begin{align*} (\forall z: \alpha) ( z\ \varepsilon\ X \leftrightarrow z\ \varepsilon\ Y) \rightarrow (X =_{\mathsf{Set}_0 (\mathbb{N})} Y). \end{align*} $$

• – Arithmetical comprehension axiom: For every $z: \mathbb {N}$ ,

  $$ \begin{align*} z\ \varepsilon\ [x: \mathbb{N}\ \vert\ P] \leftrightarrow P [z/x], \end{align*} $$
  where P is arithmetical.

On the basis of the previous considerations about the formalization of predicative analysis in $\mathbf {ACA}_0$ , we want to show that $\mathcal {LM}_0$ and $\mathbf {ACA}_0$ are mutually interpretable. In this way, we can vindicate the claim that the restricted process is enough for developing predicative analysis in the style of Das Kontinuum.

The translation from $\mathbf {ACA}_0$ to $\mathcal {LM}_0$ is defined in a straightforward way: numerical terms are sent to terms of type $\mathbb {N}$ and set variables to variables of type $\mathsf {Set}_0(\mathbb {N})$ . The inductive clauses of the translation are given in the following definition.

Definition 3.22. The map $(-)^\tau $ from the language of $\mathbf {ACA}_0$ to the language of $\mathcal {LM}_0$ is defined as follows: in the case of terms we have

$$ \begin{align*} (x)^\tau &{\ :\equiv\ } x & (X)^\tau &{\ :\equiv\ } X & (0)^\tau &{\ :\equiv\ } 0 &\\[3pt] (t + 1)^\tau &{\ :\equiv\ } \mathsf{succ}(t^\tau) & ( t + s)^\tau &{\ :\equiv\ } t^\tau + s^\tau & (t \cdot s)^\tau &{\ :\equiv\ } t^\tau \cdot s^\tau \end{align*} $$

for arithmetical formulas we have

$$ \begin{align*} (t = s)^\tau & {\ :\equiv\ } t^\tau =_{\mathbb{N}} s^\tau \\ (t \in X)^\tau & {\ :\equiv\ } t^\tau\ \varepsilon\ X^\tau \\ (\neg P)^\tau & {\ :\equiv\ } \neg P^\tau \\ (P\ \Box\ Q)^\tau & {\ :\equiv\ } P^\tau\ \Box\ Q^\tau \\ (\mathcal{Q} x.P)^\tau & {\ :\equiv\ } \mathcal{Q} x: \mathbb{N}. P^\tau \end{align*} $$

and the definition extends naturally to arbitrary formulas in the language of $\mathbf {ACA}_0$ , therefore only the clauses for quantifiers are given

$$ \begin{align*} (\forall X. P)^\tau & {\ :\equiv\ } \forall X: \mathsf{Set}_0(\mathbb{N}).P^\tau \\ (\exists X. P)^\tau & {\ :\equiv\ } \exists X: \mathsf{Set}_0(\mathbb{N}).P^\tau. \\ \end{align*} $$

Next, we show that the translation $(-)^\tau $ is sound.

Proof. The proof is a straightforward induction over the derivation of $\phi $ . The induction axiom is trivially validated by the corresponding axiom in $\mathcal {LM}_0$ . While, arithmetical comprehension is validated as follows: given a formula $\phi (n)$ with $n: \mathbb {N}$ , we can introduce the set $[ n : \mathbb {N}\ \vert \ \phi (n)]: \mathsf {Set}_0 (\mathbb {N}) $ . Then, the following trivially holds:

$$ \begin{align*} \forall n: \mathbb{N}\ (n\ \varepsilon\ [n: \mathbb{N}\ \vert\ \phi(n)]\ \leftrightarrow\ \phi(n)). \end{align*} $$

Hence, we conclude $\exists X: \mathsf {Set}_0 (\mathbb {N})\ \forall n: \mathbb {N}\ ( n\ \varepsilon \ X\ \leftrightarrow \ \phi (n))$ . This allows to interpret arithmetical comprehension.

In order to define a translation from $\mathcal {LM}_0$ to $\mathbf {ACA}_0$ , we follow a strategy similar to that employed in [Reference Adams and Luo3].

For each numerical term a of $\mathcal {LM}_0$ , we define an arithmetical formula of $\mathbf {ACA}_0\, \eta _a(x)$ , with x fresh, such that $\mathbf {ACA}_0 \ \vdash \ \exists !x.\eta _a(x)$ . To each set-term A of $\mathcal {LM}_0$ , we associate an arithmetical formula $\theta _A(x)$ , with x fresh, such that $\mathbf {ACA}_0 \vdash \exists ! X. \forall x (x \in X \leftrightarrow \theta _A(x))$ . An arithmetical proposition P is translated as an arithmetical formula $ P^\star $ and an arbitrary proposition is translated as an arbitrary formula in the language of $\mathbf {ACA}_0$ . Finally, it must be noted that in the language of $\mathbf {ACA}_0$ as defined in Definition 3.18 equality of sets is not included. However, the extension with the definition

$$ \begin{align*} X = Y\ :=\ \forall x\ (x \in X\ \leftrightarrow\ x\in Y) \end{align*} $$

is trivially a definitional extension of $\mathbf {ACA}_0$ , because we can derive within the theory that if for all $x\, (x \in X\ \leftrightarrow \ x =x)$ and for all x, $ (x \in Y\ \leftrightarrow \ x =x)$ hold, then $X = Y$ follows. This guarantees that the arithmetical sets interpreting set-terms of $\mathcal {LM}_0$ are unique and, moreover, that we can interpret the axiom of extensionality for sets.

Definition 3.24. The translation from $\mathcal {LM}_0$ terms and propositions to $\mathbf {ACA}_0$ is defined as follows:

$$ \begin{align*} \eta_{x_i}(x) &:= x = x_i \end{align*} $$

$$ \begin{align*} \begin{aligned}[t] \eta_0(x) &:= x = 0 \\[6pt] \theta_A(x) &:= x \in A \\[6pt] ( P \land Q )^\star &:= P^\star \land Q^\star \\[6pt] ( P \rightarrow Q )^\star &:= P^\star \rightarrow Q^\star \\[6pt] ((\exists x: \mathbb{N}) P )^\star &:= \exists x\, P^\star \\[6pt] ( a =_{\mathbb{N}} b )^\star &:= \exists x (\eta_a(x) \land \eta_b(x)) \\[6pt]((\forall X : \mathsf{Set}_0(\mathbb{N})) P )^\star &:= \forall X.\, P^\star \end{aligned} \begin{aligned}[t] \eta_{\mathsf{succ}(a)}(x) &:= \exists y\ (\eta_a(y) {\land} x {=} y {+} 1) \\[6pt] \theta_{[y \vert P]}(x) &:= P^\star [x/y] \\[6pt] ( P \lor Q )^\star &:= P^\star \lor Q^\star \\[6pt] (\neg P )^\star &:= \neg P^\star \\[6pt] ((\forall x: \mathbb{N}) P )^\star &:= \forall x\, P^\star \\[6pt] ( a\ \varepsilon\ A )^\star &:= \exists x (\eta_a(x) \land \theta_A(x)) \\[6pt] ((\exists X : \mathsf{Set}_0(\mathbb{N})) P)^\star &:= \exists X.\, P^\star. \end{aligned} \end{align*} $$

The following lemmas are proved by induction.

Proof. The proof is by induction over the derivations. In the case of comprehension, we get

$$ \begin{align*}\exists y\ \eta_z (y) \land P^\star [y/x] \leftrightarrow ( P [z/x] )^\star,\end{align*} $$

which holds by the substitution lemma.

For the set extensionality axiom, let us assume that for all x,

$$ \begin{align*} \eta_z(x) \land \theta_X(x)\ \leftrightarrow\ \theta_Y (x). \end{align*} $$

Then, in particular, we have that $z \in X \leftrightarrow z\in Y$ by definition of the interpretation. This corresponds to $X = Y$ . The induction axiom is trivially validated by the corresponding axiom in $\mathbf {ACA}_0$ .

Furthermore, the following facts hold.

This allows us to conclude that $\mathcal {LM}_0$ is conservative over $\mathbf {ACA}_0$ .

4.1 Preliminaries

We will work with a version of type theory including the following type constructors:

$$ \begin{align*} A,B\ ::=\ \mathbf{0}\ \vert\ \mathbb{N}\ \vert\ \Sigma_{(x:A)}B\ \vert\ \Pi_{(x:A)}B\ \vert\ A + B\ \vert\ \mathrm{Id_A}\ \vert\ \vert\vert A\vert\vert\ \vert\ \mathcal{U}_i. \end{align*} $$

In particular, for each external natural number i, the universe $\mathcal {U}_i$ is univalent. We assume a countable and cumulative hierarchy of univalent universes.

The Univalence Axiom is the following principle:

$$ \begin{align*} (UA)\ \mathrm{the\ map}\ \mathsf{ideqv}: (A =_{\mathcal{U}} B) \rightarrow (A \simeq B)\ \mathrm{is\ an\ equivalence,} \end{align*} $$

where the type $A \simeq B$ is the type of equivalences as defined in [22].

We recall that the following two principles are derivable in the presence of UA:

• – Function extensionality: Let us suppose $f, g: \Pi _{(x:A)} B$ . The map

  $$ \begin{align*} \mathsf{happ}(f,g): \mathrm{Id}_{(\Pi_{(x:A)}B}(f,g) \rightarrow \Pi_{(x:A)} \mathrm{Id}_B (f(x), g(x)) \end{align*} $$
  is an equivalence.

• – Propositional extensionality: Let us suppose $P, Q: \mathcal {U}$ are h-propositions. The map

  $$ \begin{align*} \mathsf{idleqv}: (P =_{\mathcal{U}} Q) \rightarrow (P \leftrightarrow Q) \end{align*} $$
  is an equivalence.

The statement of propositional extensionality involves the notion of h-proposition that is defined as follows.

Definition 4.2. A type $A: \mathcal {U}_i$ is an h-proposition if the following type is inhabited:

$$ \begin{align*} \mathsf{isProp}(A)\ :=\ \Pi_{(x,y:A)}\mathrm{Id_A}(x,y). \end{align*} $$

In the same way, we can introduce the notion of h-set.

Definition 4.3. A type $A: \mathcal {U}_i$ is an h-set if the following type is inhabited:

$$ \begin{align*} \mathsf{isSet}(A)\ :=\ \Pi_{(x,y:A)} \mathsf{isProp}(\mathrm{Id_A}(x,y)). \end{align*} $$

Therefore, we can introduce a proof-term witnessing the fact that if A is an h-set, then its identity type is an h-proposition:

$$ \begin{align*} \pi_{Id}: \Pi_{(A: \mathcal{U}_i)} \Pi_{(s: \mathsf{isSet}(A))} \Pi_{(x,y:A)} \mathsf{isProp}(\mathrm{Id_A}(x,y)). \end{align*} $$

In general, it is possible to introduce a hierarchy of homotopy levels such that if A is of h-level $n+1$ , then $\mathrm {Id_A}$ is of h-level n (see [22, chap. 3]). Furthermore, such a hierarchy is cumulative [22, theorem 7.1.7].

In particular, it holds that every h-proposition is an h-set and thus we can introduce the following proof-term:

$$ \begin{align*} \sigma_{coe}: \Pi_{(A: \mathcal{U}_i)} \mathsf{isProp}(A) \rightarrow \mathsf{isSet}(A). \end{align*} $$

H-propositions in HoTT satisfy the following closure properties.

We can define the logic of h-propositions as follows:

$$ \begin{align*} \begin{array}{lll} \top & {\ :\equiv\ } & \textbf{1} \\ \bot & {\ :\equiv\ } & \textbf{0} \\ P\land Q & {\ :\equiv\ } & P \times Q \\ P\supset Q & {\ :\equiv\ } & P \rightarrow Q \\ \forall_{(x:A)} \ P(x) & {\ :\equiv\ } & \Pi_{(x:A)} \ P(x). \end{array} \end{align*} $$

The previous lemma allows us to introduce the following proof-terms, which we will need in the interpretation of $\mathcal {LM}$ :

$$ \begin{align*} \begin{array}{l} \pi_{\bot}: \mathsf{isProp}(\bot) \\ \pi_{\land}: \Pi_{(P, Q: \mathcal{U}_i)} \Pi_{(p: \mathsf{isProp}(P))} \Pi_{(q: \mathsf{isProp}(Q))} \mathsf{isProp}(P \land Q) \\ \pi_{\supset}: \Pi_{(P, Q: \mathcal{U}_i)} \Pi_{(q: \mathsf{isProp}(Q))} \mathsf{isProp}(P \supset Q) \\ \pi_{\forall}: \Pi_{(A: \mathcal{U}_i)} \Pi_{(P: A \rightarrow \mathcal{U}_i)} \Pi_{(p: \Pi_{(x:A)} \mathsf{isProp}(P(x)))} \mathsf{isProp}(\forall_{(x:A)} P(x)). \end{array} \end{align*} $$

As it stands, the logic of h-propositions suffers from severe limitations. In particular, it cannot express disjunction and existential quantification, since h-propositions are not closed under coproducts and dependent sums. The solution to these problems is provided by propositional truncation, which is an example of higher inductive type. This type constructor is given by the following rules:

• – Formation: If $A: \mathcal {U}_i$ , then $\lvert \lvert A\rvert \rvert : \mathcal {U}_i$ .

• – Introduction $_{1}$ : If $a : A$ , then $\lvert a\rvert : \lvert \lvert A \rvert \rvert $ .

• – Introduction $_{2}$ : If $a,b: \lvert \lvert A \rvert \rvert $ , then $\mathsf {sq}(a,b): \mathrm {Id_{\lvert \lvert A \rvert \rvert }}(a,b)$ .

• – Elimination: Let $C(z)$ be a family of types over $z: \lvert \lvert A \rvert \rvert $ . If $t: \lvert \lvert A \rvert \rvert $ , $c_0 : C(\lvert a\rvert )$ and $c_1: \mathsf {sq}(x,y)_{\ast }(d) =_{C(y)} e$ Footnote ¹³ under the assumptions $x,y: \lvert \lvert A \rvert \rvert $ , $d: C(x)$ and $e: C(y)$ , then $\mathsf {ind}_{\lvert \lvert \ \rvert \rvert }(t, c_0, c_1): C(t)$ .

Since the propositional truncation of a type is always an h-proposition, we can introduce the following proof-term:

$$ \begin{align*} \pi_{\lvert\lvert\ \rvert\rvert}: \Pi_{(A: \mathcal{U}_i)} \mathsf{isProp}(\lvert\lvert A \rvert\rvert). \end{align*} $$

Thanks to propositional truncation, disjunction and existential quantification can be defined as follows:

$$ \begin{align*} & P \lor Q\ {\ :\equiv\ }\ \lvert\lvert P + Q\rvert\rvert \\ & \exists_{(x:A)} P(x)\ {\ :\equiv\ }\ \lvert\lvert \Sigma_{(x:A)} P(x) \rvert\rvert. \end{align*} $$

The following proof-terms are introduced to encode the fact that these are h-propositions:

$$ \begin{align*} \pi_{\lor}\ &{\ :\equiv\ }\ \lambda P. \lambda Q. \pi_{\lvert\lvert\ \rvert\rvert} (P + Q): \Pi_{(P, Q: \mathcal{U}_i} \mathsf{isProp}(P \lor Q)\\ \pi_{\exists}\ &{\ :\equiv\ }\ \lambda A. \lambda P. \pi_{\lvert\lvert\ \rvert\rvert}(\Sigma_{(x:A)} P(x)): \Pi_{(A: \mathcal{U}_i)} \Pi_{(P: A \rightarrow \mathcal{U}_i)} \mathsf{isProp}(\exists_{(x:A)} P(x)). \end{align*} $$

In HoTT it is possible to show that h-sets satisfy the following closure properties.

We can introduce the following proof-terms witnessing that h-sets are closed under the corresponding type constructors:

$$ \begin{align*} &\sigma_{\mathbb{N}}: \mathsf{isSet}(\mathbb{N})\\ & \sigma_{\times}: \Pi_{(A,B:\mathcal{U}_i)} \mathsf{isSet}(A \times B)\\ &\sigma_{\rightarrow}: \Pi_{(A, B:\mathcal{U}_i)} \Pi_{(s: \mathsf{isSet}(B)} \mathsf{isSet}(A \rightarrow B). \end{align*} $$

H-sets are also closed under a classifier for h-propositions sitting within a universe $\mathcal {U}_i$ :

$$ \begin{align*} \mathsf{Prop}_{\mathcal{U}_i}\ {\ :\equiv\ }\ \Sigma_{(P: \mathcal{U}_i)} \mathsf{isProp}(P). \end{align*} $$

Such a type is an h-set:

$$ \begin{align*} \sigma_{\mathsf{prop_i}}: \mathsf{isSet}(\mathsf{Prop}_{\mathcal{U}_i}). \end{align*} $$

The type of h-sets within a universe $\mathcal {U}_i$ is denoted by

$$ \begin{align*} \mathsf{Set}_{\mathcal{U}_i}\ {\ :\equiv\ }\ \Sigma_{(X : \mathcal{U}_i)} \mathsf{isSet}(X). \end{align*} $$

Finally, we state the following lemma (see Lemma 2.3.1 in [22]) that we will use later.

4.2 The interpretation

We are going to show that $\mathcal {LM}^i$ can be interpreted in a fragment of the theory presented in [22] with propositional truncation as primitive type former and a cumulative hierarchy of univalent universes $\mathcal {U}_i$ . Furthermore, the interpretation extends to $\mathcal {LM}$ whenever HoTT is extended with the law of excluded middle.

The basic idea underlying the interpretation can be easily explained: a type $\alpha $ of $\mathcal {LM}^i$ is interpreted as an h-set in HoTT. More in detail, to each $\mathcal {LM}^i$ -type $\alpha $ , we associate a pair $(\alpha ^{\circ }, \sigma _{\alpha ^{\circ }}): \mathsf {Set}_{\mathcal {U}_i}$ , where the first element is a type in $\mathcal {U}_i$ and the second element is a proof that such a type is an h-set. Moreover, the universe level i is equal to $\ell (\alpha )$ . Therefore, in this interpretation ramification levels of $\mathcal {LM}^i$ -types are managed through universe levels in HoTT. In general, a term a with type $\alpha $ will be interpreted as $a^\circ : \mathsf {pr}_1(\alpha ^\circ )$ . In the case of propositions—that is, terms of type $\Omega _n$ —we have that a proposition $P: \Omega _i$ is interpreted as a pair $(P^\circ , \pi _{P^\circ })$ in $\mathsf {Prop}_i$ : the first element of the pair is a type in $\mathcal {U}_i$ and and the second element is a proof that $P^\circ $ is an h-proposition. Therefore, the derivation of a sequent with conclusion P is interpreted as the derivation of a judgement asserting that the type $P^\circ $ is inhabited.

Definition 4.8. We define an interpretation function $(-)^\circ $ from $\mathcal {LM}^i$ types and terms into HoTT types and terms as follows:

$$ \begin{align*} \begin{array}{@{}ll} (\mathbb{N})^\circ\ :=\ (\mathbb{N}, \sigma_{\mathbb{N}}) & (\bot)^\circ\ :=\ (\mathbf{0}, \pi_{\mathbf{0}})\\(\Omega_n)^\circ\ :=\ (\mathsf{Prop}_{\mathcal{U}_n}, \sigma_{\mathsf{prop}_n}) & (P \land Q)^\circ\ :=\ (\mathsf{pr}_1(P^\circ) \land \mathsf{pr}_1(Q^\circ), \pi_\land)\\(\alpha \times \beta)^\circ\ :=\ (\alpha^\circ \times \beta^\circ, \sigma_{\alpha^\circ \times \beta^\circ}) & (P \lor Q)^\circ\ :=\ (\mathsf{pr}_1(P^\circ) \lor \mathsf{pr}_1(Q^\circ), \pi_\lor)\\(\mathsf{Set}_n (\alpha))^\circ\ :=\ (\alpha^\circ \rightarrow \mathsf{Prop}_{\mathcal{U}_n}, \sigma_{\alpha^\circ \rightarrow \mathsf{Prop}_{\mathcal{U}_n}}) & (P \rightarrow Q)^\circ\ :=\ (\mathsf{pr}_1(P^\circ) \supset \mathsf{pr}_1(Q^\circ), \pi_{\supset})\\(x : \alpha)^\circ\ :=\ x: \mathsf{pr}_1(\alpha^\circ) & ((\exists x: \alpha) P)^\circ\ :=\ (\exists_{(x : \mathsf{pr}_1(\alpha^\circ))} \mathsf{pr}_1(P^\circ), \pi_\exists)\\(0: \mathbb{N})^\circ\ :=\ 0 : \mathbb{N} & ((\forall x: \alpha) P)^\circ\ :=\ (\forall_{(x : \mathsf{pr}_1(\alpha^\circ))} \mathsf{pr}_1(P^\circ), \pi_\forall)\\(\mathtt{succ}(a): \mathbb{N})^\circ\ :=\ \mathtt{s}(a^\circ) : \mathbb{N} & (a =_\alpha b)^\circ\ :=\ (\mathrm{Id}_{\mathsf{pr}_1(\alpha^\circ)}(a^\circ, b^\circ), \pi_{\mathrm{Id}})\\(a + b: \mathbb{N})^\circ\ :=\ a^\circ + b^\circ : \mathbb{N} & \\(a \cdot b:\mathbb{N})^\circ\ :=\ a^\circ \cdot b^\circ : \mathbb{N} & \\([x : \alpha\ \vert\ P ])^\circ\ :=\ \lambda x: \mathsf{pr}_1(\alpha^\circ).\mathsf{pr}_1(P^\circ) :&\\ \quad\mathsf{pr}_1(\alpha^\circ) \rightarrow \mathsf{Prop}_{\mathcal{U}_n} & \\(a\ \mathbin{\varepsilon}\ b)^\circ\ :=\ b^\circ (a^\circ) & \\((a,b) : \alpha \times \beta)^\circ\ :=\ (a^\circ, b^\circ ) :&\\ \quad\mathsf{pr}_1(\alpha^\circ) \times \mathsf{pr}_1(\beta^\circ) & \\(\mathsf{pr}_1(c) : \alpha)^\circ\ :=\ \mathsf{pr}_1(c^\circ): \mathsf{pr}_1(\alpha^\circ) & \\(\mathsf{pr}_2(c) : \beta)^\circ\ :=\ \mathsf{pr}_2(c^\circ): \mathsf{pr}_1(\beta^\circ). & \\ \end{array} \end{align*} $$

For the sake of brevity, proof-terms witnessing h-propositions have been written without spelling out their arguments: e.g., $\pi _\land $ is an abbreviation for $\pi _\land (\mathsf {pr}_1(P^\circ ), \mathsf {pr}_1(Q^\circ ), \mathsf {pr}_2(P^\circ ), \mathsf {pr}_2(Q^\circ ))$ that is of type $ \mathsf {isProp}(\mathsf {pr}_1(P^\circ ) \land \mathsf {pr}_1(Q^\circ ))$ . On the other hand, proof-terms for h-sets have been written with their type arguments as subscripts.

Proof. If $P\ :=\ Q_1 \land Q_2 : \Omega _n$ , then by induction hypothesis $Q_1^\circ , Q_2^\circ : \mathsf {Prop}_{\mathcal {U}_n}$ . This means that $\mathsf {pr}_1(Q_1^\circ ), \mathsf {pr}_1 (Q_2^\circ ): \mathcal {U}_n$ and $\mathsf {pr}_2(Q_1^\circ ): \mathsf {isProp}(\mathsf {pr}_1(Q_1^\circ ))$ and $\mathsf {pr}_2(Q_2^\circ ): \mathsf {isProp}(\mathsf {pr}_1(Q_2^\circ ))$ . Then, it follows that

$$ \begin{align*} \mathsf{pr}_1(Q_1^\circ) \land \mathsf{pr}_1(Q_2^\circ): \mathcal{U}_n \end{align*} $$

and

$$ \begin{align*} \pi_\land (\mathsf{pr}_1(Q_1^\circ), \mathsf{pr}_1(Q_2^\circ), \mathsf{pr}_2(Q_1^\circ), \mathsf{pr}_2(Q_2^\circ)): \mathsf{isProp}(\mathsf{pr}_1(Q_1^\circ) \land \mathsf{pr}_1(Q_2^\circ)) \end{align*} $$

that amounts to $(Q_1 \land Q_2)^\circ : \mathsf {Prop}_{\mathcal {U}_n}$ .

If $P\ :=\ (\forall x: \alpha )\ Q: \Omega _n$ , then by induction hypothesis $\alpha ^\circ : \mathsf {Set}_{\mathcal {U}_n}$ and $Q^\circ : \mathsf {Prop}_{\mathcal {U}_n}$ . Then, in particular $\mathsf {pr}_1(Q^\circ ): \mathcal {U}_n$ with $\mathsf {pr}_2(Q^\circ ): \mathsf {isProp}(\mathsf {pr}_1(Q^\circ ))$ . Therefore, we can form

$$ \begin{align*} \forall_{(x: \mathsf{pr}_1(\alpha^\circ))} \mathsf{pr}_1(Q^\circ): \mathcal{U}_n \end{align*} $$

with $\pi _\forall (\mathsf {pr}_1(\alpha ^\circ ), x.\mathsf {pr}_1(Q^\circ (x)), x.\mathsf {pr}_2(Q^\circ (x))): \mathsf {isProp}( \forall _{(x: \mathsf {pr}_1(\alpha ^\circ ))} \mathsf {pr}_1(Q^\circ ))$ .

But this means that $(\forall (x : \alpha )\ Q)^\circ : \mathsf {Prop}_{\mathcal {U}_n}$ .

If $P\ :=\ a =_\alpha b: \Omega _n$ , then by induction hypothesis we have $\alpha : \mathsf {Set}_{\mathcal {U}_n}$ and $a^\circ , b^\circ : \mathsf {pr}_1(\alpha ^\circ )$ . Then, we can form the type $\mathrm {Id}_{\mathsf {pr}_1(\alpha ^\circ )} (a^\circ , b^\circ ): \mathcal {U}_n$ .

By induction hypothesis we also have $\mathsf {pr}_2(\alpha ^\circ ): \mathsf {isSet}(\mathsf {pr}_1(\alpha ^\circ ))$ , hence we can derive the following proof-term:

$$ \begin{align*} \pi_{\mathrm{Id}}(\mathsf{pr}_1(\alpha^\circ), \mathsf{pr}_2(\alpha^\circ), a^\circ, b^\circ): \mathsf{isProp}(\mathrm{Id}_{\mathsf{pr}_1(\alpha^\circ)} (a^\circ, b^\circ)). \end{align*} $$

Therefore, $( a =_\alpha b :\Omega _n)^\circ : \mathsf {Prop}_{\mathcal {U}_n}$ .

If $P\ :=\ a\ \varepsilon \ B: \Omega _n $ , then by induction hypothesis we have $a^\circ : \mathsf {pr}_1(\alpha ^\circ )$ , where $\alpha ^\circ : \mathsf {Set}_{\mathcal {U}_n}$ , and $B^\circ : \mathsf {pr}_1(\alpha ^\circ ) \rightarrow \mathsf {Prop}_{\mathcal {U}_n}$ . Therefore, it is immediate that $B^\circ (a^\circ ): \mathsf {Prop}_{\mathcal {U}_n}$ and so $(a\ \varepsilon \ B)^\circ : \mathsf {Prop}_{\mathcal {U}_n}$ .

When $\alpha $ is a ground type, the result is immediate by definition of the interpretation. When $\alpha $ is $\beta _1 \times \beta _2$ or $\mathsf {Set}_n (\beta )$ , then the result follows by the definition of the interpretation and the elementary closure properties of h-sets.

Proof. The proof proceeds by induction over the derivation. In general, a context $\Gamma \mid \Delta $ , where $\Gamma := [ x_1: \alpha _1, \ldots , x_n :\alpha _n]$ and $\Delta := [Q_1, \ldots , Q_n]$ , is interpreted as a context in HoTT with the following form:

$$ \begin{align*} x_1: \alpha_1^\circ, \ldots, x_n: \alpha_n^\circ, y_1: \mathsf{pr}_1(Q_1^\circ), \ldots, \mathsf{pr}_1(Q_n^\circ). \end{align*} $$

For the logical rules, we consider the following examples, since it is straightforward to extend the proof to the other cases as well.

For the conjunction introduction rule, we reason as follows: by induction hypothesis, we have constructed proof-terms $p: \mathsf {pr}_1(P^\circ )$ and $q : \mathsf {pr}_1(Q^\circ )$ , where $P^\circ , Q^\circ : \mathsf {Prop}_{\mathcal {U}_n}$ . Then, it follows that

$$ \begin{align*} (p,q): \mathsf{pr}_1(P^\circ) \land \mathsf{pr}_1(Q^\circ), \end{align*} $$

which is the interpretation of the conclusion. For the elimination rules, we reason as follows: by induction hypothesis, we have constructed a proof-term $p: \mathsf {pr}_1(P^\circ ) \land \mathsf {pr}_2(Q^\circ )$ , then it is immediate to conclude $\mathsf {pr}_1(p): \mathsf {pr}_1(P^\circ )$ . The other case is treated in the same way by applying the second projection.

For the disjunction introduction rules, we proceed as follows: by induction hypothesis, we have constructed a proof-term $p: \mathsf {pr}_1(P^\circ )$ , where $P^\circ : \mathsf {Prop}_{\mathcal {U}_n}$ . Then, it follows

$$ \begin{align*} \lvert \mathsf{inr}(p) \rvert : \mathsf{pr}_1(P^\circ) \lor \mathsf{pr}_1(Q^\circ), \end{align*} $$

where $\mathsf {pr}_1(P^\circ ) \lor \mathsf {pr}_1(Q^\circ )$ is an h-proposition in $\mathcal {U}_n$ and thus the conclusion is validated. The other rule is derived in the same way using $\lvert \mathsf {inl}(q) \rvert $ .

For the elimination rule, we reason as follows: by induction hypothesis we have constructed proof-terms $c: \mathsf {pr}_1(P^\circ ) \lor \mathsf {pr}_1(Q^\circ ), d_0(x): \mathsf {pr}_1(R^\circ )$ where $x: \mathsf {pr}_1(P^\circ )$ and $d_1(y): \mathsf {pr}_1(R^\circ )$ where

$y: \mathsf {pr}_1(Q^\circ )$ .

Then by the elimination rule for propositional truncation, we get

$$ \begin{align*} \mathsf{ind}_{\lvert\lvert\ \rvert\rvert}(c, z.\mathsf{ind}_+ (z, x.d_0(x), y.d_1(y)), \pi_{R^\circ}): \mathsf{pr}_1(R^\circ), \end{align*} $$

which abbreviates as

$$ \begin{align*} \mathsf{ind}_\lor (c, x.d_0(x), y.d_1(y)): \mathsf{pr}_1(R^\circ), \end{align*} $$

and hence the conclusion is valid.

The introduction rule of the universal quantifier is interpreted as follows: by induction hypothesis, we have constructed a proof-term $p: \mathsf {pr}_1(P^\circ (x))$ with $x: \mathsf {pr}_1(\alpha ^\circ )$ . Then, we can derive the following term: $\lambda x.p$ with type $\forall _{(x : \mathsf {pr}_1(\alpha ^\circ ))} \mathsf {pr}_1 (P^\circ )$ and we know that such a type is an h-proposition.

For the elimination rule, we reason as follows: by induction hypothesis we have $p: \forall _{(x : \mathsf {pr}_1(\alpha ^\circ ))} \mathsf {pr}_1 (P^\circ )$ and $a^\circ : \mathsf {pr}_1(\alpha ^\circ )$ . Therefore, it is immediate to conclude by the elimination rule $p(a^\circ ): \mathsf {pr}_1(P^\circ [a^\circ /x])$ .

For the interpretation of the first equality rule, by induction hypothesis we have $t^\circ : \mathsf {pr}_1(\alpha ^\circ )$ . Therefore, it is immediate to conclude by the introduction rule for propositional equality

$$ \begin{align*} \textbf{refl}(t^\circ): \mathrm{Id}_{\mathsf{pr}_1(\alpha^\circ)}(t^\circ,t^\circ), \end{align*} $$

which amounts to the interpretation of the conclusion.

The second equality rule is validated as follows: by induction hypothesis, we have constructed $p: \mathrm {Id}_{\mathsf {pr}_1(\alpha ^\circ )}(s^\circ , t^\circ )$ and $q: \mathsf {pr}_1(P^\circ )(s^\circ )$ .

Therefore, by applying Lemma 4.7, we get $p_\ast (q): \mathsf {pr}_1(P^\circ (t^\circ ))$ .

For the other axioms of $\mathcal {LM}^i$ , let us first remark that the image of their interpretations in HoTT turns out to be an h-prop and so a pair. We show that the first component of the pair is inhabited to derive the validity of the axioms.

The first three axioms for natural numbers are easily derivable in HoTT and, moreover, since they have the form of implications between h-propositions, it follows that they are h-propositions. The derivation of the axioms for addition and multiplication is also entirely standard. In the case of the induction scheme, instead, it is easy to show that it can be derived by an application of a particular instance of the elimination rule for $\mathbb {N}$ in HoTT. Since $\mathcal {LM}^i$ -types are interpreted as h-sets, then it follows that the axioms for $\times $ are h-propositions. Furthermore, that the interpretations of these axioms are inhabited follow from the rules for $\times $ in HoTT.Footnote ¹⁴

The axiom of extensionality for sets is interpreted as follows: given $X^\circ , Y^\circ : \mathsf {pr}_1(\alpha ^\circ ) \rightarrow \mathsf {Prop}_{\mathcal {U}_n}$ , we want to prove that

$$ \begin{align*}\Pi_{(z: \mathsf{pr}_1(\alpha^\circ))} (X^\circ (z) \leftrightarrow Y^\circ(z)) \rightarrow \mathrm{Id}_{(\mathsf{pr}_1(\alpha^\circ) \rightarrow \mathsf{Prop}_{\mathcal{U}_n}})(X^\circ, Y^\circ)\ .\end{align*} $$

Let $z : \mathsf {pr}_1(\alpha ^\circ )$ and $t: X^\circ (z) \leftrightarrow Y^\circ (z) $ , then by propositional extensionality we get a proof of $\mathrm {Id}_{\mathsf {Prop}_{\mathcal {U}_n}}(X^\circ (z), Y^\circ (z))$ .

By discharging the assumption, we get a proof of $\Pi _{(z: \mathsf {pr}_1(\alpha ^\circ ))} \mathrm {Id}_{\mathsf {Prop}_{\mathcal {U}_n}}(X^\circ (z), Y^\circ (z))$ . Finally by function extensionality, we conclude that $\mathrm {Id}_{(\mathsf {pr}_1(\alpha ^\circ ) \rightarrow \mathsf {Prop}_{\mathcal {U}_n})}(X^\circ , Y^\circ )$ is inhabited.

Extensionality for propositions is immediately validated by propositional extensionality in HoTT.

Finally, the Comprehension Axiom is interpreted as follows. Given $z: \mathsf {pr}_1(\alpha ^\circ )$ , we want to show that

$$ \begin{align*}(\lambda x: \mathsf{pr}_1(\alpha^\circ). \mathsf{pr}_1(P^\circ))(z) \leftrightarrow \mathsf{pr}_1(P^\circ[z/x])\ .\end{align*} $$

This follows from the validity of the corresponding equality and an application of propositional extensionality.

It follows from the results in [Reference Rathjen, Jäger and Sieg20] that the proof-theoretic strength of the fragment of HoTT assumed to carry out the interpretation of $\mathcal {LM}^i$ is $\Gamma _0$ .

It is important to observe that the interpretation can be carried out without assuming the type of well-founded trees $\mathcal {W}$ . This is crucial for the above corollary.

It is possible to extend HoTT with the law of excluded middle for h-propositions:

$$ \begin{align*} \mathtt{lem}: \Pi_{(P:\ \mathcal{U}_n)} \mathsf{isProp}(P) \rightarrow P \lor \neg P. \end{align*} $$

However, in this case it is not possible to conclude that $\Gamma _0$ is an upper bound for the theory, because HoTT becomes fully impredicative when extended with classical logic. Therefore, the translation is not very informative proof-theoretically in the classical case. In any case, it is reasonable to expect that the strength of the classical system $\mathcal {LM}$ is below $\Gamma _0$ .