The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule (Q1577487): Difference between revisions
From MaRDI portal
Created a new Item |
Added link to MaRDI item. |
||
links / mardi / name | links / mardi / name | ||
Revision as of 01:34, 1 February 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule |
scientific article |
Statements
The non-constructive \(\mu\) operator, fixed point theories with ordinals, and the bar rule (English)
0 references
16 July 2001
0 references
The author considers a first-order applicative theory \(\text{AutBON}(\mu)\), and shows that it is proof-theoretically equivalent to predicative analysis, hence its proof-theoretical ordinal is Schütte-Feferman's \(\Gamma_0\). Here, BON stands for the basic theory of operations and numbers (Feferman et al.), and \(\mu\) is the unbounded (hence non-constructive) minimum operator. Further, this theory has the inductiion scheme, and the bar rule: infer \(\text{TI}(\prec,A)\) from \(\text{TI}(\prec, U)\), where \(U\) is a unary predicate variable, \(A\) is any formula, \(\prec\) is a recursive binary relation, and TI expresses transfinite induction. The method of proof is standard: \(\Aut(\Pi^1_0)\) is interpreted in the theory in question to give the lower bound, and the theory is, in turn, interpreted in \(\text{PA}^w_\Omega+ (\text{Subst})\) for the upper bound. Here, \(\Aut(\Pi^1_0)\) is second-order arithmetic with autonomously iterated \(\Pi^1_0\) jumps, and \(\text{PA}^w_\Omega\) is the fixed-point theory (so, with inductive operator axioms) over PA with ordinals \(\Omega\), and \(\Delta_0\)-inductions \(w\). To determine the strength of the last theory, the author uses systems with infinitary rules, cut-elimination, asymmetric interpretation, and so forth. In the form of an appendix, the author gives similar consideration to the theory whose underlying applicative system is recursive, and shows that it is equivalent to ramified analysis in all finite levels and hence its ordinal is \(\varphi 20\) in the Veblen hierarchy.
0 references
first-order applicative theory \(\text{AutBON}(\mu)\)
0 references
predicative analysis
0 references
proof-theoretical ordinal
0 references
bar rule
0 references
transfinite induction
0 references
second-order arithmetic
0 references
fixed-point theory
0 references
systems with infinitary rules
0 references
ramified analysis
0 references