Reverse mathematics and dimension of posets
Pith reviewed 2026-05-15 08:40 UTC · model grok-4.3
The pith
Over RCA0, the poset dimension bounding principles DBi_n and DBc_n are equivalent to WKL0, while DB_p and its strengthening DB^+_p follow from WKL0 and IΣ^0_2 but not from BΣ^0_2.
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
Core claim
Over RCA0 both DBi_n and DBc_n are equivalent to WKL0. The principle DB_p and its natural strengthening DB^+_p are provable from WKL0 and from IΣ^0_2, while BΣ^0_2 does not suffice to prove DB^+_p; moreover the statement that DB^+_p is computably true is equivalent to IΣ^0_2.
What carries the argument
The bounding principles DBi_n, DBc_n, DB_p and the strengthened DB^+_p, which assert that the dimension of a poset is bounded by a function of the dimensions of subposets formed by deleting chains or single points.
If this is right
- Dimension inequalities obtained by deleting chains or points are provable already in WKL0.
- The computable version of the point-removal bound requires the induction strength of IΣ^0_2.
- BΣ^0_2 is too weak to guarantee that dimension is bounded after point deletion even for computable posets.
- Order dimension joins the class of combinatorial properties whose reverse-mathematical strength is exactly WKL0 or IΣ^0_2.
Where Pith is reading between the lines
- Similar bounding statements for other poset invariants such as width or height may have the same calibration against WKL0 and IΣ^0_2.
- The equivalence between computable truth of DB^+_p and IΣ^0_2 supplies a new combinatorial characterization of this induction axiom.
- One could test whether the same strength hierarchy appears when the underlying order is a computable partial order on the natural numbers rather than an arbitrary countable poset.
Load-bearing premise
The posets under study are countable and the bounding principles are formalized using the classical definition of order dimension inside second-order arithmetic over RCA0.
What would settle it
A model of RCA0 + BΣ^0_2 in which DB^+_p fails for some countable poset, or a computable poset whose dimension cannot be recovered from the dimensions of its proper subposets without assuming IΣ^0_2.
read the original abstract
Order dimension theory measures the complexity of partially ordered sets by quantifying how far they are from being linearly ordered. In this paper we study classical bounding results for order dimension within the framework of reverse mathematics. We focus on principles asserting that the dimension of a poset can be bounded in terms of the dimension of subposets obtained by removing chains or points, denoted by $\mathsf{DBi_n}$, $\mathsf{DBc_n}$, and $\mathsf{DB_p}$. We prove that, over $\mathsf{RCA}_0$, both $\mathsf{DBi_n}$ and $\mathsf{DBc_n}$ are equivalent to $\mathsf{WKL}_0$. To analyze $\mathsf{DB_p}$, we introduce a natural strengthening $\mathsf{DB^+_p}$ and show that both $\mathsf{DB_p}$ and $\mathsf{DB^+_p}$ are provable from $\mathsf{WKL}_0$ and from $\mathsf{I}\Sigma^0_2$, while $\mathsf{B}\Sigma^0_2$ does not suffice to prove $\mathsf{DB^+_p}$. The latter result is obtained by showing that the statement \lq\lq $\mathsf{DB^+_p}$ is computably true\rq\rq\ is equivalent to $\mathsf{I}\Sigma^0_2$.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The manuscript studies the reverse-mathematical strength of bounding principles for the order dimension of posets. Over RCA0 it proves that both DBi_n and DBc_n are equivalent to WKL0. It introduces the strengthening DB^+_p of DB_p and shows that both DB_p and DB^+_p are provable from WKL0 and from IΣ^0_2, while BΣ^0_2 does not suffice for DB^+_p; the latter separation is obtained by proving that the statement 'DB^+_p is computably true' is equivalent to IΣ^0_2.
Significance. If the results hold, they give a precise calibration of the logical strength of dimension-bounding principles, relating them directly to the standard systems WKL0, IΣ^0_2 and BΣ^0_2. The use of computable truth to obtain the separation from BΣ^0_2 is a clean application of standard techniques and strengthens the contribution. The work extends reverse mathematics to order-theoretic notions in a technically careful way.
major comments (2)
- [Theorem 3.2 and surrounding construction] In the proof that DBi_n implies WKL0 (the direction establishing the equivalence in the main theorem on DBi_n/DBc_n), the poset construction used to encode a tree must be verified to have dimension exactly bounded by n; the argument appears to rely on the classical definition of dimension being correctly rendered as a Σ^1_1 statement, but a small gap in the induction step for the height-n case would undermine the equivalence.
- [Section 5, the computability argument] For the claim that BΣ^0_2 does not prove DB^+_p, the model witnessing the separation (via the equivalence to 'DB^+_p is computably true') must explicitly satisfy BΣ^0_2 while failing the bounding principle; confirm that the computable enumeration of posets used in the IΣ^0_2-equivalence argument does not inadvertently satisfy a stronger induction axiom.
minor comments (2)
- [Section 2] The formalization of order dimension inside second-order arithmetic is stated clearly, but a short paragraph early in the paper recalling the exact Σ^1_1 / Π^1_1 complexity of the dimension predicate would help readers.
- Notation for the principles (DBi_n, DBc_n, DB_p, DB^+_p) is consistent, yet a small summary table listing the equivalences and separations would improve readability.
Simulated Author's Rebuttal
We thank the referee for the positive recommendation to accept and for the detailed reading of the manuscript. We address each major comment below.
read point-by-point responses
-
Referee: [Theorem 3.2 and surrounding construction] In the proof that DBi_n implies WKL0 (the direction establishing the equivalence in the main theorem on DBi_n/DBc_n), the poset construction used to encode a tree must be verified to have dimension exactly bounded by n; the argument appears to rely on the classical definition of dimension being correctly rendered as a Σ^1_1 statement, but a small gap in the induction step for the height-n case would undermine the equivalence.
Authors: We appreciate the referee highlighting this part of the proof. The poset P_T constructed from a tree T is defined so that its order dimension is at most n precisely when T is infinite, using the standard characterization of dimension via linear extensions. This is expressed as a Σ^1_1 statement over RCA0. The induction on height proceeds by removing a maximal chain, which lowers the height to at most n-1; the inductive hypothesis then bounds the dimension of the resulting subposet by n-1, yielding the bound n for the original poset. The classical dimension theory carries over directly in this formalization, and we do not identify a gap in the induction. To address the concern and improve readability, we will expand the explanation of the induction step with an additional paragraph in the revised version. revision: partial
-
Referee: [Section 5, the computability argument] For the claim that BΣ^0_2 does not prove DB^+_p, the model witnessing the separation (via the equivalence to 'DB^+_p is computably true') must explicitly satisfy BΣ^0_2 while failing the bounding principle; confirm that the computable enumeration of posets used in the IΣ^0_2-equivalence argument does not inadvertently satisfy a stronger induction axiom.
Authors: The separation is established by proving that the computable truth of DB^+_p is equivalent to IΣ^0_2 over RCA0. The witnessing model is the standard computable model in which BΣ^0_2 holds but IΣ^0_2 fails; within this model we exhibit a computable sequence of posets whose dimension bounds require the full strength of IΣ^0_2. The enumeration of these posets is carried out by a computable function that does not invoke any induction beyond BΣ^0_2. We will insert an explicit paragraph in Section 5 confirming that the model satisfies BΣ^0_2 and that the enumeration remains within the resources of BΣ^0_2. revision: yes
Circularity Check
No significant circularity; derivations are self-contained equivalences to standard subsystems
full rationale
The paper proves equivalences and separations (DBi_n ≡ WKL0, DBc_n ≡ WKL0, DB_p and DB^+_p provable from WKL0 and IΣ^0_2 but not from BΣ^0_2, and 'DB^+_p computably true' ≡ IΣ^0_2) over RCA0 by rendering the classical order-dimension definition as Σ^1_1/Π^1_1 statements on countable posets. These are standard reverse-mathematics techniques with no self-definitional reductions, no fitted parameters renamed as predictions, and no load-bearing self-citations; the bounding principles are independently formalized from the classical notion, so the derivation chain does not reduce to its own inputs by construction.
Axiom & Free-Parameter Ledger
axioms (2)
- standard math RCA0 (recursive comprehension axiom)
- domain assumption Standard definition of order dimension via linear extensions
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.