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.

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.

Equations

$$0$$

$$\begin{array}{c}\Gamma ,x^{\rho },\Delta ⊢x:\rho \Gamma ⊢\mathtt{C}:\rho \frac{\Gamma ,x^{\rho }⊢t:\sigma }{\Gamma ⊢\lambda x^{\rho }.t:\rho \to \sigma }\frac{\Gamma ⊢u:\rho \to \sigma \Gamma ⊢v:\rho }{\Gamma ⊢uv:\sigma }\end{array}$$

$$P\subseteq Q$$

$$\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\forall n^{\mathbb{N}}\left[\gamma(\overline{\alpha}n)>0\operatorname{\,\rightarrow\,}f(\alpha)=\gamma(\overline{\alpha}n)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{$\cdot$}\hss\crcr$-$}}1\right],$$

$$S_{\gamma }(a)\equiv \gamma (a)>0.$$

$$S_{\gamma }\subseteq Q\wedge \mathrm{Ind}(Q)\to Q(⟨⟩),$$

$$\mathrm{Ind}(Q)\equiv \forall a^{{\mathbb{N}}^{\ast }}\left[\forall n^{\mathbb{N}}Q(a\ast ⟨n⟩)\to Q(a)\right].$$

$$\forall k^{\mathbb{N}}\forall a^{{\mathbb{N}}^{\ast }}\left[\mathrm{Ind}(Q)\wedge \forall b^{{\mathbb{N}}^{\ast }}\left(|b|=k\to Q(a\ast b)\right)\to Q(a)\right].$$

$${\mathrm{HA}}^{\omega }⊢S_{\gamma }\subseteq Q\wedge \mathrm{Ind}(Q)\to Q(⟨⟩).$$

$$\eta$$

$${\mathsf{KE}}_{\mathbb{N}}$$

$$\mathsf{At}$$

$$\_\bullet \_$$

$$\eta (n)\bullet \alpha$$

$$f(\gamma \bullet \alpha )\bullet \alpha$$

$$\mathsf{At}(n)\bullet \alpha$$

$$T_{{\mathbb{N}}^{\mathbb{N}}}(x_0:{\rho }_0,\dots ,x_{n-1}:{\rho }_{n-1})$$

$$T_{{\mathbb{N}}^{\mathbb{N}}}(\Gamma ⊢t:\rho )$$

$${\mathbb{N}}^{†}$$

$${(\rho \to \sigma )}^{†}$$

$${(\Gamma ,x:\rho ,\Delta ⊢x:\rho )}^{†}$$

$${(\Gamma ⊢\mathtt{C}:\rho )}^{†}$$

$${(\Gamma ⊢\lambda x^{\rho }.t^{\sigma }:\rho \to \sigma )}^{†}$$

$${(\Gamma ⊢u^{\rho \to \sigma }{v}^{\rho }:\sigma )}^{†}$$

$$0^{†}$$

$${\mathsf{Succ}}^{†}$$

$${\Omega }^{†}$$

$${{\mathsf{Rec}}_{\rho }}^{†}$$

$${\mathsf{KE}}_{\rho \to \sigma }:=\lambda f^{\mathbb{N}\to {\rho }^{†}\to {\sigma }^{†}}.\lambda u^{{\mathbb{N}}^{†}}.\lambda v^{{\rho }^{†}}.{\mathsf{KE}}_{\sigma }(\lambda x^{\mathbb{N}}.fxv)u.$$

$$\gamma {\sim }_{\mathbb{N}}f$$

$$G{\sim }_{\rho \to \sigma }F$$

$$\displaystyle\begin{multlined}\mathrm{HA}^{\omega}\vdash\forall u_{0}^{\rho_{0}^{\dagger}}\cdots\forall u_{n-1}^{\rho_{n-1}^{\dagger}}\forall y_{0}^{\mathbb{N}^{\mathbb{N}}\to\rho_{0}}\cdots\forall y_{n-1}^{\mathbb{N}^{\mathbb{N}}\to\rho_{n-1}}\Bigl{[}u_{0}\sim_{\rho_{0}}y_{0}\wedge\cdots\wedge u_{n-1}\sim_{\rho_{n-1}}y_{n-1}\\ \operatorname{\,\rightarrow\,}t^{\dagger}[\overline{u}/{\overline{x}}^{\dagger}]\sim_{\rho}\lambda\alpha^{\mathbb{N}^{\mathbb{N}}}.t[\alpha/\Omega,\overline{y}(\alpha)/\overline{x}]\Bigr{]}\end{multlined}\mathrm{HA}^{\omega}\vdash\forall u_{0}^{\rho_{0}^{\dagger}}\cdots\forall u_{n-1}^{\rho_{n-1}^{\dagger}}\forall y_{0}^{\mathbb{N}^{\mathbb{N}}\to\rho_{0}}\cdots\forall y_{n-1}^{\mathbb{N}^{\mathbb{N}}\to\rho_{n-1}}\Bigl{[}u_{0}\sim_{\rho_{0}}y_{0}\wedge\cdots\wedge u_{n-1}\sim_{\rho_{n-1}}y_{n-1}\\ \operatorname{\,\rightarrow\,}t^{\dagger}[\overline{u}/{\overline{x}}^{\dagger}]\sim_{\rho}\lambda\alpha^{\mathbb{N}^{\mathbb{N}}}.t[\alpha/\Omega,\overline{y}(\alpha)/\overline{x}]\Bigr{]}$$

$$\begin{array}{rl}{t}^{†}[\overline{u}/{\overline{x}}^{†}]& \equiv t^{†}[u_0/x_0^{†},\dots ,u_{n-1}/x_{n-1}^{†}],\\ t[\alpha /\Omega ,\overline{y}(\alpha )/\overline{x}]& \equiv t[\alpha /\Omega ,y_0(\alpha )/x_0,\dots ,y_{n-1}(\alpha )/x_{n-1}].\end{array}$$

$${\mathrm{HA}}^{\omega }⊢\forall g^{\mathbb{N}\to {\rho }^{†}}\forall f^{\mathbb{N}\to {\mathbb{N}}^{\mathbb{N}}\to \rho }\left[\forall n^{\mathbb{N}}g(n){\sim }_{\rho }f(n)\to {\mathsf{KE}}_{\rho }(g){\sim }_{\mathbb{N}\to \rho }\lambda \alpha .\lambda n.fn\alpha \right].$$

$${\mathsf{KE}}_{\mathbb{N}}(g)(\gamma )\bullet \alpha$$

$$=f(\gamma \bullet \alpha )(\alpha )$$

$$=f(h\alpha )\alpha$$

$$=(\lambda n.fn\alpha )(h\alpha ).$$

$${\mathsf{KE}}_{\sigma \to \tau }(g)(\gamma ){\sim }_{\sigma \to \tau }\lambda \alpha .f(h(\alpha ))\alpha ,$$

Full text

Keywords: Intuitionistic mathematics; Bar induction; Neighbourhood functions; Dialogue trees

MSC2010: 03F55; 03F50; 03F10

1 Introduction

In “On the domains of definition of functions” [3], Brouwer claims that every function from the Baire space to natural numbers is not only continuous but also contains a bar for which so-called bar induction holds. In terms of the modern constructive mathematics, Brouwer’s claim can be stated as follows, which we refer to as bar theorem:

For any function $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$, there is a neighbourhood function $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ of $f$ such that its domain $S_{\gamma}:=\left\{a\in\mathbb{N}^{*}\mid\gamma(a)>0\right\}$ satisfies the following induction principle: any inductive predicate $Q$ on ${\mathbb{N}^{*}}$ which contains $S_{\gamma}$ necessarily contains the empty sequence.

Here, a predicate $Q$ on $\mathbb{N}^{*}$ is inductive if $\forall a^{\mathbb{N}^{*}}\left[\forall n^{\mathbb{N}}Q(a*\langle n\rangle)\operatorname{\,\rightarrow\,}Q(a)\right]$: if every one-step extension of $a$ satisfies $Q$, then $a$ satisfies $Q$. A neighbourhood function of $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ is an algorithm which tells us whether a given initial segment of an input $\alpha$ of $f$ is long enough to compute the value $f(\alpha)$; when the initial segment is not long enough, its value stays at [math] waiting for more input to be supplied; when it has read enough initial segment of $\alpha$ to compute the value $f(\alpha)$, it outputs a positive value $f(\alpha)+1$. See Section 3 for the precise definition.

