# Representing definable functions of $\mathrm{HA}^{\omega}$ by neighbourhood functions

## TL;DR

This paper proves that every definable function from Baire space to natural numbers in $ ext{HA}^ ext{ω}$ can be represented by a neighbourhood function, using an internal interpretation of G"odel's system T, without complex proof-theoretic methods.

## Contribution

It demonstrates that Brouwer's claim about neighbourhood functions is provable in $ ext{HA}^ ext{ω}$ for definable functions, introducing a new internal interpretation approach.

## Key findings

- Proves Brouwer's claim within $ ext{HA}^ ext{ω}$ for definable functions.
- Establishes uniform continuity of certain functions on the Cantor space.
- Shows closure properties of $ ext{HA}^ ext{ω}$ under bar induction and bar recursion.

## Abstract

Brouwer (1927) claimed that every function from the Baire space to natural numbers is induced by a neighbourhood function whose domain admits bar induction. We show that Brouwer's claim is provable in Heyting arithmetic in all finite types ($\mathrm{HA}^{\omega}$) for definable functions of the system. The proof does not rely on elaborate proof theoretic methods such as normalisation or ordinal analysis. Instead, we internalise in $\mathrm{HA}^{\omega}$ the dialogue tree interpretation of G\"{o}del's system T due to Escard\'{o} (2013). The interpretation determines a syntactic translation of terms, which yields a neighbourhood function from a closed term of $\mathrm{HA}^{\omega}$ with the required property. As applications of this result, we prove some well-known properties of $\mathrm{HA}^{\omega}$: uniform continuity of definable functions from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ on the Cantor space; closure under the rule of bar induction; and closure of bar recursion for the lowest type with a definable stopping function.