Representing definable functions of HA^ by neighbourhood functions

DOI10.1016/J.APAL.2019.04.011MaRDI QIDQ2417962zbMATH OpenOpenAlexWikidataFDO

Authors Tatsuji Kawai

Publication date 31 May 2019

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1901.11270

zbMATH Keywords

bar inductiondialogue treesintuitionistic mathematicsneighbourhood functions

Mathematics Subject Classification ID

Higher-type and set recursion theory (03D65) Functionals in proof theory (03F10) First-order arithmetic and fragments (03F30) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

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}^{mathbbN}$ to $mathbbN$ 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.

Recommendations

• Characterising Brouwer's continuity by bar recursion on moduli of continuity
• The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation
• Higher order functions and Brouwer's thesis
• Minimal readability of intuitionistic arithmetic and elementary analysis
• Principles of bar induction and continuity on Baire space

Cites work

• A direct proof of Schwichtenberg's bar recursion closure theorem
• Constructivism in mathematics. An introduction. Volume I
• Continuity of Gödel's system T definable functionals via effectful forcing
• Formal systems for some branches of intuitionistic analysis
• Functional completeness of cartesian categories
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• On bar recursion of types 0 and 1
• Ordinal analysis of terms of finite type

Cited in

(2)

• Higher order functions and Brouwer's thesis
• scientific article; zbMATH DE number 7269245 (Why is no real title available?)

This page was built for publication: Representing definable functions of \(\mathrm{HA}^{\omega}\) by neighbourhood functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2417962)