Functorial bounds for cut elimination inL βω . I

DOI10.1007/BF02007146zbMath0558.03026OpenAlexW4255129992MaRDI QIDQ3222838

Marie-Christine Ferbus

Publication date: 1984

Published in: Archiv für Mathematische Logik und Grundlagenforschung (Search for Journal in Brave)

Full work available at URL: https://eudml.org/doc/138028

zbMATH Keywords

infinitary rulefunctorial boundsfunctorial logiclogic with infinite conjunctionsmajorization treesordinal bounds

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Related Items (2)

Functorial bounds for cut elimination inL βω . II ⋮ Cut-elimination and interpolation for \(\Omega\)-logic

Cites Work

• Set recursion and \(\Pi ^ 1_ 2\)-logic
• Functors and ordinal notations. I: A functorial construction of the veblen hierarchy
• Π12-logic, Part 1: Dilators

This page was built for publication: Functorial bounds for cut elimination inL βω . I