The purpose of this paper is to show that bar theorem holds for closed terms of Heyting arithmetic in all finite types $\mathrm{HA}^{\omega}$ (i.e., closed terms of Gödel’s system $\mathsf{T}$). Specifically, given a closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathrm{HA}^{\omega}$, one can construct a neighbourhood function of $Y$ as a closed term of $\mathrm{HA}^{\omega}$ for which bar induction is valid. The existing literature suggests that our result is not surprising: it is known that a closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of system $\mathsf{T}$ has a $\mathsf{T}$-definable modulus of continuity (see e.g., Schwichtenberg [13]); moreover, $\mathrm{HA}^{\omega}$ is closed under the rule of bar induction (Howard [6, Section 5]).111The proof by Howard in [6, Section 5] applies to those variants of $\mathrm{HA}^{\omega}$ that admit Gödel’s Dialectica interpretation into system $\mathsf{T}$. On the other hand, we work with the extensional version of $\mathrm{HA}^{\omega}$, which does not admit Dialectica interpretation (cf. Howard [5]). However, our proof does not rely on sophisticated proof theoretic methods such as normalisation of infinite terms or ordinal analysis used in those works. Nor do we use forcing, which is often used to prove the fan rule, a weaker form of bar induction rule (see Beeson [2, Chapter XVI, Section 4]).

Instead, our proof of bar theorem is inspired by the dialogue tree model of system $\mathsf{T}$ by Escardó [4] (see Section 4.2.1). His main idea is to represent a $\mathsf{T}$-definable function $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ by a certain well-founded tree, called dialogue tree, which can be thought of as a computation tree of $f$. Since dialogue trees are inductively defined, one can extract strong continuity properties of $\mathsf{T}$-definable functions. In this respect, his approach is similar to the elimination of choice sequences (Kreisel and Troelstra [9, Section 7]), where a term containing a variable for a choice sequence is represented as a Brouwer-operation (see also Section 4.2.2). Our proof of bar theorem for $\mathrm{HA}^{\omega}$ uses a mix of both approaches: the simplicity of the dialogue model lends itself for direct formalisation in $\mathrm{HA}^{\omega}$, while the representation of terms by Brouwer-operations would immediately yield a proof of bar theorem. We elaborate on how these ideas can be combined to give a proof of bar theorem for closed terms of $\mathrm{HA}^{\omega}$.

The basic idea of our proof is to formalise Escardó’s model in $\mathrm{HA}^{\omega}$. Instead of directly formalising his model, however, we extract essential properties of the dialogue tree model that is needed for the representation theorem. By so doing, we define a family of models for the structure sharing these essential properties (Section 4). By instantiating this abstract model with a structure other than dialogue trees, one obtains a representation theorem of closed terms of $\mathrm{HA}^{\omega}$ for that particular structure. In particular, instantiated with Brouwer-operations, the model immediately yields a proof of bar theorem in $\mathrm{HA}^{\omega}$ extended with the type of Brouwer-operations (Section 4.2.2). Finally, the use of the transfinite type, that of Brouwer-operation, is eliminated by reformulating the Brouwer-operation model in terms of neighbourhood functions.

This last step of the proof, presented in Section 5, is inspired by Oliva and Steila [11], who showed that Spector’s bar recursion for the lowest type is definable in Gödel’s system $\mathsf{T}$ when its stopping function is $\mathsf{T}$-definable. The structure and technique used in their proof are similar to those of ours. However, we believe that our proof is more perspicuous, having presented its essential structure in a more abstract setting in Section 4. Moreover, as far as we know, it is still open whether bar induction follows from bar recursion. In this respect, our result is stronger than their result (see Section 6.3).

As applications of bar theorem, 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.

Remark 1.1*.*

Our proof of the existence of a $\mathsf{T}$-definable neighbourhood function for a closed system-$\mathsf{T}$ term is similar to the proof for the existence of a $\mathsf{T}$-definable majorant for a closed system-$\mathsf{T}$ term (see Howard [5] and Kohlenbach [8, Chapter 6]). As an application of existence of majorants, Kohlenbach [7] gave a simple proof of the fan rule for $\mathrm{HA}^{\omega}$, which yields uniform continuity of $\mathsf{T}$-definable functions from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ on the Cantor space [7, 3.6 Application]. His proof is much simpler than the one presented in Section 6.1, although we derive the result from a stronger result (i.e. the bar theorem).

Organisation

Section 2 fixes the formal system $\mathrm{HA}^{\omega}$; Section 3 introduces bar theorem for $\mathrm{HA}^{\omega}$; Section 4 formalises a family of models abstracted from Escardó’s dialogue tree model; Section 5 presents the proof of bar theorem for $\mathrm{HA}^{\omega}$; Section 6 presents applications of bar theorem.

The paper is essentially self-contained without Section 4. Thus, the reader who is only interested in the proof of bar theorem and its applications can skip Section 4 entirely. However, Section 4 explains how one can view our proof of bar theorem as an instance of Escardó’s dialogue tree model, thereby putting our work in a wider picture.

2 Heyting arithmetic in all finite types

We work with the extensional version of Heyting arithmetic in all finite types ($\mathrm{HA}^{\omega}$) with lambda operators (see Troelstra [14, Section 1.8.4]).

Finite types are defined as usual: $\mathbb{N}$ is a type; if $\sigma,\tau$ are types, so is $\sigma\to\tau$, which is sometimes written $\tau^{\sigma}$. For convenience, we assume the existence of type $\mathbb{N}^{*}$ of finite sequences of objects of $\mathbb{N}$, which is identified with $\mathbb{N}$ via coding. We use metavariables $\rho,\sigma,\tau$ for types.

Terms of $\mathrm{HA}^{\omega}$ are those of simply typed lambda calculus with natural number objects: There are demumerable list of variables $x^{\rho},y^{\rho},z^{\rho},\ldots$ for each type $\rho$, the lambda operator $\lambda x^{\rho}$, and constants [math], $\mathsf{Succ}$, and $\mathsf{Rec}_{\rho}$ (for each type $\rho$) of the following types:

[TABLE]

A context is a finite list $x_{0}^{\rho_{0}},\dots,x_{n-1}^{\rho_{n-1}}$ of variables, which is sometimes written as $x_{0}\colon{\rho_{0}},\dots,x_{n-1}\colon{\rho_{n-1}}$. We use $\Gamma,\Delta$ for contexts. Terms in contexts $\Gamma\vdash t\colon\rho$ are inductively defined as follows:

[TABLE]

where $\mathtt{C}\colon{\rho}$ denotes a constant of type $\rho$. The term $uv$ is sometimes written as $u(v)$. Closed terms of $\mathrm{HA}^{\omega}$ are terms in the empty context.

Prime formulas are equations $t=_{\rho}u$ between terms (in the same context) of the same type $\rho$. Other formulas are built up from prime formulas using logical constants $\bot$, $\wedge$, $\vee$, $\operatorname{\,\rightarrow\,}$, $\forall x^{\rho}$, $\exists x^{\rho}$. When a formula $A$ is derivable in $\mathrm{HA}^{\omega}$, we write $\mathrm{HA}^{\omega}\vdash A$.

Notations*.*

We use variables $k,l,m,n,\dots,x,y,z,\dots$ for objects of type $\mathbb{N}$ and $\alpha,\beta,\gamma,\dots$ for objects of type $\mathbb{N}\to\mathbb{N}$. We assume fixed bijective coding of $\mathbb{N}^{*}$ in $\mathbb{N}$, and identify finite sequences with their codes. We use variables $a,b,c,\dots$ for finite sequences.

