Timeline for Impredicativity
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 29, 2010 at 9:42 | comment | added | Neel Krishnaswami | Even internally to type theory, impredicative formation rules for inductive types are (imo) clearer and more flexible than syntactic positivity conditions. Eg, replace syntactic positivity with a condition that you can take the fixed point of a type operator $F$ when $\Pi \alpha,beta.\; (\alpha \to \beta) \to F(\alpha) \to F(\beta)$ is derivable. (Externally, this condition amounts to saying $F$ is monotone on the provability lattice of types, but requires impredicative quantification to internalize.) | |
| May 28, 2010 at 22:10 | comment | added | Andrej Bauer | Because sometimes (often?) impredicative constructions are slicker than the predicative ones. | |
| May 28, 2010 at 19:54 | history | answered | Christoph-Simon Senjak | CC BY-SA 2.5 |