<p><a href="https://www.cs.swan.ac.uk/%7Ecsetzer/" rel="noreferrer">Anton Setzer</a> has work on type theories that are stronger than standard induction-recursion. In some ways, though, it's still in terms of simultaneous inductive and recursive definitions. The difference is in the intricacy and details of all the simultaneous definitions.</p>
<p>There are two papers that build up to and define this type theory. <a href="https://www.cs.swan.ac.uk/%7Ecsetzer/articles/modeltypetheoryinaccessiblemahlo.pdf" rel="noreferrer">The first</a> goes through 'normal' universes and up to Mahlo universes, which are the sort of universes Agda has, that are themselves closed under inductive-recursive definitions. Then <a href="https://www.cs.swan.ac.uk/%7Ecsetzer/articles/modelpi3refluniv.pdf" rel="noreferrer">the second</a> goes beyond this, finally defining a &quot;<span class="math-container">$Π_3$</span>-reflecting universe,&quot; which I believe could also be called a &quot;weakly compact&quot; universe by analogy to large cardinal properties (similar to &quot;Mahlo&quot;).</p>
<p>I only have a limited understanding of all this myself, but the idea goes something like this:</p>
<p>A starting point is the &quot;Mahlo universe&quot; which is a universe closed under inductive-recursive definitions. In some sense, this is like a universe closed under (standard) universe formation, because induction-recursion allows you to define types similar to the universe in ordinary Martin-löf type theory. So, a sort of 'obvious' next step is to try to define a universe that is closed under some amount of Mahlo-universe formation. You need to take care with this, though, because a universe both being Mahlo and having an inductive eliminator is contradictory. So, the method of definition has to be somewhat different than induction-recursion.</p>
<p>The idea introduced is to keep track of the &quot;Mahlo degree&quot; of universes. The degrees are well-founded trees, and a universe of Mahlo degree <span class="math-container">$d$</span> is closed under universes in a similar way to a Mahlo universe (e.g. for every map <span class="math-container">$F : \mathsf{ IFam}(\mathsf{U},\mathsf{El}) → \mathsf{IFam}(\mathsf{U},\mathsf{El})$</span>, there is a universe <span class="math-container">$\hat{\mathsf{U}}_F : \mathsf{U}$</span> closed under <span class="math-container">$F$</span>), but with the proviso that there is actually one <span class="math-container">$\hat{\mathsf{U}}_F^e$</span> itself of degree <span class="math-container">$e$</span>, for each <span class="math-container">$e &lt; d$</span>. So, for <span class="math-container">$d = 0$</span> we get plain universes, containing no further universes, for <span class="math-container">$d = 1$</span> we get Mahlo universes. And the type of degrees is defined simultaneously with <span class="math-container">$\mathsf{U}$</span>, so that 'new' values of <span class="math-container">$\mathsf{U}$</span> introduce new, larger degrees, similarly to an inductive-recursive definition.</p>
<p>The final step he takes to get to the <span class="math-container">$Π_3$</span> universe is to extend the notion of degree. Whereas before it was supposed to essentially be the same as <span class="math-container">$\mathsf{W\ U\ El}$</span>, instead the degrees themselves are defined in a similar way to Mahlo universes. Essentially, <span class="math-container">$\mathsf{Deg}$</span> is now the inductive type with constructor:</p>
<p><span class="math-container">$$\mathsf{deg} : (\mathsf{IFam}(\mathsf{U},\mathsf{El}) → \mathsf{Fam}_{\mathsf{Deg}}(\mathsf{U},\mathsf{El})) → \mathsf{Deg}$$</span></p>
<p><em>But</em>, this is all still simultaneous with the definition of <span class="math-container">$\mathsf{U}$</span> and such.</p>
<p>If you find this unclear, even after studying the papers, I think you're probably in good company. I've tried <a href="https://hub.darcs.net/dolio/universes/browse/src/Universe/Super/Autonomous.agda" rel="noreferrer">formalizing</a> something similar to the second-to-last step above in Agda, with some commentary. Setzer calls his construction the &quot;autonomous Mahlo universe,&quot; because its Mahlo degree is given by the well-founded trees definable over itself. My formalization attempts to show that Agda's Mahlo universes are &quot;autonomous super universes,&quot; where super universes are a weaker notion than Mahlo, that aren't contradictory when having an induction principle.</p>
<p>While writing this, I also tried extending the notion of degree in that file to the <span class="math-container">$Π_3$</span> one, and it seemed to work. I'm not sure what the result is, however. But you can try to work all this out in Agda to develop a better understanding of how things interleave. It's just that the 'degrees' are with respect to a fundamentally weaker notion of universe, because universes with an eliminator cannot themselves be Mahlo (if you try to write what such a thing would be, you will be rejected by Agda's positivity checker).</p>
<p>One thing to note, I suppose, is that it's difficult to see what one would <em>do</em> with these sort of universes (that can't already be done with less). Setzer is, in this work, primarily interested in understanding proof theory through the lens of type theory, so the ordinal-alike presentation is not much of a barrier in that respect. However, (large) induction-recursion has some pretty simple practical motivations, while I don't think the same can be said about a <span class="math-container">$Π_3$</span>-reflecting universe. Perhaps there's some simpler notion similar to induction-recursion that is equivalent in power to <span class="math-container">$Π_3$</span>-reflection, and seeing that would suggest more 'mundane' uses. But I don't think it's at all clear what that would be, just given the Setzer presentation.</p>

