The Dimension Axiom

The dimension of a partially ordered set measures how far it deviates from being a total order — how many linear extensions are needed to reconstruct the partial order from their intersection. Removing an element or a chain from a poset can change its dimension, and classical theorems bound how much.

Marcone and Volpi calibrate these bounding principles against foundational axiom systems in reverse mathematics.

The results are precise. The principle that removing an element decreases dimension by at most one, and that removing a chain decreases it by at most one — both are equivalent to WKL₀, the weak König’s lemma, over the base system RCA₀. This is a second-order arithmetic system strictly between computable mathematics and full arithmetic. The dimension-bounding principles are not computably true, but they don’t require the full strength of mathematical induction either. They sit exactly at the König’s lemma level.

A strengthened principle — that dimension decreases by at most one even under a more general operation — requires IΣ⁰₂ (induction for Σ⁰₂ formulas) but not the weaker BΣ⁰₂ (bounding for the same class). The strengthening shifts the calibration from a compactness principle (WKL₀) to an induction principle (IΣ⁰₂), revealing that the combinatorial content of the stronger theorem is genuinely different in kind, not just degree.

Reverse mathematics asks: which axioms are necessary and sufficient for which theorems? For poset dimension, the answer places these concrete combinatorial facts at specific, well-understood positions in the logical hierarchy. The mathematics of partial orders is as strong as the logic of trees — no more, no less.