Models of Bounded Arithmetic and variants of Pigeonhole Principle

TL;DR

This paper proves the bijective pigeonhole principle formulated for a binary relation symbol $R$ is formulated for all polynomial-time decidable relations with oracle access to $R by means of forcing.

Abstract

We give elementary proof that theory $T^1_2(R)$ augmented by the weak pigeonhole principle for all $Δ^b_1(R)$-definable relations does not prove the bijective pigeonhole principle for $R$. This can be derived from known more general results but our proof yields a model of $T^1_2(R)$ in which $ontoPHP^{n+1}_n(R)$ fails for some nonstandard element $n$ while $PHP^{m+1}_m$ holds for all $Δ^b_1(R)$-definable relations and all $m \leq n^{1-ε}$, where $ε> 0$ is a fixed standard rational parameter. This can be seen as a step towards solving an open question posed by M. Ajtai.

Theorems & Definitions (48)

• Definition 2.1
• Definition 3.1
• Definition 3.2
• Proposition 3.3
• Proposition 3.4
• proof
• Definition 3.5
• Corollary 3.6
• Theorem 3.7
• Definition 3.8