Skip to main content

All Questions

Tagged with
5 votes
0 answers
231 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