<p>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 <em>pure type system</em> (<a href="https://en.wikipedia.org/wiki/Pure_type_system" rel="nofollow noreferrer">https://en.wikipedia.org/wiki/Pure_type_system</a>) <span class="math-container">$\mathrm{\lambda HOPL}$</span> which contains an embedding</p>

<p><span class="math-container">$$ [\!| \_\mid\!] :\mathrm{HOL}\rightarrow \mathrm{\lambda HOPL}$$</span></p>

<p>Which is both <em>sound</em> and <em>complete</em>, that is:</p>

<p><span class="math-container">$$\Gamma\vdash_{\mathrm{HOL}}P\quad \mbox{iff}\quad [\!|\Gamma|\!]\vdash_{\mathrm{\lambda HOPL}} [\!| P|\!]$$</span></p>

<p>But this is <em>without</em> any axioms, in particular without <span class="math-container">$$\mathrm{PROPEXT}: (P \leftrightarrow Q)\ \rightarrow\ P=Q$$</span> for every <span class="math-container">$P$</span> and <span class="math-container">$Q$</span>.</p>

<p>This is explained in some detail by Tonino and Fujita in <a href="https://www.sciencedirect.com/science/article/pii/016800729290044Z" rel="nofollow noreferrer">On the adequacy of representing higher order intuitionistic logic as a pure type system</a>. I think the proof can also be found in Herman Geuvers' dissertation, but I'm a bit lazy to check at the moment.</p>

<p>With PROPEXT, this stops being true, I believe, <em>however</em>, the rule
<span class="math-container">$$ (P\leftrightarrow Q)\quad \rightarrow\quad C\ P \rightarrow C\ Q$$</span></p>

<p>is <em>admissible</em> for any <em>closed</em> predicate transformer <span class="math-container">$C:\mathrm{Prop}\rightarrow\mathrm{Prop}$</span>, by a pretty straightforward induction on (normal forms of) <span class="math-container">$C$</span>, so in some weaker sense, PROPEXT is justified in such a system (we can define equality to be <span class="math-container">$P=Q\ :=\ \forall C, C\ P \rightarrow C\ Q$</span>).</p>

<p>Note that this breaks down if you identify <span class="math-container">$\mathrm{Prop}$</span> and <span class="math-container">$\mathrm{Type}$</span>, as explained by Geuvers in <a href="https://pdfs.semanticscholar.org/2756/587b1fbb97001aa3f23eec5f4d4ad93ef1a7.pdf" rel="nofollow noreferrer">The Calculus of Constructions and Higher Order Logic</a> (i.e. CoC with this axiom is not conservative over HOL). In <em>this</em> sense, PROPEXT is not justified by the Martin-Löf propositions-as-types viewpoint.</p>

<p>I think you can form a similar story with the <span class="math-container">$J$</span>-axiom. I'm not certain equality reflection needs to come into it, since you don't have that many dependent shenanigans resulting from the embedding.</p>

<p>In response to your other questions:</p>

<ul>
<li><p>There is definitely some kind of canonicity result, which gets more subtle as you add classical axioms. Certainly the axiom-free system with only the <span class="math-container">$\forall$</span>, <span class="math-container">$\rightarrow$</span> and equality rules admits cut-elimination.</p></li>
<li><p>I'm less sure about the sub-formula properties, but I'm pretty sure they hold in the usual manner, once one has correctly formulated them in the higher order setting. They're a bit less satisfying though, since one may need to take instances of formulae quantifying over propositions themselves. I don't see a lot of use for such theorems in the meta-theory of HOL.</p></li>
</ul>

CC BY-SA 4.0
2020-06-11T15:30:26.737Z
2020-06-13T18:08:05.963Z
2020-06-13T18:08:05.963Z
cody
<p>HOL is a <a href="https://plato.stanford.edu/entries/type-theory-church/" rel="nofollow noreferrer">simple type theory</a>, while Martin-Löf's is a <em>dependent</em> type theory. That is the fundamental difference between the two.</p>

<p>One can embed HOL into <em>extensional</em> type theory, i.e., type theory with identity types and the equality reflection principle
<span class="math-container">$$\frac{\vdash p : \mathrm{Id}_A(s,t)}{\vdash s \equiv_A t}$$</span>
You could try a less drastic principle, such as Streicher's <span class="math-container">$K$</span> axiom or uniqueness of identity proofs, in which case you will be interested in conservativity of intensional type theory with <span class="math-container">$K$</span> over extensional type theory. But perhaps you don't want to dig into such details right now.</p>

CC BY-SA 4.0
2020-06-10T00:24:54.140Z
Section 5 of [The HOL Light manual](https://www.cl.cam.ac.uk/~jrh13/hol-light/manual-1.1.pdf) indeed affirms that the basis of HOL Light it a simple type theory.
Łukasz Lew
CC BY-SA 4.0
2020-06-10T00:39:20.010Z
What do we require from the extensional type theory to make the embedding work? You pointed out existence of identity types and equality reflection principle. Nit: does it make a difference if we add a constant $r : Id_T (\lambda x.t x\;,\; t)$ or assert that equality definitionally (Indeed let's ignore the finesse of K)?  Importantly, how do we interpret HOL 'bool' type? Perhaps as the universe, or should we need to add a Prop type? Could and should 'Hilbert choice operator' and 'ind' type be just defined as constant?
Łukasz Lew
CC BY-SA 4.0
2020-06-10T06:20:39.847Z
You can interpret `bool` as `bool` (the inductive type with two constants). Equality reflection implies the $\eta$-law that you're asking about. You can even throw in other forms of extensionality, such as function extensionality, as equlity reflection is very powerful.
Andrej Bauer
CC BY-SA 4.0
2020-06-09T06:20:16.473Z
2020-06-09T06:20:16.473Z
Andrej Bauer
<p>I'm trying to understand how <a href="https://en.m.wikipedia.org/wiki/HOL_Light#logical_foundations" rel="nofollow noreferrer"><code>HOL Light</code></a> deductive rules relate to mainstream intuitionistic type theories.
Here is a sample of questions that come to my mind. </p>

<p>Does <code>HOL Light</code> derivations admit cut-elimination and what sub-formula property would mean? Is there some kind of canonicity result?</p>

<p>Can HOL equality be modeled with Identity types (with J axiom)?</p>

<p>Somewhat specific question: <code>DEDUCT_ANTISYM_RULE</code> axiom allows us to deduce that if you have  (entilement) both <span class="math-container">$q \vdash p$</span> and <span class="math-container">$p \vdash q$</span>, we can deduce <span class="math-container">$\vdash p=q$</span>. How can we assert that rule without a condition that the entailments are "each other inverses forming an isomorphism"?</p>

<p>I realize that many of these question might be wrong questions to ask. Perhaps I even am wrong to focus on the deduction rules? 
How should I be thinking when comparing theories such as HOL Light and some intuitionistic type theories?</p>

CC BY-SA 4.0
2020-06-09T03:26:07.843Z
Regarding the DEDUCT_ANTISYM_RULE of your question, this is what is usually called *propositional extensionality* (and it basically presumes some kind of proof irrelevance).
Stefan
<type-theory><proof-assistants><hol-light><hol>
What is the relation of HOL Light type theory and some of the intuitionistic type theories?
Łukasz Lew
# What is the relation of HOL Light type theory and some of the intuitionistic type theories?

(Asked by: username_0 on 2020-06-08)

I'm trying to understand how [`HOL Light`](https://en.m.wikipedia.org/wiki/HOL_Light#logical_foundations) deductive rules relate to mainstream intuitionistic type theories.
Here is a sample of questions that come to my mind.

Does `HOL Light` derivations admit cut-elimination and what sub-formula property would mean? Is there some kind of canonicity result?

Can HOL equality be modeled with Identity types (with J axiom)?

Somewhat specific question: `DEDUCT_ANTISYM_RULE` axiom allows us to deduce that if you have (entilement) both $q \vdash p$ and $p \vdash q$, we can deduce $\vdash p=q$. How can we assert that rule without a condition that the entailments are "each other inverses forming an isomorphism"?

I realize that many of these question might be wrong questions to ask. Perhaps I even am wrong to focus on the deduction rules?
How should I be thinking when comparing theories such as HOL Light and some intuitionistic type theories?

**Tags:** type-theory, proof-assistants, hol-light, hol
> **Comments:**
> **username_1**: Regarding the DEDUCT_ANTISYM_RULE of your question, this is what is usually called *propositional extensionality* (and it basically presumes some kind of proof irrelevance).  

---

## 2 answers

### Answer by username_2 on 2020-06-11. Score: 2 | Accepted answer

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>) $\mathrm{\lambda HOPL}$ which contains an embedding

$$ [\!| \\_\mid\!] :\mathrm{HOL}\rightarrow \mathrm{\lambda HOPL}$$

Which is both *sound* and *complete*, that is:

$$\Gamma\vdash\_{\mathrm{HOL}}P\quad \mbox{iff}\quad [\!|\Gamma|\!]\vdash\_{\mathrm{\lambda HOPL}} [\!| P|\!]$$

But this is *without* any axioms, in particular without $$\mathrm{PROPEXT}: (P \leftrightarrow Q)\ \rightarrow\ P=Q$$ for every $P$ and $Q$.

This is explained in some detail by Tonino and Fujita in [On the adequacy of representing higher order intuitionistic logic as a pure type system](https://www.sciencedirect.com/science/article/pii/016800729290044Z). I think the proof can also be found in Herman Geuvers' dissertation, but I'm a bit lazy to check at the moment.

With PROPEXT, this stops being true, I believe, *however*, the rule
$$ (P\leftrightarrow Q)\quad \rightarrow\quad C\ P \rightarrow C\ Q$$

is *admissible* for any *closed* predicate transformer $C:\mathrm{Prop}\rightarrow\mathrm{Prop}$, by a pretty straightforward induction on (normal forms of) $C$, so in some weaker sense, PROPEXT is justified in such a system (we can define equality to be $P=Q\ :=\ \forall C, C\ P \rightarrow C\ Q$).

Note that this breaks down if you identify $\mathrm{Prop}$ and $\mathrm{Type}$, as explained by Geuvers in [The Calculus of Constructions and Higher Order Logic](https://pdfs.semanticscholar.org/2756/587b1fbb97001aa3f23eec5f4d4ad93ef1a7.pdf) (i.e. CoC with this axiom is not conservative over HOL). In *this* sense, PROPEXT is not justified by the Martin-Löf propositions-as-types viewpoint.

I think you can form a similar story with the $J$-axiom. I'm not certain equality reflection needs to come into it, since you don't have that many dependent shenanigans resulting from the embedding.

In response to your other questions:

* There is definitely some kind of canonicity result, which gets more subtle as you add classical axioms. Certainly the axiom-free system with only the $\forall$, $\rightarrow$ and equality rules admits cut-elimination.
* I'm less sure about the sub-formula properties, but I'm pretty sure they hold in the usual manner, once one has correctly formulated them in the higher order setting. They're a bit less satisfying though, since one may need to take instances of formulae quantifying over propositions themselves. I don't see a lot of use for such theorems in the meta-theory of HOL.


---

### Answer by username_3 on 2020-06-09. Score: 2

HOL is a [simple type theory](https://plato.stanford.edu/entries/type-theory-church/), 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 identity types and the equality reflection principle
$$\frac{\vdash p : \mathrm{Id}\_A(s,t)}{\vdash s \equiv\_A t}$$
You could try a less drastic principle, such as Streicher's $K$ axiom or uniqueness of identity proofs, in which case you will be interested in conservativity of intensional type theory with $K$ over extensional type theory. But perhaps you don't want to dig into such details right now.

> **Comments:**
> **username_0**: Section 5 of [The HOL Light manual](https://www.cl.cam.ac.uk/~jrh13/hol-light/manual-1.1.pdf) indeed affirms that the basis of HOL Light it a simple type theory.  
> **username_0**: What do we require from the extensional type theory to make the embedding work? You pointed out existence of identity types and equality reflection principle. Nit: does it make a difference if we add a constant $r : Id_T (\lambda x.t x\;,\; t)$ or assert that equality definitionally (Indeed let's ignore the finesse of K)?  Importantly, how do we interpret HOL 'bool' type? Perhaps as the universe, or should we need to add a Prop type? Could and should 'Hilbert choice operator' and 'ind' type be just defined as constant?  
> **username_3**: You can interpret `bool` as `bool` (the inductive type with two constants). Equality reflection implies the $\eta$-law that you're asking about. You can even throw in other forms of extensionality, such as function extensionality, as equlity reflection is very powerful.  

---

