5
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • $\begingroup$ For the strength of MLTT see Can you build w-types out of natural numbers predicatively. Don't know about HOL-light however. $\endgroup$
    – Couchy
    Commented Nov 2, 2022 at 0:48
  • $\begingroup$ 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. $\endgroup$
    – Ilk
    Commented Nov 2, 2022 at 1:46
  • 3
    $\begingroup$ 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). $\endgroup$
    – aws
    Commented Nov 2, 2022 at 20:20
  • 3
    $\begingroup$ 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. $\endgroup$
    – aws
    Commented Nov 4, 2022 at 14:50
  • 1
    $\begingroup$ 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? $\endgroup$
    – Loïc Pujet
    Commented Nov 4, 2022 at 18:05

0

Reset to default

Your Answer

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