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

Question

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 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?

Answer 1

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. 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 (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 2

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 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.