Odniesienie do faktu, że (0 = 1) oznacza fałsz, wymaga wszechświata w MLTT

Jest to dość dobrze znany fakt, że wywodzenie sprzeczności z nierówności (na przykład ) w teorii typu Martina-Loefa wymaga wszechświata. $(0=1) \to \bot$

Dowód jest również dość prosty - w przypadku braku wszechświatów możemy usunąć zależności od dowolnego typu zależnego, aby uzyskać prosty typ jako jego kształt, a więc udowodnienie, że oznacza, że możemy udowodnić dla dowolnego atomu , co oczywiście nie jest możliwe. $(0=1) \to \bot$ $p \to \bot$ $p$

Nie mogę jednak znaleźć, kto udowodnił to pierwszy! Czy ktoś ma referencje?

— Neel Krishnaswami
źródło

„Nowy paradoks w teorii typów” Coquanda (94) opisuje wartościową semantykę minimalnej logiki wyższego rzędu i sugeruje, że ta interpretacja była znana wcześniej. Wydaje mi się, że pamiętam wzmiankę o takim modelu nawet w przypadku teorii typu Russella, ale nie mogę go znaleźć ...

— cody

Ten tekst Martina Hoffmana potwierdza odniesienie Jana Smitha w odpowiedzi i ma rozsądną prezentację tego dowodu z kategoryczną semantyką w ćwiczeniach ioc.ee/~james/ITT9200/SyntaxAndSemanticsof%20DependentTypes.pdf

— 833970

Wiem o:

Jan M. Smith, Niezależność czwartego aksjomatu Peano od teorii typów Martina-Löfa bez wszechświatów, The Journal of Symbolic Logic 53 (3), s. 1. 840–845, 1988.

— Ulrik Buchholtz
źródło