Timeline for Subset Collection axiom
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 10, 2021 at 23:58 | vote | accept | ToucanIan | ||
| Oct 10, 2021 at 22:43 | comment | added | aws | Do you mean Dedekind-McNeille completion? That would not provably be a set in CZF. The most common approach I've seen is to allow lattices to be proper classes to include this case, but then require the lattice to have a set of generators, or some variation of this so you still have some control over it. As it happens, this is mentioned in the paper by Gambino I linked to (section 2). | |
| Oct 10, 2021 at 22:39 | history | edited | aws | CC BY-SA 4.0 |
correct url
|
| Oct 10, 2021 at 22:24 | comment | added | ToucanIan | Thanks for the reply. I am specifically interested in the completion of a lattice in a constructive set theory. To preform the completeness one must take certain subsets of the lattice (complete ideals) and show that they form a complete lattice. In IZF (Intuitionistic Set Theory) the power set axiom allows for us to consider these subsets but I'm unsure if this is possible CZF (Constructive Set Theory) which instead uses Subset Collection. | |
| Oct 10, 2021 at 19:37 | history | answered | aws | CC BY-SA 4.0 |