Complete anti-chain lattices and the axiom of choice Hello, everyone. I'm trying to find out about lattices of anti-chains, and was wondering whether you could help me with getting to grips with a Comp. Sci. paper I'm struggling with.
I've been reading two related papers on algorithms that operate over a lattice of anti-chains. The authors give a construction for deriving the lattice of anti-chains from an underlying powerset algebra and make claims that the resulting structures are complete. I have a feeling that the authors make the hidden assumption that the powerset algebra is finite for their completeness argument (which makes sense, since the authors are ultimately concerned with finite automata), and was wondering whether someone could help me figure out whether a partial fix requires the axiom of choice. 
My interest in this is with respect to finding completeness conditions for lattices of anti-chains.
I will try to summarise the general construction given in the paper. I hope I'm not misrepresenting.

Let $(\wp(S),\subseteq, \cap,\cup)$ be a powerset algebra with glb (meet) $\cap$ and lub (join) $\cup$. An anti-chain is a subset $C$ of $S$ such that all pairs of distinct elements $c,c' \in C$ are mutually incomparable, i.e., $c \not \subseteq c'$ and $c \not \supseteq c'$. We denote the set of all anti-chains of $\wp(S)$ as ${\mathbb{C}}$.
The set of anti-chains $\mathbb{C}$ is partially ordered by the binary relation $\sqsubseteq \in \wp(\mathbb{C}\times\mathbb{C})$ defined as follows:
  $$C \sqsubseteq C' \text{ exactly if for all }c \in C\text{ there exists a }c' \in C'\text{ such that }c \sqsubseteq c'$$

So far so good. The authors go on to define binary meets and joins, here's my first suspicion that something is missing:

We can define binary meets and joins over the poset $(\mathbb{C},\sqsubseteq)$ as follows, where $\max S$ and $\min S$ denote, respectively, the maximal and minimal elements of a set $S$.
  \begin{align*} 
C \sqcap C' &= \max \{ c \cap c' ~|~ c \in C \land c' \in C'\} & 
C \sqcup C' &= \max \{ c ~|~ c \in C \lor c \in C'\} 
\end{align*}

Hold on there. This obviously works for finite lattices, but I'm not so sure about the meet in the infinite case. What if $C$ and $C'$ are infinitely big antichains, couldn't the set $\{ c \cap c' | c \in C \land c' \in C' \}$ simply lack maximal elements?
Then the authors go on to give operators for the non-binary joins and meets. In this paper one can reasonably assume that the authors simply forgot to mention that what they say only holds in finite lattices, but the other (section 2) explicitly defines meets and joins for arbitrary sets, and I don't see how they work. Here's what they say:

For a set of antichains $Q \subseteq \mathbb{C}$, we can define 
  \begin{align*}
\sqcap Q &= \max \{ \bigcap_{q \in Q} s_q ~|~ s_q \in q \} &
\sqcup Q &= \max \{ s_q ~|~ \exists q \in Q.~s_q \in q \} 
\end{align*}

So again, I think there's the problem that these maximal elements may not exist. Consider the case where the underlying powerset algebra has infinite ascending chains, e.g., consider $\wp(\mathbb{N})$ and the chain:
$$ \{1\} \subseteq \{1,2\} \subseteq \{1,2,3\} \ldots $$
Now we can derive an ascending chain of singleton anti-chains:
$$ \{\{1\}\} \sqsubseteq \{\{1,2\}\} \sqsubseteq \{\{1,2,3\}\} \sqsubseteq \ldots$$ 
But following the join operator for sets given above we get $\emptyset$ as the join of this chain, since there is no maximal element. Am I missing something?
Also, one could attempt to fix this, by requiring that the underlying lattice satifies the ascending chain condition (i.e., that it does not have ascending chains). But then I still find the definition of the meet troubling. I have a bit of trouble parsing what it means, and I can't clearly explain why. I think it is equivalent to the definition below:
$$\sqcap Q = \max \{ \bigcap_{q \in Q} f(q) ~|~ \text{ for choice function $f: Q \to \bigcup_{q \in Q} q$ s.t. $\forall q\in Q. f(q) \in q$}\}$$ 
This does require the axiom of choice doesn't it? Or does it somehow get around that by not actually being interested in the choice function itself, but just in its codomain? 
I'm happy for any suggestions / ideas / insight. Are my issues making sense or am I missing something?
 A: I claim that the lattice described above is a complete lattice if and only if $X$ is finite.
Let $X$ be a countably infinite set. Assume that the set $\{\{R\}|R\subseteq X,|R|<\infty\}$ has a least upper bound $\mathcal{A}$. Put a relation $\simeq$ on $P(X)$ where $R\simeq S$ iff there is a bijection $f:X\rightarrow X$ with $f[R]=S$. Then if $R,S\subseteq X,R\simeq S$, then $R\in\mathcal{A}$ iff $S\in\mathcal{A}$. Therefore $\mathcal{A}$ is the union of a collection of equivalence classes. However, we take note that the equivalence classes are the sets of the forms $\{R\subseteq X:|R|=n\},\{R\subseteq X:|X\setminus R|=n\},\{R\subseteq X:|R|=|X\setminus R|=\infty\}$. However, the set $\mathcal{A}$ cannot contain more than one equivalence class since $\mathcal{A}$ must be an antichain. Therefore $\mathcal{A}$ is precisely one equivalence class. The set $\mathcal{A}$ cannot be any of the equivalence classes of the form $\{R\subseteq X:|R|=n\}$ since the sets $\{R\subseteq X:|R|=n\}$ are not upper bounds of $\{\{R\}|R\subseteq X,|R|<\infty\}$.  Furthermore, $\mathcal{A}\neq\{R\subseteq X:|R|=|X\setminus R|=\infty\}$ since
$\{R\subseteq X:|R|=|X\setminus R|=\infty\}$ is not an antichain. Therefore, $\mathcal{A}=\{R\subseteq X:|X\setminus R|=n\}$ for some $n$. On the other hand, $\{R\subseteq X:|X\setminus R|=n+1\}$ is another antichain and
$\{R\subseteq X:|R|=n\}\leq\{R\subseteq X:|X\setminus R|=n+1\}<\{R\subseteq X:|X\setminus R|=n\}$, This contradicts the fact that $\mathcal{A}=\{R\subseteq X:|X\setminus R|=n\}$ is the least upper bound of $\{\{R\}|R\subseteq X,|R|<\infty\}$. Therefore the collection of antichains in $P(X)$ is not an complete lattice.
What goes wrong? If $X$ is a set, then we say $L\subseteq P(X)$ is a lower set if whenever $R\in L$ and $S\subseteq R$, then $S\in L$ as well. Let $\mathcal{L}(X)$ denote the collection of lower sets in $X$. Then $\mathcal{L}(X)$ is clearly a complete lattice.
For finite sets, the antichains are in a one-to-one correspondence with the lower sets by the following correspondences. If $A$ is an anti-chain, then one simply takes the lower set generated by $A$. If $L$ is a lower set, then the collection of all maximal elements in $L$ is an anti-chain. Therefore since $\mathcal{L}(X)$ is a complete lattice, the collection of all anti-chains also forms a complete lattice.
On the other hand, for infinite sets, there are lower sets with no maximal elements such as the collection of all finite subsets of an infinite set $X$. Therefore this one-to-one correspondence breaks down for infinite sets.
