16
$\begingroup$

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.

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.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
13
$\begingroup$

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 of dependent type theory, which was the first to invalidate uniqueness of identity proofs.

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

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. This provides a wealth of possibilities, but one must now learn homotopy theory to get hands on the models.

Improve this answer
$\endgroup$
5
  • 2
    $\begingroup$ 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... $\endgroup$
    – cody
    Oct 29, 2012 at 19:57
  • $\begingroup$ @cody: good point, normal forms can be very useful. $\endgroup$
    – Andrej Bauer
    Nov 3, 2012 at 4:20
  • $\begingroup$ @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? $\endgroup$
    – Blaisorblade
    Mar 12, 2014 at 20:12
  • $\begingroup$ @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. $\endgroup$
    – cody
    Mar 13, 2014 at 20:21
  • $\begingroup$ 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: cstheory.stackexchange.com/q/21534/989 $\endgroup$
    – Blaisorblade
    Mar 13, 2014 at 23:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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