2 added 731 characters in body

The axiom system PRA of "primitive-recursive arithmetic" is finitistic, but it has been known for a few decades that it has the same set of $\Pi^0_1$ consequences as the infinitistic theory $\text{WKL}_0$ of second-order arithmetic. In particular, there is a primitive recursive function $f$ that turns a formal proof of a $\Pi^0_1$ statement in $\text{WKL}_0$ into a proof in PRA. Roughly put, a $\Pi^0_1$ formula says that all natural numbers have some particular property, depending on the formula, where the property can be stated using a formula in the language of rings with no quantifiers.

The advantage of working in $\text{WKL}_0$ is that the proofs can be much shorter. I think this was always suspected, but Caldon and Ignjatovic recently established (pdf) a formal superexponential lower bound for $f$, at least on an infinite set of formulas. Their result is phrased for a different infinitary system, $I\Sigma^0_1$, that lies between PRA and $\text{WKL}_0$. $I\Sigma^0_1$ is a fragment of Peano arithmetic, unlike $\text{WKL}_0$; its main difference from PRA is that $I\Sigma^0_1$ allows direct universal quantification over the set of natural numbers during the proof, while PRA does not.

In their paper, the set of formulas for the lower bound is explicitly laid out. These may not be particularly concrete, because they relate to consistency statements.

If we expand PRA to allow for existential quantification, we can get a slightly larger theory in which $\Pi^0_2$ statements can be expressed. It is known that $\text{WKL}_0$ is still conservative over this larger theory for $\Pi^0_2$ statements. In 1994, Kikuchi and Tanaka (pdf) gave a nice example of how this could be used to show that the second incompleteness theorem is provable in PRA, by using model-theoretic, infinitary methods in $\text{WKL}_0$ and relying on the conservation result.

1

The axiom system PRA of "primitive-recursive arithmetic" is finitistic, but it has been known for a few decades that it has the same set of $\Pi^0_1$ consequences as the infinitistic theory $\text{WKL}_0$ of second-order arithmetic. In particular, there is a primitive recursive function $f$ that turns a formal proof of a $\Pi^0_1$ statement in $\text{WKL}_0$ into a proof in PRA. Roughly put, a $\Pi^0_1$ formula says that all natural numbers have some particular property, depending on the formula, where the property can be stated using a formula in the language of rings with no quantifiers.

The advantage of working in $\text{WKL}_0$ is that the proofs can be much shorter. I think this was always suspected, but Caldon and Ignjatovic recently established (pdf) a formal superexponential lower bound for $f$, at least on an infinite set of formulas. Their result is phrased for a different infinitary system, $I\Sigma^0_1$, that lies between PRA and $\text{WKL}_0$. $I\Sigma^0_1$ is a fragment of Peano arithmetic, unlike $\text{WKL}_0$; its main difference from PRA is that $I\Sigma^0_1$ allows direct universal quantification over the set of natural numbers during the proof, while PRA does not.