Return to Question

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 concerned unfounded or is there a way to avoid any potential issues with such statements?

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?

In Aczel's Constructive Set Theory (CZF) a non-degenerate complete lattice is not 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 concerned unfounded or is there a way to avoid any potential issues with such statements?

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 concerned unfounded or is there a way to avoid any potential issues with such statements?

In Aczel's Constructive Set Theory (CZF) a non-degenerate complete lattice is not 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?

In Aczel's Constructive Set Theory (CZF) a non-degenerate complete lattice is not 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 concerned unfounded or is there a way to avoid any potential issues with such statements?