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....

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....