26
$\begingroup$

It is possible (with some cleverness) to prove false from type-in-type. For instance, Girard proved false in Martin Lof's original system (as described in the introduction of An Intuitionistic Theory of Types). This answer has a good account of the formal details.

Most systems allow type-in-type, through a configured opt-in and sometimes even by default (Pebble, Cayenne, some Trellys languages).

Has anyone ever "proven" an incorrect theorem with type-in-type, without intending to show that the system is unsound?

$\endgroup$

2 Answers 2

35
$\begingroup$

Yes. In fact, there is a very interesting example which is tied to the history of dependent type theory:

Per Martin-Löf, in his 1971 manuscript*, studied a system with type-in-type which famously turned out to be non-normalizing and inconsistent.

However, this manuscript does includes a proof of normalization and consistency for the system. It proceeds in the now-standard (although innovative at the time) way of associating a reducibility predicate to every type, and then proving by induction on typing derivations that every well-typed term satisfies the corresponding reducibility predicate. The proof is correct as far as I know, but proving that the universe satisfies its own reducibility predicate requires type-in-type in the meta-theory.

TL;DR: using type-in-type, Per Martin-Löf proved that type-in-type is normalizing and consistent.


*which was never published, but is available as a historical document with the permission of the author.

$\endgroup$
7
  • 2
    $\begingroup$ You're referring specifically to 5.1.4.1, where V is the symbol for type universes? If I'm reading this correctly the meta-theoretic impredicativity is implicit? That manuscript is incredible. $\endgroup$
    – user833970
    Mar 31 at 17:40
  • 1
    $\begingroup$ Precisely, yes! In 5.1.1.1, τV is defined to be the type of triples (τ, ω, θ) where τ is a type and ω and θ are [...]. Then in 5.1.4.1, "We have to show that [...] the triple (τV, ωV, θV) is an object of type τV, which is immediately clear" is an instance of type-in-type. $\endgroup$
    – Loïc
    Mar 31 at 18:16
  • $\begingroup$ I guess it's reasonable to assume that Martin Lof was doing the meta theory in some informal type theory with type:type. $\endgroup$
    – user833970
    Mar 31 at 18:24
  • 2
    $\begingroup$ And the obvious next question is, has anyone unintentionally proven a false theorem with type-in-type (or naive set theory) outside of the areas of logic and set theory? $\endgroup$
    – user21820
    Apr 1 at 13:53
  • $\begingroup$ @user21820 I think that could make a good follow up question. Though we should be carful about the phrasing. For instance, would Mike Shulman's answer count as "logic" or "set theory"? $\endgroup$
    – user833970
    Apr 4 at 14:20
34
+50
$\begingroup$

I did this myself!

(At least, if you interpret "incorrect" as "probably not true" rather than "demonstrably false".)

In the early days of homotopy type theory, we were starting to use multiple universes in ways that, I believe, had rarely been done before in type theory. Since Coq didn't support universe polymorphism yet, the only way to formalize some results was using type-in-type. In particular, I used it when formalizing some of the initial work on modalities that eventually became the RSS paper.

One of the results I proved, at that time, was that an (idempotent monadic) modality is left exact if and only if the universe of modal types is modal. This was a really striking application of, and justification for, the notion of left exactness. In particular, it implies that the modal types for a left exact modality form a model of type theory on their own, which is useful when constructing higher-topos models of type theory since any topos is a left exact localization of a presheaf topos.

Unfortunately, when we later went back to write up and formalize these results correctly using universe polymorphism, I realized that the proof was invalid. When universe levels are tracked, what I had proven was that the type of modal types in one universe $U$ was null with respect to all $U$-small modally-connected types; but since $U$ is not $U$-small, that doesn't imply $U$ is modal — unless we assume the modality is generated by a $U$-small family, i.e. that it is $U$-accessible. (In this form, the result is Theorem 3.11 in RSS.)

I don't have a counterexample to the statement in the non-accessible case, but I doubt it is true. In fact, for a non-accessible modality there isn't necessarily a canonical way to extend a modality on one universe to a modality on larger universes, so if we have a lex modality on $U$-small types, it's not even obvious what it means to say that $U$ is modal.

Ever since this experience, I've been unconvinced by any argument along the lines of "type-in-type is okay as long as you don't do anything stupid". I'm willing to grant that what I did was stupid; the point is that it's possible to do stupid things by accident.

$\endgroup$
5
  • 7
    $\begingroup$ I wish there was a way to accept multiple answers. $\endgroup$
    – user833970
    Apr 1 at 18:05
  • 3
    $\begingroup$ A hilarious and informative anecdote! :) $\endgroup$ Apr 2 at 0:01
  • 1
    $\begingroup$ @user833970 I wish there was a way to accept multiple answers. Award each one a small bounty. Then it will be obvious that you find each one of equal value. The minimum bounty is 50 points. Examples of bounties (ref) $\endgroup$
    – Guy Coder
    Apr 2 at 12:39
  • $\begingroup$ @GuyCoder sounds like a good idea, though I'll wait a bit in case other people have more answers. It's also possible that a more clean cut example exists which might deserve the checkmark most (not having to assume the nature of ML's informal meta-theory, knowing for sure the theorem statement was false). $\endgroup$
    – user833970
    Apr 4 at 14:16
  • 1
    $\begingroup$ @user833970 possible that a more clean cut example exists which might deserve the checkmar I find that one should wait at least 5 days minimum on this site before accepting and then no earlier than a Monday evening. Seems some users only show up here on Sunday afternoon. If my finding is correct one of them in the group is a legend. $\endgroup$
    – Guy Coder
    Apr 4 at 14:25

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.