Cut elimination algorithms

Gentzen's Hauptsatz in first order logic includes an algorithm taking any proof in the sequent calculus with cut rule, and delivering a proof without cut rule (and with the subformula property). So far as I know cut elimination in the simple theory of types (STT) has no such algorithm. Rather, one proves non-constructively that the system without cut rule is complete for the same models as the system with.

But is there such an algorithm for STT, or is it known there cannot be?

And what about the proof that $\mathsf{ACA}_0$ is conservative over PA? (Compare Emil Jeřábek's answer to What metatheory proves $\mathsf{ACA}_0$ conservative over PA?) Does that come with an algorithm for producing PA proofs?

As Noah pointed out, if it's provable, there must be an algorithm for cut-elimination for STT because the underlying statement is $\Pi_2$ (for any deduction in STT, there is a corresponding deduction without cut). Moreover, if you can prove cut-elimination for STT in some theory T for which you do have an algorithm for cut-elimination, the algorithm for T "suffices" in some sense for STT. (For example, bounds on growth in T give you bounds in STT.) That said, I don't know the literature on cut-elimination for STT, so someone else will have to comment on what's actually in the literature about the algorithm. (For instance, if anyone has written it out explicitly.)

For your second question, the proof via cut-elimination Emil Jeřábek mentioned is constructive. One should be careful about terminology: the cut-elimination needed isn't the fancy stuff for $\mathrm{PA}$. The proof uses the much easier cut-elimination for pure first-order logic (which has a known algorithm!). In the presence of non-logical axioms, you can't eliminate all cuts, but you can eliminate all "free cuts" (cuts over formulas which are not parts of non-logical axioms). Then you add a new argument showing that cuts over the new axioms in $\mathrm{ACA}_0$ can be eliminated, basically in the obvious way: if you have a cut between $$\exists X\forall x(\phi(x)\leftrightarrow x\in X),$$ and $$\forall X\neg\forall x(\phi(x)\leftrightarrow x\in X),\Gamma,$$ you obtain a proof of $\Gamma$ by replacing $t\in X$ with $\phi(t)$ everywhere. (Details depend on the formulation and how you're handling induction axioms.)

• So, going from $\mathsf{ACA}_0$ to PA we get all the information we could hope for. Nice – Colin McLarty Aug 25 '13 at 20:25

In some sense, the answer is trivially yes: if you know a theory $T$ proves $\varphi$ using only deduction rules from among $\mathcal{D}$, then (assuming $T$ and $\mathcal{D}$ are appropriately computable) you can just search through all appropriate proofs. This certainly holds in both cases you mention, and (I believe) in all cases of interest.

If you're asking about "feasible" algorithms, then of course things get more complicated. I don't know about STT and cut elimination, but in the case of $PA$ versus $ACA_0$, the conservativity proof is very straightforward - given $\mathcal{M}\models PA$, the structure $$(\mathcal{M}, \{X\subseteq\vert\mathcal{M}\vert: X\text{ is arithmetically definable in \mathcal{M} with parameters}\})$$ is a model of $ACA_0$ - and that would seem to yield a very direct conversion of $ACA_0$-proofs to $PA$-proofs. (By "direct" here I just mean that there is a clear intuition behind the algorithm which is better than "unbounded search," not that it (a) converges quickly or (b) generates a proof of reasonable length.)

EDIT: I believe the paper "A Relative Consistency Proof" by Shoenfield addresses the issue of going from $ACA_0$-proofs to $PA$-proofs; also, see Reducing ACA₀ proof to First Order PA.

• Your first point is fair. I must ask for something about the algorithm. My concern is not so much feasibility as information. Given a proof of $P$ in $\mathsf{ACA}_0$ what can we learn about a corresponding proof in PA besides the last line $P$? The method of searching all proofs in the base theory gives a result independent of which proof you know in the conservative extension, so we learn nothing about one from the other, beyond that they prove the same formula. I will pursue the reference. – Colin McLarty Aug 25 '13 at 19:16
• We don't have an efficient algorithm even for the propositional sequent calculus (as the size of cut-eliminated proof can be much larger). – Kaveh Aug 26 '13 at 9:17