Substructural logics are logical systems which disallow all or some of the structural rules: weakening, permutation, contraction. These logical systems have various applications. They are used to model reasoning about limited resources: if a formula $A$ denotes a resource, it is not equivalent to "$A \mbox{ and } A$," that is, the contraction rule is not valid.

Non-commutative substructural logics (those without the permutation rules) are used to describe natural language syntax, where word order matters. Logics without the weakening rule (if $A$, then $B \to A$ for any $B$) are called relevant ones, and these logics model arguments where all premises should be essentially used. Thus, these logics exclude arguments which are classically valid, but weird from the natural language point of view, e.g., "If it will rain tomorrow, then $2+2 = 4$." In this course, we plan to give a general overview of substructural logics and present several most interesting results concerning these unusual logical systems.

Programme

1. Sequent calculi for substructural logics: the multiplicative-additive Lambek calculus and its extensions. Algebraic semantics: residuated lattices.
2. PSPACE-completeness of the derivability problem for the multiplicative-additive Lambek calculus.
3. Roorda's interpolation lemma for the Lambek calculus. Pentus' theorem about Lambek grammars and context-free grammars. A counter-example to Pentus' theorem in the commutative case.
4. Andréka – Mikulás' completeness theorem for the Lambek calculus w.r.t. models on algebras of binary relations.
5. The distributive multiplicative-additive Lambek calculus (Kozak's system), its algorithmic decidability and the finite model property.
6. Girard's linear logic. Conservativity of classical linear logic over the intuitionistic one (in the absence of constant "zero").
7. Algorithmic undecidability of linear logic and its non-commutative multiplicative-exponential variant.
8. Relevant logical systems; Urquhart's results on their algorithmic undecidability.
9. Non-associative Lambek, its ternary semantics, a polynomial algorithmic for the derivability problem.
10. The Lambek calculus with Kleene iteration ("action logic") and its infinitary version. Algorithmic undecidability results.

Lecturers
Kuznetsov Stepan Lvovich
Pshenitsyn Tikhon Grigor'evich

Financial support
The course is supported by the Ministry of Science and Higher Education of the Russian Federation (the grant to the Steklov International Mathematical Center, agreement no. 075-15-2022-265).

Institutions
Steklov Mathematical Institute of Russian Academy of Sciences, Moscow
Steklov International Mathematical Center