The empty sequence is denoted by $\langle\,\rangle$, and a singleton sequence is denoted by $\langle x^{\mathbb{N}}\rangle$. Concatenation of finite sequences $a$ and $b$ is denoted by $a*b$, and concatenation of finite sequence $a$ and a sequence $\alpha$ is denoted by $a*\alpha$. For a finite sequence $a$, its length is denoted by $|a|$; if $n<|a|$ then $a_{n}$ denotes the $n$-th entry of $a$. For any $\alpha$ and $n$, we write $\overline{\alpha}n$ for the initial segment of $\alpha$ of length $n$. We write $\widehat{a}$ for $a*(\lambda n.0)$.

If $P$ and $Q$ are predicates on a type $\rho$, we use abbreviations

[TABLE]

Type superscripts $t^{\rho}$ and subscripts $=_{\rho}$ are omitted whenever they can be inferred from the context.

3 Bar theorem for closed terms of $\mathrm{HA}^{\omega}$

We recall some technical notions that are needed for our main theorem; see Troelstra and van Dalen [15, Chapter 4] for more details.

Definition 3.1**.**

A function $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ is called a neighbourhood function if

$\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\exists n^{\mathbb{N}}\gamma(\overline{\alpha}n)>0$, 2. 2.

$\forall a^{\mathbb{N}^{*}}\left[\gamma(a)>0\operatorname{\,\rightarrow\,}\forall b^{\mathbb{N}^{*}}\gamma(a)=\gamma(a*b)\right]$.

Given a neighbourhood function $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ and a function $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$, we say that $\gamma$ induces $f$ if

[TABLE]

where \mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}} is the primitive recursive cut-off minus operation. We say that a function $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ has a neighbourhood function if there exists a neighbourhood function $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ which induces $f$. In this case, we also say that $\gamma$ is a neighbourhood function of $f$.

Note that a function $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ may have many different neighbourhood functions. Moreover, if $f$ has a neighbourhood function, then $f$ is continuous.

Definition 3.2**.**

A predicate $P$ on $\mathbb{N}^{*}$ is

• •

a bar if $\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\exists n^{\mathbb{N}}P(\overline{\alpha}n)$;

• •

decidable if $\forall a^{\mathbb{N}^{*}}\left[P(a)\vee\neg P(a)\right]$;

• •

monotone if $\forall a^{\mathbb{N}^{*}}\forall b^{\mathbb{N}^{*}}\left[P(a)\operatorname{\,\rightarrow\,}P(a*b)\right]$.

A neighbourhood function $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ determines a decidable monotone bar $S_{\gamma}$ by

[TABLE]

We say that $\gamma$ satisfies bar induction if for any predicate $Q$ on $\mathbb{N}^{*}$

[TABLE]

where

[TABLE]

A predicate $Q$ on $\mathbb{N}^{*}$ for which $\operatorname{\textrm{{Ind}}}(Q)$ holds is said to be inductive.

Lemma 3.3**.**

Let $Q$ be a predicate on $\mathbb{N}^{*}$. Then

[TABLE]

Proof.

By a straightforward induction on $k$. ∎

We can now introduce our main theorem.

Theorem 3.4** (Bar theorem).**

For any closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathrm{HA}^{\omega}$, there is a closed term $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ of $\mathrm{HA}^{\omega}$ such that

\mathrm{HA}^{\omega}\vdash\text{\gamma$is a neighbourhood function of$Y}, 2. 2.

for any predicate $Q$ on ${\mathbb{N}^{*}}$

[TABLE]

The proof of Theorem 3.4 is given in Section 5.

4 Non-standard representation of terms of $\mathrm{HA}^{\omega}$

Escardó [4] showed that every definable function $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of Gödel’s system $\mathsf{T}$ can be represented by a dialogue tree. Escardó presented his result as a property of $\mathsf{T}$-definable function in the set-theoretical model of system $\mathsf{T}$. Here, we formalise his result in $\mathrm{HA}^{\omega}$, but we abstract away from the concrete model of dialogue trees.

Proposition 4.1**.**

Suppose that we have a type $T\mathbb{N}$ and closed terms

[TABLE]

which satisfy the following equations:

[TABLE]

Then, for each closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathrm{HA}^{\omega}$, there exists a closed term $\gamma\colon T\mathbb{N}$ such that $\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\gamma\mathop{\bullet}\alpha=Y\alpha.$

The term $\_\bullet\_$ allows us to regard an object of type $T\mathbb{N}$ as a function from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$. Thus, the proposition says that every closed $\mathrm{HA}^{\omega}$-term of type $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ can be represented by an object of type $T\mathbb{N}$. Intuitively, a term of type $T\mathbb{N}$ derived from a closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ tells us more about the computation of $Y$.

4.1 Proof of Proposition 4.1

Let $\mathcal{T}_{\Omega}$ be the set of terms in contexts in an indeterminate $\Omega\colon{\mathbb{N}\to\mathbb{N}}$, i.e., $\mathcal{T}_{\Omega}$ is defined by the rule described in (2.1) but with an extra constant $\Omega\colon{\mathbb{N}\to\mathbb{N}}$. A term in indeterminate $\Omega$ will be written as $t[\Omega]$. We define two interpretations of $\mathcal{T}_{\Omega}$ in $\mathrm{HA}^{\omega}$: one is a standard interpretation; the other is a non-standard interpretation into the type structure over $T\mathbb{N}$.

4.1.1 Standard interpretation

In the standard interpretation, a term in context $\Gamma\vdash t[\Omega]\colon{\rho}\in\mathcal{T}_{\Omega}$ is interpreted as $\Gamma\vdash\lambda\alpha.t[\alpha/\Omega]\colon\mathbb{N}^{\mathbb{N}}\to\rho$, where $t[\alpha/\Omega]$ is a substitution of $\alpha$ for $\Omega$ in $t$.

Remark 4.2*.*

The interpretation is standard in the following sense: from the viewpoint of categorical logic [12], the interpretation determines an equivalence between the two categories: the category $\mathsf{Con}[\Omega]$ of contexts and terms in indeterminate $\Omega$; and the Kleisli category of a monad $T_{\mathbb{N}^{\mathbb{N}}}$ on the category $\mathsf{Con}$ of contexts and terms in the original language, where $T_{\mathbb{N}^{\mathbb{N}}}$ is defined as follows:

[TABLE]

See Lambek [10, Section 5]. Thus, the standard interpretation transforms a term in context in indeterminate $\Omega$ into an essentially equivalent representation expressed in the original language.

4.1.2 Non-standard interpretation

Let $(T\mathbb{N},\eta,\mathsf{KE}_{\mathbb{N}},\mathsf{At},\_\bullet\_)$ be the structure specified in Proposition 4.1. We define a translation $\rho\mapsto{\rho}^{\dagger}$ of the standard type structure over $\mathbb{N}$ into the non-standard type structure over $T\mathbb{N}$ as follows:

[TABLE]

Each context $\Gamma\equiv x_{0}\colon\rho_{0},\dots,x_{n-1}\colon\rho_{n-1}$ is translated to a context ${\Gamma}^{\dagger}\equiv{x_{0}}^{\dagger}\colon{\rho_{0}}^{\dagger},\dots,{x_{n-1}}^{\dagger}\colon{\rho_{n-1}}^{\dagger}$, where we assume a fixed assignment ${x}^{\dagger}\colon{\rho}^{\dagger}$ of a variable to each variable $x\colon\rho$. Then, a term in context $\Gamma\vdash t[\Omega]\colon\rho$ is translated to a term in context ${\Gamma}^{\dagger}\vdash{t[\Omega]}^{\dagger}\colon{\rho}^{\dagger}$ of $\mathrm{HA}^{\omega}$ as follows:

[TABLE]

Here, each constant $\mathtt{C}$ is translated as follows:

[TABLE]

where for higher types, we define

[TABLE]

4.1.3 Relating two interpretations

We relate two interpretations by a logical relation. Define a binary predicate $\sim_{\rho}$ on $\rho^{\dagger}$ and $\mathbb{N}^{\mathbb{N}}\to\rho$ by induction on types:

[TABLE]

