I saw a PowerPoint that claimed to achieve $\psi_0(\Gamma_{\Omega+1})$ in Agda without any axioms. I was wondering if a better lower bound exists in 2024?

My personal estimates:

  1. the lower bound at Agda should already exceed $\psi(\Omega_L)$, because of W-type and Setω+n. But it is by no means possible to reach $\psi(\Omega_{M+\omega})$: to support extended predicative Mahlo universe would require more reforms of Agda.
  • Update: I now agreed that the standard Agda is no less than the Mahlo type theory, which is $\mathsf{PTO(Agda)}>\psi(\Omega_{M+\omega})$.
  1. the lower bound on Cubical Agda is probably lower than that of standard Agda, since the full inductive families is not supported.
  2. the lower bound at Coq should already be over B, since Coq also supports type W-type. In fact, it could support more, even more than $\sf PTO(Intuitionistic-Zermelo)$. but I have no idea how to write Coq code to implement a stronger universe, like Mahlo / $Π_3$-Reflection / $Π_1^1$-reflection / $Π_N$-Collection...
  • Update: According to "Sets in Coq, Coq in Set", Coq should have at least the strength of IZF + a Grothendieck universes. However, according to Appendix B, no more universes are available...

It would be great if you could answer the question with some code. I have always believed that there is a very simple correspondence between inductive types, ordinal notation, and universes, but I have never been able to capture the right code.

  • $\begingroup$ The universes in Agda are Mahlo, so the proof theoretic ordinal should be at least the $\psi(Ω_{M+ω})$ of one Mahlo universe. I'm not certain how much stronger $ω \cdot 2$ Mahlo universes is than just one. I've also never understood enough ordinal analysis to know how to demonstrate the relevant ordinals. $\endgroup$
    – Dan Doel
    Commented Jun 13 at 18:10
  • $\begingroup$ @DanDoel The Git repository connection provided in the paper "extended predicative Mahlo" is not accessible. The closest I can see to success is this, but it still doesn't seem to work. Given that the authors claim in the paper that Mahlo goes beyond indexed inductive-recursive definitions, I can't confirm that Agda actually implements some Mahlo type theory. $\endgroup$ Commented Jun 13 at 18:50
  • 1
    $\begingroup$ That repository is mine. But I'm not sure what you mean by, "it still doesn't seem to work." I also don't know why someone would claim that a Mahlo universe is beyond induction-recursion. For example. the definition in that file appears to match the rules for the Mahlo universe in this paper. $\endgroup$
    – Dan Doel
    Commented Jun 13 at 19:25
  • $\begingroup$ @DanDoel The paper I mentioned is here, and the missing Git repository is this. Notice that the paper you and I mentioned have a co-author, so we should believe that Agda does have a model for the Mahlo universe, although the exact implementation and the cost involved is missing... $\endgroup$ Commented Jun 13 at 19:41
  • 2
    $\begingroup$ Oh, I think I know what is going on. It is possible to add induction-recursion to type theory as a method for defining types. This is weaker than having a universe type that is closed under induction-recursion, which is (effectively) what a Mahlo universe is, and what Agda actually has. I think the paper is using the weaker theory where effectively only the 'meta-universe of all types' is Mahlo. $\endgroup$
    – Dan Doel
    Commented Jun 13 at 20:04


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.