The order dimension of a partially ordered set is the least cardinality of a family of total orders on whose intersection is . Such a family is called a realizer of the partial order.
A partially ordered set is two-dimensional when there are two total orders and on its ground set such that
A partially ordered set is two-dimensional if every one of its finite induced suborders is two-dimensional. Encode two candidate total orders by propositional variables; every finite collection of the order, extension, and intersection clauses concerns a finite induced suborder, so the propositional compactness theorem supplies two global realizing orders.
