---
tag: C19Z3B6V4P
kind: definition
name: Proof-theoretic ordinal
msc: ["03F15", "03F30"]
defines: C72RBH0CDR
uses: [0RDJK7EQYY, 0F1D6PK9RZ, 0QFT7Z76N5, 0ZHQMQ2C1N, KT50SMH3EC, KZSB5E471K]
sources:
  - url: https://en.wikipedia.org/wiki/Ordinal_analysis
---

## Definition

Let $T$ be a recursively axiomatized theory that contains enough arithmetic to speak about [[computable|KZSB5E471K]] relations on $\N$.
For a computable binary relation $\prec$ on $\N$, let $\mathrm{WF}(\prec)$ be the statement in the language of $T$ that $\prec$ is a [[well-order|0F1D6PK9RZ]].
For first-order theories, $\mathrm{WF}(\prec)$ is replaced by the scheme of [[transfinite induction|0ZHQMQ2C1N]] along $\prec$ for all formulas.
The *proof-theoretic ordinal* of $T$ is written $\abs{T}$.
It is the supremum of the order types of all computable well-orders $\prec$ on $\N$ such that $T$ proves $\mathrm{WF}(\prec)$.

## Remarks

Example: for [[Peano arithmetic|0QFT7Z76N5]], $\abs{\mathrm{PA}} = \varepsilon_0$, the ordinal [[epsilon nought|KT50SMH3EC]].
Gentzen showed that PA proves transfinite induction along a standard notation system for each ordinal below $\varepsilon_0$, and not along the one for $\varepsilon_0$ itself.
Non-example: the least uncountable [[ordinal|0RDJK7EQYY]] $\omega_1$ is not the proof-theoretic ordinal of any such theory, because a computable well-order on $\N$ has countable order type.
Suppose that every computable order that $T$ proves well-founded is in fact well-founded.
Then $\abs{T}$ is below the Church–Kleene ordinal $\omega_1^{\mathrm{CK}}$, the least ordinal that is not the order type of a computable well-order.
Several inequivalent definitions are in use, for example with primitive recursive in place of computable orders, or with $\Pi^0_2$ consequences in place of well-foundedness.
For the usual theories they give the same ordinal.