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

Abstract

We show that the theory ${\mathsf{WKL}}_0^{\ast }+\mathsf{CAC}$ is polynomially simulated by ${\mathsf{RCA}}_0^{\ast }$ with respect to $\forall {\Pi }_3^0$ 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^{\ast }+{\mathsf{RT}}_2^2$ has non-elementary speedup over ${\mathsf{RCA}}_0^{\ast }$.