Finite specializing conditions

Let $T$ be an Aronszajn tree as in Aronszajn, Suslin and special trees. A finite specializing condition is a function $p$ whose domain is a finite subset of $T$, whose values lie in $\omega$, and such that

$x{<}_{T}y\text{ and }x,y\in \mathrm{dom}(p)⟹p(x)\mathrm{\ne }p(y)\mathrm{.}$

Let $P(T)$ be the set of these functions, ordered by $q\le p$ iff $q\supseteq p$ as graphs. Reflexivity and transitivity follow from graph inclusion; mutual inclusion gives equality, so this is a partial order. Its greatest condition is the empty function. The displayed inequality concerns distinct comparable nodes; it imposes no condition on $p(x)$ compared with itself. In particular every singleton assignment is a condition.

Two conditions $p,q$ are compatible in the sense of Compatibility, ccc and Knaster for posets iff their union is a function and is a specializing condition. Indeed a common lower bound extends both graphs, so they agree on their overlap and all pairs in their union inherit its unequal-label requirement. Conversely, if $p\cup q$ is a condition then it extends both and is a common lower bound. Equivalently, they must agree on their common domain and assign different labels to any distinct comparable pair in the combined domain. Agreement on overlap alone does not verify the second requirement. The union of two finite domains is finite; the union with the empty condition is the original condition.