Abstract
This is an attempt to present a uniform algebraic framework for semantical approach to cut elimination. The basic idea came from a paper by S. Maehara of 1991. Using the notion of quasi-homomorphisms essentially due to Maehara, an algebraic condition called semi-completeness of a given sequent system is introduced. It is shown that for a given sequent system S, semi-completeness for the system \(\mathbf{S}^-\) implies cut elimination for S, where \(\mathbf S^-\) is obtained from S by deleting cut rule. In the present paper it is confirmed that many of existing semantical proofs of cut elimination using either Kripke semantics or algebraic one will fall into our algebraic framework. In fact, semi-completeness is considered to be an intelligible algebraic criterion of cut elimination which is applicable to both single- and multiple-succedent sequent systems for wide variety of nonclassical logics, including modal logics and substructural logics. For modal logics and intuitionistic logic, connections of quasi-homomorphisms with downward saturations, the conditions which are used in the constructions of canonical Kripke models, will be clarified. On the other hand, for substructural logics, quasi-homomorphisms will be discussed in relation to quasi-embeddings which are crucial in algebraic approaches to cut elimination. In the last three sections, semi-completeness arguments are extended so as to cover semantical proofs of cut elimination for nonclassical predicate logics. This can be carried out by generalizing quasi-homomorphisms on expanded algebraic structures. In this way, semi-completeness will provide a unified view of comprehending various semantical approaches to cut elimination.
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
Similar content being viewed by others
Notes
- 1.
For further exposition of Maehara’s semantical proof of cut elimination for second order calculi, see a recent paper by Arai (2017).
- 2.
See Footnote 3.
- 3.
The word valuation in place of homomorphism might be suitable. But, for further generalization, here we call it homomorphism, considering \(\varOmega _M\) as a freely generated modal algebra. By the same reason, we use the word quasi-homomorphism instead of quasi-valuation in Definition 2 given below.
- 4.
By abuse of symbols, we use \(\rightarrow \) for both logical connective and algebraic operation.
- 5.
- 6.
Again, we use the same symbol \(\cdot \) for both fusion and monoid operation.
- 7.
When S is a single-succedent system, \(\varDelta \) contains at most one formula and \(\varSigma \) is empty.
- 8.
Otherwise, the axiom of constant domain \(\forall x (\alpha \vee \beta ) \rightarrow (\forall x \alpha \vee \beta )\), which is not provable in intuitionistic predicate logic, becomes provable in the system, where x does not occur in \(\beta \) as a free variable.
References
Arai, T. (2017). Cut-eliminability in second order logic calculi, from https://arxiv.org/abs/1701.00929, submitted on 2017.
Belardinelli, F., Jipsen, P., & Ono, H. (2004). Algebraic aspects of cut elimination. Studia Logica, 77, 209–240.
Dragalin, A. G. (1988). Mathematical intuitionism: introduction to proof theory: American Mathematical Society.
Gabbay, D. M., Shehtman, V., & Shehtman, D. (2009). Quantification in nonclassical logic I (Vol. 153)., Studies in Logic and the Foundations of Mathematics: Elsevier.
Galatos, N., Jipsen, P., Kowalski, T., & Ono, H. (2007). Residuated lattices: an algebraic glimpse at substructural logics (Vol. 151)., Studies in Logic and the Foundations of Mathematics: Elsevier.
Goldblatt, R. (2011). Quantifiers, propositions and identity: admissible semantics for quantified modal and substructural logics., Lecture Notes in Logic, Association for Symbolic Logic: Cambridge University Press.
Lafont, Y. (1997). The finite model property for various fragments of linear logic. Journal of Symbolic Logic, 62, 1202–1208.
Lahav, O., & Avron, A. (2014). A unified semantic framework for fully-structural propositional sequent systems. ACM Transactions on Computational Logic, 165, 26–48.
Maehara, S. (1991). Lattice-valued representation of the cut elimination theorem. Tsukuba Journal of Mathematics, 15, 509–521.
Okada, M., & Terui, K. (1999). The finite model property for various fragments of intuitionistic linear logic. Journal of Symbolic Logic, 64, 790–802.
Ono, H. (1993). Semantics for substructural logics. In K. Dosen & P. Schroeder-Heister (Eds.), Substructural logics (Vol. 2, pp. 259–291)., Studies in Logic and Computation: Oxford University Press.
Ono, H. (2015). Semantical approach to cut elimination and subformula property in modal logic. In C.-M. Yang, D.-M. Deng, & H. Lin (Eds.), Structural Analysis of Non-Classical Logics, The Proceedings of the Second Taiwan Philosophical Logic Colloquium (pp. 1–15)., Logic in Asia: Springer.
Acknowledgements
The author would like to express many thanks to C.-M. Yang and K. Sano for their helpful comments and suggestions, and also to T. Kowalski for valuable discussions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer Nature Singapore Pte Ltd.
About this paper
Cite this paper
Ono, H. (2017). A Uniform Algebraic Approach to Cut Elimination via Semi-completeness. In: Yang, SM., Lee, K., Ono, H. (eds) Philosophical Logic: Current Trends in Asia. Logic in Asia: Studia Logica Library. Springer, Singapore. https://doi.org/10.1007/978-981-10-6355-8_2
Download citation
DOI: https://doi.org/10.1007/978-981-10-6355-8_2
Published:
Publisher Name: Springer, Singapore
Print ISBN: 978-981-10-6354-1
Online ISBN: 978-981-10-6355-8
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)