AUC Philosophica et Historica (Acta Universitatis Carolinae Philosophica et Historica) is a multidisciplinary academic journal focused on the humanities with more than 50 years of tradition.
The journal is indexed in CEEOL, DOAJ, and EBSCO.
AUC PHILOSOPHICA ET HISTORICA, Vol 2022 No 1 (2022), 77–93
A note on generalized generalization
Vítězslav Švejdar
DOI: https://doi.org/10.14712/24647055.2025.5
published online: 28. 02. 2025
abstract
The generalization rules of sequent calculi allow, under some restrictions, to derive a formula ∃χφ or ∀χφ from a formula φχ (γ), i.e. from the formula obtained by substituting a variable γ for all free occurrences of χ in φ. We introduce modified generalization rules that make it possible to derive ∃χφ or ∀χφ from φχ (t) even in some cases where t is a complex term. These modified rules were invented in connection with attempts to prove the interpolation theorem for classical predicate logic without equality but with function symbols. This theorem seems (and remains) to be an unresolved case in the literature.
keywords: generalization; sequent; interpolation
references (13)
1. [Bíl07] M. Bílková. Uniform interpolation and propositional quantifiers in modal logics. Studia Logica, 85(1):1-31, 2007. CrossRef
2. [Bus98] S. R. Buss. An introduction to proof theory. In S. R. Buss, ed., Handbook of Proof Theory, no. 137 in Studies in Logic and the Foundations of Mathematics, chap. I, pp. 1-78. Elsevier, 1998. CrossRef
3. [Cra57a] W. Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Logic, 22(3):250-268, 1957. CrossRef
4. [Cra57b] W. Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Logic, 22(3):269-285, 1957. CrossRef
5. [GR08] R. Goré and R. Ramanayake. Valentini's cut-elimination for provability logic resolved. In C. Areces and R. Goldblatt, eds., Advances in Modal Logic 7 (AiML'08 Nancy), pp. 67-86. College Publications, London, 2008.
6. [Hen63] L. Henkin. An extension of the Craig-Lyndon interpolation theorem. J. Symb. Logic, 28:201-216, 1963. CrossRef
7. [Lyn59a] R. C. Lyndon. An interpolation theorem in the predicate calculus. Pacific J. Math., 9(1):129-142, 1959. CrossRef
8. [Lyn59b] R. C. Lyndon. Properties preserved under homomorphism. Pacific J. Math., 9(1):143-154, 1959. CrossRef
9. [Min02] G. Mints. A Short Introduction to Intuitionistic Logic. The University Series in Mathematics. Kluwer, 2002.
10. [MOU13] G. Mints, G. Olkhovikov, and A. Urquhart. Failure of interpolation in constant domain intuitionistic logic. J. Symb. Logic, 78(3):937-950, 2013. CrossRef
11. [SV82] G. Sambin and S. Valentini. The modal logic of provability: The sequential approach. J. Phil. Logic, 11:311-342, 1982. CrossRef
12. [Sol76] R. M. Solovay. Provability interpretations of modal logic. Israel J. Math., 25:287-304, 1976. CrossRef
13. [Tak75] G. Takeuti. Proof Theory. North-Holland, 1975.
A note on generalized generalization is licensed under a Creative Commons Attribution 4.0 International License.
