#матлог #учёба #спецсеминар #не_мехмат #МИАН #ТД

Дорогие участники Logic Online Seminar (https://www.mathnet.ru/eng/conf876), в ближайший понедельник мы присоединяемся к Proof Society Seminar (https://www.proofsociety.org/activities-and-resources/proof-society-seminar/), где выступит Степан Кузнецов.

The Proof Society Seminar presents talks by leading researchers in proof theory and from all areas of logic related to proofs. The talks take place online via Zoom, usually on Mondays, approximately once per month. They start at 13:00 UTC and may last up to 75 minutes plus questions.

28 April 2025, 13:00 UTC

Speaker: Stepan Kuznetsov (Steklov Mathematical Institute of RAS, https://homepage.mi-ras.ru/~sk/)

Title: Circular and infinitary proofs for complexity analysis of action logic

Abstract: Action logic is the extension of the full Lambek calculus (intuitionistic-style non-commutative substructural logic) with the operation of Kleene iteration. The natural algebraic semantics for action logic is given by residuated Kleene lattices (RKLs). Action logic appears in two variants: the logic of all RKLs (action logic itself), with an inductive axiomatisation for iteration, and a stronger infinitary system, where iteration is governed by an omega-rule. The latter corresponds to the natural subclass of *-continuous RKLs. In this talk, we discuss how calculi with circular and infinitary proofs help analyse algorithmic complexity for theoremhood and entailment from hypotheses in action logic and its infinitary extension. Namely, using circular proofs we show \Sigma^0_1-completeness of action logic. The theoremhood problem in infinitary action logic is \Pi^0_1-complete. For entailment from *-free hypotheses in the latter, we get an \omega^\omega upper bound on the closure ordinal (for the system with an omega-rule) and the corresponding hyperarithmetical complexity bound, which is actually exact. Finally, entailment from arbitrary hypotheses in infinitary action logic is \Pi^1_1-complete, the closure ordinal being \omega_1^{CK}.

Partially based on joint work with Tikhon Pshenitsyn and Stanislav Speranski.

➰ ВК