At the base type, $\gamma\sim_{\mathbb{N}}f$ means that $\gamma$ represents $f$. At higher types, the definition of $\sim_{\rho\to\sigma}$ requires application to respect the relation $\sim$: on the left, $Gx$ is the application in the type structure over $T\mathbb{N}$; on the right, $\lambda\alpha.F\alpha(y\alpha)$ corresponds to the application in the Kleisli category of the monad $T_{\mathbb{N}^{\mathbb{N}}}$ (see Remark 4.2).222If we regard $y^{\mathbb{N}^{\mathbb{N}}\to\rho}$ and $F^{\mathbb{N}^{\mathbb{N}}\to(\rho\to\sigma)}$ as global points in the Kleisli category of $T_{\mathbb{N}^{\mathbb{N}}}$, then $\lambda\alpha.F\alpha(y\alpha)$ is obtained by composing $\langle F,y\rangle$ with the term $u\colon\sigma^{\rho},v\colon\rho\vdash\lambda\alpha.uv\colon\mathbb{N}^{\mathbb{N}}\to\sigma$, which represents an evaluation morphism.

Lemma 4.3**.**

For any term $\Gamma\vdash t[\Omega]:{\rho}$ in indeterminate $\Omega$ and context $\Gamma\equiv x_{0}^{\rho_{0}},\dots,x_{n-1}^{\rho_{n-1}}$,

[TABLE]

The proof of Lemma 4.3 relies on the following lifting property.

Lemma 4.4**.**

For each type $\rho$,

[TABLE]

Proof.

By induction on types.

$\rho\equiv\mathbb{N}$: Fix $g^{\mathbb{N}\to{\mathbb{N}}^{\dagger}}$ and $f^{\mathbb{N}\to\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}$, and suppose that $\forall n^{\mathbb{N}}g(n)\sim_{\mathbb{N}}f(n)$. Let $\gamma^{\mathbb{N}^{\dagger}}$ and $h^{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}$ satisfy $\gamma\sim_{\mathbb{N}}h$. Then, for any $\alpha$,

[TABLE]

Thus $\mathsf{KE}_{\mathbb{N}}(g)(\gamma)\sim_{\mathbb{N}}\lambda\alpha.(\lambda n.fn\alpha)(h\alpha)$. Hence $\mathsf{KE}_{\mathbb{N}}(g)\sim_{\mathbb{N}\to\mathbb{N}}\lambda\alpha.(\lambda n.fn\alpha)$.

$\rho\equiv\sigma\to\tau$: Fix $g^{\mathbb{N}\to(\sigma\to\tau)^{\dagger}}$ and $f^{\mathbb{N}\to\mathbb{N}^{\mathbb{N}}\to\sigma\to\tau}$, and suppose that $\forall n^{\mathbb{N}}g(n)\sim_{\sigma\to\tau}f(n)$. Let $\gamma^{\mathbb{N}^{\dagger}}$ and $h^{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}$ satisfy $\gamma\sim_{\mathbb{N}}h$. We must show that

[TABLE]

where $\mathsf{KE}_{\sigma\to\tau}(g)(\gamma)=\lambda u^{\sigma^{\dagger}}.\mathsf{KE}_{\tau}(\lambda x^{\mathbb{N}}.gxu)\gamma$. To this end, fix $u^{\sigma^{\dagger}}$ and $y^{\mathbb{N}^{\mathbb{N}}\to\sigma}$, and suppose that $u\sim_{\sigma}y$. We must show that

[TABLE]

By induction hypothesis, it suffices to show that

[TABLE]

But this follows from the assumptions $\forall n^{\mathbb{N}}g(n)\sim_{\sigma\to\tau}f(n)$ and $u\sim_{\sigma}y$. ∎

Proof of Lemma 4.3..

By induction on terms in contexts.

$\Gamma,x^{\rho},\Delta\vdash x\colon{\rho}$: Trivial.

$\Gamma\vdash\mathtt{C}\colon{\rho}$: We deal with each constant:

$0^{\mathbb{N}}$: We must show $\eta(0)\bullet\alpha=0$, which follows from (4.1).

$\mathsf{Succ}^{\mathbb{N}\to\mathbb{N}}$: By Lemma 4.4, it suffices to show that $\forall n^{\mathbb{N}}\eta(\mathsf{Succ}(n))\sim_{\mathbb{N}}\lambda\alpha.\mathsf{Succ}(n)$. This follows from (4.1).

$\Omega^{\mathbb{N}\to\mathbb{N}}$: By Lemma 4.4, it suffices to show that $\forall n^{\mathbb{N}}\mathsf{At}(n)\sim_{\mathbb{N}}\lambda\alpha.\alpha(n)$. This follows from (4.3).

$\mathsf{Rec}_{\rho}$: Let $u^{\rho^{\dagger}}$ and $y^{\mathbb{N}^{\mathbb{N}}\to\rho}$ such that $u\sim_{\rho}y$, and let $F^{\mathbb{N}^{\dagger}\to\rho^{\dagger}\to\rho^{\dagger}}$ and $f^{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}\to\rho\to\rho}$ such that $F\sim_{\mathbb{N}\to\rho\to\rho}f$. We must show that

[TABLE]

By Lemma 4.4, it suffices to show that

[TABLE]

which follows by a straightforward induction on $n$.

$\Gamma\vdash\lambda x^{\rho}.t^{\sigma}\colon\rho\to\sigma$: Immediate from induction hypothesis for $\Gamma,x^{\rho}\vdash t:\sigma$.

$\Gamma\vdash u^{\rho\to\sigma}v^{\rho}$: Immediate from induction hypothesis. ∎

We now complete the proof of the representation theorem.

Proof of Proposition 4.1.

Let $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ be a closed term of $\mathrm{HA}^{\omega}$. Then $Y\Omega$ is a closed term of type $\mathbb{N}$ in indeterminate $\Omega$. Put $\gamma:={(Y\Omega)}^{\dagger}={Y}^{\dagger}\textup{{gen}}$. By Lemma 4.3, we have $\gamma\sim_{\mathbb{N}}\lambda\alpha.Y\alpha$, i.e., $\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\gamma\bullet\alpha=Y\alpha$. ∎

4.2 Examples

We give some examples of the structure $(T\mathbb{N},\eta,\mathsf{KE}_{\mathbb{N}},\mathsf{At},\_\bullet\_)$ specified in Proposition 4.1.

4.2.1 Dialogue trees

We show how Escardó’s dialogue model [4] fits into the framework of Proposition 4.1. The type $\mathrm{DT}$ of dialogue trees has two constructors

[TABLE]

The constructor $\eta$ creates a leaf node of a tree labelled by a natural number, which represents a possible result of the computation. The constructor $\mathtt{D}$ creates an internal node which is labelled by a natural number and has countably many branches. Internal nodes guide the computation toward the leaves; see definition of $\_\bullet\_$ below.

The recursor $\mathcal{R}^{\mathrm{DT}}_{\rho}$ (for each type $\rho$) of dialogue trees has a type

[TABLE]

and satisfies the following defining equations:

[TABLE]

With the help of recursors, functions $\mathsf{KE}_{\mathbb{N}}\colon(\mathbb{N}\to\mathrm{DT})\to(\mathrm{DT}\to\mathrm{DT})$ and $\_\bullet\_\colon\mathrm{DT}\to\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ are defined as

[TABLE]

Finally, $\mathsf{At}\colon\mathbb{N}\to\mathrm{DT}$ is defined as $\mathsf{At}:=\lambda x^{\mathbb{N}}.\mathtt{D}x\eta$.

Let $\mathrm{HA}^{\omega}+\mathrm{DT}$ be an extension of $\mathrm{HA}^{\omega}$ with the type $\mathrm{DT}$ of dialogue trees as an extra base type. The extension includes the constructors and recursors of dialogue trees, the defining equations of the recursors, and the following induction schema for dialogue trees:

[TABLE]

