Iterating reflection over intuitionistic arithmetic

TL;DR

This paper explores iterative reflection principles over Heyting Arithmetic, providing new proofs and extending classical results to intuitionistic logic, enhancing understanding of proof-theoretic strength.

Contribution

It offers a novel proof of Dragalin's extension of Feferman's completeness theorem to HA using Rathjen's methods, advancing the study of reflection in intuitionistic arithmetic.

Findings

Established a new proof for uniform reflection over HA

Extended Feferman's completeness theorem to intuitionistic logic

Enhanced understanding of reflection principles in proof theory

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.