2
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ 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). $\endgroup$ – Stefan Jun 9 at 3:26
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Section 5 of The HOL Light manual indeed affirms that the basis of HOL Light it a simple type theory. $\endgroup$ – Łukasz Lew Jun 10 at 0:24
  • $\begingroup$ 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? $\endgroup$ – Łukasz Lew Jun 10 at 0:39
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Jun 10 at 6:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.