Organizer: Lev D. Beklemishev

Proof Theory seminar is a working seminar aimed, among others, at graduate and PhD students. The purpose of the seminar is to jointly look into the details of new or old but important results. Very often, talks extend to two consequtive meetings of the seminar (two academic hours each). The topics are not exclusively Proof Theory related, they include non-classical logics, modal logic and universal algebra, set theory, etc. The working language is mostly Russian, depending on the speaker and those in the audience.

Logic Online Seminar features online talks presented by international speakers on a broad range of Logic related topics. Logic Online Seminar is hosted by the Department of Mathematical Logic of Steklov Mathematical Institute. Logic Online Seminar has been established in 2014 and featured online talks by Sergei Artemov, Michael Rathjen, Stephen Simpson, Albert Visser, among others. Our working language is English.

Join our mailing lists: Mathlogic-Moscow, mailing lists of several seminars on Mathematical Logic (including the Proof Theory seminar) at Steklov Mathematical Institute of RAS, Moscow M.V. Lomonosov State University, and National Research University Higher School of Economics.

Logic Online Seminar, join this group if you only want to receive notifications about online talks of the Logic Online Seminar and possibly other online talks in English.

The login information to join the meetings of Logic Online Seminar is available via the mailing lists above.

Announcements

New place and time: Monday 16:00, Room 313, Steklov Mathematical institute + online.

The talks will be presented either online or in a mixed format. We will indicate if a speaker is online or onsite. In any case, it will be possible to join online.

28.01.2025 We will be joining the newly organized international Proof Society Seminar. Announcements will be published on this page and in the mailing lists of Logic Online Seminar.

04.02.2025 Due to techincal circumstances, we will have to use a new platform (Kontur Talk rather than Zoom) for the Logic Online Seminar meetings. It works from browser more or less like Zoom, no registration is requred. The links to join will be communicated via our mailing lists.

Forthcoming talks

Logic Online Seminar, Monday 16:00 MSK (UTC+3), MIAN Room 313 + Kontur Talk

15.12.2025, Proof Society Seminar, Anton Freund (University of Wuerzburg): Approaching Girard's functor Lambda

Girard has claimed that Pi^1_1-comprehension corresponds to his functor Lambda on dilators. He described a plausible proof around 1980, but it seems that details remain difficult. This talk presents joint work with Aguilera and Weiermann, in which we give a detailed proof that Pi^1_1-comprehension corresponds to a variant of Lambda, namely the functor J of Päppinghaus. No prior knowledge of dilators is assumed.

08.12.2025, Sergei Odintsov (Sobolev Institute of Mathematics, Novosibirsk)

Past talks

Recordings of past talks can be found at the bottom of this page

01.12.2025, M. Skopenkov (HSE University and KAUST): Incidences, tilings, and fields (online)

The master theorem, introduced independently by Richter-Gebert and by Fomin and the first author, provides a method for proving incidence theorems of projective geometry (more precisely, quasi-identities) using triangular tilings of surfaces. We investigate which incidence theorems over C and R can or cannot be proved via the master theorem. For this, we formalize the notion of a tiling proof. We introduce a hierarchy of classes of theorems based on the underlying topological spaces. A key tool is considering the same theorems over finite fields. This is a joint work with P. Pylyavskyy.

24.11.2025, jointly with S.I. Adian seminar, I.G. Lysenok (Steklov Mathematical Institute): A sample iterated small cancellation theory for groups of Burnside type

17.11.2025, Proof Society Seminar, Juliette Kennedy (University of Helsinki): How first order is first order logic?

27.10.2025 A.S. Morozov (Sobolev institute of mathematics): Representability of algebraic structures over reals

20.10.2025 D. Rogozin (continuation, online)

13.10.2025 D. Rogozin (Noeon Research, UK): Categorial models of linear type theory with subexponentials (online only, in Russian)

29.09.2025, 06.10.2025, jointly with S.I. Adian seminar, A.A. Gaifullin (Steklov Mathematical Institute): Finite generation of abelianizations of some automorphism groups (on site, in Russian)

