14
$\begingroup$

$\newcommand{\omegaoneck}{\omega_1^{\text{CK}}}$ Pardon the extremely basic question - this isn't quite my area - but I'm confused about the definition of proof theoretic ordinals.

The proof theoretic ordinal of a theory is defined to be the smallest ordinal that the theory cannot prove is well founded. In other words, it gives us a measure of how much transfinite induction the theory allows us to do. There is a countable ordinal $\omegaoneck$ such that every recursive theory has a proof theoretic ordinal $\alpha\in\omegaoneck$.

This seems fine, except that there exist recursive theories (such as ZFC) in which we can prove transfinite induction over all ordinals. My first thought was that perhaps ZFC can't prove the existence of ordinals larger than its own proof-theoretic ordinal $\omega_{ZFC}$, so 'induction over all ordinals' is the same as 'induction up to $\omega_{ZFC}$', within ZFC. But that can't be true: ZFC can prove Hartogs' Lemma, which gives us arbitrarily large ordinals (and they can be shown to be arbitrarily large within ZFC).

One possibility might be that ZFC can't reason about its own proof-theoretic ordinal, and can't show that it's less than any given ordinal. But that seems rather strange, given that ZFC can construct ordinals such as $\omega_1$ that are far far larger than even $\omegaoneck$, even in cardinality.

Improve this question
$\endgroup$
4
  • 12
    $\begingroup$ The proof theoretic ordinal is the smallest recursive ordinal the theory cannot prove well-founded. ZFC thinks it can prove the well-foundedness of crazy huge ordinals, but it does not know how to represent them by recursive relations on the integers. $\endgroup$
    – Emil Jeřábek
    Commented Jan 27, 2016 at 12:00
  • $\begingroup$ @EmilJeřábek Ah, I see. So really it is a double condition: the smallest ordinal that the theory can prove is recursive, but can't prove is well founded. $\endgroup$
    – John Gowers
    Commented Jan 27, 2016 at 12:02
  • 12
    $\begingroup$ Basically, yes. But more precisely, you first take a recursive representation of the ordinal, and then ask if the theory proves it well-founded (which, for ZFC, might involve unwinding the recursive definition into the von Neumann representation that ZFC internally uses for ordinals). One reason for this is to have a comparison across theories: say, ZFC has an ordinal it calls $\omega_3$, and a fancy theory X (that does not look at all like set theory) has an ordinal it calls PSM9. Are they the same? Which one is longer? These would be meaningless questions, ... $\endgroup$
    – Emil Jeřábek
    Commented Jan 27, 2016 at 12:19
  • 9
    $\begingroup$ ... as the objects never live in the same model. With recursive ordinals as a common representation that is reasonably absolute, we can ask about the same ordinal in two different theories. $\endgroup$
    – Emil Jeřábek
    Commented Jan 27, 2016 at 12:20

2 Answers 2

Reset to default
14
$\begingroup$

Just slightly expanding the comment of Emil Jeřábek: on one hand, in ZFC we can define some objects we call ordinals and prove transfinite induction of each of them. This is not what we mean by the ordinal of ZFC. The latter is defined roughly as follows (although there are several nonequivalent definitions):

  1. You take some recursive relation, such that in the actual natural numbers, this relation is well-founded and you actually fix some algorithm which describes this relation (as a set of pairs).

  2. Then you ask, whether the theory in question proves that the relation given by this algorithm is a well-founded one.

For instance, think of the following relation $R$: $R(m,n)$ iff $m<n$ and there is no proof of $0 \neq 0$ from the axiom of ZFC using less than $m$ symbols or $m>n$ otherwise. This relation is easily verified to be a recursive linear order by even very weak theories but is wellfounded (namely isomorphic to $\omega$) iff ZFC is consistent, so ZFC does not even prove that $\omega$ is well-founded under totally arbitrary presentation of $\omega$.

Notice that the above example could give an impression that no theory can have its prof-theoretic ordinal bigger than $\omega,$ therefore precise definition of this concept is a rather subtle issue and there are several nonequivalent definitions. But the rough idea, of what may go wrong is precisely this.

Improve this answer
$\endgroup$
7
$\begingroup$

This is a difference between internal and external quantification. Proof-theoretic ordinal analysis involves an external quantification over (external, recursive) ordinals. What is provable in ZFC is an internal quantification over (internal) ordinals.

Skolem’s Paradox is the classic illustration of why one can’t generally expect internal and external interpretations of a statement to be equivalent.

Improve this answer
$\endgroup$
1
  • $\begingroup$ I talked about the difference between internal and external quantification in my question. But ZFC has $\omega_1$ as an internal ordinal, and FC can prove that $\omega_1$ is larger than any countable ordinal, so internal vs external quantification doesn't tell the whole story. $\endgroup$
    – John Gowers
    Commented Jan 27, 2016 at 16:11

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .