Interpolants, cut elimination and flow graphs for the propositional calculus (Q674415)

This paper is about the use of logical flow graphs in propositional calculus, particularly in connection with the interpolation and the cut elimination theorems. These graphs, which were introduced by \textit{S. Buss} [Ann. Pure Appl. Logic 53, 75-102 (1991; Zbl 0749.03039)], are designed to trace how occurrences of subformulas migrate through proofs in the sequent calculus and hence how these occurrences are related to one another. By means of these graphs one can excavate ``inner proofs'' from the given proof. These are rather obvious intuitive ideas, but to give precise definitions and to clarify details require many pages and examples. The author uses this tool to obtain proofs of the interpolation theorem, sometimes without eliminating cuts first, and to estimate the size of interpolants when the given proof is not too complicated. For instance, if \(A\to B\) is a tautology and \(A\) or \(B\) does not contain the negation or the implication sign, there is an interpolant whose size is linear in those of \(A\) and \(B\). Gentzen's procedure of eliminating cuts loses local information; and the author gives a new procedure that has the inversion property. Namely, given a proof \(\pi\), the new procedure produces a cut-free proof \(\pi'\) in such a way that from any inner proof in \(\pi'\) one can recover the corresponding proof in the original \(\pi\). Due to the nature of the subject and of the writing, this article is lengthy.