Timeline for Impredicativity
Current License: CC BY-SA 2.5
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 9, 2022 at 22:58 | comment | added | ToucanIan | Great answer. I find your addendum really interesting. Especially in relation to the comment right before about Supremum. In many cases the construction of a supremum is fine predicativly but some still argue that the definition of the supremum is impredicative because it quantifies over the set of upper bounds. Can you say something about this? | |
| May 29, 2010 at 18:49 | comment | added | Andrej Bauer | You don't have to use "all ordinals", that's more or less a manner of speaking: typically we know in advance that the iteration will stabilize, say at an ordinal whose cardinality exceeds the cardinality of everything in sight. But since it is just as easy to write down the definition of iteration for all ordinals as for ordinals up to some bound, people usually opt for the unbounded way. Mind you, I did not use "all ordinals, just enough of them to be blue in the face... | |
| May 29, 2010 at 8:26 | vote | accept | dumb student | ||
| May 29, 2010 at 8:26 | comment | added | dumb student | Thanks, I guess it's best to give attention to both impredicative and predicative concepts/proofs, as the former is usually very "slick" as you said below and the latter gives further insight. Another side question: for the predicative proof of Knaster-Tarski theorem, why do you use all ordinals? Zorn's lemma (from axiom of choice) also uses all ordinals, but we can just use a well ordered set with cardinality greater than the partially ordered set in question. | |
| May 28, 2010 at 13:41 | comment | added | Carl Mummert | I have seen people write that completeness of the real line is impredicative because the definition of "least upper bound" can be written in a way that quantifies over all upper bounds. This does not stand up to scrutiny, of course, because one can construct least upper bounds in predicative systems such as ACA. But maybe it explains that part of the original question above. | |
| May 28, 2010 at 9:20 | history | edited | Andrej Bauer | CC BY-SA 2.5 |
added 325 characters in body
|
| May 28, 2010 at 8:52 | history | edited | Andrej Bauer | CC BY-SA 2.5 |
spelling
|
| May 28, 2010 at 6:22 | history | answered | Andrej Bauer | CC BY-SA 2.5 |