Set-theoretic trees, heights, levels, branches and antichains

A tree is a set $T$ with an irreflexive transitive relation ${<}_T$ such that $P_t=\{s\in T:s{<}_{T}t\}$ is strictly well-ordered for each $t\in T$. Use the strict convention in Well-order and well-ordered set and the ordinals of Ordinal (von Neumann). Write $s{\le }_{T}t$ for $s{<}_{T}t$ or $s=t$.

The height ${\mathrm{ht}}_T(t)$ is the ordinal order type of $P_t$. Put $T_{\alpha }=\{t\in T:{\mathrm{ht}}_T(t)=\alpha \}$, $T_{<\alpha }={\bigcup }_{\beta <\alpha }{T}_{\beta }$, and $\mathrm{ht}(T)=\sup \{{\mathrm{ht}}_T(t)+1:t\in T\}$. A root has height zero. The empty tree has height zero.

A chain is a subset whose distinct elements are comparable; a branch is a chain maximal under inclusion. A branch is cofinal when its node heights are unbounded in $\mathrm{ht}(T)$: for every $\alpha <\mathrm{ht}(T)$ it contains a node of height at least $\alpha$. An antichain is a subset whose distinct elements are incomparable. These definitions allow empty chains and antichains; in the empty tree the empty chain is the unique branch and is vacuously cofinal. A singleton tree has one root and one branch.

These are set-theoretic trees, with no assumption that nodes are finite sequences. The order-type theorem Every well-order has a unique order type supplies the unique ordinal used in the height definition: the predecessor relation is a set well-order, hence well-founded and extensional. Indeed distinct elements of a strict linear order have different initial segments.