# Are Logics Based on Dependent Types Stronger Than Ones Without?

There have been several times during I came across statements like Isabelle/HOL's logic is not rich enough to formalize X on various places online and in during personal discussions. Or similar statements that HOL is weaker than CoC or similar because of the lack of dependent types.

Can someone explain what this means? For example, can someone give an example for X and explain why this is not possible to formalize in a system like HOL?

• Related. (Not a duplicate, though.) Feb 23, 2022 at 18:15
• One thing that make type theories occurring in most PAs strictly logically (consistency-wise) stronger is the availability of universes. I would think that one universe is enough to build a model of HOL (and thus showing that is stronger by Gödels 2nd). By the same token, “There exists a model of HOL” can't be proved in HOL. OTOH, Isabelle/HOL includes a theory (ZFC_in_HOL) that builds a set theoretic universe, so you recover some strength. Nevertheless, these comments are independent of the fact that implementing some stuff in DTT might be more direct than in HOL. Feb 23, 2022 at 19:37
• As @PedroSánchezTerraf is noting your question seems to be conflating logical strength with expressivity/easy-of-use. The former is well defined while the later is more subjective. Almost all common mathematical objects can be defined in HOL, but some like Kevin Buzzard would argue it is easier or more natural to define some of them in DTT. However Isabelle/HOL users would likely push back on this assertion. Feb 23, 2022 at 20:09
• If you put in enough axioms you can formalize anything. It's just that you need to take far more effort to do something one way, and far less the other. And by far I mean at least thousands of times.
– Trebor
Feb 24, 2022 at 2:52

For completeness I'm adding the specific example that the OP is asking for, turning my comment above and Jason Rute's into an answer.

One thing that make type theories occurring in most PAs strictly logically (consistency-wise) stronger is the availability of universes. I would think that one universe is enough to build a model of HOL (and thus showing that is stronger by Gödels 2nd incompleteness theorem). By the same token, “There exists a model of HOL” can't be proved in HOL. On the other hand, Isabelle/HOL includes a theory (ZFC_in_HOL) that builds a set theoretic universe, so you recover some strength.

That said, the great majority of results in math do not need logical strength greater than few orders on top arithmetic: For instance, McLarty showed that Fermat's Last Theorem can be formalized in something like third order arithmetic (while every HOL system provides you with all the finite orders).

Nevertheless, these comments are independent of the fact that implementing some stuff in DTT might be more direct than in HOL. This is the point usually made by K. Buzzard.

EDIT: Some references that were kindly provided by user9716869: the document The HOL System Logic provides HOL semantics (effectively in $$V(\omega+\omega)$$ without the empty set). Sets in Types, Types in Sets shows that ZFC with n inaccessibles can be encoded in CiC with a variant of the Axiom of Choice and $$n+1$$ universes.

Pretty much always, it means "this gadget is more annoying to formalise in HOL", not "this gadget is not possible to formalise in HOL."

A simple example of this is formalising finite dimensional Euclidean spaces -- basically, spaces $$\mathbb{R}^n$$ where $$n$$ is a natural number.

The dimension $$n$$ is a natural example of type dependency, and so proving things about them in HOL is subtle enough that John Harrison wrote a whole TPHOLS paper about it, titled (obviously enough) A HOL Theory of Euclidean space.