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?



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.