Full and hat inductive definitions are equivalent in NBG (Q2257106)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Full and hat inductive definitions are equivalent in NBG |
scientific article |
Statements
Full and hat inductive definitions are equivalent in NBG (English)
0 references
23 February 2015
0 references
The author analyzes the logical strength of mathematical statements spanning many topics, including fixed points, transfinite recursion, and inductive definitions. This analysis is carried out over both second-order arithmetic base systems and over weak set theoretic base systems. For example, the principles \(\Delta^0_1\)-FP asserting the existence of a fixed point, and its extension \(\Delta^0_1\)-LFP asserting existence of a least fixed point are examined. Over the second-order arithmetic subsystem ACA\(_0\), \(\Delta^0_1\)-LFP is strictly stronger than \(\Delta^0_1\)-FP. However, over von Neumann-Bernays-Gödel set theory (NGB), the two fixed point principles are equivalent. This article extends the author's previous work on relative predicativity [J. Symb. Log. 79, No. 3, 712--732 (2014 Zbl 1353.03073)].
0 references
subsystems of Morse-Kelley set theory
0 references
von Neumann-Bernays-Gödel set theory
0 references
higher-order number theory
0 references
elementarity of well-foundedness
0 references
proof-theoretic strength
0 references
transfinite recursion
0 references
fixed point
0 references
inductive definitions
0 references
0 references