<p>The question is about dependent type theory, but, if the type you are trying to show non-inhabited can be expressed as a first-order formula, you can also use <strong>classical logic</strong>. You either prove classically the negation of your formula, hence your formula can not be proven intuitionistically, for were it provable you would get a contradiction classically. Or, you can use the very rich field of classical Model Theory to find a counter-model for your formula, showing that the formula is not provable classically, hence also intuitionistically.</p>
<p>Moreover, in case you are concerned about giving constructive arguments of the non-provability, the above use of classical reasoning (model theory) is totally constructive: since the Soundness Theorem for classical first order logic is intuitionistic, the existence of a classical counter-model intuitionistically implies the non-provability of the formula.</p>

CC BY-SA 4.0
2023-07-14T15:04:27.957Z
2023-07-14T15:04:27.957Z
Danko Ilik
<p>That a formula is not provable can essentially be done in two ways. With some luck we might be able to show within type theory that the formula implies one which is already known to be not provable. The other way is to find a model in which the formula is invalid, and this can be quite hard. For example, it took a very long time to find the <a href="http://homotopytypetheory.org/references/hofmann-streicher-the-groupoid-interpretation-of-type-theory/">groupoid model</a> of dependent type theory, which was the first to invalidate <a href="http://coq.inria.fr/library/Coq.Logic.EqdepFacts.html#UIP_">uniqueness of identity proofs</a>.</p>

<p>The question "what is a model of dependent type theory?" has a somewhat complicated answer. If you ignore certain properties of substitution, a model is a <a href="http://ncatlab.org/nlab/show/locally+cartesian+closed+category">locally cartesian closed category</a>, and that might be the simplest answer. If you want a "real" model, then there are several options, see the nLab page on <a href="http://ncatlab.org/nlab/show/categorical+model+of+dependent+types">categorical models of dependent type theory</a>. In any case, the answer is always a bit complicated because dependent type theory is a fairly complex formal system.</p>

<p>If I were to suggest just one article on the subject, I would probably recommend the original paper by Robert Seely, <a href="http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf">"Locally cartesian closed categories and type theory"</a>. If I were to suggest another one, it would probably be one that explains what needs to be corrected in Seely's paper, e.g., Martin Hoffman's <a href="http://www.dcs.ed.ac.uk/home/mxh/csl94.ps.gz">"On the Interpretation of Type Theory in Locally Cartesian Closed Categories"</a>.</p>

<p>A recent important advance in this area is the realization that homotopy-theoretic models are also models of dependent type theory, see <a href="http://homotopytypetheory.org/references/">homotopytypetheory.org references</a>. This provides a wealth of possibilities, but one must now learn homotopy theory to get hands on the models.</p>

CC BY-SA 3.0
2012-10-29T19:57:21.857Z
This answer is quite nice, though it ignores perhaps the simplest possible way to prove that a type is not inhabited: induction on normal forms! In particular, it is easy to prove that the excluded middle can not be inhabited in the Calculus of Constructions by such induction.

Of course, you then need to show that every term can be put into a normal form of the same type, and that does involve a model construction...
cody
CC BY-SA 3.0
2012-11-03T04:20:11.280Z
@cody: good point, normal forms can be very useful.
Andrej Bauer
CC BY-SA 3.0
2014-03-12T20:12:40.847Z
@cody: "you then need to show that every term can be put into a normal form of the same type": isn't that a standard part of the metatheory for a "good" type system (as long as you don't have axioms), or a "good" logic (where this is cut elimination)? So you can just reuse the existing proof, right?
Blaisorblade
CC BY-SA 3.0
2014-03-13T20:21:34.437Z
@Blaisorblade: of course you only need to prove cut-elimination once. May point was that using induction on normal forms instead of model constructions was a way of begging the question: you already are constructing a model to show that every term can be put into normal form. In some sense you are working in the "normal form model", rather than doing strictly syntactic work.
cody
CC BY-SA 3.0
2014-03-13T23:06:44.470Z
I see - I was thinking about the "proof effort", while I guess you're reasoning about how the whole proof is implemented.
But you've made me question yet again the distinction between syntactic and semantic approaches, given constructions such as term models. So I asked a separate question on that: http://cstheory.stackexchange.com/q/21534/989
Blaisorblade
CC BY-SA 3.0
2012-10-28T03:41:45.053Z
2012-10-28T03:53:18.243Z
2012-10-28T03:53:18.243Z
Andrej Bauer
<p>For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, to disprove a formula, we can restrict to one Heyting algebra where each formula is represented by an open subset of $\mathbb{R}$.</p>

