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 ...
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) $\...
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 ...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
hol × 3lo.logic × 2
type-theory × 2
proof-assistants × 2
hol-light × 2
computability × 1
functional-programming × 1