<p>I know of:</p>

<p>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.</p>

CC BY-SA 3.0
2015-01-22T14:46:24.787Z
2015-01-22T14:46:24.787Z
Ulrik Buchholtz
<p>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. </p>

<p>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.</p>

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

CC BY-SA 3.0
2015-01-22T15:56:43.440Z
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...
cody
CC BY-SA 4.0
2019-05-28T16:24:57.313Z
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 https://www.ioc.ee/~james/ITT9200/SyntaxAndSemanticsof%20DependentTypes.pdf
user833970
<reference-request><lo.logic><pl.programming-languages><type-theory><dependent-type>
Reference for the fact that (0=1) implies false requires a universe in MLTT
Neel Krishnaswami
# Reference for the fact that (0=1) implies false requires a universe in MLTT

(Asked by: username_0 on 2015-01-22)

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?

**Tags:** reference-request, lo.logic, pl.programming-languages, type-theory, dependent-type

> **Comments:**
> **username_1**: 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...  
> **username_2**: 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 https://www.ioc.ee/~james/ITT9200/SyntaxAndSemanticsof%20DependentTypes.pdf  

---

## 1 answers

### Answer by username_3 on 2015-01-22. Score: 11 | Accepted answer

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.


---