<p>For example, if we want to show that $\forall\alpha.\alpha\lor(\alpha\rightarrow\bot)$ is not inhabited, we construct a mapping $\phi$ from formulas to open subsets of $\mathbb{R}$ by defining:
\begin{align}
\phi(\alpha) &amp;= (-\infty, 0)
\end{align}
Then
\begin{align}
\phi(\alpha\rightarrow\bot) &amp;= \mbox{int}( [0, \infty) ) \\ &amp; = (0,\infty) \\
\phi(\alpha\lor(\alpha\rightarrow\bot)) &amp;= (-\infty, 0) \cup (0,\infty) \\
  &amp;= \mathbb{R} \setminus {0}.
\end{align}
This shows that the original formula cannot be provable, since we have a model where it's not true, or equivalently (by Curry-Howard isomorphism) the type cannot be inhabited.</p>

<p>Another possibility would be to use <a href="https://en.wikipedia.org/wiki/Kripke_frame">Kriepke frames</a>.</p>

<hr>

<p>Are there any similar methods for systems with dependent types? Like some generalization of Heyting algebras or Kripke frames?</p>

<p>Note: I'm not asking for a decision procedure, I know there cannot be any. I'm asking just for a mechanism that allows to witness unprovability of a formula - to convince someone that it's unprovable.</p>

CC BY-SA 4.0
2023-07-14T21:26:29.517Z
This is gonna seem obvious, but sometimes one can prove $T\rightarrow\bot$, in fact this is the preferred method!
cody
<lo.logic><dependent-type><model-theory><calculus-of-constructions>
How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?
Petr
# How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?

(Asked by: username_0 on 2012-10-27)

For systems without dependent types, like Hindley-Milner type system, the types correspond to formulas of intuitionistic logic. There we know that its models are Heyting algebras, and in particular, to disprove a formula, we can restrict to one Heyting algebra where each formula is represented by an open subset of $\mathbb{R}$.

For example, if we want to show that $\forall\alpha.\alpha\lor(\alpha\rightarrow\bot)$ is not inhabited, we construct a mapping $\phi$ from formulas to open subsets of $\mathbb{R}$ by defining:
\begin{align}
\phi(\alpha) &= (-\infty, 0)
\end{align}
Then
\begin{align}
\phi(\alpha\rightarrow\bot) &= \mbox{int}( [0, \infty) ) \\ & = (0,\infty) \\
\phi(\alpha\lor(\alpha\rightarrow\bot)) &= (-\infty, 0) \cup (0,\infty) \\
&= \mathbb{R} \setminus {0}.
\end{align}
This shows that the original formula cannot be provable, since we have a model where it's not true, or equivalently (by Curry-Howard isomorphism) the type cannot be inhabited.

