New types in higher order logic

Question

From my understanding, most descriptions of higher order logic have a clear "phase distinction":

• We first describe the types, which are usually syntactically simple trees. For concreteness, let's say there are product types $A \times B$ and power types $\mathcal P (A)$, and base types $\mathbb N, \Omega, \bf 1$ for natural numbers, propositions and the unit type.
• Next, we describe the terms in these types. We have syntax for pairs $(a,b)$, set comprehension $\{x :A \mid \varphi(x)\}$, $0, \mathsf{succ}$ for natural numbers, $*$ for the unit type, and we have all the required proposition formers in the proposition type. These come equipped with the natural notion of free variables and substitution.
• Finally, we describe a judgement like $p \vdash_{\Gamma} q$, where $p,q$ are terms of type $\Omega$ in the context $\Gamma$, formalizing the notion of proofs. These may come with the expected metatheorems, like cut elimination, stability under substitution etc.

It is this distinction between these three layers that separate higher order logic (aka simple type theory) from dependently typed proof systems. However, this is quite tedious to use. For example, this presentation doesn't have a function type, and they should be encoded by a particular subset of $\mathcal P(A \times B)$. So every time we need a function, we actually take an element $f :\mathcal P(A \times B)$ with a proof of $\vdash \textrm{isFunctional}(f)$. Similarly, a group cannot be considered as a single object, but rather a carrier type $A$, a subset of that type $S : \mathcal P(A)$ (since we rarely care about group structures which happen to be on one of the built-in types), an operation $\times$, and a bunch of proofs of the required axioms.

I'm wondering about how practical HOL users overcome this issue. The first idea that I have is to use some syntactic sugar to bundle these data together, and Isabelle locales and records seems to be roughly along this line. And indeed I found the group theory formalization to follow this. However for quotients, the rat and real type in Isabelle/HOL seems to break the phase distinction, by allowing the generation of a quotient type, dependent on a type and a term. HOL light also seems to have similar primitive type formers coming from new_basic_type_definition.

This raises several closely related questions:

• If types can now depend on terms, what separates HOL from dependent type theory?
  • Still, there is no Curry–Howard correspondence, but dependent type theory can refrain from using CH too.
  • I noticed that the new types are declared a new name, and declaring the same type twice under different names will result in different types. Is there a name for this?
• What are some other ways to overcome the issue above in practice, if not letting types depend on terms?

Answer 1

First, there is no reason to remove function types, so you should put those in. Then you can remove special treatment of propositions because they are just functions with codomain $\Omega$. So far we have:

• simple types, including $1$, $\mathbb{N}$, $\Omega$, $A \times B$ and $A \to B$
• $\lambda$-calculus over these, but no characterization of $\Omega$

To get $\Omega$ going we need some form of comprehension, which is what the subtype $\lbrace x : A \mid \phi \rbrace$ is for. Note that here $x : A \vdash \phi : \Omega$, i.e., $\phi$ is not allowed to contain extra parameters (or else we would get dependent types). Ah, we probably need equality as a map $=_A : A \times A \to \Omega$, with suitable laws. (Lambek & Scott's book has an equational presentation of topos logic.)

There is one last bit that we need to make things somewhat workable: type variables. We can use these schematically (in computer science parlance we're doing parametric polymorphism), but we cannot quantify over them. Isabelle/HOL allows this, of course.

We must also allow mechanisms for introducing definitions and abbreviations. These can be thought of as meta-level concepts, and while we are at it, we can allow bunching them together into "structures" so that we can treat, say, a group as a single entity rather than 6 separate things.

Of course, we're just inching closer and closer to having a dependent type theory. I personally do not have a really good answer why simple type theory might be better for formalization than dependent type theory - I am sure someone else can explain what the advantages are.

I would just like to point out that the correspondence between elementary toposes and higher-order intuitionistic logic is not the only one possible. Since every topos is also a locally cartesian closed category, we can have another correspondence, namely between toposes and extensional dependent type theories with $\Omega$.

Actually, has anyone bothered to write down precisely what sort of dependent type theories elementary toposes are sound and complete for? Perhaps:

• dependent type theory with $\Pi$, $\Sigma$, $\mathrm{Id}$, $\mathbb{N}$,
• equality reflection,
• propositional truncation,
• a type $\Omega$ classifying propositions.

On the category-theoretic side we might have to modify the definition of the topos a little bit and present it fibration-style, so that coherence of substitution can be dealt with.