CC BY-SA 4.0
2023-01-01T21:25:02.237Z
"You need to take care with this, though, because a universe both being Mahlo and having an inductive eliminator is contradictory" I swear I don't know how you know these things. Reference?
cody
CC BY-SA 4.0
2023-01-01T22:55:43.510Z
I think I first encountered the fact in one of the footnotes of the second paper above. However, actual proofs are given in Setzer's [Proof Theory of Martin-löf Type Theory](https://www.cs.swan.ac.uk/~csetzer/articles/overviewProofTheoryTypeTheory2004.pdf) (page 19), and Palmgren's [On Universes in Type Theory](http://www2.math.uu.se/~palmgren/universe.pdf) (page 11).
Dan Doel
CC BY-SA 4.0
2023-01-02T16:31:21.713Z
Oh, one more thing that occurred to me. Palmgren comments that it's predicatively suspicious that a Mahlo universe is incompatible with the 'expected' inductive eliminator, since it's presented inductively. But in his talks on HOTT, Mike Shulman has separately suggested that it might make sense to think of a universe as being coinductively defined instead. So perhaps there is a nice dovetailing where a Mahlo universe is a coinductive one closed under inductive-recursively defined (sub-)universes, so we don't "expect" the inconsistent principle.
Dan Doel
CC BY-SA 4.0
2023-01-01T16:06:16.723Z
2023-01-01T18:53:38.160Z
2023-01-01T18:53:38.160Z
Dan Doel
<p>Are there type theories in the literature with &quot;induction&quot; principles stronger than induction-recursion? <a href="https://cstheory.stackexchange.com/q/48563">This answer</a> gives System F as an example of a theory stronger than MLTT + induction-recursion, but I'm interested in principles similar to ordinary induction and induction-recursion, not impredicativity.</p>

CC BY-SA 4.0
2023-01-01T15:06:07.743Z
Hi, I have later asked a question in a similar vein on proofassistant se and it is quite tricky to state the restriction on formal system that would make it predicative. There is some trickiness involved with these principles, as impredicativity can be hidden. Thinking about it now, maybe a good definition of predicativity is consistency with negation of power set in all universes, but that might not be the definition you are thinking of.
https://proofassistants.stackexchange.com/questions/1829/uniform-notions-of-pattern-matching-at-dependent-types-with-impredicative-proof
Ilk
<reference-request><lo.logic><type-theory>
Stronger "induction" principles than induction-recursion
technosentience
# Stronger "induction" principles than induction-recursion

(Asked by: username_0 on 2022-12-31)

Are there type theories in the literature with "induction" principles stronger than induction-recursion? [This answer](https://cstheory.stackexchange.com/q/48563) gives System F as an example of a theory stronger than MLTT + induction-recursion, but I'm interested in principles similar to ordinary induction and induction-recursion, not impredicativity.

**Tags:** reference-request, lo.logic, type-theory
> **Comments:**
> **username_1**: Hi, I have later asked a question in a similar vein on proofassistant se and it is quite tricky to state the restriction on formal system that would make it predicative. There is some trickiness involved with these principles, as impredicativity can be hidden. Thinking about it now, maybe a good definition of predicativity is consistency with negation of power set in all universes, but that might not be the definition you are thinking of. https://proofassistants.stackexchange.com/questions/1829/uniform-notions-of-pattern-matching-at-dependent-types-with-impredicative-proof  

---

## 1 answers

### Answer by username_2 on 2023-01-01. Score: 11 | Accepted answer

[Anton Setzer](https://www.cs.swan.ac.uk/%7Ecsetzer/) has work on type theories that are stronger than standard induction-recursion. In some ways, though, it's still in terms of simultaneous inductive and recursive definitions. The difference is in the intricacy and details of all the simultaneous definitions.

There are two papers that build up to and define this type theory. [The first](https://www.cs.swan.ac.uk/%7Ecsetzer/articles/modeltypetheoryinaccessiblemahlo.pdf) goes through 'normal' universes and up to Mahlo universes, which are the sort of universes Agda has, that are themselves closed under inductive-recursive definitions. Then [the second](https://www.cs.swan.ac.uk/%7Ecsetzer/articles/modelpi3refluniv.pdf) goes beyond this, finally defining a "$Π\_3$-reflecting universe," which I believe could also be called a "weakly compact" universe by analogy to large cardinal properties (similar to "Mahlo").

I only have a limited understanding of all this myself, but the idea goes something like this:

A starting point is the "Mahlo universe" which is a universe closed under inductive-recursive definitions. In some sense, this is like a universe closed under (standard) universe formation, because induction-recursion allows you to define types similar to the universe in ordinary Martin-löf type theory. So, a sort of 'obvious' next step is to try to define a universe that is closed under some amount of Mahlo-universe formation. You need to take care with this, though, because a universe both being Mahlo and having an inductive eliminator is contradictory. So, the method of definition has to be somewhat different than induction-recursion.

The idea introduced is to keep track of the "Mahlo degree" of universes. The degrees are well-founded trees, and a universe of Mahlo degree $d$ is closed under universes in a similar way to a Mahlo universe (e.g. for every map $F : \mathsf{ IFam}(\mathsf{U},\mathsf{El}) → \mathsf{IFam}(\mathsf{U},\mathsf{El})$, there is a universe $\hat{\mathsf{U}}\_F : \mathsf{U}$ closed under $F$), but with the proviso that there is actually one $\hat{\mathsf{U}}\_F^e$ itself of degree $e$, for each $e < d$. So, for $d = 0$ we get plain universes, containing no further universes, for $d = 1$ we get Mahlo universes. And the type of degrees is defined simultaneously with $\mathsf{U}$, so that 'new' values of $\mathsf{U}$ introduce new, larger degrees, similarly to an inductive-recursive definition.

The final step he takes to get to the $Π\_3$ universe is to extend the notion of degree. Whereas before it was supposed to essentially be the same as $\mathsf{W\ U\ El}$, instead the degrees themselves are defined in a similar way to Mahlo universes. Essentially, $\mathsf{Deg}$ is now the inductive type with constructor:

$$\mathsf{deg} : (\mathsf{IFam}(\mathsf{U},\mathsf{El}) → \mathsf{Fam}\_{\mathsf{Deg}}(\mathsf{U},\mathsf{El})) → \mathsf{Deg}$$

*But*, this is all still simultaneous with the definition of $\mathsf{U}$ and such.

If you find this unclear, even after studying the papers, I think you're probably in good company. I've tried [formalizing](https://hub.darcs.net/dolio/universes/browse/src/Universe/Super/Autonomous.agda) something similar to the second-to-last step above in Agda, with some commentary. Setzer calls his construction the "autonomous Mahlo universe," because its Mahlo degree is given by the well-founded trees definable over itself. My formalization attempts to show that Agda's Mahlo universes are "autonomous super universes," where super universes are a weaker notion than Mahlo, that aren't contradictory when having an induction principle.

While writing this, I also tried extending the notion of degree in that file to the $Π\_3$ one, and it seemed to work. I'm not sure what the result is, however. But you can try to work all this out in Agda to develop a better understanding of how things interleave. It's just that the 'degrees' are with respect to a fundamentally weaker notion of universe, because universes with an eliminator cannot themselves be Mahlo (if you try to write what such a thing would be, you will be rejected by Agda's positivity checker).

One thing to note, I suppose, is that it's difficult to see what one would *do* with these sort of universes (that can't already be done with less). Setzer is, in this work, primarily interested in understanding proof theory through the lens of type theory, so the ordinal-alike presentation is not much of a barrier in that respect. However, (large) induction-recursion has some pretty simple practical motivations, while I don't think the same can be said about a $Π\_3$-reflecting universe. Perhaps there's some simpler notion similar to induction-recursion that is equivalent in power to $Π\_3$-reflection, and seeing that would suggest more 'mundane' uses. But I don't think it's at all clear what that would be, just given the Setzer presentation.

> **Comments:**
> **username_3**: "You need to take care with this, though, because a universe both being Mahlo and having an inductive eliminator is contradictory" I swear I don't know how you know these things. Reference?  
> **username_2**: I think I first encountered the fact in one of the footnotes of the second paper above. However, actual proofs are given in Setzer's [Proof Theory of Martin-löf Type Theory](https://www.cs.swan.ac.uk/~csetzer/articles/overviewProofTheoryTypeTheory2004.pdf) (page 19), and Palmgren's [On Universes in Type Theory](http://www2.math.uu.se/~palmgren/universe.pdf) (page 11).  
> **username_2**: Oh, one more thing that occurred to me. Palmgren comments that it's predicatively suspicious that a Mahlo universe is incompatible with the 'expected' inductive eliminator, since it's presented inductively. But in his talks on HOTT, Mike Shulman has separately suggested that it might make sense to think of a universe as being coinductively defined instead. So perhaps there is a nice dovetailing where a Mahlo universe is a coinductive one closed under inductive-recursively defined (sub-)universes, so we don't "expect" the inconsistent principle.  

---

