Skip to main content

Questions tagged [hol]

Use this tag for the HOL Interactive Theorem Prover. Do not use this tag for other proof assistants in the HOL family such as HOL Light. For questions about higher order logic use the tag (higher-order-logic).

1 question with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
5 votes
0 answers
225 views

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-...
Ilk's user avatar
  • 547