A non-speedup result for the chain-antichain principle over a weak base theory
Katarzyna W. Kowalik
TL;DR
The paper addresses the question of proof-size conservation for Ramsey-type principles in weak base theories by proving a polynomially tight relation between CAC and WKL-type systems. The core method is a two-step forcing interpretation: first, a restricted Δ^0_1 ultrapower-like construction via a forcing interpretation τ1 inside a weak theory, and second, a generic cut construction via τ2 that enforces CAC. By composing these interpretations and proving a polynomial Γ-reflection, the author establishes that $\mathsf{WKL}_0^*+\mathsf{CAC}$ is polynomially simulated by $\mathsf{RCA}_0^*$ with respect to $\forall\Pi^0_3$ sentences, in contrast to known non-elementary speedups for other Ramsey principles. The result sharpens our understanding of proof-size behavior in weak arithmetical frameworks and demonstrates a robust syntactic route to conservation theorems via forcing interpretations. It also situates CAC among a distinct class where polynomial simulation holds, highlighting nuanced differences with results for $\mathsf{RT}^2_2$ and related principles.
Abstract
We show that the theory $\mathsf{WKL}^*_0+\mathsf{CAC}$ is polynomially simulated by $\mathsf{RCA}_0^*$ with respect to $\forallΠ^0_3$ formulas. For the proof, we use the method of forcing interpretations and syntactically simulate a two-step model-theoretic argument, which involves construction of a restricted definable ultrapower, followed by a generic cut satisfying $\mathsf{CAC}$. Our result sharply contrasts with the previously known fact that $\mathsf{RCA}_0^*+\mathsf{RT}^2_2$ has non-elementary speedup over $\mathsf{RCA}_0^*$.