Takeuti–Feferman–Buchholz ordinal

In the mathematical fields of set theory and proof theory, the Takeuti–Feferman–Buchholz ordinal (TFBO) is a large countable ordinal, which acts as the limit of the range of Buchholz's psi function and Feferman's theta function.[1][2] It was named by David Madore,[2] after Gaisi Takeuti, Solomon Feferman and Wilfried Buchholz. It is written as ${\displaystyle \psi _{0}(\varepsilon _{\Omega _{\omega }+1})}$ using Buchholz's psi function,[3] an ordinal collapsing function invented by Wilfried Buchholz,[4][5][6] and ${\displaystyle \theta _{\varepsilon _{\Omega _{\omega }+1}}(0)}$ in Feferman's theta function, an ordinal collapsing function invented by Solomon Feferman.[7][8] It is the proof-theoretic ordinal of several formal theories:

• ${\displaystyle \Pi _{1}^{1}-CA+BI}$,[9] a subsystem of second-order arithmetic
• ${\displaystyle \Pi _{1}^{1}}$-comprehension + transfinite induction[3]
• ID_ω, the system of ω-times iterated inductive definitions[10]

Despite being one of the largest large countable ordinals and recursive ordinals, it is still vastly smaller than the proof-theoretic ordinal of ZFC.[11]