On some formalized conservation results in arithmetic (Q1264147)

I\(\Sigma_ n\) and \(B\Sigma_ n\) are well known fragments of first-order arithmetic with induction and collection for \(\Sigma_ n\) formulas respectively; \(I\Sigma^ 0_ n\) and \(B\Sigma^ 0_ n\) allow free second-order variables. \(RCA_ 0\) is the well known fragment of second- order arithmetic with recursive comprehension; \(WKL_ 0\) is \(RCA_ 0\) plus weak König's lemma. We first strengthen Harrington's conservation result by showing that \(WKL_ 0+B\Sigma^ 0_ n\) is \(\Pi^ 1_ 1\)- conservative over \(RCA_ 0+B\Sigma^ 0_ n\). Then we develop some model theory in \(WKL_ 0\) and illustrate the use of formalized model theory by giving a relatively simple proof of the fact that \(I\Sigma_ 1\) proves \(B\Sigma_{n+1}\) to be \(\Pi_{n+2}\)-conservative over \(I\Sigma_ n\). Finally, we present a proof-theoretic proof of the stronger fact that the \(\Pi_{n+2}\) conservation result is provable already in \(I\Delta_ 0+\sup er\exp\). Thus \(I\Sigma_{n+1}\) proves \(1\)- Con(B\(\Sigma_{n+1})\) and \(I\Delta_ 0+\sup er\exp\) proves \(Con(I\Sigma_ n)\leftrightarrow Con(B\Sigma_{n+1})\).