06054428

j

06054428 Kreuzer, Alexander P. Primitive recursion and the chain antichain principle. Notre Dame J. Formal Logic 53, No. 2, 245-265 (2012). 2012 University of Notre Dame, Notre Dame, IN; Duke University Press, Durham, NC EN proof mining chain-antichain principle conservation bar recursion Erd\H{o}s-Moser principle tournament CAC WKL

doi:10.1215/00294527-1715716

euclid:ndjfl/1336588253

The author proves that $\mathrm{WKL}^\omega_0+\mathrm{CAC}$ (weak K\"onig'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 [{\it C. T. Chong}, {\it T. A. Slaman} and {\it 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 06059021)]. The paper also discusses the Erd\H{o}s-Moser (tournament) principle. Jeffry L. Hirst (Boone)