Christopher - I don't know exactly what rules you're trying to follow, and I'm not an expert on constructive mathematics, but constructive mathematicians do have some way of dealing with infinite joins: after all, \$$\exists\$$ is the classic example of a join.

For example, suppose \$$f \colon S \to \textbf{Bool} \$$ is a function from a possibly infinite set to to the poset \$$\textbf{Bool} = \lbrace \texttt{true},\texttt{false}\rbrace \$$. Then the join

$\bigvee_{x \in S} f(x)$

is another way of talking about the proposition

$\exists x \in S \; f(x) .$

Now, we can't compute this in general when \$$S\$$ is infinite, since in general we can't go through infinitely many elements \$$x \in S\$$ and evaluate \$$f(x)\$$ for all of these. But if we can exhibit an element \$$x \in S\$$ with \$$f(x) = \texttt{true}\$$ then we know

$\bigvee_{x \in S} f(x) = \texttt{true}$

And sometimes we can prove that no such element exists, and then we know

$\bigvee_{x \in S} f(x) = \texttt{false} .$

More generally, for any poset \$$X\$$ and function \$$f : S \to X\$$, we know \$$f(x)\$$ is a lower bound on \$$\bigvee_{x \in S} f(x) \$$.

I don't know if this helps....