Feferman's completeness theorem

TL;DR

This paper provides two new proofs of Feferman's 1962 completeness theorem, which links arithmetical theorems to transfinite iterations of reflection, and explores the bounds on order types needed for completeness in the arithmetical hierarchy.

Contribution

It offers novel proofs of Feferman's completeness theorem and establishes sharp bounds on the order types of well-orders required for completeness levels.

Findings

Two new proofs of Feferman's completeness theorem

Sharp bounds on order types for arithmetical hierarchy completeness

Enhanced understanding of the theorem's foundational aspects

Abstract

Feferman proved in 1962 that any arithmetical theorem is a consequence of a suitable transfinite iteration of full uniform reflection of $\mathsf{PA}$. This result is commonly known as Feferman's completeness theorem. The purpose of this paper is twofold. On the one hand this is an expository paper, giving two new proofs of Feferman's completeness theorem that, we hope, shed light on this mysterious and often overlooked result. On the other hand, we combine one of our proofs with results from computable structure theory due to Ash and Knight to give sharp bounds on the order types of well-orders necessary to attain the completeness for levels of the arithmetical hierarchy.