English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Brouwer (1927) claimed that every function from the Baire space to naturalnumbers is induced by a neighbourhood function whose domain admits barinduction. We show that Brouwer's claim is provable in Heyting arithmetic inall finite types ($\mathrm{HA}^{\omega}$) for definable functions of thesystem. The proof does not rely on elaborate proof theoretic methods such asnormalisation or ordinal analysis. Instead, we internalise in$\mathrm{HA}^{\omega}$ the dialogue tree interpretation of G\"{o}del's system Tdue to Escard\'{o} (2013). The interpretation determines a syntactictranslation of terms, which yields a neighbourhood function from a closed termof $\mathrm{HA}^{\omega}$ with the required property. As applications of thisresult, we prove some well-known properties of $\mathrm{HA}^{\omega}$: uniformcontinuity of definable functions from $\mathbb{N}^{\mathbb{N}}$ to$\mathbb{N}$ on the Cantor space; closure under the rule of bar induction; andclosure of bar recursion for the lowest type with a definable stoppingfunction.

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