Abstract
We provide a natural formulation of the sequent calculus with equality and establish the cut elimination theorem. We also briefly outline and comment on its application to the logic of partial terms, when “existence” is formulated as equality with a (bound) variable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baaz, M., Iemhoff, M.R.: On the Proof Theory of the Existence Predicate We will show them! Essays in honour of Dov Gabbay, pp. 125–166. College Publication (2005)
Feferman, S.: Definedness. Erkenntnis 43, 295–329 (1995)
Hintikka, J.: Existential Presupposition and Existential Commitments. Journal of Philosophy 56, 125–137 (1959)
Kanger, S.: A Simplified Proof Method for Elementary Logic. In: Braffort, P., Hirshberg, D. (eds.) Computer Programming and Formal Systems, pp. 87–94. North-Holland, Amsterdam (1963)
Leblank, H., Hailperin, H.T.: Nondesignating Singulatr Terms. Philosophical Review 68, 239–243 (1959)
Lifschitz, A.V.: Specialization of the form of deduction in the predicate calculus with equality and function symbols. In: Orevkov, V.P. (ed.) The Calculi of Symbolic Logic. I, Proceedings of the Steklov Institute of Mathematics 98 (1971)
van Plato, J., Negri, S.: Cut Elimination in the Presence of Axioms. The Bulletin of Symbolic Logic 147, 418–435 (1998)
van Plato, J., Negri, S.: Structural Proof Theory. Cambridge University Press, Cambridge (2001)
Parlamento, F.: Truth-value semantics and functional extensions for classical logic of partial terms based on equality. ArXiv:1112.6331 (2011) (to appear in the Notre Dame J. of Form. Logic)
van Quine, W.O.: On What there is. Review of Metaphisics 2, 21–38 (1948)
Scott, D.S.: Identity and Existence in Intuitionistic Logic. In: Proc. Res. Symp. on Application of Sheaves 1977, Durham. Lect. Notes Math., vol. 763, pp. 660–696 (1979)
Szabo, M.E.: The Collected Papers of Gerhard Gentzen. North Holland, Amsterdam (1969)
Takeuti, G.: Proof Theory. Studies in Logic and the Foundations of Mathematics, vol. 81. North Holland, Amsterdam (1975)
Troelstra, A.S., Schwichtemberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Parlamento, F., Previale, F. (2013). Cut Elimination for Gentzen’s Sequent Calculus with Equality and Logic of Partial Terms. In: Lodaya, K. (eds) Logic and Its Applications. ICLA 2013. Lecture Notes in Computer Science, vol 7750. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36039-8_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-36039-8_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36038-1
Online ISBN: 978-3-642-36039-8
eBook Packages: Computer ScienceComputer Science (R0)