A non-speedup result for the chain-antichain principle over a weak base theory

We show that the theory WKL^*₀+CAC is polynomially simulated by RCA₀^* with respect to ∀Π⁰₃ 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 CAC. Our result sharply contrasts with the previously known fact that RCA₀^*+RT²₂ has non-elementary speedup over RCA₀^*.