La referencia al hecho de que (0 = 1) implica falso requiere un universo en MLTT

10

Es un hecho bastante conocido que derivar una contradicción de una desigualdad (por ejemplo, ) en la teoría de tipo Martin-Loef requiere un universo.(0=1)→⊥

La prueba también es bastante sencilla: en ausencia de universos, podemos borrar las dependencias de cualquier tipo dependiente para obtener un tipo simple como su forma, y ​​así demostrar que implica que podemos probar p → ⊥ para un átomo arbitrario p , que por supuesto no es posible.(0=1)→⊥p→⊥p

Sin embargo, no puedo encontrar quién demostró esto primero. ¿Alguien tiene una referencia?

reference-request lo.logic pl.programming-languages type-theory dependent-type Neel Krishnaswami
fuente
"Una nueva paradoja en la teoría del tipo" de Coquand (94) describe la semántica valorada en la verdad de la lógica mínima de orden superior, y parece sugerir que esta interpretación era conocida antes. Me parece recordar una mención de un modelo de este tipo, incluso para la teoría de tipos de Russell, pero me parece que no puede encontrarlo ...
Cody
Este texto de Martin Hoffman confirma la referencia de Jan Smith en la respuesta, y tiene una presentación razonable de esa prueba con semántica categórica en los ejercicios ioc.ee/~james/ITT9200/SyntaxAndSemanticsof%20DependentTypes.pdf
user833970

Respuestas:

10

Yo se de:

Jan M. Smith, La independencia del cuarto axioma de Peano de la teoría de tipos sin universos de Martin-Löf, The Journal of Symbolic Logic 53 (3), p. 840-845, 1988.

Ulrik Buchholtz
fuente