First, I would like to say that I asked this question (a more general one actually) on math.stackexchange.com.

Consider the set $\varPhi$ of statements in the language of ZF that are weaker than AC (assuming ZF). If we define $\varphi\preceq\psi$ by $\sf ZF\vdash\varphi\rightarrow\psi$ then $\preceq$ is a preorder on $\varPhi$. This induces a partial order $\leq$ on $\varPhi/\sim$, where $\sim$ is the equivalence relation defined by $\sf ZF\vdash\varphi\leftrightarrow\psi$. The theorems of ZF form a single class in this equivalence relation, and it is the greatest element $\gamma$ under this partial order. The class of statements equivalent to AC under ZF (let's call it $\lambda$) is the least element.

I would like to know if it's possible to prove that there are no finite maximal chains or finite maximal antichains (other then the trivial $\{\lambda\}$ and $\{\gamma\}$). More generally, what are the possible (finite) cardinalities of maximal chains and antichains?

If there are other non-trivial things that can be said about this order, I would appreciate those too.