Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut

Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 28)


In logical sequent calculi, initial sequents expressing the axiom of identity can be required to be atomic, without affecting the deductive strength of the system. When extending the logical system with right- and left-introduction rules for atomic formulas, one can analogously require that initial sequents be restricted to “uratoms”, which are undefined (not even vacuously defined) atoms. Depending on the definitional clauses for atoms, the resulting system is possibly weaker than the unrestricted one. This weaker system may however be preferable to the unrestricted system, as it enjoys cut elimination and blocks unwanted derivations arising from non-wellfounded definitions, for example in the context of paradoxes.


  1. 1.
    J. Brotherston, A. Simpson, Complete sequent calculi for induction and infinite descent, in Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science (LICS) (IEEE Press, Los Alamitos, 2007), pp. 51–62Google Scholar
  2. 2.
    A.G. Dragalin, Mathematical Intuitionism: Introduction to Proof Theory (American Mathematical Society, Providence, Rhode Island, 1987). Russian original 1979Google Scholar
  3. 3.
    J. Ekman, Normal proofs in set theory, Ph.D. thesis, Unversity of Göteborg, 1994Google Scholar
  4. 4.
    J. Ekman, Self-contradictory reasoning, in Advances in Proof-Theoretic Semantics, ed. by T. Piecha, P. Schroeder-Heister (Springer, Cham, 2016), pp. 211–229Google Scholar
  5. 5.
    F.B. Fitch, A system of formal logic without an analogue to the Curry W operator. J. Symb. Log. 1, 92–100 (1936)CrossRefzbMATHGoogle Scholar
  6. 6.
    L. Hallnäs, Partial inductive definitions. Theoret. Comput. Sci. 87, 115–142 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    L. Hallnäs, On the proof-theoretic foundation of general definition theory. Synthese 148, 589–602 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    L. Hallnäs, P. Schroeder-Heister, A proof-theoretic approach to logic programming: I. Clauses as rules. II. Programs as definitions. J. Logic Comput. 1, 261–283, 635–660 (1990/91)Google Scholar
  9. 9.
    G. Jäger, R.F. Stärk, A proof-theoretic framework for logic programming, in Handbook of Proof Theory, ed. by S.R. Buss (Elsevier, Amsterdam, 1998), pp. 639–682Google Scholar
  10. 10.
    P. Kreuger, Axioms in definitional calculi, in Extensions of Logic Programming. 4th International Workshop, ELP’93, St Andrews, U.K., Mar/Apr 1993. Proceedings ed. by R. Dyckhoff. (Lecture Notes in Computer Science, vol. 798), (Springer, Berlin, 1994), pp. 196–205Google Scholar
  11. 11.
    P. Martin-Löf, Hauptsatz for the intuitionistic theory of iterated inductive definitions, in Proceedings of the Second Scandinavian Logic Symposium, ed. by J.E. Fenstad (North-Holland, Amsterdam, 1971), pp. 179–216CrossRefGoogle Scholar
  12. 12.
    S. Negri, J. von Plato, Structural Proof Theory (Cambridge University Press, Cambridge, 2001)Google Scholar
  13. 13.
    P. Schroeder-Heister, Cut elimination in logics with definitional reflection, in Nonclassical Logics and Information Processing: International Workshop (Berlin, November 1990), Proceedings, ed. by D. Pearce, H. Wansing, (Lecture Notes in Computer Science, vol. 619) (Springer, Berlin, 1992), pp. 146–171Google Scholar
  14. 14.
    P. Schroeder-Heister, Rules of definitional reflection, in Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science (Montreal 1993) (IEEE Press, Los Alamitos, 1993), pp. 222–232Google Scholar
  15. 15.
    P. Schroeder-Heister, On the notion of assumption in logical systems, in Selected Papers Contributed to the Sections of GAP5, Fifth International Congress of the Society for Analytical Philosophy, Bielefeld, 22–26 Sept 2003, ed. by R. Bluhm, C. Nimtz (Mentis, Paderborn, 2004), pp. 27–48. Online publication:
  16. 16.
    P. Schroeder-Heister, Paradoxes and structural rules, in Insolubles and Consequences: Essays in Honour of Stephen Read, ed. by C. Dutilh Novaes, O. Hjortland (College Publications, 2012), pp. 203–211Google Scholar
  17. 17.
    P. Schroeder-Heister, Proof-theoretic semantics, self-contradiction, and the format of deductive reasoning, Topoi 31, 77–85 (2012)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Wilhelm-Schickard-Institut für Informatik, Universität TübingenTübingenGermany

Personalised recommendations