22.09.2025 Sergei Artemov (Graduate Center CUNY): Representing and proving the consistency of PA in PA

15.09.2025, Logical Perspectives Open Lectures

08.09.2025, Logical Perspectives Open Lectures

25.08.2025 V.L. Selivanov (St. Petersburg State Univ.): On constructive variants of Wadge reducibility (onsite, in Russian)

4.08.2025 M. Zhukovskii (University of Sheffield): First-order complexity of random finite structures (onsite, in Russian)

7.07.2025 Fedor Pakhomov (Steklov Mathematical institute and Ghent University): Reflection calculi and linearity: fragments of the theory of bar-induction (onsite, in Russian)

16.06.2025, 16:00, jointly with S.I. Adian seminar, I.A. Dynnikov (Steklov Mathematical Institute): Algorithmic comparison of Legendrian knots (onsite, in Russian)

2.06.2025, 17:00, jointly with S.I. Adian seminar, O.V. Sipacheva (MSU): Topological universal algebra: a symbiosis of algebra and topology (onsite, in Russian)

19.05.2025 Mikhail Panov (HSE University, St. Petersburg): Epistemic Model with Boundedly Rational Players (onsite, in Russian)

12.05.2025, jointly with S.I. Adian seminar, Vladimir Podolskii (Steklov Mathematical Institute and Tufts University): Randomized Lifting to Semi-Structured Communication Complexity

28.04.2025, Proof Society Seminar, 13:00 UTC (16:00 MSK), Stepan Kuznetsov (Steklov Mathematical Institute): Circular and infinitary proofs for complexity analysis of action logic (online)

21.04.2025 Anna Dmitrieva (U. of East Anglia): Complex field with quasiminimal structure (online)

14.04.2025 L. D. Beklemishev: Fragments of arithmetic and cyclic proofs (onsite)

07.04.2025 Yanjing Wang (Peking University): Knowing how to understand intuitionistic logic (and its relatives)

24.03.2025 V.L. Selivanov, I.V. Smirnov (SPb State University): Ordinal invariants of homomorphic quasiorders of k-labelled forests (online)

10.03.2025 Tikhon Pshenitsyn (MIAN, postgraduate): Intuitionistic First-Order Linear Logic and Hypergraph Languages (onsite)

03.03.2025, Proof Society Seminar, 13:00 UTC (16:00 MSK), Henry Towsner (University of Pennsylvania): Proofs that Modify Proofs (online)

24.02.2025 Denis I. Saveliev (MIPT): On relations between Rudin–Keisler and Comfort preorders, part I (onsite)

17.02.2025, jointly with S.I. Adian seminar, Alexei Miasnikov (Stevens Institute of Technology): First-order classification, non-standard models, and interpretations

10.02.2025 Alexandar Perović (Beograd, Srbija): Beyond the class of locally finite height Kripke models for provability logic (online)

03.02.2025, Proof Society Seminar, 13:00 UTC (16:00 MSK) Jeremy Avigad (Carnegie Mellon University): Verifying Proofs on Blockchain

23.12.2024 Mikhail Valinkin (MSU), Stepan Kuznetsov (MI RAS): Relational models for the Lambek calculus with the local contraction subexponential (onsite, in Russian).

16.12.2024 Alexei Kanel-Belov (Bar Ilan, MIPT, MSU): Algorithmic undecidability of the problem of embeddability of algebraic varieties (onsite, in Russian)

02.12.2024 Wei Wang (Sun Yat-sen University, Guangzhou): Definable Combinatorial Principles in Fragments of Arithmetic (online)

25.11.2024 Johan van Benthem (Stanford, Tsinghua University, University of Amsterdam): Two Perspectives on Recursion and Induction: Modal Provability Logic and Fixed-Point Logics (online)

28.10.2024 Maxim Vishnikin (MSU): Expressive power of categorial grammars with unique category assignment (onsite, in Russian)

21.10.2024 Carlos Zapata-Carratalá (Society for Multidisciplinary and Fundamental Research; Wolfram Foundation): Higher-arity algebras and hypergraphs (online)

