The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals

DOI10.1007/s001530050105zbMath0920.03057OpenAlexW1981577462MaRDI QIDQ1267848

Thomas Strahm, Markus Marzetta

Publication date: 9 September 1999

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001530050105

zbMATH Keywords

cut-eliminationexplicit mathematicsproof-theoretic ordinalsasymmetric interpretationiterated fixed-point theory

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Metamathematics of constructive systems (03F50) Recursive ordinals and ordinal notations (03F15) Relative consistency and interpretations (03F25)

Related Items (6)

Theories with self-application and computational complexity. ⋮ The Operational Perspective: Three Routes ⋮ Universes in explicit mathematics ⋮ The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule ⋮ Systems of explicit mathematics with non-constructive \(\mu\)-operator and join ⋮ Universes over Frege structures

This page was built for publication: The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals