Given a Heyting Algebra $H$ we define a complete ideal (or c-ideal) $I$ to be a subset of $H$ satisfying.

  1. $\bot \in I$
  2. $b \in I$ and $a \leq b$ implies $a \in I$
  3. $X \subseteq I$ and $\bigvee X$ exists in $H$ implies $\bigvee X \in I$.

Note $H$ is not necessarily complete so arbitrary joins do not neccesarily exist in $H$. A complete ideal generalizes the notion of an ideal from binary joins to arbitrary joins if they exist.

We can use c-ideals to complete the Heyting Algebra $H$. Let $H'$ be the set of c-ideals of $H$. Let $I_{\alpha}$ be a family of c-ideals where $\alpha \in \mathcal{J}$ some index set.

We define the meet in $H'$ to be the intersections of $I_{\alpha}$ that is $\underset{\alpha \in \mathcal{J}}{\bigwedge} I_{\alpha} = \underset{\alpha \in \mathcal{J}}{\bigcap} I_{\alpha}$. It is easy enough to show that the intersection of c-ideals is a c-ideal and it is in fact the meet. Unfortunately, the union of c-ideals is not, in general, a c-ideal. So for the join things are a bit more complicated. We define the join below

$$ \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha} = \{ \bigvee X \ | \ X \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \ \text{and} \ \bigvee X \ \text{exists in H} \}. $$

I am struggling to show that this object is even a c-ideal, in particular on showing 2. and 3. hold.


  1. $\emptyset \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$ and $\bigvee \emptyset = \bot$ exists in $H$ so $\bot \in \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$
  2. Let $b \in \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$ and $a \leq b$. There exists $X \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$ such that $\bigvee X = b$. We need to show that there exists $Y \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$ such that $\bigvee Y = a$. Some candidates for $Y$ are $\downarrow a$, $X \cap \downarrow a$ and $\underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \cap \downarrow a$. The upside of $\downarrow a$ is that $\bigvee \downarrow a = a$ but there is no way to show $\downarrow a \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$. The upside of the latter two is that they obviously satisfy the subset requirement but there is no obvious way to show that there join is $a$.
  3. Let $Y \subseteq \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$ and $\bigvee Y$ exist in $H$. To show $\bigvee Y \in \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$ it suffices to show $Y \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$. Let $x \in Y$ then by assumption $x \in \underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha}$. Thus for some $X \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$ we have $x = \bigvee X$. Again I am stuck because we cannot say $x \in X$ and conclude $x \in \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha}$.

Reference: [1] A.S. Troelstra, D. Van Dalen. Constructivism in Mathematics An Introduction vol. 2.


2 Answers 2


Here is some insight for you.

Consider a partially ordered set $S$ which has all meets. We will prove that $S$ has all joins.

Let us consider some indexed collection $\{s_i \in S\}_{i \in I}$. Let $J = \{x \in S \mid \forall i \in I (s_i \leq x)\}$. I claim that $\bigwedge J$ is the join of $s$.

Indeed, we first note that for all $i$, for all $x \in J$, $s_i \leq x$ (by the very definition of $J$). Therefore, $s_i \leq \bigwedge J$.

Now suppose that for all $i \in I$, $s_i \leq x$. Then $x \in J$, so $\bigwedge J \leq x$. This completes the proof. $\square$

Your definition also works. Let's work through it.

First, we must show that $Q := \{ \bigvee X \mid X \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$ and $\bigvee X$ exists$\}$ is in fact a $c$-ideal.

As you have shown, (1) is trivial.

For (2), suppose that $X \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$ and $\bigvee X$ exists, and that $a \leq \bigvee X$. Then $a = a \land \bigvee X = \bigvee \{a \land x \mid x \in X\}$ (using the fact that $a \land$ is the left adjoint to $a \implies$ and therefore preserves any colimits that do exist). Since each $I_\alpha$ is downward closed, if $x \in I_\alpha$ then $a \land x \in I_\alpha$. And thus, we see that $\{a \land x \mid x \in X\} \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$. Thus, $a \in Q$.

For (3), we need to get a big cleverer if we wish to avoid choice. Given $a \in Q$, let $f(a) = \{w \in \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha \mid w \leq a\}$; then clearly, $a = \bigvee f(a)$.

Now suppose we have some family $\{x_k \in Q\}_{k \in K}$, and that $\bigvee\limits_{k \in K} x_k$ exists. Then in particular, we have $\bigvee\limits_{k \in K} x_k = \bigvee\limits_{k \in K} \bigvee f(x_k) = \bigvee \bigcup \limits_{k \in K} f(x_k)$. Note that $f(x_k) \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$ by definition, so $\bigcup \limits_{k \in K} f(x_k) \subseteq \bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha$. Therefore, $\bigvee\limits_{k \in K} x_k = \bigvee \bigcup \limits_{k \in K} f(x_k) \in Q$.

