Algorithmic structuring of cut-free proofs

Baaz, Matthias, and Richard Zach. 1993. “Algorithmic Structuring of Cut-Free Proofs.” In Computer Science Logic. CSL’92, San Miniato, Italy. Selected Papers, edited by Egon Börger, Gerhard Jäger, Hans Kleine Büning, Simone Martini, and Michael M. Richter, 29–42. LNCS 702. Berlin: Springer. DOI: 10.1007/3-540-56992-8_4

We investigate the problem of algorithmic structuring of proofs in the sequent calculi LK and LKB (LK where blocks of quantifiers can be introduced in one step), where we distinguish between linear proofs and proofs in tree form.

In this framework, structuring coincides with the introduction of cuts into a proof. The algorithmic solvability of this problem can be reduced to the question of k/l-compressibility: “Given a proof of \(\Gamma \vdash \Delta\) of length k, and l < k: Is there is a proof of \(\Gamma \vdash \Delta\) of length < l?” When restricted to proofs with universal or existential cuts, this problem is shown to be

  1. undecidable for linear or tree-like LK-proofs,
  2. undecidable for linear LKB-proofs, and
  3. decidable for tree-like LKB-proofs.

(1) corresponds to the undecidability of second order unification, (2) to the undecidability of semi-unification, and (3) to the decidability of a subclass of semi-unification.

Continue reading