Questions tagged [hol]
The hol tag has no usage guidance.
3
questions
1
vote
0
answers
55
views
Primitive recursion relative to a logical system
In various places I have read that the normally considered non-primitive recursive Ackermann function is primitive recursive in higher-order logic. It's claimed to be due to "Reynolds, 1985",...
- 900
4
votes
2
answers
152
views
What is the relation of HOL Light type theory and some of the intuitionistic type theories?
I'm trying to understand how HOL Light deductive rules relate to mainstream intuitionistic type theories.
Here is a sample of questions that come to my mind.
Does ...
- 1,177
4
votes
1
answer
94
views
Why REFL rule is primitive in HOL Light?
HOL Light
assumed REFL as a primitive.
Why does it need to do so?
Can't REFL rule be deduced in this way using ...
- 1,177