Advances in Proof Theory pp 339-351 | Cite as

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

## Abstract

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.

## References

- 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.A.G. Dragalin,
*Mathematical Intuitionism: Introduction to Proof Theory*(American Mathematical Society, Providence, Rhode Island, 1987). Russian original 1979Google Scholar - 3.J. Ekman,
*Normal proofs in set theory*, Ph.D. thesis, Unversity of Göteborg, 1994Google Scholar - 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.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.L. Hallnäs, Partial inductive definitions. Theoret. Comput. Sci.
**87**, 115–142 (1991)MathSciNetCrossRefzbMATHGoogle Scholar - 7.L. Hallnäs, On the proof-theoretic foundation of general definition theory. Synthese
**148**, 589–602 (2006)MathSciNetCrossRefzbMATHGoogle Scholar - 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.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.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.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.S. Negri, J. von Plato,
*Structural Proof Theory*(Cambridge University Press, Cambridge, 2001)Google Scholar - 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.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.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: http://www.gap5.de/proceedings - 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.P. Schroeder-Heister, Proof-theoretic semantics, self-contradiction, and the format of deductive reasoning, Topoi
**31**, 77–85 (2012)Google Scholar