In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic.
are referred to as "the formal theories of ν-times iterated inductive definitions".
IDν extends PA by ν iterated least fixed points of monotone operators.
The formal theory IDω (and IDν in general) is an extension of Peano Arithmetic, formulated in the language LID, by the following axioms:[1] The theory IDν with ν ≠ ω is defined as: A set
is called inductively defined if for some monotonic operator
denotes the least fixed point of
, is obtained from that of first-order number theory,
, by the addition of a set (or predicate) constant IA for every X-positive formula A(X, x) in LN[X] that only contains X (a new set variable) and x (a number variable) as free variables.
The term X-positive means that X only occurs positively in A (X is never on the left of an implication).
We allow ourselves a bit of set-theoretic notation: Then ID1 contains the axioms of first-order number theory (PA) with the induction scheme extended to the new language as well as these axioms: Where
is closed under the arithmetically definable set operator
is meant to be the least pre-fixed-point, and hence the least fixed point of the operator
To define the system of ν-times iterated inductive definitions, where ν is an ordinal, let
be a primitive recursive well-ordering of order type ν.
We use Greek letters to denote elements of the field of
by the addition of a binary predicate constant JA for every X-positive
that contains at most the shown free variables, where X is again a unary (set) variable, and Y is a fresh binary predicate variable.
, thinking of x as a distinguished variable in the latter formula.
The system IDν is now obtained from the system of first-order number theory (PA) by expanding the induction scheme to the new language and adding the scheme
expressing transfinite induction along
, is the least fixed point (among definable sets) for the operator
γ ≺ μ
Note how all the previous sets
is instead called inductively defined if for some monotonic operator
This subtle difference makes the system significantly weaker:
, not only does it use fixed points rather than least fixed points, and has induction only for positive formulas.
This once again subtle difference makes the system even weaker:
The amount of weakening compared to regular iterated inductive definitions is identical to removing bar induction given a certain subsystem of second-order arithmetic.
It is not exactly a first-order arithmetic system, but captures what one can get by predicative reasoning based on ν-times iterated generalized inductive definitions.
The amount of increase in strength is identical to the increase from