This chapter surveys the known facts about the

Fundamental problem. Is bounded arithmetic S2 finitely axiomatizable?

As we shall see (Theorem 10.2.4), this question is equivalent to the question whether there is a model of S2 in which the polynomial time hierarchy PH does not collapse.

Finite axiomatizability ofSandT

In this section we summarize the information about the fundamental problem that we have on the grounds of the knowledge obtained in the previous chapters.

Theorem 10.1.1. Each of the theories S and T is finitely axiomatizable for i ≤ 1.

Proof. By Lemma 6.1.4, for i ≤ 1 there is a formula UNIVi(x, y, z) that is a universal formula (provably in). This implies that and, i ≤ 1, are finitely axiomatizable over.

To see that is also finitely axiomatizable, verify that only a finite part of is needed in the proof of Lemma 6.1.4.

The next statement generalizes this theorem.

Theorem 10.1.2. Let 1 ≤ and 2 ≥ j. Then the set of the consequences of

is finitely axiomatizable.

The sets and are also finitely axiomatizable.