# Proof-theoretic strength of HOL compared to predicative dependent types

By HOL I mean something like inference rules of HOL Light with the 3 axioms of infinity, extensionality and choice ($$\varepsilon$$ operator).

By predicative dependent types, I am thinking of MLTT + W-types + infinitely many predicative universes, and MLTT + infinite hierarchy of universes with induction-recursion.

For a long time I thought that HOL is weaker than predicative dependent type theories, but now I am doubting this. It might have just been a mirage due to ease of use and expressiveness of abstractions. In HOL we use booleans in the type of equalities, $$\alpha \: \rightarrow \: \alpha \: \rightarrow \: Bool$$, which gives HOL a slightly impredicative flavour. On the other hand we use a universe in the type of equalities in predicative dependent types, $$(\alpha : Set) \: \rightarrow \: \alpha \: \rightarrow \: \alpha \: \rightarrow Set$$. What is the relationship? I believe this reduces to something like is the proof-theoretic ordinal of HOL known to be smaller or larger than that of MLTT.

• For the strength of MLTT see Can you build w-types out of natural numbers predicatively. Don't know about HOL-light however. Nov 2, 2022 at 0:48
• I think the answer regarding the ordinal of HOL should be in this paper here: randall-holmes.github.io/Bibliography/maltapaper.pdf, but I still have to process it.
– Ilk
Nov 2, 2022 at 1:46
• I'm not totally familiar with HOL Light, but if you have power sets and a natural number type, then you can interpret $n$th order arithmetic with classical logic and full comprehension for all $n$, which is stronger than Martin-Löf type theory (even with induction-recursion if I recall correctly).
– aws
Nov 2, 2022 at 20:20
• For $n$th order arithmetic full comprehension is stratified - there's no collection of all sets so nothing else would make sense in the language. Here full just means there's no other restrictions on formulas, like in ATR, $\Pi^1_1$-CA etc. Also NF is only (believed to be) weak relative to ZF - it is still stronger than MLTT.
– aws
Nov 4, 2022 at 14:50
• I believe that aws is correct: HOL light with the aforementioned axioms is equivalent to classical higher-order arithmetic with choice, which is stronger than MLTT even with induction-recursion. Maybe you should write this as an answer instead of a comment? Nov 4, 2022 at 18:05