3
$\begingroup$

The Bachmann-Howard ordinal (BHO) is a large recursive ordinal defined using ordinal collapsing functions. Kripke-Platek set theory (KP) is a fragment of ZF obtained by removing powerset, swapping replacement and separation with collection and separation both restricted to formulae with only bounded quantifiers. The program of ordinal analysis reveals that the proof-theoretic ordinal of KP is the BHO, i.e. the BHO is a sharp upper bound on the order types of recursive ordinal notations that KP proves well-founded. (A good exposition of ordinal analysis is Rathjen's "The Realm of Ordinal Analysis".)

Since KP cannot prove "$\prec$ is well-founded" for any recursive well-ordering $\prec$ of $\mathbb N$ with order type BHO (specifically there is no index $e$ of a computable well-ordering of order type BHO such that KP can prove "$\{e\}$ well-orders $\mathbb N$"), there must be a model of KP which thinks there is no computable well-ordering with order type BHO. However, does the same result happen when looking at $\emptyset'$ well-orderings with order type BHO?

I am not sure how to apply any kind of compactness result to construct such a model, or if there is a generalization of ordinal analysis about $\emptyset'$ ordinal notations instead of computable ones.

$\endgroup$
3
  • $\begingroup$ In fact, KP proves that every ${\bf 0'}$-computable well-order has a computable copy. Spector's theorem is overkill for this; the simpler argument in Ash/Knight goes through much more clearly in $\mathsf{KP}$. $\endgroup$ Aug 19, 2023 at 17:48
  • $\begingroup$ Thank you! I think this would fit as an answer. $\endgroup$
    – C7X
    Aug 19, 2023 at 20:01
  • $\begingroup$ 'Tis done (and I've added some more info). $\endgroup$ Aug 19, 2023 at 20:05

1 Answer 1

1
$\begingroup$

In fact, $\mathsf{KP}$ proves that every ${\bf 0'}$-computably-presentable well-order has a computable copy. The classical result along these lines is of course Spector's theorem, that every hyperarithmetic well-order has a computable copy. I believe that Spector's theorem goes through in $\mathsf{KP}$ - in particular, I think the argument for a more general result goes through in $\mathsf{KP}$ - but checking this takes a bit of care. Fortunately, we don't need Spector here: there's a much simpler result in Ash/Knight's book Computable structures and the hyperarithmetic hierarchy that for any ${\bf 0'}$-computably-presentable linear order $L$ the linear order $\omega\cdot L$ (= "replace each point in $L$ by a copy of $\omega$") has a computable copy. This is their Theorem 9.8; unfortunately, the proof is an exercise for the reader, but it's a simple finite-injury priority argument and goes through without difficulty in $\mathsf{KP}$.

$\endgroup$

You must log in to answer this question.

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