Buchholz's ID hierarchy

From Wikipedia, the free encyclopedia

In set theory and logic, Buchholz's ID hierarchy is a hierarchy of subsystems of first-order arithmetic. The systems/theories are referred to as "the formal theories of ν-times iterated inductive definitions". IDν extends PA by ν iterated least fixed points of monotone operators.

Definition[]

Original definition[]

The formal theory IDω (and IDν in general) is an extension of Peano Arithmetic, formulated in the language LID, by the following axioms:

  • for every LID-formula F(x)

The theory IDν with ν ≠ ω is defined as:

  • for every LID-formula F(x) and each u < ν

Explanation / alternate definition[]

ID1[]

A set is called inductively defined if for some monotonic operator , , where denotes the least fixed point of . The language of ID1, , 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:

  • means
  • For two formulas and , means .

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 ranges over all formulas.

Note that expresses that  is closed under the arithmetically definable set operator , while  expresses that  is the least such (at least among sets definable in ).

Thus,  is meant to be the least pre-fixed-point, and hence the least fixed point of the operator .

IDν[]

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 . The language of IDν, is obtained from by the addition of a binary predicate constant JA for every X-positive formula that contains at most the shown free variables, where X is again a unary (set) variable, and Y is a fresh binary predicate variable. We write instead of , 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 for an arbitrary  formula  as well as the axioms:

where  is an arbitrary  formula. In  and  we used the abbreviation  for the formula , where  is the distinguished variable. We see that these express that each , for , is the least fixed point (among definable sets) for the operator . Note how all the previous sets , for , are used as parameters.

We then define .

Variants[]

- is a weakened version of . In the system of , a set is instead called inductively defined if for some monotonic operator , is a fixed point of , rather than the least fixed point. This subtle difference makes the system significantly weaker: , while .

is weakened even further. In , 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: , while .

is the weakest of all variants of , based on W-types. The amount of weakening compared to regular iterated inductive definitions is identical to removing bar induction given a certain subsystem of second-order arithmetic. , while .

is an "unfolding" strengthening of . 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 to : , while .

Various formulas[]

  • Let ν > 0. If a ∈ T0 contains no symbol Dμ with ν < μ, then "a ∈ W0" is provable in IDν.
  • IDω is contained in .
  • If a -sentence is provable in IDν, then there exists such that .
  • If the sentence A is provable in IDν for all ν < ω, then there exists k ∈ N such that .

Proof-theoretic ordinal(s)[]

  • The proof-theoretic ordinal of ID is equal to .
  • The proof-theoretic ordinal of IDν is equal to .
  • The proof-theoretic ordinal of is equal to .
  • The proof-theoretic ordinal of for is equal to .
  • The proof-theoretic ordinal of is equal to .
  • The proof-theoretic ordinal of for is equal to .
  • The proof-theoretic ordinal of for is equal to .
  • The proof-theoretic ordinal of is equal to .
  • The proof-theoretic ordinal of is equal to .
  • The proof-theoretic ordinal of is equal to .
  • The proof-theoretic ordinal of is equal to .
  • The proof-theoretic ordinal of is equal to .
  • The proof-theoretic ordinal of is equal to .
  • The proof-theoretic ordinal of ID1 (the Bachmann-Howard ordinal) is also the proof-theoretic ordinal of , , and .
  • The proof-theoretic ordinal of W-IDω () is also the proof-theoretic ordinal of .
  • The proof-theoretic ordinal of IDω (the Takeuti-Feferman-Buchholz ordinal) is also the proof-theoretic ordinal of , and .
  • The proof-theoretic ordinal of ID<ω^ω () is also the proof-theoretic ordinal of .
  • The proof-theoretic ordinal of ID<ε0 () is also the proof-theoretic ordinal of and .

References[]

Retrieved from ""