A referência ao fato de que (0 = 1) implica false requer um universo no MLTT

10

É um fato bastante conhecido que derivar uma contradição de uma desigualdade (por exemplo, ) na teoria do tipo Martin-Loef requer um universo.(0 0=1 1)→⊥

A prova também é bastante direta - na ausência de universos, podemos apagar as dependências de qualquer tipo dependente para obter um tipo simples como sua forma e provar que implica que podemos provar p → ⊥ para um átomo arbitrário p , o que obviamente não é possível.(0 0=1 1)→⊥p→⊥p

No entanto, não consigo encontrar quem provou isso primeiro! Alguém tem uma referência?

reference-request lo.logic pl.programming-languages type-theory dependent-type Neel Krishnaswami
fonte
Coquand, "Um Novo Paradoxo na Teoria dos Tipos" (94), descreve a semântica com valor de verdade da lógica mínima de ordem superior e parece sugerir que essa interpretação era conhecida antes. Eu me lembro de uma menção de um tal modelo, mesmo para Teoria Tipo de Russell, mas eu não consigo encontrá-lo ...
Cody
Este texto de Martin Hoffman confirma a referência de Jan Smith na resposta e apresenta uma apresentação razoável dessa prova com semântica categórica nos exercícios ioc.ee/~james/ITT9200/SyntaxAndSemanticsof%20DependentTypes.pdf
user833970

Respostas:

10

Eu sei de:

Jan M. Smith, A independência do quarto axioma de Peano da teoria dos tipos de Martin-Löf sem universos, The Journal of Symbolic Logic 53 (3), p. 840-845, 1988.

Ulrik Buchholtz
fonte