In $\mathrm{HA}^{\omega}+\mathrm{DT}$, one can show that the structure $(\mathrm{DT},\eta,\mathsf{KE}_{\mathbb{N}},\mathsf{At},\_\bullet\_)$ satisfies (4.1), (4.2), and (4.3) (cf.  Escardó [4, Section 3]). Hence, Proposition 4.1 instantiated with the type of dialogue trees is valid in $\mathrm{HA}^{\omega}+\mathrm{DT}$: every closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathrm{HA}^{\omega}$ can be represented by a dialogue tree.

4.2.2 Brouwer-operations

Dialogue trees are convenient for studying continuity properties of definable functions. For the proof of bar theorem, however, Brouwer-operations (inductively defined neighbourhood functions [15, Chapter 4, Section 8.4]) are more suitable.

The type $\mathrm{BT}$ of Brouwer-operations has two constructors

[TABLE]

where $\eta$ creates a leaf node labelled by a natural number, and $\sup$ creates an internal node from countably many subtrees.

The recursor $\mathcal{R}^{\mathrm{BT}}_{\rho}$ (for each type $\rho$) of Brouwer-operations has a type

[TABLE]

and satisfies the defining equations:

[TABLE]

With the help of recursors, functions $\mathsf{KE}_{\mathbb{N}}\colon(\mathbb{N}\to\mathrm{BT})\to(\mathrm{BT}\to\mathrm{BT})$ and $\_\bullet\_\colon\mathrm{BT}\to\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ are defined as

[TABLE]

Here $\mathsf{Aux}\colon(\mathbb{N}\to\mathrm{BT})\to\mathrm{BT}\to\mathbb{N}^{*}\to\mathrm{BT}$ is a function defined with a help of another auxiliary function $\mathsf{skip}\colon\mathrm{BT}\to\mathbb{N}^{*}\to\mathrm{BT}$ as follows:

[TABLE]

Finally, $\mathsf{At}\colon\mathbb{N}\to\mathrm{BT}$ is defined by a primitive recursion:

[TABLE]

Let $\mathrm{HA}^{\omega}+\mathrm{BT}$ be an extension of $\mathrm{HA}^{\omega}$ with the type $\mathrm{BT}$ of Brouwer-operations as an extra base type.333$\mathrm{HA}^{\omega}+\mathrm{BT}$ is similar to system $\mathsf{T}_{1}$ described in Zucker [17, 6.3.6 (b)]. The extension includes the constructors and recursors of Brouwer-operations, the defining equations of the recursors, and the following induction schema for Brouwer-operations:

[TABLE]

In $\mathrm{HA}^{\omega}+\mathrm{BT}$, one can show that

[TABLE]

for all $f$, $\gamma$, $a$, and $\alpha$, from which (4.2) follows. Conditions (4.1) and (4.3) are easy to check. Hence, Proposition 4.1 instantiated with the type of Brouwer-operations is valid in $\mathrm{HA}^{\omega}+\mathrm{BT}$.

Furthermore, Theorem 3.4 holds in $\mathrm{HA}^{\omega}+\mathrm{BT}$: for any closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathrm{HA}^{\omega}$, there is a closed term $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ of $\mathrm{HA}^{\omega}+\mathrm{BT}$ such that

\mathrm{HA}^{\omega}+\mathrm{BT}\vdash\text{\gamma$is a neighbourhood function of$Y}, 2. 2.

$\mathrm{HA}^{\omega}+\mathrm{BT}\vdash S_{\gamma}\subseteq Q\wedge\operatorname{\textrm{{Ind}}}(Q)\operatorname{\,\rightarrow\,}Q(\langle\,\rangle)$ for any predicate $Q$ on ${\mathbb{N}^{*}}$.

To see this, first, each Brouwer-operation $\gamma$ determines a neighbourhood function $\delta(\gamma)\colon\mathbb{N}^{*}\to\mathbb{N}$ as follows:

[TABLE]

It is easy to see that if a Brouwer-operation $\gamma$ represents a function $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$, i.e., $\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\gamma\bullet\alpha=f(\alpha)$, then $\delta(\gamma)$ is a neighbourhood function of $f$.

Second, it is well known that $\delta(\gamma)$ satisfies induction over unsecured sequences [15, Chapter 4, Proposition 8.12], i.e., $S_{\delta(\gamma)}\subseteq Q\wedge\operatorname{\textrm{{Ind}}}(Q)\operatorname{\,\rightarrow\,}Q(\langle\,\rangle)$ for any predicate $Q$ on $\mathbb{N}^{*}$.

4.3 Non-standard representation as a model construction

If we think of Proposition 4.1 as a set-theoretical model construction as in Escardó [4] — reading $\mathbb{N}$ as the set of natural numbers, $T\mathbb{N}$ as another set, and $\eta,\mathsf{KE}_{\mathbb{N}},\mathsf{At}$, and $\_\bullet\_$ as functions — then we obtain a family of representation theorems for system $\mathsf{T}$ definable functions from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$. Specifically, any $\mathsf{T}$-definable set-theoretical function $f\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ can be represented by an element of $T\mathbb{N}$. In the following, we assume this set-theoretical reading of Proposition 4.1. The argument in this subsection can be carried out in a suitable constructive set theory, e.g., Aczel’s $\mathrm{CZF}$ [1] extended with generalised inductive definitions.

If one is interested in strong continuity properties of $\mathsf{T}$-definable functions, then the dialogue model of Escardó [4] or set-theoretical version of Brouwer-operation model presented in Section 4.2.2 seem to be most suitable. These models allow us to show, for example, uniform continuity of $\mathsf{T}$-definable functions from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ on the Cantor space (cf. Section 6.1). Note, however, that the constructions of these models require generalised inductive definitions.

If one is merely interested in point-wise continuity of $\mathsf{T}$-definable functions, then one can use the following structure:

[TABLE]

where the lambda notations in (4.9) should be read set-theoretically.444This model was suggested by Martín Escardó. With this model, one has that every $\mathsf{T}$-definable function from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ is point-wise continuous.

If one is interested in stronger continuity properties in the absence of generalised inductive definitions, one may instantiate the structure $(T\mathbb{N},\eta,\mathsf{KE}_{\mathbb{N}},\mathsf{At},{\_\bullet\_})$ with neighbourhood functions instead of Brouwer-operations:

[TABLE]

where $\cdot$ is the multiplication, $\operatorname{\mathsf{sg}}$ is the signum function, and $\mu n.A(n)$ is the bounded search function. Note that in the definition of $\_\bullet^{\prime}\!\_$, the condition $\gamma(\overline{\alpha}n)>0$ is satisfied for some $n$ because $\gamma$ is a neighbourhood function.

The idea behind the “neighbourhood function model” presented in (4.10) is expressed in the following lemma.

Lemma 4.5**.**

Let $(T\mathbb{N},\eta,\mathsf{KE}_{\mathbb{N}},\mathsf{At},{\_\bullet\_})$ be the continuous model presented in $\eqref{eq:ContModel}$ and let $(T\mathbb{N}^{\prime},\eta^{\prime},\mathsf{KE}_{\mathbb{N}}^{\prime},\mathsf{At}^{\prime},{\_\bullet^{\prime}\!\_})$ be the neighbourhood function model presented in (4.10). Then

For each $n\in\mathbb{N}$, $\eta^{\prime}(n)$ and $\mathsf{At}^{\prime}(n)$ are neighbourhood functions of $\eta(n)$ and $\mathsf{At}(n)$, respectively; 2. 2.

If $h\colon\mathbb{N}\to T\mathbb{N}^{\prime}$ and $f\colon\mathbb{N}\to T\mathbb{N}$ are functions such that $h(n)$ is a neighbourhood function of $f(n)$ for each $n\in\mathbb{N}$, and if $\gamma$ is a neighbourhood function of $g$, then $\mathsf{KE}_{\mathbb{N}}^{\prime}(h)(\gamma)$ is a neighbourhood function of $\mathsf{KE}_{\mathbb{N}}(f)(g)$; 3. 3.

If $\gamma$ is a neighbourhood function of $f$, then $\gamma\bullet^{\prime}\alpha=f\bullet\alpha$ for all $\alpha\in\mathbb{N}^{\mathbb{N}}$.

Proof.

Straightforward. ∎

