Full and hat inductive definitions are equivalent in NBG

TitleFull and hat inductive definitions are equivalent in NBG
Publication TypeJournal Article
Year of Publication2015
AuthorsSato, K
JournalArchive for Mathematical Logic
AbstractA new research project has, quite recently, been launched to clarify how different, from systems in second order number theory extending ACA 0, those in second order set theory extending NBG (as well as those in n + 3-th order number theory extending the so-called Bernays?Gödel expansion of full n + 2-order number theory etc.) are. In this article, we establish the equivalence between {$Δ$}10{$\backslash$}bf-LFP and {$Δ$}10{$\backslash$}bf-FP, which assert the existence of a least and of a (not necessarily least) fixed point, respectively, for positive elementary operators (or between {$Δ$}n+20{$\backslash$}bf-LFP and {$Δ$}n+20{$\backslash$}bf-FP). Our proof also shows the equivalence between ID 1 and {\^{ }}ID1, both of which are defined in the standard way but with the starting theory PA replaced by ZFC (or full n + 2-th order number theory with global well-ordering).