Collegium Logicum pp 87-100 | Cite as

# The Craig Interpolation Theorem for Schematic Systems

## Abstract

The notion of Schematic System has been introduced by Parikh in the early seventies. It is a metamathematical notion describing the concept of deduction system and the operation of substitution of terms and formulas in it. We show a generalization of the Craig Interpolation Theorem for a natural class of schematic systems while we determine sufficient conditions for a schematic system to enjoy Interpolation. These conditions are much weaker than the usual conditions of symmetricity that are satisfied by the logics usually studied. The proof of the Craig Interpolation Theorem that we propose is a refinement of Maehara’s construction and it is based on the idea of tracing the flow of formulas in a proof.

## Keywords

Schematic System Schematic Axiom Predicate Variable Schematic Rule Main Formula## Preview

Unable to display preview. Download preview PDF.

## References

- 1.M. Baaz, C.G. Fermiiller and R. Zach. Systematic construction of natural deduction systems for many-valued logics.
*Proc. 23rd International Symposium on Multiple-valued Logics*, Sacramento CA, IEEE Press, 208–213, 1993.Google Scholar - 2.S. Buss. The undecidability of k-provability. Annals
*of*Pure and*Applied Logic*, 53: 72–102, 1991.MathSciNetGoogle Scholar - 3.A. Carbone. On
*Logical Flow Graphs*. Ph.D. Dissertation, Department of Mathematics of the Graduate School of The City University of New York, May 1993.Google Scholar - 4.A. Carbone. Interpolants, Cut Elimination and Flow Graphs. To appear in Annals
*of Pure*and*Applied Logic*, 1995.Google Scholar - 5.W. Craig. Linear Reasoning. A new form of the Herbrand-Gentzen Theorem. In Journal
*of Symbolic Logic*, 22:250–268, 1957.MathSciNetMATHCrossRefGoogle Scholar - 6.W. Farmer. A unification-theoretic method for investigating the k-provability problem. In Annals
*of*Pure and*Applied Logic*, 51:173–214, 1991.MathSciNetMATHCrossRefGoogle Scholar - 7.J.Y. Girard. Linear Logic. In
*Theoretical Computer Science*, 50:1–102, 1987.MathSciNetMATHCrossRefGoogle Scholar - 8.G. Kreisel. A survey of proof theory II. In J.E. Fenstad, editor,
*Proceedings Second Scandinavian Logic Symposium*, pages 109–170. 1971.CrossRefGoogle Scholar - 9.J. Krajícek. On the number of steps in proofs. In Annals
*of*Pure and*Applied Logic*, 41:153–178, 1989.MathSciNetMATHCrossRefGoogle Scholar - 10.R. Parikh. Some results on the length of proofs. In
*Transaction of the American Mathematical Society*, 177:29–36, 1973.MathSciNetMATHCrossRefGoogle Scholar - 11.D. Prawitz. Ideas and results in proof theory. In J.E. Fenstad, editor,
*Proceedings Second Scandinavian Logic Symposium*, pages 235–307. 1971.Google Scholar - 12.D. Roorda.
*Resource Logics: Proof-theoretical Investigations*. Ph.D. Dissertation, Department of Mathematics and Computer Science of the University of Amsterdam, September 1991.Google Scholar - 13.M.E. Szabó.
*Algebra of Proofs*. North-Holland, Amsterdam, 1977.Google Scholar - 14.G. Takeuti.
*Proof Theory*. Studies in Logic 81. North Holland, Amsterdam, 2nd Edition, 1987.Google Scholar