07.10.2024 Lev Dvorkin (MSU, 6 year): On interpretations of normal modal logics and additive formulas in S4, S5, Grz, K and GL. (onsite, in Russian)

30.09.2024 V.I. Danilov (CEMI, Moscow): Magari algebras and Plott choice functions (onsite, in Russian)

23.09.2024 V. B. Shehtman (HSE University, Moscow): Completeness for predicate modal logics (onsite)

16.09.2024 Maxim Zubkov (Kazan Federal University): Computable linearly ordered structures (onsite, in Russian)

27.05.2024 A.V. Kudinov (IITP RAS, HSE): Complexity of non-normal logics and the logics with counting of axioms applications (onsite, in Russian)

21.05.2024 jointly with S.I. Adian seminar. David Fernández-Duque (Univeristy of Barcelona): Provable well-orders and hyperarithmetical soundness (online)

13.05.2024 Ali Enayat (Gothenburg University): Categoricity-like properties in the first order realm (online)

22.04.2024 Ilya Shapirovsky (New Mexico and IITP): Filtrations of some pretransitive logics (online, in Russian)

15.04.2024 Saeed Salehi (Tabriz University): How (not) to compute the halting probability or validate the heuristic principle (online)

01 and 08.04.2024 N. Bazhenov (Novosibirsk State University), I. Kalimullin (Kazan Federal University): Punctual structures, automatic structures and index sets (onsite + Zoom).

25.03.2024 S.O. Speranski (Steklov Mathematical Institute): On the elementary theory of atomless probability spaces. Onsite talk, in Russian.

11.03.2024 D. Shamkanov (Steklov Mathematical Institute) and P. Razumny (MIPT). On the extension of the modal predicate logic QGL by non-wellfounded derivations (onsite talk, in Russian)

11.03.2024 S. Kuznetsov (Steklov Mathematical Institute): Undecidability of the theory of Kleene algebras with commutativity conditions

04.03.2024 Taishi Kurahashi (Kobe University): Modal logics of provability predicates

26.02.2024 Vseslav Sekorin (Tver State University): On the expressivity properties of partial fixed point operator for finite and infinite systems. Onsite talk, in Russian.

12.02 and 19.02.2024 Lev Dvorkin (Moscow State University): On the finite model property of a class of pretransitive logics. Onsite talk, in Russian.

18.12.2023 Zoran Ognjanović (Matematički institut SANU, Beograd, Srbija): Logics with Probability Operators. Completeness and Decidability. Online talk.

04.12 and 11.12.2023 Juan Aguilera (Vienna University of Technology): Dilators and $\Pi_2^1$-ordinal analysis (continuation)

27.11.2023 jointly with S.I. Adian seminar, 14:00 MSK (UTC+3). Bakhadyr Khoussainov (Computer Science School, The UESTC, China): On finitely presented expansions of semigroups, groups, and algebras. Online talk.

20.11.2023 Sergei Slavnov (HSE University): The logic of tensor terms for categorial grammars: a simple union of commutative and noncommutative operations of linear logic. Оnsite talk.

6.11.2023 Juan Aguilera (Vienna University of Technology): Dilators and $\Pi_2^1$-ordinal analysis

23.10.2023 Sergei Odintsov (Sobolev Institute of Mathematics, Novosibirsk): Constructive logic N4 and connexive logic C: similarities and differences

16.10.2023 Matthias Baaz (Vienna University of Technology): Andrews skolemization may shorten proofs non-elementarily

02.10.2023 L. Beklemishev and Y. Wang (Peking University): General topological frames for polymodal provability logic based on periodic sets of ordinals

