A simplification of Girard's paradox
| Autor: | Antonius J. C. Hurkens |
|---|---|
| Rok vydání: | 1995 |
| Předmět: | |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783540590484 TLCA |
| DOI: | 10.1007/bfb0014058 |
| Popis: | In 1972 J.-Y. Girard showed that the Burali-Forti paradox can be formalised in the type system U. In 1991 Th. Coquand formalised another paradox in U−. The corresponding proof terms (that have no normal form) are large. We present a shorter term of type ⊥ in the Pure Type System λU− and analyse its reduction behaviour. The idea is to construct a universe U and two functions such that a certain equality holds. Using this equality, we prove and disprove that a certain object in U is well-founded. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|