---
tag: 5VNT564Y2W
kind: concept
name: Theories of iterated inductive definitions
aliases: [buchholzs-id-hierarchy]
sources:
  - wikipedia: en:68497153@r1327123101
    locator: Theories of iterated inductive definitions
    note: adopted
    mention: wikipedia://en/68497153
    sections: [Summary]
same_as:
  wikidata: Q108377893
  wikipedia: Theories of iterated inductive definitions
inventory: [7QJKEPVE9T]
---

## Summary

In set theory and logic, **Buchholz's ID hierarchy** is a hierarchy of subsystems of [[first-order arithmetic|0QFT7Z76N5]]. The systems/theories $\mathsf{ID}_\nu$ are referred to as "the formal theories of *ν*-times iterated inductive definitions". ID<sub>*ν*</sub> extends [[PA|0QFT7Z76N5]] by *ν* iterated least fixed points of monotone operators.
