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][1] [related][2] 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][1] one can reasonably assume that the authors simply forgot to mention that what they say only holds in finite lattices, but [the other][2] (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?

[1]: http://www.ulb.ac.be/di/ssd/ldoyen/papers/antichains-universality-cav06.pdf
[2]: http://research.microsoft.com/en-us/um/people/leino/ifip-wg2.3/media/45/raskin-paper.pdf