6 votes
Accepted

Why REFL rule is primitive in HOL Light?

DEDUCT_ANTISYM_RULE only applies to propositions, while REFL applies to all terms of all types. Your suggestion only shows that ...
Andrej Bauer's user avatar
  • 28.8k
2 votes
Accepted

What is the relation of HOL Light type theory and some of the intuitionistic type theories?

There are a number of ways to see HOL as an instance of a "dependent" type theory, in a way that is reasonable, that is there is a pure type system (https://en.wikipedia.org/wiki/Pure_type_system) $\...
cody's user avatar
  • 13.9k
2 votes

What is the relation of HOL Light type theory and some of the intuitionistic type theories?

HOL is a simple type theory, while Martin-Löf's is a dependent type theory. That is the fundamental difference between the two. One can embed HOL into extensional type theory, i.e., type theory with ...
Andrej Bauer's user avatar
  • 28.8k

Only top scored, non community-wiki answers of a minimum length are eligible