Order dimension measures how far a partially ordered set is from being a linear order — the minimum number of linear extensions whose intersection gives the original partial order. Classical results bound a poset's dimension in terms of dimensions of subposets obtained by removing chains or points. But what axiom strength do these bounding principles require?
This paper answers the question in reverse mathematics. The principles DBi_n and DBc_n — bounding dimension after removing chains — are equivalent to WKL_0, the weak König's lemma. For DB_p — bounding dimension after removing individual points — the situation is more subtle. A strengthened version DB⁺_p requires WKL_0 plus IΣ⁰_2 (induction for existential formulas), while the base system BΣ⁰_2 is provably insufficient. The statement that DB⁺_p is computably true is itself equivalent to IΣ⁰_2.
The results calibrate exact proof-theoretic strength: chain removal requires compactness (WKL_0), while point removal additionally requires a form of induction. Removing a single point from a poset is structurally simpler than removing a chain, but reasoning about the dimensional consequences is axiomatically harder. The combinatorial simplicity of the operation inversely correlates with the logical complexity of the bound.