Advertisement

The Craig Interpolation Theorem for Schematic Systems

  • A. Carbone
Part of the Collegium Logicum book series (COLLLOGICUM, volume 2)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 2.
    S. Buss. The undecidability of k-provability. Annals of Pure and Applied Logic, 53: 72–102, 1991.MathSciNetGoogle Scholar
  3. 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. 4.
    A. Carbone. Interpolants, Cut Elimination and Flow Graphs. To appear in Annals of Pure and Applied Logic, 1995.Google Scholar
  5. 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. 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. 7.
    J.Y. Girard. Linear Logic. In Theoretical Computer Science, 50:1–102, 1987.MathSciNetMATHCrossRefGoogle Scholar
  8. 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. 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. 10.
    R. Parikh. Some results on the length of proofs. In Transaction of the American Mathematical Society, 177:29–36, 1973.MathSciNetMATHCrossRefGoogle Scholar
  11. 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. 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. 13.
    M.E. Szabó. Algebra of Proofs. North-Holland, Amsterdam, 1977.Google Scholar
  14. 14.
    G. Takeuti. Proof Theory. Studies in Logic 81. North Holland, Amsterdam, 2nd Edition, 1987.Google Scholar

Copyright information

© Springer-Verlag/Wien 1996

Authors and Affiliations

  • A. Carbone
    • 1
  1. 1.Institut für Algebra und Diskrete MathematikTechnische Universität WienAustria

Personalised recommendations