Showing the existence of an infinite (strong) antichain Suppose $P$ is a poset such that there exist (strong) antichains of size $n$ for all $n \in {\bf N}$; i.e. there exist sets $S_n$ of size $n$ in $P$ such that no pair of elements of $S_n$ has a common lower bound.
Must $P$ have an infinite antichain?
 A: If there is an infinite set of minimal elements (or rather elements that below them the order is linear), we're done.
So let's work under the assumption there are no minimal elements (or rather, every element has two incompatible smaller elements), as there are only finitely many of them, and they have to be in every maximal antichain.
Now proceed by induction: pick an element $a$, and two incompatible elements smaller than $a$, call them $a_0$ and $b_0$. Now $a'$ has two incompatible elements below it, so we can choose one to be $a_1$ and $b_1$. Proceed by induction splitting $b_n$ to $a_{n+1}$ and $b_{n+1}$. Then $\{a_n\mid n\in\Bbb N\}$ is the antichain you seek.
Choice is necessary, since without choice it is consistent there are counterexamples. For example, if $S$ is a set which is a countable union of pairs that no infinite set of pairs admits a choice function, then the tree of choice functions from finitely many pairs will satisfy this.
A: This is shown to be true for $\mathbb P=\tau\setminus\{\emptyset\}$ in
Lemma 2.10 of [0]. It's likely known
for general $\mathbb P$, but I can't find a citation, so I'll roll
my own proof here. Assume $\mathbb P$ has (strong) antichains of size $n$
for all $n<\omega$. For compatible $p,q\in\mathbb P$,
write $p\not\perp q$ and let $p\wedge q$ satisfy $p\wedge q\leq p,q$.
If $p,q$ are incompatible, write $p\perp q$.
Let $p^\downarrow=\{q\in\mathbb P:q\leq p\}$.
Say $p\in\mathbb P$ is bad if there exists $r_p\leq p$ such that
$r_p^\downarrow$ is pairwise compatible. Let
$\mathbb P_{bad}$ collect all bad points in $\mathbb P$, and say
$p\sim q$ for $p,q\in\mathbb P_{bad}$ if $r_p\not\perp r_q$.
This is obviously symmetric and reflexive, and if we assume
$p\sim q,q\sim t$, then let $s_p=r_p\wedge r_q$ and
$s_r=r_q\wedge r_t$. Since $r_q^\downarrow\in\mathbb P_{bad}$,
$s_p\not\perp s_r$, so $r_p\not\perp r_t$ and thus
$p\sim t$. Thus $\sim$ is an equivalence relation.
If $\mathbb P_{bad}/\sim$ is infinite, we may choose $p_i\in\mathbb P_{bad}$
such that $p_i\not\sim p_j$ for $i<j<\omega$. Thus
$r_{p_i}\perp r_{p_j}$ for $i<j<\omega$, giving us
an infinite antichain $\{r_{p_i}:i<\omega\}$.
Otherwise $|\mathbb P_{bad}/\sim|=n<\omega$, and choose an antichain
$\{p_i:i\leq n\}$ in $\mathbb P$. If $\{p_i:i<n\}\subseteq\mathbb P_{bad}$,
$p_i\perp p_j$ implies $r_{p_i}\perp r_{p_j}$
and $p_i\not\sim p_j$ for all
$i\leq n$. Thus $\mathbb P_{bad}=\bigcup_{i<n}\overset{\sim}{p_i}$,
and $p_n\not\in\mathbb P_{bad}$.
So we've found $b_0\in\mathbb P\setminus\mathbb P_{bad}$.
Given $b_n\in\mathbb P\setminus\mathbb P_{bad}$, we may choose
$a_n,b_{n+1}\leq b_n$ such that $a_n\perp b_{n+1}$.
Thus by construction, $a_n\perp a_{m+1}$ for all
$n\leq m<\omega$. Therefore
$\{a_n:n<\omega\}$ is an antichain.
[0]: W.  W.  Comfort  and  S.  Negrepontis. Chain  Conditions  in  Topology.   Cambridge  Tracts  in Mathematics. Cambridge University Press, 1982.