With the neighbourhood function model, one has that every $\mathsf{T}$-definable function from $\mathbb{N}^{\mathbb{N}}$ to $\mathbb{N}$ has a neighbourhood function.

5 Proof of bar theorem

The proof of bar theorem (Theorem 3.4) is based on the set-theoretical neighbourhood function model presented in (4.10). However, since the type of “neighbourhood functions” is not directly available in $\mathrm{HA}^{\omega}$, we need to make some adjustments to the proof of Proposition 4.1. Moreover, the domain of a neighbourhood function, unlike that of a Brouwer-operation, does not necessarily admit bar induction. Nevertheless, when a neighbourhood function is presented as a concrete term of $\mathrm{HA}^{\omega}$, we can draw stronger properties from it using logical relations and induction on terms. Those are the basic ideas of the proof presented below.

First, we translate each type $\rho$ to the corresponding type in the type structure over $\mathbb{N}^{*}\to\mathbb{N}$:

[TABLE]

We think of $\mathbb{N}^{\dagger}$ as the type of neighbourhood functions. Obviously, $\mathbb{N}^{\dagger}$ contains functions that are not neighbourhood functions. We take care of this issue by modifying the logical relation below.

We translate each term in context $\Gamma\vdash t[\Omega]\colon\rho$ in indeterminate $\Omega$ as in Section 4.1.2, instantiating $\eta$, $\mathsf{KE}_{\mathbb{N}}$, and $\mathsf{At}$ with the following terms:

[TABLE]

where $\cdot$ and $\operatorname{\mathsf{sg}}$ are the primitive recursive multiplication and signum function, respectively. Note that (5.1) defines terms of $\mathrm{HA}^{\omega}$ while (4.10) defines set-theoretical functions.

The main difference between the interpretation in this section and that of Section 4.1.2 is the lack of term $\_\bullet\_\colon{\mathbb{N}}^{\dagger}\to\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$. Ideally, we would define it as a partial application \gamma\bullet\alpha:=\gamma(\overline{\alpha}(\mu n.\gamma(\overline{\alpha}n)>0))\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1, which would be total if ${\mathbb{N}}^{\dagger}$ were the type of neighbourhood functions (which is not).

We deal with the lack of function $\_\bullet\_$ by modifying the logical relation (4.4) as follows: for each type $\rho$, define a binary predicate $\approx_{\rho}$ on $\rho^{\dagger}$ and $\mathbb{N}^{\mathbb{N}}\to\rho$ by induction on types:

[TABLE]

The proof of Lemma 4.4 has to be adapted to $\approx_{\rho}$.

Lemma 5.1**.**

For each type $\rho$,

[TABLE]

Proof.

By induction on types.

$\rho\equiv\mathbb{N}$: Fix $g^{\mathbb{N}\to\mathbb{N}^{\dagger}}$ and $f^{\mathbb{N}\to\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}$, and suppose that $\forall n^{\mathbb{N}}g(n)\approx_{\mathbb{N}}f(n)$. Let $\gamma^{\mathbb{N}^{\dagger}}$ and $h^{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}}$ satisfy $\gamma\approx_{\mathbb{N}}h$. Put

[TABLE]

We must show that $\delta$ is a neighbourhood function of $\lambda\alpha.f(h(\alpha))\alpha$.

To this end, fix $\alpha$. Since $\gamma$ is a neighbourhood function, there exists an $n$ such that $\gamma(\overline{\alpha}n)>0$. Put i:=\gamma(\overline{\alpha}n)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1. Since $g(i)$ is a neighbourhood function (of $f(i)$), there exists an $m$ such that $g(i)(\overline{\alpha}m)>0$. Put $N:=\max\{n,m\}$ and $a:=\overline{\alpha}N$. Then $\gamma(a)>0$, i=\gamma(a)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1, and $g(i)(a)>0$. Thus $\delta(a)>0$.

Next, suppose that $\delta(a)>0$. Then $\gamma(a)>0$ and g(\gamma(a)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1)(a)>0. Thus, for any $b$,

[TABLE]

Hence, $\delta$ is a neighbourhood function.

Lastly, let $\alpha$ and $n$ such that $\delta(\overline{\alpha}n)>0$. Then $\gamma(\overline{\alpha}n)>0$, and so h(\alpha)=\gamma(\overline{\alpha}n)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1. Since g(\gamma(\overline{\alpha}n\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1))(\overline{\alpha}n)=g(h(\alpha))(\overline{\alpha}n)>0, we have f(h(\alpha))\alpha=g(h(\alpha))(\overline{\alpha}n)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1=\delta(\overline{\alpha}n)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1. Hence, $\delta$ induces $\lambda\alpha.f(h(\alpha))\alpha$.

$\rho\equiv\sigma\to\tau$: The proof is exactly the same as in the inductive case of Lemma 4.4. ∎

Lemma 5.2**.**

For any term $\Gamma\vdash t[\Omega]\colon{\rho}$ in indeterminate $\Omega$ and context $\Gamma\equiv x_{0}^{\rho_{0}},\dots,x_{n-1}^{\rho_{n-1}}$,

[TABLE]

where $t^{\dagger}[\overline{u}/{\overline{x}}^{\dagger}]$ and $t[\alpha/\Omega,\overline{y}(\alpha)/\overline{x}]$ are defined as in (4.8).

Proof.

By induction on terms in contexts.

$\Gamma,x^{\rho},\Delta\vdash x\colon{\rho}$: Trivial.

$\Gamma\vdash\mathtt{C}\colon{\rho}$: We deal with each constant:

$0^{\mathbb{N}}$: We must show that $0^{\dagger}=\eta(0)=\lambda a.\mathsf{Succ}(0)$ is a neighbourhood function of $\lambda\alpha.0$, which is obvious.

$\mathsf{Succ}^{\mathbb{N}\to\mathbb{N}}$: By Lemma 5.1, it suffices to show that for each $n$, $\eta(\mathsf{Succ}(n))=\lambda a.\mathsf{Succ}(\mathsf{Succ}(n))$ is a neighbourhood function of $\lambda\alpha.\mathsf{Succ}(n)$, which is obvious.

$\Omega^{\mathbb{N}\to\mathbb{N}}$: By Lemma 5.1, it suffices to show that for each $n$, $\mathsf{At}(n)$ is a neighbourhood function of $\lambda\alpha.\alpha(n)$, which follows from the definition of $\mathsf{At}$.

$\mathsf{Rec}_{\rho}$: Let $u^{\rho^{\dagger}}$ and $y^{\mathbb{N}^{\mathbb{N}}\to\rho}$ such that $u\sim_{\rho}y$, and let $F^{\mathbb{N}^{\dagger}\to\rho^{\dagger}\to\rho^{\dagger}}$ and $f^{\mathbb{N}^{\mathbb{N}}\to\mathbb{N}\to\rho\to\rho}$ such that $F\sim_{\mathbb{N}\to\rho\to\rho}f$. We must show that

[TABLE]

By Lemma 5.1, it suffices to show that

[TABLE]

which follows by a straightforward induction on $n$.

$\Gamma\vdash\lambda x^{\rho}.t^{\sigma}\colon\rho\to\sigma$: Immediate from induction hypothesis for $\Gamma,x^{\rho}\vdash t:\sigma$.

$\Gamma\vdash u^{\rho\to\sigma}v^{\rho}$: Immediate from induction hypothesis. ∎

For each predicate $Q$ on $\mathbb{N}^{*}$, define a predicate $P^{Q}_{\rho}$ on $\rho^{\dagger}$ by induction on types:

[TABLE]

First, we prove the following lifting property.

Lemma 5.3**.**

For each type $\rho$,

[TABLE]

Proof.

By induction on types.

$\rho\equiv\mathbb{N}$: Fix $g^{\mathbb{N}\to{\mathbb{N}}^{\dagger}}$ and suppose that $\forall n^{\mathbb{N}}\,P^{Q}_{\mathbb{N}}(g(n))$. We must show that $P^{Q}_{\mathbb{N}\to\mathbb{N}}(\mathsf{KE}_{\mathbb{N}}(g))$, i.e.,

