10
$\begingroup$

It's a fairly well-known fact that deriving a contradiction from a disequality (for example, $(0=1) \to \bot$) in Martin-Loef type theory requires a universe.

The proof is also fairly straightforward -- in the absence of universes, we can erase the dependencies from any dependent type to get a simple type as its shape, and so proving that $(0=1) \to \bot$ implies we can prove $p \to \bot$ for an arbitrary atom $p$, which is of course not possible.

However, I can't find who proved this first! Does anyone have a reference?

$\endgroup$
  • $\begingroup$ Coquand's "A New Paradox in Type Theory" (94) describes the truth valued semantics of minimal higher-order logic, and seems to suggest that this interpretation was known before. I seem to recall a mention of such a model even for Russell's Type Theory but I can't seem to find it... $\endgroup$ – cody Jan 22 '15 at 15:56
  • $\begingroup$ This Martin Hoffman text confirms the Jan Smith reference in the answer, and has a reasonable presentation of that proof with categorical semantics in the exercises ioc.ee/~james/ITT9200/SyntaxAndSemanticsof%20DependentTypes.pdf $\endgroup$ – user833970 May 28 at 16:24
10
$\begingroup$

I know of:

Jan M. Smith, The independence of Peano's fourth axiom from Martin-Löf's type theory without universes, The Journal of Symbolic Logic 53(3), p. 840-845, 1988.

$\endgroup$

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.