In Aczel's Constructive Set Theory (CZF), no non-degenerate complete lattice can be proved to be a set. There are hallmark examples of complete lattices that are proper classes in CZF, including the Dedekind–MacNeille completion of a lattice/poset.


Is there a way to talk about the collection of Complete Lattices in CZF without introducing a hierarchy? This may seem like a splitting of hairs but I’m concerned about making statements about “all complete heyting algebras”. Is this concern unfounded or is there a way to avoid any potential issues with such statements?



Collection of proper classes with in CZF
Unfortunately the only answer I can give is that there is not a good way to do this in general, and since no one else has answered yet, that is probably the only real answer.


Having said that, there are a few techniques that work in some special situations, and can still be useful.


The most relevant one here is that you can still talk about all lattices that arise as Dedekind-MacNeille completions of set sized posets by proving statements of the form "for every poset, the Dedekind-MacNeille completion has X property." If I recall correctly you can get a more general version of this by talking about lattices arising from set presented formal topologies.


It is also sometimes possible to give a proof in the meta theory along the lines "if $\mathbf{CZF}$ proves a certain binary relation is the ordering of a (class sized) lattice, then it also proves the lattice has X property."


Finally, adding (suitably formulated) inaccessible sets to $\mathbf{CZF}$ is not so bad. It is still constructive in some sense, and the consistency strength is still a long way below many commonly studied theories with classical logic.