Another possibility would be to use [Kriepke frames](https://en.wikipedia.org/wiki/Kripke_frame).

---

Are there any similar methods for systems with dependent types? Like some generalization of Heyting algebras or Kripke frames?

Note: I'm not asking for a decision procedure, I know there cannot be any. I'm asking just for a mechanism that allows to witness unprovability of a formula - to convince someone that it's unprovable.

**Tags:** lo.logic, dependent-type, model-theory, calculus-of-constructions
> **Comments:**
> **username_1**: This is gonna seem obvious, but sometimes one can prove $T\rightarrow\bot$, in fact this is the preferred method!  

---

## 2 answers

### Answer by username_3 on 2012-10-28. Score: 13 | Accepted answer

That a formula is not provable can essentially be done in two ways. With some luck we might be able to show within type theory that the formula implies one which is already known to be not provable. The other way is to find a model in which the formula is invalid, and this can be quite hard. For example, it took a very long time to find the [groupoid model](http://homotopytypetheory.org/references/hofmann-streicher-the-groupoid-interpretation-of-type-theory/) of dependent type theory, which was the first to invalidate [uniqueness of identity proofs](http://coq.inria.fr/library/Coq.Logic.EqdepFacts.html#UIP_).

The question "what is a model of dependent type theory?" has a somewhat complicated answer. If you ignore certain properties of substitution, a model is a [locally cartesian closed category](http://ncatlab.org/nlab/show/locally+cartesian+closed+category), and that might be the simplest answer. If you want a "real" model, then there are several options, see the nLab page on [categorical models of dependent type theory](http://ncatlab.org/nlab/show/categorical+model+of+dependent+types). In any case, the answer is always a bit complicated because dependent type theory is a fairly complex formal system.

If I were to suggest just one article on the subject, I would probably recommend the original paper by Robert Seely, ["Locally cartesian closed categories and type theory"](http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf). If I were to suggest another one, it would probably be one that explains what needs to be corrected in Seely's paper, e.g., Martin Hoffman's ["On the Interpretation of Type Theory in Locally Cartesian Closed Categories"](http://www.dcs.ed.ac.uk/home/mxh/csl94.ps.gz).

A recent important advance in this area is the realization that homotopy-theoretic models are also models of dependent type theory, see [homotopytypetheory.org references](http://homotopytypetheory.org/references/). This provides a wealth of possibilities, but one must now learn homotopy theory to get hands on the models.

> **Comments:**
> **username_1**: This answer is quite nice, though it ignores perhaps the simplest possible way to prove that a type is not inhabited: induction on normal forms! In particular, it is easy to prove that the excluded middle can not be inhabited in the Calculus of Constructions by such induction.  Of course, you then need to show that every term can be put into a normal form of the same type, and that does involve a model construction...  
> **username_3**: @cody: good point, normal forms can be very useful.  
> **username_4**: @cody: "you then need to show that every term can be put into a normal form of the same type": isn't that a standard part of the metatheory for a "good" type system (as long as you don't have axioms), or a "good" logic (where this is cut elimination)? So you can just reuse the existing proof, right?  
> **username_1**: @Blaisorblade: of course you only need to prove cut-elimination once. May point was that using induction on normal forms instead of model constructions was a way of begging the question: you already are constructing a model to show that every term can be put into normal form. In some sense you are working in the "normal form model", rather than doing strictly syntactic work.  
> **username_4**: I see - I was thinking about the "proof effort", while I guess you're reasoning about how the whole proof is implemented. But you've made me question yet again the distinction between syntactic and semantic approaches, given constructions such as term models. So I asked a separate question on that: http://cstheory.stackexchange.com/q/21534/989  

---

### Answer by username_2 on 2023-07-14. Score: 1

The question is about dependent type theory, but, if the type you are trying to show non-inhabited can be expressed as a first-order formula, you can also use **classical logic**. You either prove classically the negation of your formula, hence your formula can not be proven intuitionistically, for were it provable you would get a contradiction classically. Or, you can use the very rich field of classical Model Theory to find a counter-model for your formula, showing that the formula is not provable classically, hence also intuitionistically.

Moreover, in case you are concerned about giving constructive arguments of the non-provability, the above use of classical reasoning (model theory) is totally constructive: since the Soundness Theorem for classical first order logic is intuitionistic, the existence of a classical counter-model intuitionistically implies the non-provability of the formula.


---

