Models of Bounded Arithmetic

We study mutual relations of various version of the pigeonhole principle over bounded arithmetic theory T^1_2(R). The main two variants are the ordinary PHP_n(R), formalizing that R is not the graph of an injective function from [n+1] into [n], and the weak PHP, WPHP_m(S) formalizing that S is not the graph of an injective function from [2m] into [m].

It is known that:

• T^2_2(R) proves WPHP_m(R) (with m universally quatified) and, in fact, also WPHP_m(S) for all relations S that are \box__1^p(R)):= p-time definable from R (Paris-Wilkie-Woods 19xy)
• neither I\exits_1(R) nor T^1_2(R) prove WPHP_m(R), (Paris-Wilkie 1985 and Krajicek 1992)
• full T_2(R) does not prove PHP_n(R), (Ajtai 19xy, Krajicek-Pudlak-Woods 19xy, Pitassi-Beame-Impagliazzo 19xy)

We generalize the method of Paris-Wilkie 1985 to show that theory T^1_2(R) + \forall m WPHP_m(\box__1^p(R)) does not prove PHP_n(R). This does follow from results mentioned above but such a combined proof involves complex probabilistic combinatorics which is difficult to modify for other principles. On the other hand our method is more elementary and thus better amenable to other principles. We demonstrate this by proving a partial result towards an open problem mentioned by Ajtai 1990.

Introduction

1 Preliminaries
  1.1 Languages and theories
  1.2 Pigeonhole principles
2 Forcing
  2.1 Theorem of Paris and Wilkie
  2.2 Forcing set-up
  2.3 WPHP for open formulas
3 WPHP for polynomial-time machines
  3.1 Case for T1_2 (R)
  3.2 Polynomial-time machines

Conclusion

Bibliography