Primitive Recursion and the Chain Antichain Principle

Notre Dame Journal of Formal Logic 53 (2):245-265 (2012)
  Copy   BIBTEX


Let the chain antichain principle (CAC) be the statement that each partial order on $\mathbb{N}$ possesses an infinite chain or an infinite antichain. Chong, Slaman, and Yang recently proved using forcing over nonstandard models of arithmetic that CAC is $\Pi^1_1$-conservative over $\text{RCA}_0+\Pi^0_1\text{-CP}$ and so in particular that CAC does not imply $\Sigma^0_2$-induction. We provide here a different purely syntactical and constructive proof of the statement that CAC (even together with WKL) does not imply $\Sigma^0_2$-induction. In detail we show using a refinement of Howard's ordinal analysis of bar recursion that $\text{WKL}_0^\omega+\text{CAC}$ is $\Pi^0_2$-conservative over PRA and that one can extract primitive recursive realizers for such statements. Moreover, our proof is finitary in the sense of Hilbert's program. CAC implies that every sequence of $\mathbb{R}$ has a monotone subsequence. This Bolzano-Weierstraß}-like principle is commonly used in proofs. Our result makes it possible to extract primitive recursive terms from such proofs. We also discuss the Erdős-Moser principle, which—taken together with CAC—is equivalent to $\text{RT}^2_2$



    Upload a copy of this work     Papers currently archived: 76,264

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Infinite chains and antichains in computable partial orderings.E. Herrmann - 2001 - Journal of Symbolic Logic 66 (2):923-934.
Charity Implies Meta-Charity.Roy Sorensen - 2004 - Philosophy and Phenomenological Research 68 (2):290 - 315.
Monotone majorizable functionals.Helmut Schwichtenberg - 1999 - Studia Logica 62 (2):283-289.
Formulating the Precautionary Principle.Neil A. Manson - 2002 - Environmental Ethics 24 (3):263-274.
Łukasiewicz on the Principle of Contradiction.Venanzio Raspa - 1999 - Journal of Philosophical Research 24:57-112.
Explicit mathematics with the monotone fixed point principle.Michael Rathjen - 1998 - Journal of Symbolic Logic 63 (2):509-542.
Finitude and Hume's Principle.Richard G. Heck Jr - 1997 - Journal of Philosophical Logic 26 (6):589 - 617.


Added to PP

28 (#418,627)

6 months
2 (#298,443)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Degrees bounding principles and universal instances in reverse mathematics.Ludovic Patey - 2015 - Annals of Pure and Applied Logic 166 (11):1165-1185.
Program extraction for 2-random reals.Alexander P. Kreuzer - 2013 - Archive for Mathematical Logic 52 (5-6):659-666.

View all 7 citations / Add more citations