Семинары
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Календарь
Поиск
Регистрация семинара

RSS
Ближайшие семинары




Семинары отдела математической логики "Теория доказательств" и "Logic Online Seminar"
18 сентября 2023 г. 18:30, г. Москва, МИАН (ул. Губкина, 8), ауд. 313 + Zoom
 


Computational expressivity of (circular) proofs with fixed points

A. Das

University of Birmingham
Видеозаписи:
MP4 3,561.2 Mb

Количество просмотров:
Эта страница:159
Видеофайлы:50



Аннотация: We study the computational expressivity of proof systems with fixed point operators, within the ‘proofs-as-programs’ paradigm. We start with a calculus μ𝖫𝖩 (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, μ𝖫𝖩 admits a standard extension to a ‘circular’ calculus 𝖢μ𝖫𝖩.
Our main result is that, perhaps surprisingly, both μ𝖫𝖩 and 𝖢μ𝖫𝖩 represent the same first-order functions: those provably total in $\Pi^1_2-CA_0$, a subsystem of second-order arithmetic beyond the ‘big five’ of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points.
For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to $\Pi^1_2-CA_0$ (due to Möllerfeld). For the upper bound we construct a novel computability model in order to give a totality argument for circular proofs with fixed points. In fact we formalise this argument itself within $\Pi^1_2-CA_0$ in order to obtain the tight bounds we are after.
Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.
Based on joint work with Gianluca Curzi, https://arxiv.org/abs/2302.14825

Язык доклада: английский
 
  Обратная связь:
 Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024