Witnessing flows in arithmetic

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F24%3A00601777" target="_blank" >RIV/67985840:_____/24:00601777 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.1017/S0960129524000185" target="_blank" >https://doi.org/10.1017/S0960129524000185</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1017/S0960129524000185" target="_blank" >10.1017/S0960129524000185</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Witnessing flows in arithmetic

Popis výsledku v původním jazyce

One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of an arithmetical theory by its proof-theoretic ordinal as a way to measure the time complexity of the functions. Unfortunately, the machinery is not sufficiently fine-grained to be applicable on the weak theories, on the one hand and to capture the bounded functions with bounded definitions of strong theories, on the other. In this paper, we develop such a machinery to address the bounded theorems of both strong and weak theories of arithmetic. In the first part, we provide a refined version of ordinal analysis to capture the feasibly definable and bounded functions that are provably total in PA +Uβ≺α TI(≺β), the extension of Peano arithmetic by transfinite induction up to the ordinals below α. Roughly speaking, we identify the functions as the ones that are computable by a sequence of PV-provable polynomial time modifications on an initial polynomial time value, where the computational steps are indexed by the ordinals below α, decreasing by the modifications. In the second part, and choosing l ≤ k, we use similar technique to capture the functions with bounded definitions in the theory T2k (resp. Sk2) as the functions computable by exponentially (resp. polynomially) long sequence of PVk−l+1-provable reductions between l-turn games starting with an explicit PVk−l+1-provable winning strategy for the first game.

Název v anglickém jazyce

Witnessing flows in arithmetic

Popis výsledku anglicky

One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of an arithmetical theory by its proof-theoretic ordinal as a way to measure the time complexity of the functions. Unfortunately, the machinery is not sufficiently fine-grained to be applicable on the weak theories, on the one hand and to capture the bounded functions with bounded definitions of strong theories, on the other. In this paper, we develop such a machinery to address the bounded theorems of both strong and weak theories of arithmetic. In the first part, we provide a refined version of ordinal analysis to capture the feasibly definable and bounded functions that are provably total in PA +Uβ≺α TI(≺β), the extension of Peano arithmetic by transfinite induction up to the ordinals below α. Roughly speaking, we identify the functions as the ones that are computable by a sequence of PV-provable polynomial time modifications on an initial polynomial time value, where the computational steps are indexed by the ordinals below α, decreasing by the modifications. In the second part, and choosing l ≤ k, we use similar technique to capture the functions with bounded definitions in the theory T2k (resp. Sk2) as the functions computable by exponentially (resp. polynomially) long sequence of PVk−l+1-provable reductions between l-turn games starting with an explicit PVk−l+1-provable winning strategy for the first game.

Druh

J_imp - Článek v periodiku v databázi Web of Science

CEP obor

—

OECD FORD obor

10101 - Pure mathematics

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Mathematical Structures in Computer Science

ISSN

0960-1295

e-ISSN

1469-8072

Svazek periodika

34

Číslo periodika v rámci svazku

7

Stát vydavatele periodika

GB - Spojené království Velké Británie a Severního Irska

Počet stran výsledku

37

Strana od-do

578-614

Kód UT WoS článku

001315748700001

EID výsledku v databázi Scopus

2-s2.0-85205112857