Finite-local characterization of two-dimensional partially ordered sets (source code)

= Finite-local characterization of two-dimensional partially ordered sets

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.