Strict partial order ($<$)

A strict partial order is an irreflexive transitive relation. In a classical set, it corresponds to a partial order through reflexification, but recovering the strict relation from the weak one requires inequality. In an arbitrary topos, this reverse operation need not be geometric or define an inverse interpretation.

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.

Reflexification turns a strict partial order into a partial order. Reflexivity is immediate, transitivity follows by the four disjunction cases, and antisymmetry follows because two opposed strict comparisons imply a forbidden self-comparison. The construction uses only coherent logic, so is preserved by inverse image functors of geometric morphisms.