Résumé
Joseph Harrison published in 1967 a quite famous result in classical recursion theory on recursive reals. It shows the counter-intuitive result that the well-ordered initial segment of a recursive order is not necessarily of recursive ordinal type. This segment can be as long as the supremum of recursive ordinals, hence of non-recursive length, even if the order is itself recursive. In the literature, a few different -but equivalent -proofs of this result can be found using arguments strictly in second order arithmetic, more precisely the fact that Σ 1 1 ̸ = Π 1 1 . In this article, we sketch a different and more elementary proof of this result, using infinite time Turing machines (ITTMs) -full proof is in [2]. To achieve this, we need to reprove, using elementary arguments only, several results on infinite (countable) binary relations, and more specifically on linear orders. This exploration leads us to an original priority proof of Spector's theorem which exposes the collapse of arithmetically defined ordinals on the recursive ones. In the context of reverse mathematics, we show that our proofs are more elementary than those mentioned before, in the sense that they reside in the proof system ACA0, which is not only strictly weaker than ATR0 where all the previous proofs of both theorems reside, but is also a natural lower theory for proving Harrison's theorem.