Witnessing flows in arithmetic

Result code in 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>

Result on the web

<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>

Result language

angličtina

Original language name

Witnessing flows in arithmetic

Original language description

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.

Czech name

—

Czech description

—

Type

J_imp - Article in a specialist periodical, which is included in the Web of Science database

CEP classification

—

OECD FORD branch

10101 - Pure mathematics

Project

—

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2024

Confidentiality

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

Name of the periodical

Mathematical Structures in Computer Science

ISSN

0960-1295

e-ISSN

1469-8072

Volume of the periodical

34

Issue of the periodical within the volume

7

Country of publishing house

GB - UNITED KINGDOM

Number of pages

37

Pages from-to

578-614

UT code for WoS article

001315748700001

EID of the result in the Scopus database

2-s2.0-85205112857