The Craig Interpolation Theorem for Schematic Systems
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.
KeywordsSchematic System Schematic Axiom Predicate Variable Schematic Rule Main Formula
Unable to display preview. Download preview PDF.
- 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
- 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
- 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