Iterating reflection over intuitionistic arithmetic

TL;DR

The paper analyzes how iterated reflection principles along ordinals interact with Heyting Arithmetic ($HA$), showing that uniform reflection iterations capture exactly recursive $\omega$-provability, while consistency and local reflection generate $HA$ plus all true $\Pi_1$ sentences; it provides a self-contained constructive proof of Dragalin’s theorem via Schütte’s canonical search trees and a $\,\Pi_2$-version of Löb’s theorem within $HA$, extending the framework to recursively enumerable extensions. The results illuminate the constructive landscape of reflection in intuitionistic arithmetic and connect Feferman-style completeness with $HA$ in the absence of classical logic. The methods combine arithmetization, self-reference, and transfinite ordinal progressions indexed by Kleene’s $\mathcal{O}$, yielding precise characterizations of what is provable under these iterative reflection schemes. Overall, the work clarifies the limits and capabilities of intuitionistic truth notions under ordinally iterated reflection and provides a robust, self-contained bridge between classical and intuitionistic completeness results.

Abstract

In this note, we investigate iterations of consistency, local and uniform reflection over $\mathbf{HA}$ (Heyting Arithmetic). In the case of uniform reflection, we give a new proof of Dragalin's extension of Feferman's completeness theorem to $\mathbf{HA}$, drawing on Rathjen's proof of Feferman's classical result.

Theorems & Definitions (75)

• Theorem 1.1: Feferman's completeness theorem; F62
• Theorem 1.2: F62
• Theorem 1.3: Dragalin's theorem Dra; see Theorem \ref{['uniform']}
• Theorem 1.4: see Theorem \ref{['local']}
• Theorem 1.5: cf. F62
• Definition 1.6
• Theorem 1.7: Dra
• Corollary 1.8: Completeness for the negative fragment
• Theorem 1.9: Dra
• Theorem 1.10: K65