Timeline for Collection of proper classes with in CZF
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 11, 2021 at 0:13 | history | bounty ended | ToucanIan | ||
| Dec 9, 2021 at 18:22 | comment | added | aws | In the reference I mentioned they work with power set, but the same argument should work in general, just giving a class sized complete Heyting algebra. You can then talk abut the collection of all complete Heyting algebras that arise from small lattices in this way. This would not give you every complete Heyting algebra, necessarily, but it would be a large enough collection of them to have a completeness theorem. | |
| Dec 9, 2021 at 18:12 | comment | added | ToucanIan | That’s exactly what I had in mind! Thank you. So we can talk about all complete Heyting Algebras as a (specified) completion of a lattice? Where in the troelstra reference the specified completion is the collection (proper class) of complete ideals of the lattice. | |
| Dec 9, 2021 at 16:58 | comment | added | aws | Sorry, I confused Dedekind MacNeille completion with a similar construction that preserves any joins already existing in the poset (Theorem 6.13 in Chapter 13 of Troelstra and Van Dalen, Constructivism in mathematics, vol 2). For that one you get a complete Heyting algebra out given a Heyting algebra to start with, but maybe not for Dedekind-MacNeille. | |
| Dec 8, 2021 at 22:58 | comment | added | ToucanIan | Soundness and completeness are very much related to what I am interested in. Why is it enough to specify them as Dedekind MacNeille completions of a poset when this is the construction of a complete lattice, not necessarily a complete Heyting Algebra. | |
| Dec 8, 2021 at 18:20 | comment | added | aws | There are a few references comparing the consistency strength of variations of CZF with classical theories, but I think Rathjen, Griffor, Palmgren, Inaccessibility in constructive set theory and type theory is probably the most standard one regarding CZF inaccessible sets. | |
| Dec 8, 2021 at 18:17 | comment | added | aws | I guess actually the most relevant approach would depend on why you are interested in complete Heyting algebras and what you want to do with them. As an example, you can use complete Heyting algebras to build models of theories in intuitionistic logic, so you can prove, for example, the soundness theorem for intuitionistic logic for all (class sized) complete Heyting algebras specified as the Dedekind MacNeille completion of a poset, which would also have a completeness theorem. | |
| Dec 8, 2021 at 17:29 | comment | added | ToucanIan | In the most relevant approach, do you have in mind for the property $X$ to be “is a heyting algebra”? If not how do you see this as the most relevant approach? Is the last statement about inaccessible sets regarding hierarchies? Do you have a good reference for this? I very much appreciate this! | |
| Dec 8, 2021 at 6:40 | vote | accept | ToucanIan | ||
| Dec 7, 2021 at 16:49 | history | answered | aws | CC BY-SA 4.0 |