Infinite-model property of a serial strict partial order (source code)

= Infinite-model property of a serial strict partial order

A <strict partial order> that is a <serial relation> has no finite nonempty <first-order model>. If the domain had $N$ elements, seriality would produce a chain of $N+1$ successive elements. The <pigeonhole principle> supplies a repeated element, and transitivity along the resulting cycle contradicts irreflexivity. An infinite example is the usual strict order on the <natural numbers>: every element has its successor. The nonempty-domain convention is essential; the displayed universal conditions hold vacuously on an empty domain if such domains are permitted.