April 18
Katarzyna W. Kowalik,
University of Warsaw
The chain-antichain principle and proof size
The chain-antichain principle $\mathsf{CAC}$ is a well-known consequence of Ramsey's theorem for pairs and two colours $\mathsf{RT}^2_2$. It says that for every partial order on $\mathbb{N}$ there exists an infinite chain or antichain with respect to this order. Both of these principles are $\Pi^0_3$-conservative over the weak base theory $\mathsf{RCA}^*_0$. Such conservation results usually prompt to ask about lengths of proofs. Kołodziejczyk, Wong and Yokoyama proved that $\mathsf{RT}^2_2$ has a non-elementary speedup over $\mathsf{RCA}^*_0$ for proofs of $\Sigma_1$ sentences. We show that the behaviour of $\mathsf{CAC}$ is the opposite: it can be polynomially simulated by $\mathsf{RCA}^*_0$ with respect to $\Pi^0_3$ sentences. Our argument uses a technique of forcing interpretation developed by Avigad. In the first step we syntactically simulate a construction of a generic computable ultrapower of a model of $\mathsf{RCA}^*_0$. Then we find a generic cut satisfying $\mathsf{CAC}$ inside the ultrapower.