13
$\begingroup$

We are all familiar with Russell's paradox, and it is known that Per Martin-Löf proved that type-in-type is normalizing and consistent (which is false), by accidentally using an assumption in his meta-theory that is essentially type-in-type. But all these arise in the areas of logic and foundations. Has anyone proven some statement Q by accidentally using some type-in-type assumption, without being aware that such an assumption is unsound, and such that Q can be shown to be surely false (say in a typical predicative type theory)?

The linked example would be considered to be under foundations. Here is another example that is not quite under logic or foundations but anyone who proves it will certainly be immediately aware that the type-in-type assumption is unsound: Let W be the type of all rooted (downward-directed) trees with no infinite (downward) path. Let T be a rooted tree whose root has exactly the members of W as children. Now T is in W...

So is there any example where the person who proved the result was still unaware (at least for a reasonable period of time) that the type-in-type assumption was unsound?

Improve this question
$\endgroup$
15
  • 1
    $\begingroup$ @AndrejBauer is this the one: proofassistants.stackexchange.com/questions/1219/… ? I don't know if this fits the question, though: I would say it is outside of logic and foundation, but Mike Shulman says he does not know whether it holds or not, so it probably cannot "be shown to be surely false" with our current knowledge… $\endgroup$
    – Meven Lennon-Bertrand ♦
    Commented Nov 23, 2022 at 16:32
  • 1
    $\begingroup$ Just about anyone who learns type theory nowadays knows about type-in-type. So if there is an example of what you're asking for, it would have to have taken place in the narrow period between Martin-Löf's type theory with type-in-type, and the realization that it's inconsistent. $\endgroup$
    – Andrej Bauer
    Commented Nov 23, 2022 at 16:59
  • 1
    $\begingroup$ @AndrejBauer: It need not be in type theory. Naive set theory also has a type-in-type assumption, even if it is not called "type". I'm not intending to restrict answers to only type theories of a particular narrow tradition. $\endgroup$
    – user21820
    Commented Nov 23, 2022 at 18:39
  • 2
    $\begingroup$ Mike's example looks like it's "just" about type theory, but it actually has a much wider applicability. $\endgroup$
    – Andrej Bauer
    Commented Nov 23, 2022 at 19:00
  • 1
    $\begingroup$ And negation is not even needed, nor is any notion at all about 'categories'. To see why, if type∈type, then let S be the 'type' of all types x such that ∀t∈{ 0 : x∈x } ( ⊥ ), and it is trivial to obtain ⊥ by constructive proof: Given any t∈{ 0 : S∈S }, we have S∈S and so ∀t∈{ 0 : S∈S } ( ⊥ ), hence ⊥. Therefore S∈S, and so ⊥. By the way, if we require a type's defining predicate to quantify over only predicative types, then we can have type∈type in a predicative system! $\endgroup$
    – user21820
    Commented Nov 26, 2022 at 19:05

0

Reset to default

Your Answer

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