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

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.