Now, let's go about proving that $Q$ is in fact the join of the $I_\alpha$.

Clearly, we see that if $x \in I_\alpha$, then $x = \bigvee \{x\} \in Q$. So $I_\alpha \subseteq Q$ for all $\alpha$.

Now suppose that we had some $y$ such that for all $\alpha$, $I_\alpha \subseteq y$. Then condition 3 ensures that $Q \subseteq y$.

  • $\begingroup$ Are you familiar with the troelstra reference? Is there any reason why he didn’t just use this well known property that you outlined in the first part of your answer? $\endgroup$
    – ToucanIan
    Commented Dec 27, 2021 at 22:50
  • 1
    $\begingroup$ @ToucanIan I haven't read it. I suspect that the explicit form of the join will be important when showing that the result is a Heyting Algebra (since it suffices to show that $a \land \bigvee\limits_{i \in I} x_i = \bigvee\limits_{i \in I} a \land x_i$ to show that $a \land$ is a left adjoint). $\endgroup$ Commented Dec 27, 2021 at 22:52
  • $\begingroup$ This was my suspicion. Thanks! $\endgroup$
    – ToucanIan
    Commented Dec 27, 2021 at 23:37
  • $\begingroup$ Can you say more about your argument in 2. involving left adjointness of $\land$. Is there a more elementary route to this? $\endgroup$
    – ToucanIan
    Commented Dec 27, 2021 at 23:51
  • 1
    $\begingroup$ @ToucanIan We have $a \land \bigvee X \leq y$ iff $\bigvee X \leq a \Rightarrow y$ iff $\forall x \in X (x \leq a \Rightarrow y)$ iff $\forall x \in X (a \land x \leq y)$ for any $y$, thus proving that $a \land \bigvee X$ is $\bigvee \{a \land x \mid x \in X\}$. Note that we use the $\land-\Rightarrow$ adjunction. $\endgroup$ Commented Dec 27, 2021 at 23:58

I found an alternative way to define the join. I would still like insight on the original question and/or a relationship to what follows.

Let $A = \{ K \in H' \ | \ \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \subseteq K \}$ that is $A$ is the set of complete ideals containing the union. Now clearly, $A$ is inhabited since $\underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \subseteq H \in H'$. Trivially we have the $\bigcap A$ is a complete ideal as it is an intersection of complete ideals. We wish to show that $\underset{\alpha \in \mathcal{J}}{\bigvee} I_{\alpha} = \bigcap A$. First note that for every $\beta \in \mathcal{J}$ we have $I_{\beta} \subseteq \underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \subseteq \bigcap A$ (where the last inclusion comes from the fact that $\underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \subseteq K$ for all $K \in A$.) So clearly, $\bigcap A$ is an upperbound. Suppose you have another upperbound $M$ in $H'$. That is for all $\beta \in \mathcal{J}$ we have $I_{\beta} \subseteq M$. Then $\underset{\alpha \in \mathcal{J}}{\bigcup} I_{\alpha} \subseteq M$ and thus $M \in A$. So we can conclude that $\bigcap A \subseteq M$.

  • 1
    $\begingroup$ Your alternate proof is essentially the same idea as the proof in my answer that any partial order with all meets has all joins (except that you have to replace $\bigcup\limits_{\alpha \in \mathcal{J}} I_\alpha \subseteq K$ with $\forall \alpha \in \mathcal{J} (I_\alpha \leq K)$, since you don't have an external notion of joins to rely on). $\endgroup$ Commented Dec 27, 2021 at 22:40
  • $\begingroup$ I’m confused by your comment. I’m on saying $K$ contains the union of the family of ideals. I’m not mentioning any joins. $\endgroup$
    – ToucanIan
    Commented Dec 27, 2021 at 23:36
  • $\begingroup$ The union is the "external notion of join". You're trying to take a subset of the complete Heyting algebra $P(H)$ and prove it's a complete Heyting algebra, and you're relying on the join in the larger algebra $P(H)$ - that is, the union. $\endgroup$ Commented Dec 28, 2021 at 0:02
  • $\begingroup$ Doesn’t then $Q$ in your original answer rely on that same external join? $\endgroup$
    – ToucanIan
    Commented Dec 28, 2021 at 0:04
  • $\begingroup$ Yes, it does. But I was referring to the first proof I gave at the top of the answer that any poset with all meets has all joins, which does not use $Q$ at all and ends with a $\square$. $\endgroup$ Commented Dec 28, 2021 at 0:05

You must log in to answer this question.

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