2
$\begingroup$

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?

Improve this question
$\endgroup$
5
  • 4
    $\begingroup$ This is just a side comment: you do know thaat no complete lattice which is a set can be exhibited in CZF? See the Main Lemma in these slides by Giovanni Curi. $\endgroup$
    – Andrej Bauer
    Commented Nov 26, 2021 at 23:46
  • $\begingroup$ I’m not sure I understand the proof. What does it mean for L to be degenerate and why does L being degenerate imply that L isn’t a set in CZF* + GUP? $\endgroup$
    – ToucanIan
    Commented Nov 27, 2021 at 21:14
  • 1
    $\begingroup$ @ToucanIan A singleton is always a complete lattice, and a complete lattice is called trivial iff it is a singleton, i.e. its top and bottom elements are the same ($0=1$). Curi's argument works by showing from GUP that if a complete lattice $L$ is a set, there exists an element $a$ such that $a = \bigvee \emptyset$ and $a = \bigvee L$, so $0 = a = 1$. Therefore every complete lattice that is a set is a singleton, under GUP. $\endgroup$
    – Robert Furber
    Commented Nov 28, 2021 at 12:55
  • 2
    $\begingroup$ I don’t know why “not necessarily” was removed: it was correct. CZF does not prove that no non-degenerate complete lattice is a set; it is only consistent with CZF that this holds. But on the other hand, classical ZF is also consistent with CZF, and then a plethora of complete lattices that are sets exists. I corrected it using another formulation if you don’t like “not necessarily” for some reason. $\endgroup$
    – Emil Jeřábek
    Commented Nov 30, 2021 at 9:45
  • $\begingroup$ Thank you for the correction. $\endgroup$
    – ToucanIan
    Commented Dec 1, 2021 at 2:57

1 Answer 1

Reset to default
4
+50
$\begingroup$

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.

Improve this answer
$\endgroup$
7
  • $\begingroup$ 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! $\endgroup$
    – ToucanIan
    Commented Dec 8, 2021 at 17:29
  • 1
    $\begingroup$ 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. $\endgroup$
    – aws
    Commented Dec 8, 2021 at 18:17
  • 1
    $\begingroup$ 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. $\endgroup$
    – aws
    Commented Dec 8, 2021 at 18:20
  • 1
    $\begingroup$ 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. $\endgroup$
    – aws
    Commented Dec 9, 2021 at 16:58
  • 1
    $\begingroup$ 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. $\endgroup$
    – aws
    Commented Dec 9, 2021 at 18:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .