Geodesic
Strong conservativity and completeness for fragments of infinitary action logic
Sibirskie èlektronnye matematičeskie izvestiâ, Tome 21 (2024) no. 2, pp. 789-809 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

We study fragments of infinitary action logic, the algebraic logic of $*$-continuous residuated Kleene lattices, from the point of view of entailment from (possibly infinite) sets of hypotheses. The contribution of this article is twofold. First, we show, by establishing a cut normalisation result, that elementary fragments obtained by restricting the set of connectives are strongly conservative. This means that conservativity holds not just for pure derivability, but also for derivability from sets of hypotheses. This is proved in the presence of iterative divisions—compound connectives of a division and Kleene iteration in the denominator. Second, for the fragment with divisions, intersection, and iterative divisions, we prove strong completeness w.r.t. natural classes of models on language algebras and algebras of binary relations.
Keywords: infinitary action logic, conservativity, strong completeness. 
@article{SEMR_2024_21_2_a4,
     author = {S. L. Kuznetsov},
     title = {Strong conservativity and completeness for fragments of infinitary action logic},
     journal = {Sibirskie \`elektronnye matemati\v{c}eskie izvesti\^a},
     pages = {789--809},
     year = {2024},
     volume = {21},
     number = {2},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/SEMR_2024_21_2_a4/}
}
TY  - JOUR
AU  - S. L. Kuznetsov
TI  - Strong conservativity and completeness for fragments of infinitary action logic
JO  - Sibirskie èlektronnye matematičeskie izvestiâ
PY  - 2024
SP  - 789
EP  - 809
VL  - 21
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/SEMR_2024_21_2_a4/
LA  - en
ID  - SEMR_2024_21_2_a4
ER  - 
%0 Journal Article
%A S. L. Kuznetsov
%T Strong conservativity and completeness for fragments of infinitary action logic
%J Sibirskie èlektronnye matematičeskie izvestiâ
%D 2024
%P 789-809
%V 21
%N 2
%U http://geodesic.mathdoc.fr/item/SEMR_2024_21_2_a4/
%G en
%F SEMR_2024_21_2_a4
S. L. Kuznetsov. Strong conservativity and completeness for fragments of infinitary action logic. Sibirskie èlektronnye matematičeskie izvestiâ, Tome 21 (2024) no. 2, pp. 789-809. http://geodesic.mathdoc.fr/item/SEMR_2024_21_2_a4/

[1] H. Andréka, Sz. Mikulás, “Lambek calculus and its relational semantics: completeness and incompleteness”, J. Logic Lang. Inf., 3:1 (1994), 1–37 | DOI | MR | Zbl

[2] H. Andréka, Sz. Mikulás, “Axiomatizability of positive algebras of binary relations”, Algebra Univers., 66:1-2 (2011), 7–34 | DOI | MR | Zbl

[3] A. Beckmann, S. Buss, “Corrected upper bounds for free-cut elimination”, Theor. Comput. Sci., 412:39 (2011), 5433–5445 | DOI | MR | Zbl

[4] W. Buszkowski, “Compatibility of a categorial grammar with an associated category system”, Z. Math. Logik Grundlagen Math., 28 (1982), 229–238 | DOI | MR | Zbl

[5] W. Buszkowski, “On the complexity of the equational theory of relational action algebras”, Relations and Kleene Algebra in Computer Science, Lect. Notes Comput. Sci., 4136, ed. R.A. Schmidt, Springer, Berlin, 2006, 106–119 | DOI | MR | Zbl

[6] W. Buszkowski, “On action logic: equational theories of action algebras”, J. Log. Comput., 17:1 (2007), 199–217 | DOI | MR | Zbl

[7] W. Buszkowski, E. Palka, “Infinitary action logic: complexity, models and grammars”, Stud. Log., 89:1 (2008), 1–18 | DOI | MR | Zbl

[8] W. Buszkowski, “Lambek calculus and substructural logics”, Linguist. Analysis, 36:1–4 (2010), 15–48 http://buszko.home.amu.edu.pl/LCaSLpr.pdf

[9] N. Galatos, P. Jipsen, T. Kowalski, H. Ono, Residuated lattices: an algebraic glimpse at substructural logics, Studies in Logic and the Foundations of Mathematics, 151, Elsevier, Amsterdam, 2007 https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/151/ | MR | Zbl

[10] M. Kanovich, S. Kuznetsov, A. Scedrov, “Language models for some extensions of the Lambek calculus”, Inf. Comput., 287 (2022), 104760 | DOI | MR | Zbl

[11] S.C. Kleene, “Representation of events in nerve nets and finite automata”, Automata Studies, eds. C. Shannon, J. McCarthy, Princeton University Press, Princeton, 1956, 3–41 | DOI | MR

[12] D. Kozen, “On action algebras”, Logic and Information Flow, eds. J. van Eijck, A. Visser, MIT Press, 1994, 78–88 | DOI | MR

[13] W. Krull, “Axiomatische Begründung der allgemeinen Idealtheorie”, Sitzber. Phys.-Med. Soc. Erlangen, 56 (1924), 47–63 https://www.zobodat.at/pdf/Sitzber-physik-med-Soc-Erlangen_56-57_0047-0063.pdf | Zbl

[14] S. Kuznetsov, “$*$-continuity vs. induction: divide and conquer”, Advances in Modal Logic, 12, eds. G. Bezhanishvili et al., College Publications, London, 2018, 493–510 http://www.aiml.net/volumes/volume12/Kuznetsov.pdf | MR | Zbl

[15] S. Kuznetsov, “The ‘long rule’ in the Lambek calculus with iteration: undecidability without meets and joins”, Advances in Modal Logic, 13, eds. N. Olivetti et al., College Publications, London, 2020, 425–440 http://www.aiml.net/volumes/volume13/Kuznetsov.pdf | MR | Zbl

[16] S.L. Kuznetsov, N.S. Ryzhkova, “A restricted fragment of the Lambek calculus with iteration and intersection operations”, Algebra Logic, 59:2 (2020), 129–146 | DOI | MR | Zbl

[17] S.L. Kuznetsov, S.O. Speranski, “Infinitary action logic with exponentiation”, Ann. Pure Appl. Logic, 173:2 (2022), 103057 | DOI | MR | Zbl

[18] S. L. Kuznetsov, “Relational models for the Lambek calculus with intersection and constants”, Log. Methods Comput. Sci., 19:4 (2023), 32 | DOI | MR | Zbl

[19] S.L. Kuznetsov, “Syntactic concept lattice models for infinitary action logic”, Logic, Language, Information, and Computation, WoLLIC 2024, Lect. Notes Comput. Sci., 14672, eds. G. Metcalfe et al., Springer, Cham, 2024, 93–107 | DOI | MR

[20] J. Lambek, “The mathematics of sentence structure”, Amer. Math. Mon., 65:3 (1958), 154–170 | DOI | MR | Zbl

[21] Sz. Mikulás, “The equational theories of representable residuated semigroups”, Synthese, 192:7 (2015), 2151–2158 | DOI | MR | Zbl

[22] Sz. Mikulás, “Lower semilattice-ordered residuated semigroups and substructural logic”, Stud. Log., 103:3 (2015), 453–478 | DOI | MR | Zbl

[23] R. Moot, C. Retoré, The logic of categorial grammars. A deductive account of natural language syntax and semantics, Lecture Notes in Computer Science, 6850, Springer, Berlin, 2012 | DOI | MR | Zbl

[24] H. Ono, Y. Komori, “Logics without the contraction rule”, J. Symb. Log., 50:1 (1985), 169–201 | DOI | MR | Zbl

[25] E. Palka, “An infinitary sequent system for the equational theory of $*$-continuous action lattices”, Fundam. Inform., 78:2 (2007), 295–309 https://content.iospress.com/articles/fundamenta-informaticae/fi78-2-06 | DOI | MR | Zbl

[26] M. Pentus, “Models for the Lambek calculus”, Ann. Pure Appl. Logic, 75:1-2 (1995), 179–213 | DOI | MR | Zbl

[27] M. Pentus, “Free monoid completeness of the Lambek calculus allowing empty premises”, Proc. Logic Colloquium '96, Lect. Notes Log., 12, eds. M. Larrazabal et al., Springer, Berlin, 1998, 171–209 | DOI | MR | Zbl

[28] V. Pratt, “Action logic and pure induction”, JELIA 1990: Logics in AI, Lect. Notes Comput. Sci., 478, ed. J. van Eijck, Springer, Berlin etc., 1991, 97–120 | DOI | MR | Zbl

[29] I. Sedlár, “Iterative division in the distributive full non-associative Lambek calculus”, Dynamic Logic. New Trends and Applications, DALI 2019, Lect. Notes Comput. Sci., 12005, eds. L. Soares Barbosa et al., Springer, Cham, 2020, 141–154 | DOI | MR | Zbl

[30] G. Takeuti, Proof theory, 2nd ed., North-Holland, Amsterdam etc., 1987 | MR | Zbl

[31] M. Ward, R.P. Dilworth, “Residuated lattices”, Trans. Am. Math. Soc., 45 (1939), 335–354 | DOI | MR | Zbl