Return to Answer

• $T^i_2$ proves the consistency (and even some form of reflection principle) of $G_i$.

• Conversely, $\mathrm{Con}_{G_i}$ implies over a weak base theory all $\forall\Delta^b_1$-consequences of $T^i_2$ (and more complex consequences of $T^i_2$ can be xiomatized by an appropriate reflection principle). A related fact is that if $T^i_2$ proves a $\forall\Sigma^b_i$ statement, one can translate it into a sequence of quantified propositional tautologies which will have polynomially bounded proofs in $T^i_2$.

• If $P$ is any propositional proof system whose consistency is provable in $T^i_2$, then $G_i$ polynomially simulates $P$.

$S_2$ is the union of its finitely axiomatizable fragments $T^i_2$. This means that $S\_2$ proves the consistency of each fragment $G_i$, but on the other hand, if it proved the consistency of the full quantified propositional calculus $G$, it would imply that $G\_i$ polynomially simulates $G$ for some $i$, and this is assumed to be false. To put it differently, the $\forall\Delta^b_1$-consequences of $S_2$ (as well as $S_2$ itself) are not assumed to be finitely axiomatizable.

• $T^i_2$ proves the consistency (and even some form of reflection principle) of $G_i$.

• Conversely, $\mathrm{Con}_{G_i}$ implies over a weak base theory all $\forall\Delta^b_1$-consequences of $T^i_2$ (and more complex consequences of $T^i_2$ can be axiomatized by an appropriate reflection principle). A related fact is that if $T^i_2$ proves a $\forall\Sigma^b_i$ statement, one can translate it into a sequence of quantified propositional tautologies which will have polynomially bounded proofs in $T^i_2$.

• If $P$ is any propositional proof system whose consistency is provable in $T^i_2$, then $G_i$ polynomially simulates $P$.

$S_2$ is the union of its finitely axiomatizable fragments $T^i_2$. This means that $S_2$ proves the consistency of each fragment $G_i$, but on the other hand, if it proved the consistency of the full quantified propositional calculus $G$, it would imply that $G_i$ polynomially simulates $G$ for some $i$, and this is assumed to be false. To put it differently, the $\forall\Delta^b_1$-consequences of $S_2$ (as well as $S_2$ itself) are not assumed to be finitely axiomatizable.

First, as explained in http://mathoverflow.net/questions/120106, the question is equivalent to provability of the consistency of FPA in $I\Delta_0+\Omega_1$. (The fact that you are using second order objects to encode proofs and formulas corresponds to using all numbers instead of just the logarithmically small ones in $I\Delta_0+\Omega_1$, hence you end up with the usual consistency statement.)

First, as explained in https://mathoverflow.net/questions/120106, the question is equivalent to provability of the consistency of FPA in $I\Delta_0+\Omega_1$. (The fact that you are using second order objects to encode proofs and formulas corresponds to using all numbers instead of just the logarithmically small ones in $I\Delta_0+\Omega_1$, hence you end up with the usual consistency statement.)

The answer is that this is one of the major open problems in the area, but it is conjectured to be false. There is a kind of correspondence of subsystems of bounded arithmetic to propositional proof systems; in particular, the fragments $T^i_2$ of $S_2$ (${}=I\Delta_0+\Omega_1$) correspond to the fragments $G_i$ of the quantified propositional calculus, obtained by restricting all formulas in the proof (or alternatively, all cut formulas in the sequent calculus formulation) to formulas in prenex form with at most $i$ quantifier blocks. This means:

$S_2$ is the union of its finitely axiomatizable fragments $T^i_2$. This means that $S\_2$ proves the consistency of each fragment $G_i$, but on the other hand, if it proved the consistency of the full quantified propositional calculus $G$, it would imply that $G\_i$ polynomially simulates $G$ for some $i$, and this is assumed to be false. To put it differently, the $\forall\Delta^b_1$-consequences of $S_2$ (as well as $S_2$ itself) are not assumed to be finitely axiomatizable.

The answer is that this is one of the major open problems in the area, but it is conjectured to be false. There is a kind of correspondence of subsystems of bounded arithmetic to propositional proof systems; in particular, the fragments $T^i_2$ of $S_2$ (${}=I\Delta_0+\Omega_1$) correspond to the fragments $G_i$ of the quantified propositional calculus, obtained by restricting all formulas in the proof (or alternatively, all cut formulas in the sequent calculus formulation) to $\Sigma^q_i$ or $\Pi^q_i$ formulas (= formulas in prenex form with at most $i$ quantifier blocks). This means:

$S_2$ is the union of its finitely axiomatizable fragments $T^i_2$. This means that $S\_2$ proves the consistency of each fragment $G_i$, but on the other hand, if it proved the consistency of the full quantified propositional calculus $G$, it would imply that $G\_i$ polynomially simulates $G$ for some $i$, and this is assumed to be false. To put it differently, the $\forall\Delta^b_1$-consequences of $S_2$ (as well as $S_2$ itself) are not assumed to be finitely axiomatizable.

The correspondence of theories and propositional proof systems also extends to complexity classes. Sets definable by $\Sigma^b_i$ formulas in the standard model of arithmetic are exactly those computable in the $i$-level $\Sigma^P_i$ of the polynomial hierarchy. The theories $T^i_2$ have induction for $\Sigma^b_i$ formulas, and their provably total $\Sigma^b_{i+1}$-definable functions are $\mathrm{FP}^{\Sigma^P_i}$, so these theories correspond to levels of the polynomial hierarchy. On the propositional side, satisfiability of $\Sigma^q_i$ formulas is a $\Sigma^P_i$-complete problem. Taking the union, $S_2$ corresponds to the full polynomial hierarchy $\mathrm{PH}$. However, the complexity class corresponding to $G$ is $\mathrm{PSPACE}$, as satisfiability of unrestricted quantified propositional formulas is $\mathrm{PSPACE}$-complete. Thus, asking $S_2$ to prove the consistency of $G$ is in the same spirit as collapsing $\mathrm{PSPACE}$ to $\mathrm{PH}$ (and therefore to some its fixed level). (Don’t quote me on this. While the collapse of the $T^i_2$ hierarchy does imply the collapse of $\mathrm{PH}$, for propositional proof systems this becomes only a loose analogy.)

In order to give also an upper bound on the consistency strength, the consistency of $G$, and therefore of FPA, is provable in theories corresponding to $\mathrm{PSPACE}$. The best known such theory is Buss’s theory $U^1_2$, which is a “second-order” extension of $S_2$ with comprehension for bounded sets defined by bounded formulas without second-order quantifiers, and length induction for bounded $\Sigma^1_1$-formulas. Notice that things get really messy here, as the first-order objects of $U^1_2$ correspond to second-order objects of FPA, and second-order objects of $U^1_2$ have no analogue in FPA. Alan Skelley formulated an equivalent (technically, RSUV-isomorphic) theory $W^1_1$. This is syntactically a third-order arithmetic, and it is more directly comparable to FPA (as numbers of one theory correspond to numbers of the other, and sets correspond to sets). $W^1_1$ proves the consistency of $G$, and thus of FPA.