[TABLE]

Let $\gamma^{\mathbb{N}^{\dagger}}$ such that $P^{Q}_{\mathbb{N}}(\gamma)$. Put

[TABLE]

As shown in the proof of Lemma 5.1, $\delta$ is a neighbourhood function. Fix $a^{\mathbb{N}^{*}}$, and suppose that $\forall b^{\mathbb{N}^{*}}\left[S_{\delta}(a*b)\operatorname{\,\rightarrow\,}Q(a*b)\right]$ and that $Q$ is inductive. We must show that $Q(a)$. Since $P^{Q}_{\mathbb{N}}(\gamma)$, it suffices to show that

[TABLE]

Let $b^{\mathbb{N}^{*}}$ such that $S_{\gamma}(a*b)$, and put i:=\gamma(a*b)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}1. Since $P^{Q}_{\mathbb{N}}(g(i))$, to see that $Q(a*b)$ holds, it suffices to show that $\forall c^{\mathbb{N}^{*}}\left[S_{g(i)}(a*b*c)\operatorname{\,\rightarrow\,}Q(a*b*c)\right]$. Let $c^{\mathbb{N}^{*}}$ such that $S_{g(i)}(a*b*c)$. Then $S_{\delta}(a*b*c)$ and so $Q(a*b*c)$ as required.

$\rho\equiv\sigma\to\tau$: Fix $g^{\mathbb{N}\to{(\sigma\to\tau)}^{\dagger}}$ and suppose that $\forall n^{\mathbb{N}}P^{Q}_{\sigma\to\tau}(g(n))$. Let $\gamma^{\mathbb{N}^{\dagger}}$ and $u^{\sigma^{\dagger}}$ such that $P^{Q}_{\mathbb{N}}(\gamma)$ and $P^{Q}_{\sigma}(u)$. We must show that $P^{Q}_{\tau}(\mathsf{KE}_{\tau}(\lambda n^{\mathbb{N}}.g(n)u)\gamma)$. Since $\forall n^{\mathbb{N}}\;P^{Q}_{\tau}(g(n)u)$, we have $P^{Q}_{\mathbb{N}\to\tau}(\mathsf{KE}_{\tau}(\lambda n^{\mathbb{N}}.g(n)u))$ by induction hypothesis. Therefore $P^{Q}_{\tau}(\mathsf{KE}_{\tau}(\lambda n^{\mathbb{N}}.g(n)u)\gamma)$. ∎

Lemma 5.4**.**

For any term $\Gamma\vdash t[\Omega]\colon{\rho}$ in indeterminate $\Omega$ and context $\Gamma\equiv x_{0}^{\rho_{0}},\dots,x_{n-1}^{\rho_{n-1}}$,

[TABLE]

Proof.

By induction on terms in contexts.

$\Gamma,x^{\rho},\Delta\vdash x\colon{\rho}$: Trivial.

$\Gamma\vdash\mathtt{C}\colon{\rho}$: We deal with each constant below:

$0^{\mathbb{N}}$: The term $0^{\dagger}\equiv\lambda a.\mathsf{Succ}(0)$ obviously satisfies the required property.

$\mathsf{Succ}^{\mathbb{N}\to\mathbb{N}}$: By Lemma 5.3, it suffices to show that $\forall n^{\mathbb{N}}.P^{Q}_{\mathbb{N}}(\lambda a.\eta(\mathsf{Succ}(n)))$, which is obvious.

$\Omega^{\mathbb{N}\to\mathbb{N}}$: By Lemma 5.3, it suffices to show that $\forall n^{\mathbb{N}}P^{Q}_{\mathbb{N}}(\mathsf{At}(n))$. Fix $n^{\mathbb{N}}$. Then $\mathsf{At}(n)$ is a neighbourhood function. Let $a^{\mathbb{N}^{*}}$ satisfy

[TABLE]

and suppose that $Q$ is inductive. Put k:=n\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}\lvert a\rvert+1. For each $b^{\mathbb{N}^{*}}$ such that $\lvert b\rvert=k$, we have $\mathsf{At}(n)(a*b)>0$, and so $Q(a*b)$. Thus, $Q(a)$ by Lemma 3.3.

$\mathsf{Rec}_{\rho}$: Let $u^{\rho^{\dagger}}$ and $F^{\mathbb{N}^{\dagger}\to\rho^{\dagger}\to\rho^{\dagger}}$ satisfy $P^{Q}_{\rho}$ and $P^{Q}_{\mathbb{N}\to\rho\to\rho}$, respectively. We must show that $P^{Q}_{\mathbb{N}\to\rho}(\mathsf{KE}_{\rho}(\mathsf{Rec}_{\rho^{\dagger}}(u,\lambda x.F(\eta(x))))).$ By Lemma 5.3, it suffices to show that $\forall n^{\mathbb{N}}\;P^{Q}_{\rho}(\mathsf{Rec}_{\rho^{\dagger}}(u,\lambda x.F(\eta(x)))n).$ This follows by a straightforward induction on $n$ using assumptions $P^{Q}_{\rho}(u)$ and $P^{Q}_{\mathbb{N}\to\rho\to\rho}(F)$ and the fact that $P^{Q}_{\mathbb{N}}(\eta(n))$ for each $n^{\mathbb{N}}$.

$\Gamma\vdash\lambda x^{\rho}.t^{\sigma}\colon\rho\to\sigma$: Immediate from induction hypothesis for $\Gamma,x^{\rho}\vdash t\colon\sigma$.

$\Gamma\vdash u^{\rho\to\sigma}v^{\rho}$: Immediate from induction hypothesis. ∎

We now complete the proof of bar theorem.

Proof of Theorem 3.4.

Let $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ be a closed term of $\mathrm{HA}^{\omega}$. Then, $Y\Omega$ is a closed term of type $\mathbb{N}$ in indeterminate $\Omega$. Thus, $\gamma\equiv(Y\Omega)^{\dagger}$ is a neighbourhood function of $Y$ by Lemma 5.2. By Lemma 5.4, we also have that $\mathrm{HA}^{\omega}\vdash P^{Q}_{\mathbb{N}}(\gamma)$ for any predicate $Q$ on $\mathbb{N}^{*}$. Hence $\mathrm{HA}^{\omega}\vdash S_{\gamma}\subseteq Q\wedge\operatorname{\textrm{{Ind}}}(Q)\operatorname{\,\rightarrow\,}Q(\langle\,\rangle).$ ∎

6 Applications of bar theorem

We prove some well-known properties of $\mathrm{HA}^{\omega}$ as applications of bar theorem.

6.1 Uniform continuity on the Cantor space

We show that the restriction of a closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ to the Cantor space (the space of binary sequences) is uniformly continuous.

Theorem 6.1**.**

For any closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ of $\mathrm{HA}^{\omega}$,

[TABLE]

Here, we use the abbreviation $\forall\alpha^{2^{\mathbb{N}}}A(\alpha)\equiv\forall\alpha^{\mathbb{N}^{\mathbb{N}}}\left[\forall n^{\mathbb{N}}\alpha n\leq 1\operatorname{\,\rightarrow\,}A(\alpha)\right].$

Proof.

Let $Y$ be a closed term of type $\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$. By Theorem 3.4, there is a neighbourhood function $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ of $Y$ which satisfies (3.2) for any predicate $Q$ on $\mathbb{N}^{*}$. In particular, consider a predicate $Q$ on $\mathbb{N}^{*}$ defined as

[TABLE]

where $\mathsf{Bin}(a)\equiv\forall n<\lvert a\rvert\;a_{n}\leq 1$. Clearly, $S_{\gamma}\subseteq Q$ and $Q$ is inductive. Hence $Q(\langle\,\rangle)$, which is the statement to be proved. ∎

6.2 Closure under the rule of bar induction

The rule of bar induction (without parameters) says that for any predicate $P$ on $\mathbb{N}^{*}$ without parameters other than $a$, if

[TABLE]

then for any predicate $Q$ on $\mathbb{N}^{*}$,

[TABLE]