25.09.2023 N. Lukashov (HSE University, Master's student): On the unification problem for polymodal provability logic

18.09.2023 Anupam Das (University of Birmingham): Computational expressivity of (circular) proofs with fixed points

23.05.2023 Juan Aguilera (Vienna, Gent, Hamburg): Non-linearities in the analytical hierarchy

16.05.2023 A.L. Semenov (MSU): Examples and problems for definability lattices (in Russian)

18.04.2023 S.L. Kuznetsov (Steklov Mathematical Institute): Algorithmic problems for substructural logics with Kleene iteration (in Russian)

11.04.2023 Iskander Kalimullin (Kazan State Federal University): The degrees of relative computable categoricity

4.04.2023 Nikolai Bazhenov (Sobolev Institute of Mathematics, Novosibirsk): Learning for families of algebraic structures

20.03 and 27.03.2023 Fedor Pakhomov (Steklov Mathematical Institute and Ghent University): Dilators, Reflection, and Forcing: A Proof-Theoretic Analysis of Π¹₁-CA₀.

06.03.2023 Mikhail Rybakov (Tver State University and IITP RAS): Computational complexity of non-classical logics of an unary predicate.

13.02.2023 and 20.02.2023 Martin Ziegler (KAIST, Korea): Bit-Complexity of Classical Solutions of Linear Evolutionary Systems of Partial Differential Equations

12.12.2022 Silvia Ghilezan (University of Novi Sad & Mathematical Institute SASA, Serbia): Kripke-style semantics in typed lambda calculus, combinatory logic and more.

05.12.2022 Carl-Fredrik Nyberg-Brodda (Université Gustave Eiffel, Paris): The Dehn functions of a class of one-relation monoids

28.11.2022 Valentin Shehtman (IITP, HSE, MSU): Simplicial models for modal predicate logics.

21.11.2022 Fedor Pakhomov (Steklov Mathematical Institute and Ghent University): How to escape Tennenbaum's Theorem?

14.11.2022 Andrei Kudinov (IITP RAS): On Strictly Positive Fragments of Modal Logics with Confluence.

07-11.11.2022 Second Conference of Russian Mathematical Centers. Section "Mathematical Logic and Theoretical Computer Science".

31.10.2022 Lev Beklemishev (Steklov Mathematical Institute): On Kreisel's explication of the concept of finitism. Lecture at the conference Formal Philosophy 2022 at the traditional time of the seminar.

17.10.2022 and 24.10.2022 Daniyar Shamkanov (Steklov Mathematical Institute): On cyclic proofs in classical first order arithmetic with inductive definitions. (in Russian)

10.10.2022 Arnon Avron (Tel Aviv): The Active Role of Language Extensions in Mathematical Reasoning.

03.10.2022 Konstantin Kovalev (MIPT): On the fragments of Peano arithmetic with quantifier-free induction schema (in Russian).

25.09.2022 Lev Dvorkin (MSU): On the provability logic of Niebergall's arithmetic (in Russian).

20.06.2022 Mojtaba Mojtahedi (Tehran): On provability logic of HA (continuation).

06.06.2022 Marta Fiori Carones (Sobolev Institute of Mathematics): The strength of some consequences of RT$^2_2$ over RCA$_0^*$.

30.05.2022 and 02.06.2022 Mojtaba Mojtahedi (Tehran): On provability logic of HA.

23.05.2022 Alexander Zapryagaev (HSE): Interpretations of Büchi arithmetics in themselves.

16.05.2022 Denis I. Saveliev (IITP RAS): On modal logics of model-theoretic relations

25.04.2022 Anupam Das (University of Birmingham): A circular version of Gödel's T and its abstraction complexity

18.04.2022 Sergei Dudakov (Tver State University): Algorithmic properties of algebras of subsets/Алгоритмические свойства алгебр подмножеств

11.04.2022 Alexander Kozachinsky (Steklov Mathematical Institute): Population protocols and Presburger arithmetic.

04.04.2022 Vladimir Kanovei (IITP RAS): Some definable counterexamples in models of set theory.

28.03.2022 Lev Beklemishev (Steklov Mathematical Institute): Reading Kreisel: what we do (not) understand

14.03.2022 Lev Beklemishev (Steklov Mathematical Institute): Conservativity spectra and generalized Ignatiev model

21.02.2022 Anastasia Onoprienko (Lomonosov Moscow State University): On topological models of logics HC and H4.

14.02.2022 Igor Sedlár (Czech Academy of Sciences, Institute of Computer Science): Substructural Logics of Programs

07.02.2022 Tikhon Pshenitsyn (Lomonosov Moscow State University): Hypergraph generalisation of the Lambek calculus and operations expressible in it.

20.12.2021 Albert Visser (Universiteit Utrecht): Interpreters as consistoids (continuation)

06.12.2021 Thomas Icard (Stanford University): Logical foundations of causal inference

22.11.2021 Albert Visser (Universiteit Utrecht): Interpreters as consistoids

15.11.2021 Michael Mendler (Universität Bamberg): The Došen Square under construction: A tale of four modalities

08.11.2021 Konstantin Kovalev (Moscow Institute of Physics and Technology): Models of quantifier-free induction for the language of arithmetic with exponentiation (in Russian)

25.10.2021 James Walsh (Cornell University): An incompleteness theorem via ordinal analysis

18.10.2021 Misha Svyatlovsky (Moscow Institute of Physics and Technology): Strictly positive fragments of K4 and its extensions

11.10.2021 Mateusz Łełyk (Department of Philosophy, University of Warsaw): The two halves of disjunctive correctness for the compositional truth predicate

04.10.2021 Victor L. Selivanov (IIS SB RAS and Novosibirsk State University): Primitive Recursive Ordered Fields and Some Applications

7-11.06.2021: Logical Perspectives 2021 Conference, для участия регистрируйтесь на сайте конференции.

24.05.2021 I.B. Shapirovsky (IITP RAS and New Mexico State University): On finite model property and complexity of logics of sums of Kripke frames (in Russian)

12.04.2021 Fedor N. Pakhomov (University of Ghent and Steklov Mathematical Institute): Generalized Fusible Numbers

22.03.2021 Joost J. Joosten (University of Barcelona): Quantified reflection calculus with one modality is decidable

15.03.2021 Wesley H. Holliday (University of California, Berkeley): Logics of Imprecise Comparative Probability

01.03.2021 Maxim Vishnikin (MSU): Basic categorial grammars with unique type assignments (in Russian)

15.02.2021 Wei Chen (Huawei, Edinburgh): Automated Mathematical Theorem Proving

18.01.2021 Rosalie Iemhoff (University of Utrecht): The role of uniform interpolation in structural proof theory

21.12.2020 Albert Visser (Utrecht University): Cyclic Henkin Logic (continuation)

14.12.2020 Albert Visser (Utrecht University): Cyclic Henkin Logic

07.12.2020 Tadeusz Litak (Friedrich-Alexander Universität Erlangen-Nürnberg): Describable Nuclei, Negative Translations and Extension Stability (continuation)

30.11.2020 Tadeusz Litak (Friedrich-Alexander Universität Erlangen-Nürnberg): Describable Nuclei, Negative Translations and Extension Stability

23.11.2020 Guram Bezhanishvili (New Mexico State University): Modal operators on rings of continuous functions: A generalization of Gelfand and Jonsson-Tarski dualities

17-18.11.2020 Logical Perspectives Open Lectures: Yuri Gurevich, Anil Nerode, Barbara Partee.

09.11.2020 Christian Wurm (HHU Düsseldorf): Language-theoretic models for the Full Lambek calculus

02.11.2020 Anna Dmitrieva (ILLC, University of Amsterdam): Axiomatizing Origami planes

27.10.2020 S.I. Adian Seminar, 18:30 MSK (UTC+3), A.A. Razborov (University of Chicago and Steklov Mathematical Institute): SAT Solvers and Ordered Decision Strategies

26.10.2020 Stepan Kuznetsov (Steklov Mathematical Institute): Decidable fragments of the Lambek calculus with subexponentials

19.10.2020 Fedor Pakhomov (Steklov Mathematical Institute and University of Ghent): Iterated ω-model reflection and Π¹₂ proof-theoretic analysis

12.10.2020 Ali Enayat (University of Gothenburg): Set theory with a proper class of indiscernibles

Seminar organizer
Beklemishev Lev Dmitrievich

Financial support
The seminar 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