In this work, we prove the undecidability (and Σ⁰₁-completeness) of several theories of semirings with fixed points. The generality of our results stems from recursion theoretic methods, namely the technique of effective inseparability. Our result applies to many theories proposed in the literature, including Conway μ-semirings, Park μ-semirings, and Chomsky algebras.

Abstract Kleene algebras are an algebraic abstraction of regular expressions, one of the central notions in computer science. While the equational theory of Kleene algebras is known to be decidable, reasoning from finite sets of hypotheses (Horn theory) quickly becomes undecidable. This happens even for simple classes of hypotheses which themselves do not involve Kleene star. One of such classes of hypotheses is formed by sum-of-letters hypotheses, of the form $$a \le b_1 + \ldots + b_k$$ a ≤ b 1 + … + b k , where $$a, b_1, \ldots , b_k$$ a , b 1 , … , b k are letters. In the present paper, we strengthen the undecidability result proved for this class of hypotheses by Doumane et al. (2019) and establish the exact complexity— $$\varSigma ^0_1$$ Σ 1 0 -completeness. Moreover, we strengthen our result and show the same complexity bounds for one fixed set of sum-of-letters hypotheses. We also accompany this result with a decidability one, for comparison.

Abstract The linguistic applications of the Lambek calculus suggest its semantics over algebras of formal languages. A straightforward approach to construct such semantics indeed yields a brilliant completeness theorem (Pentus 1995, Ann. Pure Appl. Logic, 75, 179–213). However, extending the calculus with extra operations ruins completeness. In order to mitigate this issue, Wurm (2017, J. Logic Lang. Inf., 26, 179–214) introduced a modification of this semantics, namely, models over syntactic concept lattices. We extend this semantics to the infinitary extension of the Lambek calculus with Kleene iteration (infinitary action logic), prove strong completeness and some interesting corollaries. We also discuss issues arising with constants—zero, unit, top—and provide some strengthenings of Wurm’s results towards including these constants into the systems involved.

We consider relational semantics (R-models) for the Lambek calculus extended with intersection and explicit constants for zero and unit. For its variant without constants and a restriction which disallows empty antecedents, Andreka and Mikulas (1994) prove strong completeness. We show that it fails without this restriction, but, on the other hand, prove weak completeness for non-standard interpretation of constants. For the standard interpretation, even weak completeness fails. The weak completeness result extends to an infinitary setting, for so-called iterative divisions (Kleene star under division). We also prove strong completeness results for product-free fragments.

Abstract We prove undecidability and pinpoint the place in the arithmetical hierarchy for commutative action logic, i.e. the equational theory of commutative residuated Kleene lattices (action lattices), and infinitary commutative action logic, the equational theory of *-continuous commutative action lattices. Namely, we prove that the former is $\varSigma _1^0$-complete and the latter is $\varPi _1^0$-complete. Thus, the situation is the same as in the more well-studied non-commutative case. The methods used, however, are different: we encode infinite and circular computations of counter (Minsky) machines.

Action logic is the algebraic logic (inequational theory) of residuated Kleene lattices. One of the operations of this logic is the Kleene star, which is axiomatized by an induction scheme. For a stronger system that uses an -rule instead (infinitary action logic), Buszkowski and Palka (2007) proved -completeness (thus, undecidability). Decidability of action logic itself was an open question, raised by Kozen in 1994. In this article, we show that it is undecidable, more precisely, -complete. We also prove the same undecidability results for all recursively enumerable logics between action logic and infinitary action logic, for fragments of these logics with only one of the two lattice (additive) connectives, and for action logic extended with the law of distributivity.

Abstract The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality while keeping Lambek’s restriction. Interestingly enough, we show that for any system equipped with a reasonable exponential modality the following holds: if the system enjoys cut elimination and substitution to the full extent, then the system necessarily violates Lambek’s restriction. Nevertheless, we show that two of the three conditions can be implemented. Namely, we design a system with Lambek’s restriction and cut elimination and another system with Lambek’s restriction and substitution. For both calculi, we prove that they are undecidable, even if we take only one of the two divisions provided by the Lambek calculus. The system with cut elimination and substitution and without Lambek’s restriction is folklore and known to be undecidable.

We prove algorithmic undecidability of the (in)equational theory of residuated Kleene lattices (action lattices), thus solving a problem left open by D. Kozen, P. Jipsen, W. Buszkowski.

Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organised as sets and multisets of formulae not being possible to organise formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.