Timeline for Where is the proof that Coq + Excluded Middle is consistent
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 18, 2011 at 14:00 | vote | accept | Mark Reitblatt | ||
| Feb 14, 2011 at 17:02 | history | edited | Neel Krishnaswami | CC BY-SA 2.5 |
typo fix
|
| Feb 14, 2011 at 16:59 | comment | added | Neel Krishnaswami | Impredicative Prop makes no difference, since $2$ is a complete lattice, and you can interpret arbitrary intersections and unions with it. It's impredicative Set that complicates everything, since set-theoretic sets don't directly justify impredicative indexing. (C.f. Reynolds' "Polymorphism Is Not Set-Theoretic" springerlink.com/content/yn417gu033x85677 ) | |
| Feb 14, 2011 at 16:31 | comment | added | Mark Reitblatt | Thanks. And for impredicative Prop? | |
| Feb 14, 2011 at 9:56 | history | answered | Neel Krishnaswami | CC BY-SA 2.5 |