×

zbMATH — the first resource for mathematics

Rules with parameters in modal logic. I. (English) Zbl 1408.03015
Summary: We study admissibility of inference rules and unification with parameters in transitive modal logics (extensions of K4), in particular we generalize various results on parameter-free admissibility and unification to the setting with parameters.
Specifically, we give a characterization of projective formulas generalizing Ghilardi’s characterization in the parameter-free case, leading to new proofs of Rybakov’s results that admissibility with parameters is decidable and unification is finitary for logics satisfying suitable frame extension properties (called cluster-extensible logics in this paper). We construct explicit bases of admissible rules with parameters for cluster-extensible logics, and give their semantic description. We show that in the case of finitely many parameters, these logics have independent bases of admissible rules, and determine which logics have finite bases.
As a sideline, we show that cluster-extensible logics have various nice properties: in particular, they are finitely axiomatizable, and have an exponential-size model property. We also give a rather general characterization of logics with directed (filtering) unification.
In the sequel, we will use the same machinery to investigate the computational complexity of admissibility and unification with parameters in cluster-extensible logics, and we will adapt the results to logics with unique top cluster (e.g., S4.2) and superintuitionistic logics.

MSC:
03B45 Modal logic (including the logic of norms)
03B55 Intermediate logics
08B20 Free algebras
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI arXiv
References:
[1] Baader, F.; Ghilardi, S., Unification in modal and description logics, Log. J. IGPL, 19, 705-730, (2011) · Zbl 1258.03018
[2] Baader, F.; Snyder, W., Unification theory, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. I, (2001), Elsevier), 445-533 · Zbl 1011.68126
[3] Chagrov, A. V.; Zakharyaschev, M., Modal logic, Oxford Logic Guides, vol. 35, (1997), Oxford University Press · Zbl 0871.03007
[4] Dzik, W., Unification of some substructural logics of BL-algebras and hoops, Rep. Math. Logic, 43, 73-83, (2008) · Zbl 1156.03022
[5] Fine, K., Logics containing K4, part I, J. Symbolic Logic, 39, 31-42, (1974) · Zbl 0287.02010
[6] Galatos, N.; Jipsen, P.; Kowalski, T.; Ono, H., Residuated lattices: an algebraic glimpse at substructural logics, Studies in Logic and the Foundations of Mathematics, vol. 151, (2007), Elsevier Amsterdam · Zbl 1171.03001
[7] Ghilardi, S., Unification in intuitionistic logic, J. Symbolic Logic, 64, 859-880, (1999) · Zbl 0930.03009
[8] Ghilardi, S., Best solving modal equations, Ann. Pure Appl. Logic, 102, 183-198, (2000) · Zbl 0949.03010
[9] Ghilardi, S.; Sacchetti, L., Filtering unification and most general unifiers in modal logic, J. Symbolic Logic, 69, 879-906, (2004) · Zbl 1069.03011
[10] Iemhoff, R., A(nother) characterization of intuitionistic propositional logic, Ann. Pure Appl. Logic, 113, 161-173, (2001) · Zbl 0988.03045
[11] Iemhoff, R., On the admissible rules of intuitionistic propositional logic, J. Symbolic Logic, 66, 281-294, (2001) · Zbl 0986.03013
[12] Iemhoff, R., On the rules of intermediate logics, Arch. Math. Logic, 45, 581-599, (2006) · Zbl 1096.03025
[13] Iemhoff, R.; Metcalfe, G., Proof theory for admissible rules, Ann. Pure Appl. Logic, 159, 171-186, (2009) · Zbl 1174.03024
[14] Jansana, R., Propositional consequence relations and algebraic logic, (Zalta, E. N., The Stanford Encyclopedia of Philosophy, (2011), CSLI, Stanford University)
[15] Jeřábek, E., Admissible rules of modal logics, J. Logic Comput., 15, 411-431, (2005) · Zbl 1077.03011
[16] Jeřábek, E., Frege systems for extensible modal logics, Ann. Pure Appl. Logic, 142, 366-379, (2006) · Zbl 1101.03038
[17] Jeřábek, E., Complexity of admissible rules, Arch. Math. Logic, 46, 73-92, (2007) · Zbl 1115.03010
[18] Jeřábek, E., Independent bases of admissible rules, Log. J. IGPL, 16, 249-267, (2008) · Zbl 1146.03008
[19] Jeřábek, E., Canonical rules, J. Symbolic Logic, 74, 1171-1205, (2009) · Zbl 1186.03045
[20] Jeřábek, E., Substitution frege and extended frege proof systems in non-classical logics, Ann. Pure Appl. Logic, 159, 1-48, (2009) · Zbl 1173.03044
[21] Katětov, M., A theorem on mappings, Comment. Math. Univ. Carolin., 8, 432-433, (1967) · Zbl 0206.51901
[22] Kruskal, J. B., The theory of well-quasi-ordering: a frequently discovered concept, J. Combin. Theory Ser. A, 13, 297-305, (1972) · Zbl 0244.06002
[23] Rybakov, V. V., A criterion for admissibility of rules in the modal system S4 and the intuitionistic logic, Algebra Logic, 23, 369-384, (1984), translated from: Algebra Logika 23 (5) (1984) 546-572 · Zbl 0598.03013
[24] Rybakov, V. V., Equations in free Topoboolean algebra, Algebra Logic, 25, 109-127, (1986), translated from: Algebra Logika 25 (2) (1986) 172-204 · Zbl 0624.03007
[25] Rybakov, V. V., Logical equations and admissible rules of inference with parameters in modal provability logics, Studia Logica, 49, 215-239, (1990) · Zbl 0729.03012
[26] Rybakov, V. V., Problems of substitution and admissibility in the modal system grz and in intuitionistic propositional calculus, Ann. Pure Appl. Logic, 50, 71-106, (1990) · Zbl 0709.03009
[27] Rybakov, V. V., Admissibility of logical inference rules, Studies in Logic and the Foundations of Mathematics, vol. 136, (1997), Elsevier · Zbl 0872.03002
[28] Rybakov, V. V., Unifiers in transitive modal logics for formulas with coefficients (meta-variables), Log. J. IGPL, 21, 205-215, (2013) · Zbl 1278.03050
[29] Rybakov, V. V., Writing out unifiers for formulas with coefficients in intuitionistic logic, Log. J. IGPL, 21, 187-198, (2013) · Zbl 1277.03004
[30] Rybakov, V. V.; Kiyatkin, V. R.; Öner, T., On finite model property for admissible rules, Math. Log. Q., 45, 505-520, (1999) · Zbl 0938.03033
[31] Shoesmith, D. J.; Smiley, T. J., Multiple-conclusion logic, (1978), Cambridge University Press · Zbl 0381.03001
[32] Zakharyaschev, M., Canonical formulas for K4. part II: cofinal subframe logics, J. Symbolic Logic, 61, 421-449, (1996) · Zbl 0884.03014
[33] Zeman, J. J., Modal logic: the Lewis-modal systems, (1973), Oxford University Press · Zbl 0255.02014
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.