The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
type: Item
instance of: scholarly article
title: The \(\mu\) quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
zbMATH Open document ID: 0920.03057
author: Markus Marzetta
author: Thomas Strahm
published in: Archive for Mathematical Logic
publication date: 1999-09-09T00:00:00Z
review text: The authors deal with two species of systems, \(\text{UTN}_n\)'s and \(\widehat{\text{ID}\Omega}_k\)'s, and determine their relations and proof-theoretic ordinals. The first is a type of ``explicit mathematics'', and ``\( \text{UTN}_n\)'' stands for ``universes \((n\) of them), types, and names''. A further axiom is (Lim), saying ``every type belongs to a universe'', and a non-constructive operation symbol \(\mu\) is added sometimes. \(\widehat {\text{ID} \Omega}_k\) is the system of iterated fixed-point theory with ordinals introduced in \(k\) stages. (The circumflex indicates that infinitary rules are used.) By comparing these and other systems like \(\text{ATR}_0\) and \((\Pi_1^0-\text{CA})_{<\gamma_n}\) by means of translations, the authors establish the main results: \(\text{UTN}_k\equiv\widehat{\text{ID}\Omega}_k\) and \(\text{UTN}_k +(\mu) \equiv\widehat {\text{LD} \Omega}_{k+1}\), and their ordinals are \(\gamma_k\) and \(\gamma_{k+1}\), respectively. And as is expected, \(\text{UTN}+ (\text{Lim}) \equiv\bigcup_k \text{UTN}_k\). The main tools used are proof-theoretic ones, namely cut-elimination and asymmetric interpretation. Technically, this paper is self-contained, as the syntax, axioms and definitions are stated. Also, further results are indicated.
Mathematics Subject Classification ID: 03F25
Mathematics Subject Classification ID: 03F50
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F15
zbMATH DE Number: 1210624
zbMATH Keywords: explicit mathematics
zbMATH Keywords: proof-theoretic ordinals
zbMATH Keywords: iterated fixed-point theory
zbMATH Keywords: cut-elimination
zbMATH Keywords: asymmetric interpretation
MaRDI profile type: Publication
full work available at URL: s001530050105
OpenAlex ID: W1981577462
DOI: 10.1007/S001530050105
Recommended article: The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule
Recommended article: On the universal and existential fragments of the \(\mu\)-calculus
Recommended article: Q4417913
Recommended article: Q5111208
Recommended article: $\aleph_1$ and the modal $\mu$-calculus
Recommended article: Systems of explicit mathematics with non-constructive \(\mu\)-operator. I
Recommended article: From Mathesis Universalis to Fixed Points and Related Set-Theoretic Concepts
Recommended article: On closure ordinals for the modal mu−calculus
Recommended article: An infinitary treatment of full \(\mu\)-calculus
Recommended article: About the proof-theoretic ordinals of weak fixed point theories
description: scientific article; zbMATH DE number 1210624