Independence of B\(\Sigma_2\) from I\(\Sigma_1\)

One thing is to prove a certain statement \( A \), another thing completely different is to prove that \( A \) is not provable! How should one go about proving something like this? By the soundness theorem (if \( A \) is provable in a theory T then \( A \) is valid in all model of T), it suffices to produce a model where \( A \) is not valid. And that's what people will normally do.

But can one answer such questions using proof-theoretic methods? In theory one can. You assume a proof of \( A \) exists. Apply a proof translation or proof interpretation to the imaginary proof. The soundness of the translation or interpretation guarantees the existence of some information or result, which, if one can show not to exist, contradicts the fact that a proof of \( A \) existed in the first place.

And that's precisely what Charles Parsons did in [1], in order to show that \( \Sigma_2 \)-Bounded Collection is not provable from \( \Sigma_1 \)-Induction. Parsons' proof uses Herbrand theorem and the recursion theorem from the previous post. Unfortunately, the proof is not only quite complicated, but I think it contains a bug (don't quote me on that though).

As a fan of proof theory I would love to see a nice and simple proof-theoretic argument proving this interesting result, some form of realizability or dialectica, but for now I will present a model theoretic proof given by Paris and Kirby in [2].

For the record, \( \Sigma_2 \)-Bounded Collection is the principle $$ \mbox{B\( \Sigma_2 \)} \quad \colon \quad \forall x < y \exists z A(x, z) \rightarrow \exists t \forall x < y \exists z < t A(x, z) $$ where \( A(x,y) \) is a \( \Sigma_2 \) formula. Because the implication from right to left is trivial, one can view the principle as stating the equivalence $$ \forall x < y \exists z A(x, z) \leftrightarrow \exists t \forall x < y \exists z < t A(x, z) $$ stating that unbounded existential quantifiers can in some sense be ``prenexed" over bounded universal quantifiers. Moreover, as we are in the classical setting the same can be said about unbounded universal quantifiers and bounded existential quantifiers $$ \exists x < y \forall z A(x, z) \leftrightarrow \forall t \exists x < y \forall z < t A(x, z). $$Theorem. There is a model of I\( \Sigma_1 \) which is not a model of B\( \Sigma_2 \).

The proof goes as follows. Start with any model \( M \) of Peano arithmetic containing non-standard \( \Sigma_2 \)-definable elements. They proceed as follows:

(1) Let \( K = \{ x \in M \; | \; \mbox{ \(x\) is \(\Sigma_2\)-definable in } M \} \)

(2) Notice that if \( A \) is \( \Sigma_2 \) then \( M \models A \) implies \( K \models A \).

(3) Clearly \( K \models \mbox{I}\Sigma_1 \), as \( K \) is a model of the least number principle for \( \Pi_1 \) formulas. (Side remark: Show that \( K \not\models \mbox{I}\Sigma_2 \) )

Let us show that \( K \not\models \mbox{B}\Sigma_2 \) by producing a concrete instance of \( {B}\Sigma_2 \) which does not hold in \( K \).

(4) Let \( \exists w A(e, w, x) \) be a universal \(\Sigma_2\)-formula, with \( A \in \Pi_1 \). Moreover, let \( t \in K \) be non-standard.

(5) For any \( a \in K \) we clearly have $$ M \models \exists e < t \exists u ( \underbrace{A(e, u_0, u_1) \wedge u_1 = a \wedge \forall z < u \neg A(e, z_0, z_1)}_{(*)}). $$ That's to say, in the model \( M \) we can find standard codes \( e \) representing \( \Sigma_2\)-formulas that uniquely define each \( a \in K \).

(6) Let \( B(e, u, a) = \exists x \forall y B_0(e, u, a, x, y) \) be a \( \Sigma_2 \) formula provably equivalent in Peano arithmetic to \( (*) \). Hence $$ M \models \exists e < t \exists u B(e, u, a).$$ (7) Note that \( \exists u B(e, u, a_0) \wedge \exists u B(e, u, a_1) \rightarrow a_0 = a_1 \).

(8) Hence, by (2), we also have $$ K \models \exists e < t \exists u B(e, u, a) $$ and in particular $$ K \models \forall a < t+1 \exists e < t \exists u \exists x \forall y B_0(e, u, a, x, y) $$ We show now that $$ K \not\models \exists r \exists s \forall a < t + 1 \exists e < t \exists u < r \exists x < s \forall y B_0(e, u, a, x, y). $$ obtaining an instance of \( B\Sigma_2 \) which does not hold in \( K \).

(9) Assume $$ K \models \exists r \exists s \exists e < t \exists u < r \exists x < s \forall y B_0(e, u, a, x, y) $$ and consequently $$ K \models \exists r \forall p \exists s \exists e < t \exists u < r \exists x < s \forall y < p B_0(e, u, a, x, y). $$ (10)  Hence, by (2) again, $$ M \models \forall a < t+1 \exists r \forall p \exists s \exists e < t \exists u < r \exists x < s \forall y < p B_0(e, u, a, x, y) $$ which is equivalent to $$ M \models \forall a < t+1 \exists e < t \exists u B(e, u, a) $$ which is a contradiction by (7) and the pigeon-hole principle in \( M \).

So that concludes the proof. I must add that the same argument works to show the independence of B\(\Sigma_{n+1}\) from I\(\Sigma_n\), one must simply adjust all the indexes above accordingly (and that's what Paris and Kirby have in [2]).

Anyway, as I said, I would love to see a nice and short proof as the one above using proof theoretic methods instead.

[1] Charles Parsons, On a number theoretic choice schema and its relation to induction, In: Intuitionism and Proof Theory (Proc. Conf., Buffalo, N.Y.,1968) (1970), pp. 459-473.

[2] J. B. Paris and L.A.S. Kirby, \( \Sigma_n \) collection schemas in arithmetic. Logic Colloquium, pp. 199-209, 1977.