Primitive recursion and the chain antichain principle (Q435242)

The author proves that \(\mathrm{WKL}^\omega_0+\mathrm{CAC}\) (weak König's lemma extended to finite types plus the chain-antichain principle) is \(\Pi^0_2\)-conservative over primitive recursive arithmetic using a variant of Howard's ordinal analysis of bar recursion. An immediate corollary is that CAC does not imply induction for \(\Sigma^0_2\) formulas. An earlier, forcing-based proof of the corollary can be found in [\textit{C. T. Chong}, \textit{T. A. Slaman} and \textit{Y. Yang}, ``\(\Pi^1_1\)-conservation of combinatorial principles weaker than Ramsey's theorem for pairs'', Adv. Math. 230, No. 3, 1060--1077 (2012; Zbl 1255.03025)]. The paper also discusses the Erdős-Moser (tournament) principle.