Seminars
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
Calendar
Search
Add a seminar

RSS
Forthcoming seminars




Seminars "Proof Theory" and "Logic Online Seminar"
September 25, 2023 18:30, Moscow, Steklov Mathematical Institute (8 Gubkina), room 313 + Zoom
 


On the unification problem for polymodal provability logic

N. Lukashov

HSE University, Moscow
Video records:
MP4 3,933.7 Mb

Number of views:
This page:109
Video files:30



Abstract: The unification problem for a given modal logic is closely related to the problem of characterization of its admissible rules. It is well-known that GL has the finitary unification type (S. Ghilardi), the problem of admissibility of rules is decidable (V.V. Rybakov), and its admissible rules admit a natural axiomatization (E. Jerabek). For the polymodal provability logic GLP, even for the language with just two modalities, these questions mostly remain open.
We show that the fragment J of GLP (in the laguage with finitely many modalities) has a finitary unification type, that is, the set of unifiers of any formula is generated by finitely many maximal ones. At the same time, the unification type of GLP itself (in the language with just two modalities) is nullary, that is, there is a unifiable formula whose set of unifiers does not have a maximal one.
Joint work with L. Beklemishev.
 
  Contact us:
 Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024