Theorem 6.2**.**

$\mathrm{HA}^{\omega}$* is closed under the rule of bar induction.*

Proof.

Let $P(a^{\mathbb{N}^{*}})$ be a predicate on $\mathbb{N}^{*}$ without parameters other than $a$. Suppose that

[TABLE]

By the modified realizability [14, Chapter 3, Section 4], we have a closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ such that

[TABLE]

By Theorem 3.4, there is a neighbourhood function $\gamma\colon\mathbb{N}^{*}\to\mathbb{N}$ of $Y$ which satisfies (3.2) for any predicate $Q$ on $\mathbb{N}^{*}$.

Let $Q$ be a predicate on $\mathbb{N}^{*}$. We show that

[TABLE]

from which (6.1) follows immediately. Suppose that $P\subseteq Q$ and that $Q$ is inductive. Let $a^{\mathbb{N}^{*}}$ satisfy $S_{\gamma}$, i.e., $\gamma(a)>0$, and put k:=\gamma(a)\mathbin{\ooalign{\hss\raise 2.58334pt\hbox{\cdot}\hss\crcr-}}\lvert a\rvert. Since $P$ is monotone, we have $P(a*b)$ for all $b$ such that $\lvert b\rvert=k$. Thus $Q(a*b)$ for all $b$ such that $\lvert b\rvert=k$. Hence $Q(a)$ by Lemma 3.3. Therefore $S_{\gamma}\subseteq Q$. ∎

6.3 Closure of bar recursion for the lowest type

For each pair of types $\tau,\sigma$, Spector’s bar recursion is the following schema:

[TABLE]

where $a\colon\tau^{*}$, $G\colon\tau^{*}\to\sigma$, $H\colon\tau^{*}\to(\tau\to\sigma)\to\sigma$, and $Y\colon(\mathbb{N}\to\tau)\to\mathbb{N}$.555Our definition of $\mathrm{HA}^{\omega}$ does not include type $\tau^{*}$ of finite sequences for an arbitrary type $\tau$. Hence, bar recursion is understood to be formulated in an extension of $\mathrm{HA}^{\omega}$ with the type $\tau^{*}$ of finite sequences for each type $\tau$.

We call a function ${\mathsf{BR}}^{\tau,\sigma}$ of type

[TABLE]

which satisfies (6.3) a bar recursor of types $\tau$ and $\sigma$. The first argument of a bar recursor, i.e., a function of type $(\mathbb{N}\to\tau)\to\mathbb{N})$, is called a stopping function of bar recursion.

Schwichtenberg [13] showed that if $Y,G$, and $H$ are closed terms of Gödel’s system $\mathsf{T}$ and the type $\tau$ is of level [math] or $1$, then the function $\lambda a.{\mathsf{BR}}(Y,G,H)(a)$ which satisfies (6.3) is $\mathsf{T}$-definable. His proof requires a detour through a system based on infinite terms. Oliva and Steila [11] strengthened Schwichtenberg’s result by giving an explicit construction of the function $\lambda G.\lambda H.\lambda a.{\mathsf{BR}}(Y,G,H)(a)$ from a closed term $Y\colon(\mathbb{N}\to\tau)\to\mathbb{N}$ (for type $\tau$ of level [math] and $1$), and showed that it satisfies the defining equation of bar recursion for any $G,H$ and $a$.

We give another construction of a bar recursive function for the lowest type from a closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$ using modified realizability.

Theorem 6.3**.**

For any type $\sigma$ and a closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$, there exists a closed term $\xi$ of type

[TABLE]

which satisfies the defining equation of the bar recursion for $Y$, i.e.,

[TABLE]

Proof.

Fix a type $\sigma$ and a closed term $Y\colon\mathbb{N}^{\mathbb{N}}\to\mathbb{N}$. By Theorem 3.4, there is a closed term $\gamma:{\mathbb{N}^{*}\to\mathbb{N}}$ which is a neighbourhood function of $Y$ and satisfies (3.2) for any predicate $Q$ on $\mathbb{N}^{*}$. Define a predicate $P_{Y}$ on $\mathbb{N}^{*}$ by

[TABLE]

For any predicate $Q$ on $\mathbb{N}^{*}$, it is straightforward to show that

[TABLE]

See the argument following (6.2). Thus

[TABLE]

Define a predicate $Q$ on ${\mathbb{N}^{*}}$ by

[TABLE]

where $\xi$ is of type $(\mathbb{N}^{*}\to\sigma)\to(\mathbb{N}^{*}\to(\mathbb{N}\to\sigma)\to\sigma)\to\mathbb{N}^{*}\to\sigma$ and $\mathcal{BR}(\xi,a)$ is the following formula:

[TABLE]

We show that $P_{Y}\cap S_{\gamma}\subseteq Q$ and that $Q$ is inductive.

$P_{Y}\cap S_{\gamma}\subseteq Q$: Let $a^{\mathbb{N}^{*}}$ satisfy $P_{Y}\cap S_{\gamma}$. Then, for any $b^{\mathbb{N}^{*}}$ we have $Y(\widehat{a*b})=Y(\widehat{a})<\lvert a\rvert\leq\lvert a\rvert+\lvert b\rvert$. Hence, the function $\xi:=\lambda G.\lambda H.G$ witnesses $Q(a)$.

$Q$ is inductive: Suppose that $\forall x^{\mathbb{N}}Q(a*\langle x\rangle)$. For each $x^{\mathbb{N}}$, there exists a function $\xi_{x}$ such that $\mathcal{BR}(\xi_{x},a*\langle x\rangle)$. By countable choice ($\mathrm{\textup{AC}_{0}}$), there exists a sequence $(\xi_{x})_{x^{\mathbb{N}}}$ of functions such that $\mathcal{BR}(\xi_{x},a*\langle x\rangle)$ for each $x$.

For any $G\colon\mathbb{N}^{*}\to\sigma$, $H\colon\mathbb{N}^{*}\to(\mathbb{N}\to\sigma)\to\sigma$ and $b\colon\mathbb{N}^{*}$, define $\xi(G,H)(b)$ by induction on the length of $b$:

[TABLE]

where $G_{x}$ and $H_{x}$ are defined by

[TABLE]

We must show that $\mathcal{BR}(\xi,a)$. Fix $G,H$, and $b$. We distinguish two cases:

Case $b\equiv\langle\,\rangle$: If $Y(\widehat{a})<\lvert a\rvert$, then $\xi(G,H)(\langle\,\rangle)=G(\langle\,\rangle)$. Otherwise

[TABLE]

Case $b\equiv\langle x\rangle*b^{\prime}$ for some $b^{\prime}$: If $Y(\widehat{a*b})<\lvert a\rvert+\lvert b\rvert$, then $Y(\widehat{a*\langle x\rangle*b^{\prime}})<\lvert a*\langle x\rangle\rvert+\lvert b^{\prime}\rvert$. Thus $\xi(G,H)(b)=\xi_{x}(G_{x},H_{x})(b^{\prime})=G_{x}(b^{\prime})=G(b).$ Otherwise

[TABLE]

Hence $\mathcal{BR}(\xi,a)$. Thus $Q$ is inductive.

Therefore $Q(\langle\,\rangle)$, and so

[TABLE]

Since $\mathcal{BR}(\xi,\langle\,\rangle)$ is a purely universal statement, modified realizability yields a witness $\xi$ as a closed term of $\mathrm{HA}^{\omega}$ for which (6.4) holds. Note that since countable choice is modified realizable, the use of countable choice is eliminated in the last step. ∎

Acknowledgements

I thank Martín Escardó, Makoto Fujiwara, Paul-André Melliès, Paulo Oliva, and Giuseppe Rosolini for useful discussions. I also thank Ulrich Kohlenbach for the reference to his proof of the fan rule for $\mathrm{HA}^{\omega}$. This work was carried out while I was visiting the Hausdorff Research Institute for Mathematics (HIM), University of Bonn, for their trimester program “Types, Sets and Constructions” (May–August 2018). I thank the institute for their support and hospitality, and the organisers of the program for creating a stimulating environment for research.