Interpolants, cut elimination and flow graphs for the propositional calculus
type: Item
instance of: scholarly article
title: Interpolants, cut elimination and flow graphs for the propositional calculus
zbMATH Open document ID: 0873.03050
DOI: 10.1016/S0168-0072(96)00019-X
author: Juan-Miguel Gracia
published in: Annals of Pure and Applied Logic
publication date: 1997-10-26T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 03F07
zbMATH DE Number: 986680
zbMATH Keywords: logical flow graphs
zbMATH Keywords: propositional calculus
zbMATH Keywords: interpolation
zbMATH Keywords: cut elimination
zbMATH Keywords: sequent calculus
zbMATH Keywords: size of interpolants
MaRDI profile type: Publication
cites work: Q4385519
cites work: The undecidability of \(k\)-provability
cites work: Q4885912
cites work: The relative efficiency of propositional proof systems
cites work: A unification-theoretic method for investigating the \(k\)-provability problem
cites work: Q3882443
cites work: Linear logic
cites work: Q5812175
cites work: The number of proof lines and the size of proofs in first order logic
cites work: Complexity of the realization of a linear function in the class of \(\Pi\)-circuits
cites work: Q3724312
cites work: Some Results on the Length of Proofs
cites work: Q3773878
cites work: The Universe of Set Theory
cites work: Q4010371
cites work: Q4323873
full work available at URL: s0168-0072(96)00019-x
OpenAlex ID: W2158086914
Recommended article: Streams and strings in formal proofs.
Recommended article: Making proofs without Modus Ponens: An introduction to the combinatorics and complexity of cut elimination
Recommended article: The cost of a cycle is a square
Recommended article: Q4263835
Recommended article: Q4530460
Recommended article: Duplication of directed graphs and exponential blow up of proofs
Recommended article: Gentzen's second consistency proof and strong cut-elimination
Recommended article: Turning cycles into spirals
Recommended article: Gentzen systems, resolution, and literal trees
Recommended article: Logical structures and genus of proofs
description: scientific article; zbMATH DE number 986680