Wider systems for linear logic with fixed points: proof theory and complexity

Anupam Das; Tikhon Pshenitsyn

doi:10.48550/arXiv.2602.10280

Wider systems for linear logic with fixed points: proof theory and complexity

Anupam Das
, Tikhon Pshenitsyn

Computer Science

Research output: Working paper/Preprint › Preprint

Abstract

We investigate infinitary wellfounded systems for linear logic with fixed points, with transfinite branching rules indexed by some closure ordinal α for fixed points. Our main result is that provability in the system for some computable ordinal α is complete for the ω^{α^ω} level of the hyperarithmetical hierarchy. To this end we first develop proof theoretic foundations, namely cut elimination and focussing results, to control both the upper and lower bound analysis. Our arguments employ a carefully calibrated notion of formula rank, calculating a tight bound on the height of the (cut-free) proof search space.

Original language	English
Publisher	arXiv
DOIs	https://doi.org/10.48550/arXiv.2602.10280
Publication status	Published - 10 Feb 2026

Access to Document

10.48550/arXiv.2602.10280Licence: Creative Commons: Attribution (CC BY)

2602.10280v1Other version, 642 KBLicence: Creative Commons: Attribution (CC BY)

Cite this

@techreport{721b0cdef3e84140b51d50c3945ccd3f,

title = "Wider systems for linear logic with fixed points: proof theory and complexity",

abstract = "We investigate infinitary wellfounded systems for linear logic with fixed points, with transfinite branching rules indexed by some closure ordinal α for fixed points. Our main result is that provability in the system for some computable ordinal α is complete for the ω\textasciicircum{}\{α\textasciicircum{}ω\} level of the hyperarithmetical hierarchy. To this end we first develop proof theoretic foundations, namely cut elimination and focussing results, to control both the upper and lower bound analysis. Our arguments employ a carefully calibrated notion of formula rank, calculating a tight bound on the height of the (cut-free) proof search space.",

author = "Anupam Das and Tikhon Pshenitsyn",

year = "2026",

month = feb,

day = "10",

doi = "10.48550/arXiv.2602.10280",

language = "English",

publisher = "arXiv",

type = "WorkingPaper",

institution = "arXiv",

}

TY - UNPB

T1 - Wider systems for linear logic with fixed points

T2 - proof theory and complexity

AU - Das, Anupam

AU - Pshenitsyn, Tikhon

PY - 2026/2/10

Y1 - 2026/2/10

N2 - We investigate infinitary wellfounded systems for linear logic with fixed points, with transfinite branching rules indexed by some closure ordinal α for fixed points. Our main result is that provability in the system for some computable ordinal α is complete for the ω^{α^ω} level of the hyperarithmetical hierarchy. To this end we first develop proof theoretic foundations, namely cut elimination and focussing results, to control both the upper and lower bound analysis. Our arguments employ a carefully calibrated notion of formula rank, calculating a tight bound on the height of the (cut-free) proof search space.

AB - We investigate infinitary wellfounded systems for linear logic with fixed points, with transfinite branching rules indexed by some closure ordinal α for fixed points. Our main result is that provability in the system for some computable ordinal α is complete for the ω^{α^ω} level of the hyperarithmetical hierarchy. To this end we first develop proof theoretic foundations, namely cut elimination and focussing results, to control both the upper and lower bound analysis. Our arguments employ a carefully calibrated notion of formula rank, calculating a tight bound on the height of the (cut-free) proof search space.

U2 - 10.48550/arXiv.2602.10280

DO - 10.48550/arXiv.2602.10280

M3 - Preprint

BT - Wider systems for linear logic with fixed points

PB - arXiv

ER -

Wider systems for linear logic with fixed points: proof theory and complexity

Abstract

Access to Document

Fingerprint

Cite this