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

We show that the theory ${\mathsf{W}\mathsf{K}\mathsf{L}}_0^{\ast }+\mathsf{C}\mathsf{A}\mathsf{C}$ is polynomially simulated by ${\mathsf{R}\mathsf{C}\mathsf{A}}_0^{\ast }$ with respect to $\mathrm{\forall }{\mathrm{\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{C}\mathsf{A}\mathsf{C}$. Our result sharply contrasts with the previously known fact that ${\mathsf{R}\mathsf{C}\mathsf{A}}_0^{\ast }+{\mathsf{R}\mathsf{T}}_2^2$ has non-elementary speedup over ${\mathsf{R}\mathsf{C}\mathsf{A}}_0^{\ast }$.