A constructive proof of the dense existence of nowhere-differentiable functions in C [ 0,1 ]

Abstract

In this paper, we show that the dense existence of nowhere-differentiable continuous functions in $C [0, 1]$ is provable, using a version of the Baire category theorem, in an intuitionistic subsystem of elementary analysis whose induction is restricted to $Σ_{1}^{0}$ formulae.

Keywords

Constructive mathematics constructive reverse mathematics Baire category theorem nowhere-differentiable functions

1. Introduction

Banach [1] proved that nowhere-differentiable continuous function exist densely in $C [0, 1]$ . This proof is based on two facts. First, the sets $G_{m, n}$ are dense and open in $C [0, 1]$ for each m and n, where $G_{m, n}$ is defined by $\begin{array}{l} G_{m, n} = {f \in C [0, 1] : \forall x \in [0, 1] \exists y \in [0, 1] (| x - y | < \frac{1}{m} \land | \frac{f (x) - f (y)}{x - y} | > n)} . \end{array}$ Second, the following Baire category theorem holds:

Let ${U_{n}}$ be a sequence of dense open sets in a complete metric space X. Then the intersection $⋂_{n = 0}^{\infty} U_{n}$ is also dense in X.

The Baire category theorem is analyzed in various mathematical settings. Bishop [3, Ch. 4, Theorem 4] gave a constructive proof of it using Dependent Choice, a principle generally accepted in his mathematics. Brown and Simpson [5] showed that ${RCA}_{0}$ , the base theory of Friedman–Simpson’s reverse mathematics, proves B.C.T.I., the Baire category theorem restricted to complete separable metric spaces. The equivalence between B.C.T.I. and $Σ_{1}^{0}$ induction was later shown over a weaker base theory ${RCA}_{0}^{*}$ in [12]. Brown and Simpson [5] also showed that a version of the Baire category theorem, which they called B.C.T.II., cannot be proved in ${RCA}_{0}$ . The main difference between B.C.T.I and B.C.T.II. is the definition of open sets in complete separable metric spaces. In the former, the statement “x is a point of an open set U” is $Σ_{1}^{0}$ and in the latter, it is $Σ_{2}^{0}$ . This shows that in a weak system of analysis the strength of the Baire category theorem depends on the formulation of the sequence of dense open sets. Ishihara and Schuster [7] proved that a kind of contraposition of B.C.T.I. holds under the assumption of weak continuity principle. Brattka [4] analyzed two versions of computable Baire category theorem in computable analysis and showed that one of them implies the existence of a computable sequence of computable and nowhere-differentiable continuous functions on $[0, 1]$ .

In this paper, we prove that Banach’s classical proof of the dense existence of nowhere-differentiable continuous functions in $C [0, 1]$ also works in a subsystem of intuitionistic elementary analysis with the induction schema restricted to $Σ_{1}^{0}$ formulae. We give a recursive definition of a sequence of open sets which acts in the same way as the above ${(G_{m, n})}_{m, n}$ in Banach’s proof. We also show the equivalence found in [12] holds constructively.

The remaining of this paper is organized as follows. In Section 2, we introduce the system ${EL}_{0}^{*}$ of elementary analysis and give basic definitions which we need in later sections. In Section 3, we show the equivalence between a version of the Baire category theorem and $Σ_{1}^{0}$ induction over ${EL}_{0}^{*}$ . In Section 4, we define $C [0, 1]$ , the space of uniformly continuous functions on $[0, 1]$ , as a complete separable metric space. In Section 5, we prove the main theorem, i.e., ${EL}_{0}^{*} + Σ_{1}^{0}$ induction proves that nowhere-differentiable continuous functions exist densely in $C [0, 1]$ .

2. Preliminaries

We use the system ${EL}_{0}^{*}$ defined in [9, Definition 2.17] as a formal base system in this paper. The language $L_{1}$ for the first order arithmetic $i Δ_{0} (exp)$ consists of the equality =, constants 0 and 1, binary function symbols +, · and exp and a binary relation symbol <. The class $Δ_{0}$ of formulae consists of formulae whose occurrences of quantifiers are of the form $(\forall i < v (j))$ or $(\exists i < v (j))$ for some term $v (j)$ in which j may occur.

The system ${i Δ}_{0} (exp)$ is based on intuitionistic logic and consists of the following axioms:

Basic arithmetic: $\begin{array}{l} i + 0 = i; i + (j + 1) = (i + j) + 1; i \cdot 0 = 0; i \cdot (j + 1) = i \cdot j + i; \\ exp (i, 0) = 1; exp (i, j + 1) = exp (i, j) \cdot i; i < i + 1; \\ i < j \to (i + 1) < j \lor i + 1 = j; \neg (i < i); i < j \land j < k \to i < k . \end{array}$

$Δ_{0} - IND$ : $A (0) \land \forall i (A (i) \to A (i + 1)) \to \forall x A (x)$ , for any $Δ_{0}$ formula.

Variables of

L_{1}

are denoted, possibly with subscripts, by lower-case Latin letters i, j, k, l, m and n.

For a standard n, a function $f : N^{n} \to N$ is bounded $Δ_{0}$ definable in ${i Δ}_{0} (exp)$ when $f (\vec{i}) = j$ if and only if $N ⊧ j < v (\vec{i}) \land B (\vec{i}, j)$ for some $Δ_{0}$ formula $B (\vec{i}, j)$ and some term $v (\vec{i})$ such that ${i Δ}_{0} (exp) ⊢ \forall \vec{i} (\exists! j < v (\vec{i})) B (\vec{i}, j)$ . In ${i Δ}_{0} (exp)$ , we fix a bounded $Δ_{0}$ definable bijective pairing $(-, -) : N \times N \to N$ and projections ${(-)}_{i}$ satisfying the following:

$m ⩽ (m, n) \land n ⩽ (m, n) \land ((m, n) \land (k, l) \to m = k \land n = l)$ ;

${((m, n))}_{0} = m \land {((m, n))}_{1} = n \land \forall k (\exists! m < k) (\exists! n < k) ({(k)}_{0} = m \land {(k)}_{1} = n)$ .

We have a

Δ_{0}

predicate

m \in N^{< N}

L_{1}

intended to express m is a code of a finite sequence of natural numbers. We can also fix bounded

Δ_{0}

definable functions length

m \mapsto | m |

, i-th element

[m, i] \mapsto m (i)

, 1-length sequence

m \mapsto ⟨ m ⟩

and concatenation

[m, n] \mapsto m * n

such that

{i Δ}_{0} (exp)

proves the following:

$m \in N^{< N} \land n \in N^{< N} \land | m | = | n | \land (\forall i < | m |) (m (i) = n (i)) \to m = n$ .

$\exists m (m \in N^{< N} \land | m | = 0)$ .

$| ⟨ m ⟩ | = 1 \land (⟨ m ⟩) (0) = m$ .

$m \in N^{< N} \land n \in N^{< N} \to m * n \in N^{< N} \land | m * n | = | m | + | n | \land \forall i ((i < | m | \to (m * n) (i) = m (i)) \land (| n | ⩽ i < | m | + | n | \to (m * n) (i) = n (i - | m |))) .$

$m \in N^{< N} \to | m | < m \land (\forall i < | m |) (m (i) < m)$

$m \in N^{< N} \land n \in N^{< N} \land | m | ⩽ | n | \land (\forall i < | m |) (m (i) ⩽ n (i)) \to m < n$ .

The language $L_{F}$ of the elementary analysis ${EL}_{0}^{*}$ is the two-sorted first order language, whose sorts are called number and function. It includes $L_{1}$ as the part of the number sort, and has, additionally,

function symbols $Ev$ and $Rest$ of arity one function and one number and of value number.

Variables of the function sort are denoted by Greek letters α, β, γ, etc.. We often write

α (i)

for

Ev (α, i)

and

\overline{α} i

for

Rest (α, i)

The class $Δ_{0}^{0}$ of $L_{F}$ formulae consists of formulae whose occurrences of quantifiers are of the form $(\forall i < v (j))$ or $(\exists i < v (j))$ for some term $v (j)$ in which j may occur. The class $Σ_{1}^{0}$ consists of formulae of the form $\exists x A$ for some $Δ_{0}^{0}$ formula A.

The system ${EL}_{0}^{*}$ is based on intuitionistic logic and consists of the following axioms:

Basic arithmetic axioms of ${i Δ}_{0} (exp)$ .

$Δ_{0}^{0} - IND$ : $A (0) \land \forall i (A (i) \to A (i + 1)) \to \forall x A (x)$ , for any $Δ_{0}^{0}$ formula.

Axioms for the restriction: $\begin{array}{l} \overline{α} 0 = ⟨ \cdot ⟩; \overline{α} (i + 1) = (\overline{α} i) * ⟨ α (i) ⟩ . \end{array}$

$Δ_{0}^{0}$ bounded search: $\exists β \forall i [(\exists j < v (i)) A (i, j) \to β (i) < t (i) \land A (i, β (i))]$ , for any $Δ_{0}^{0}$ formula A.

$Δ_{0}^{0} - {AC}^{00}$ : $\forall i \exists j A (i, j) \to \exists β \forall i A (i, β (i))$ , for any $Δ_{0}^{0}$ formula A.

In [9, Definition 2.10], the system consisting of 1-4 is called

{EL}_{0}^{-}

, which is explained as almost equivalent to the system

{EL}_{ELEM}

defined in [6, 16.2]. In [9, Section 5.1], it is shown that

{EL}_{0}^{*}

and

{RCA}_{0}^{*}

are mutually

Π_{2}^{0}

preservingly interpretable.

Lemma 2.1.
${EL}_{0}^{}$ proves* $Σ_{1}^{0} - Bdg$ and $Σ_{1}^{0} - {DC}^{0}$ , where $Σ_{1}^{0} - Bdg$ is $\begin{array}{l} (\forall i < m) \exists j A (i, j) \to \exists n (\forall i < m) (\exists j < n) A (i, j), for any Σ_{1}^{0} formula A, \end{array}$ and $Σ_{1}^{0} - {DC}^{0}$ is $\begin{array}{l} \forall i, j (A (i, j) \to \exists k A (j, k)) \to \forall i, j [A (i, j) \to \exists α (α (0) = i \land \forall n A (α (n), α (n + 1)))], \end{array}$ for any $Σ_{1}^{0}$ formula A.
Proof.
See [9, Lemma 2.16 (3)ii and (4)ii]. □

Using paring function $(-, -)$ , we can code integers $Z$ , rationals $Q$ and finite sequences of them into natural numbers, develop the elementary theory of operations on $Z$ and $Q$ and prove their basic properties in ${EL}_{0}^{}$ . We use metavariables, possibly with subscripts, a, b, c and d for rationals, s, t and u for finite sequences of rationals and $Q^{< N}$ for the sets of finite sequences of rationals. For real numbers, we adopt the definitions given in [2, Section 2]. A real number* is an infinite sequence ${(a_{n})}_{n}$ of rationals such that $\begin{array}{l} \forall m n (| a_{m} - a_{n} | < 2^{- m} + 2^{- n}) . \end{array}$ The relations <, ⩽ and = between real numbers $x = {(a_{n})}_{n}$ and $y = {(b_{n})}_{n}$ are defined by $\begin{array}{l} x < y \Leftrightarrow \exists n (2^{- n + 2} < b_{n} - a_{n}), \end{array}$ $x ⩽ y \Leftrightarrow \neg (y < x)$ , and $y = x \Leftrightarrow x ⩽ y \land y ⩽ x$ , respectively. We can define the arithmetical operations on reals and prove basic theorems on them in ${EL}_{0}^{}$ ; see [13, Ch.5, 2 and 3].

We use the following definition of complete separable metric space. Similar definitions were given in [6, 16.6] and [11, II.5]. Definition 2.2.
A complete separable metric space $X_{ρ}$ is a pair $(X, ρ)$ of $X \subseteq N$ and a pseudometric* $ρ \in X^{2} \to R$ , that is for all i, j and k in X $\begin{array}{l} ρ (i, i) = 0; ρ (i, j) = ρ (j, i); ρ (i, j) ⩽ ρ (i, k) + ρ (k, j); \end{array}$ A point of the complete separable metric space $X_{ρ}$ is a function $α : N \to X$ such that $\begin{array}{l} \forall m n (ρ (α (m), α (n)) < 2^{- m} + 2^{- n}) . \end{array}$ We write $α \in X_{ρ}$ if α is a point of $X_{ρ}$ . The pseudometric between the points of $X_{ρ}$ is defined by $\begin{array}{l} ρ (α, β) : = lim_{k \to \infty} ρ (α (k), β (k)) . \end{array}$ The equality = on $X_{ρ}$ is defined by $ρ (α, β) = 0$ . Then ρ is a metric on $X_{ρ}$ , i.e., a pseudometric satisfying $ρ (α, β) = 0 \to α = β$ . For $i \in X$ and $α \in X_{ρ}$ , we write $ρ (α, i)$ and $ρ (i, α)$ , respectively, for $ρ (α, λ j . i)$ and $ρ (λ j . i, α)$ , where $λ j . i$ is a function β defined by $β (j) = i$ .

We can show the completeness of complete separable metric space in ${EL}_{0}^{*}$ by a straightforward modification of the proof [13, Ch.5, 4.2].

3. The Baire category theorem

An open set in a complete separable metric space $X_{ρ}$ is a sequence $β : N \to (X \times Q^{+}) \cup {0}$ . A point $α \in X_{ρ}$ is in β, denoted by $α \in β$ , if there is $n \in N$ such that $β (n) = (i, b)$ for some $(i, b) \in X \times Q^{+}$ and $ρ (α, i) < b$ . An open set β in $X_{ρ}$ is dense if, for any $α \in X_{ρ}$ and $l \in N$ , there is $γ \in X_{ρ}$ such that $ρ (α, γ) < 2^{- l}$ and $γ \in β$ .

Remark 3.1.
An open set β in $X_{ρ}$ is dense if and only if the following (∗) holds: $()$
For any $α \in X_{ρ}$ and $l \in N$ , there are $i, j \in X$ and $k \in N$ such that $β (k) = (j, b)$ and $ρ (α, i) < 2^{- l}$ and $ρ (i, j) < b$ .
It is easy to see that (∗) implies that β is dense. For the converse, assume that β is dense in $X_{ρ}$ . Then, for each $α \in X_{ρ}$ and $l \in N$ , there are $k \in N$ , $j \in X$ and $γ \in X_{ρ}$ such that $ρ (α, γ) < 2^{- (l + 1)}$ , $β (k) = (j, b)$ and $ρ (γ, j) < b$ . Take i such that $2^{- i} < b - ρ (γ, j)$ and let $m = max {l + 2, i + 1}$ . Then we have $\begin{array}{l} ρ (α, γ m) ⩽ ρ (α, γ) + ρ (γ, γ m) < 2^{- (l + 1)} + 2^{- (l + 1)} = 2^{- l} and \\ ρ (γ m, j) ⩽ ρ (γ m, γ) + ρ (γ, j) ⩽ 2^{- i} + ρ (γ, j) < b . \end{array}$

The Baire category theorem* ( $BCT$ ) is stated as follows:
$BCT$ :
Let $X_{ρ}$ be a complete separable metric space. If $⟨ β_{n} : n \in N ⟩$ is a sequence of dense open sets in $X_{ρ}$ , then, for each $α \in X_{ρ}$ and $l \in N$ , there is $γ \in X_{ρ}$ such that $ρ (γ, α) < 2^{- l}$ and $γ \in β_{n}$ for all n.

In [12], it is proved that $BCT$ is equivalent to $Σ_{1}^{0}$ induction over ${RCA}_{0}^{}$ . As we see next, this proof also works in ${EL}_{0}^{}$ .
Lemma 3.2.
${EL}_{0}^{} + Σ_{1}^{0} - IND$ proves* $BCT$ .
Proof.
This proof is almost the same to the proof of [5, Theorem 2.1], using $Δ_{0}^{0} - {AC}^{00}$ and $Δ_{0}^{0} - {DC}^{0}$ instead of minimization and primitive recursion. □

Let ${[N]}^{< N}$ be the set of finite strict increasing sequence of natural numbers, i.e., the set of $s \in N^{< N}$ such that $i < j < | s |$ implies $s (i) < s (j)$ . For a formula A and a sequence $s \in {[N]}^{< N}$ , we write $s \subseteq A$ if $A (s (i))$ for all $i < | s |$ . Intuitively, s and A represent the sets ${s (0), \dots, s (| s | - 1)}$ and ${x : A (x)}$ of natural numbers, respectively.
Lemma 3.3.
The following are equivalent over ${EL}_{0}^{}$ .
$Σ_{1}^{0} - IND$ ;

$\forall x (\exists y > x) A (y) \to \forall x \exists s \in {[N]}^{< N} (s \subseteq A \land | s | = x)$ , for* $Δ_{0}^{0}$ formula $A (y)$ .

Proof.
This is proved in [8, Theorem 99]. Although the proof is given over the system $i Σ_{1}$ of first order intuitionistic arithmetic with $Σ_{1}^{0}$ induction, we can similarly prove it in ${EL}_{0}^{}$ . In [14, Lemma 3.2], a proof over a classical system is given. □

The Cantor space* ${0, 1}^{N}$ is a complete separable metric space $X_{ρ}$ given by $X = {0, 1}^{< N} = {s \in N^{< N} : (\forall i < | s |) (s (i) < 2)}$ and d defined by $\begin{array}{l} d (s, t) = \{\begin{matrix} 2^{- i} & if i is the least j < min {| s |, | t |} with s (j) \neq t (j); \\ 2^{- i} & if s ⊊ t and i is the least j with j ⩾ | s | \land t (j) = 1; \\ 2^{- i} & if t ⊊ s and i is the least j with j ⩾ | t | \land s (j) = 1; \\ 0 & if such j does not exist, \end{matrix} \end{array}$ where $s ⊊ t$ is an abbreviation of $| s | < | t | \land (\forall i < | s |) (s (i) = t (i))$ . A point in $α \in {0, 1}^{N}$ is identified with a sequence $β \in {0, 1}^{N}$ defined by $β (n) = (α (2 n)) (n)$ if $| α (2 n) | > n$ and $β (n) = 0$ otherwise. Then, for $β, γ \in {0, 1}^{N}$ and $s \in {0, 1}^{< N}$ , $d (β, γ) = {lim}_{i \to \infty} d (\overline{β} i, \overline{γ} i)$ and $d (s, β) = d (β, s) = {lim}_{i \to \infty} d (\overline{β} i, s)$ . Lemma 3.4.
${EL}_{0}^{} + BCT$ proves* $Σ_{1}^{0} - IND$ .
Proof.
This can be proved in almost the same way to the proof of the implication $4 \Rightarrow 1$ of [12, Theorem 1]. Instead of Lemma 1 and $⟨ D_{i} : i \in N ⟩$ used in the proof, use Lemma 3.3 and a sequence $⟨ β_{i} : i \in N ⟩$ of open sets in the Cantor space defined by $\begin{array}{l} β_{i} (n) = \{\begin{matrix} (s, 2^{- | s |}) & if n is a (code of) sequence of the form s * ⟨ 1 ⟩ * 0^{k} * ⟨ 1 ⟩ * 0^{i} * ⟨ 1 ⟩ \\ for some s \in {0, 1}^{< N} and k such that k > | s | \land A (k); \\ 0 & otherwise, \end{matrix} \end{array}$ where $0^{k}$ is the sequence s of length k such that $(\forall i < k) (s (i) = 0)$ . □

4. The space C[0,1]

In what follows, we work in ${EL}_{0}^{*}$ .

Let $s = ⟨ a_{0}, \dots, a_{2^{m}} ⟩$ be a finite sequence of rationals with length $2^{m} + 1$ for some m. Then s is a code of the function $℘_{s} (x) : R \to R$ which attains $a_{k}$ at $2^{- m} k$ and it is linear on $[2^{- m} j, 2^{- m} (j + 1)]$ for each $k ⩽ 2^{m}$ and $j < 2^{m}$ . More precisely, for each sequence $s = ⟨ a_{0}, a_{1} ⟩$ of rationals with length 2, let $℘_{s} (x)$ be the function defined by $℘_{s} (x) = (a_{1} - a_{0}) x + a_{0}$ . When $℘_{t}$ and $℘_{u}$ are defined, $| t | = | u | = 2^{m}$ and $t (2^{m}) = u (0)$ , then $℘_{s}$ for $s = ⟨ t (0), \dots, t (2^{m}), u (1), \dots u (2^{m}) ⟩$ is defined by, if $u (0) ⩾ \frac{t (2^{m} - 1) - u (2^{m})}{2}$ , $\begin{array}{l} ℘_{s} (x) = \{\begin{matrix} ℘_{t} (2 x) if x ⩽ \frac{1}{2}; \\ min {\frac{℘_{t} (1) - ℘_{t} (1 - 2^{- m})}{2^{m + 1}} (x - \frac{1}{2}) + ℘_{t} (1), \frac{℘_{u} (2^{m}) - ℘_{t} (0)}{2^{m + 1}} (x - \frac{1}{2}) + ℘_{u} (0)} \\ if 2^{- (m + 1)} (2^{m} - 1) < x < 2^{- (m + 1)} (2^{m} + 1); \\ ℘_{u} (2 (x - \frac{1}{2})) x ⩾ \frac{1}{2}, \end{matrix} \end{array}$ and otherwise $\begin{array}{l} ℘_{s} (x) = \{\begin{matrix} ℘_{t} (2 x) if x ⩽ \frac{1}{2}; \\ max {\frac{℘_{t} (1) - ℘_{t} (1 - 2^{- m})}{2^{m + 1}} (x - \frac{1}{2}) + ℘_{t} (1), \frac{℘_{u} (2^{m}) - ℘_{t} (0)}{2^{m + 1}} (x - \frac{1}{2}) + ℘_{u} (0)} \\ if 2^{- (m + 1)} (2^{m} - 1) < x < 2^{- (m + 1)} (2^{m} + 1); \\ ℘_{u} (2 (x - \frac{1}{2})) x ⩾ \frac{1}{2}, \end{matrix} \end{array}$ Let $PL [0, 1]$ be the set ${℘_{s} : s \in Q^{< N} \land (\exists m < | s |) (| s | = 2^{m} + 1)}$ .

In [2, Section 2], a uniformly continuous function $f : [0, 1] \to R$ is defined to be a pair of functions $φ : Q \times N \to Q$ and $ν : N \to N$ such that $f (a) = {(φ (a, n))}_{n} \in R$ and $\begin{array}{l} | a - b | < 2^{- ν (k)} \to | f (a) - f (b) | < 2^{- k} \end{array}$ for each $k \in N$ and $a, b \in Q \cap [0, 1]$ . Then, for each $x \in [0, 1]$ , $f (x)$ is defined by $\begin{array}{l} {(f (x))}_{n} = φ (min {max {a_{μ (n)}, 0}, 1}, n + 1) \end{array}$ and $f (x) = {({(f (x))}_{n})}_{n}$ , where $x = {(a_{n})}_{n}$ and $μ (n) = ν (n + 1) + 1$ . Then μ is the modulus of uniform continuity of f, i.e., a function such that for each $n \in N$ and x, $y \in [0, 1]$ , $\begin{array}{l} | x - y | < 2^{- μ (n)} \to | f (x) - f (y) | < 2^{- n} . \end{array}$ Let $p = ℘_{s}$ be an element of $PL [0, 1]$ and $s = ⟨ a_{0}, \dots, a_{2^{m} + 1} ⟩$ . Then $c = max {| a_{i} - a_{i + 1} | : i < 2^{m}}$ satisfies $| a - b | < 2^{- (m + n)} / c \to | p (a) - p (b) | < 2^{- n}$ . Therefore p is a uniformly continuous function consists of $φ : N \to N \times Q^{+}$ and $ν : N \to N$ defined by $\begin{array}{l} φ (a, n) = p (a) and ν (n) = n + m + i for the least i such that 2^{i} ⩾ c . \end{array}$

For each $℘_{s} \in PL [0, 1]$ , the value $‖ ℘_{s} ‖ : = {sup}_{x \in [0, 1]} | ℘_{s} (x) | = {max}_{x \in [0, 1]} | ℘_{s} (x) |$ exists as follows: Let $| s | = 2^{m} + 1$ . Then, for each $x \in [0, 1]$ , we have $| x - 0 | < 1$ or $| 1 - x | < 1$ by $x < 3 / 4$ or $1 / 4 < x$ . By iterating this, we can find $i ⩽ m$ such that $| x - 2^{- m} \cdot i | < 2^{- m}$ . Let $a = min {℘_{s} (j \cdot 2^{- m}) : max {0, i - 1} ⩽ j ⩽ min {2^{m}, i + 1}}$ and $b = max {℘_{s} (j \cdot 2^{- m}) : max {0, i - 1} ⩽ j ⩽ min {2^{m}, i + 1}}$ . Then, by the linearity of $℘_{s}$ , we have $a ⩽ ℘_{s} (x) ⩽ b$ and so $| ℘_{s} (x) | ⩽ max {| a |, | b |}$ . Hence $| ℘_{s} (x) | ⩽ max {| ℘_{s} (i \cdot 2^{- m}) | : 0 ⩽ i ⩽ 2^{m}}$ , and so ${sup}_{x \in [0, 1]} | ℘_{s} (x) | = {max}_{x \in [0, 1]} | ℘_{s} (x) | = max {| ℘_{s} (i \cdot 2^{- m}) | : 0 ⩽ i ⩽ 2^{m}}$ . Define $p - q$ by $(p - q) (x) = p (x) - q (x)$ . Then we can find s such that $℘_{s} \in PL [0, 1]$ and $℘_{s} (x) = (p - q) (x)$ for all $x \in R$ . We can also show that $ρ (p, q) = ‖ p - q ‖$ is a pseudometric on $PL [0, 1]$ . Let $C [0, 1]$ be the complete separable metric space $(PL [0, 1], ρ)$ .

Now we show that $C [0, 1]$ consists of all uniformly continuous functions.

Lemma 4.1.
For each point ${(p_{n})}_{n}$ of $C [0, 1]$ and $x \in [0, 1]$ , we have ${(p_{n} (x))}_{n} \in R$ .
Proof.
This follows from $| p_{m} (x) - p_{n} (x) | ⩽ {sup}_{x \in [0, 1]} | p_{m} (x) - p_{n} (x) | = ρ (p_{m}, p_{n}) < 2^{- m} + 2^{- n}$ . □

By the above lemma, we can define a function $α : [0, 1] \to R$ by $α (x) = {lim}_{n \to \infty} p_{n} (x)$ , for each point $α = {(p_{n})}_{n}$ in $C [0, 1]$ .
Lemma 4.2.
For each point α of $C [0, 1]$ , there is a uniformly continuous function f on $[0, 1]$ satisfying $α (x) = f (x)$ for all $x \in [0, 1]$ .
Proof.
Let $α = {(p_{n})}_{n}$ be a point of $C [0, 1]$ . Since each $p_{n}$ is a uniformly continuous function, for each n, there is a pair $(φ_{n}, ν_{n})$ such that $φ_{n} : Q \times N \to Q$ , $ν_{n} : N \to N$ and that $| a - b | < 2^{- ν_{n} (k)}$ implies $| p_{n} (a) - p_{n} (b) | < 2^{- k}$ for each $a, b \in Q \cap [0, 1]$ . Define $φ : Q \times N \to Q$ by $φ (a, n) = p_{n} (a)$ and $ν : N \to N$ by $ν (l) = ν_{l + 2} (l + 2)$ . Let $f (a) = {(φ (a, n))}_{n}$ . Then $f (a) \in R$ by Lemma 4.1. Since $| φ (a, n) - φ (a, m) | ⩽ {sup}_{x \in [0, 1]} | p_{n} (x) - p_{m} (x) | = ρ (p_{n}, p_{m}) < 2^{- n} + 2^{- m}$ , we have $| p_{n} (a) - f (a) | ⩽ 2^{- n}$ for each $a \in Q \cap [0, 1]$ . Therefore $f (a)$ satisfies, for each $a, b \in Q \cap [0, 1]$ with $| a - b | < 2^{- ν (l)}$ , $\begin{array}{l} | f (a) - f (b) | & ⩽ | f (a) - p_{l + 2} (a) | + | p_{l + 2} (a) - p_{l + 2} (b) | + | p_{l + 2} (b) - f (b) | < 3 \cdot 2^{- (l + 2)} < 2^{- l} . \end{array}$ Therefore f is a uniformly continuous function consists of φ and ν.

We show $f (x) = α (x)$ for each $x \in [0, 1]$ . Let $x = {(a_{n})}_{n}$ and $b_{n} = min {max {a_{μ (n)}, 0}, 1}$ , where $μ (n) = ν (n + 1) + 1$ . Then, for each n and $m ⩾ n$ , $\begin{array}{l} | b_{n} - b_{m} | ⩽ | a_{μ (n)} - a_{μ (m)} | < 2^{- μ (n)} + 2^{- μ (m)} ⩽ 2 \cdot 2^{- ν (n + 1) + 1} ⩽ 2^{- ν (n + 1)} \end{array}$ and so $\begin{array}{l} | {(f (x))}_{n} - {(f (x))}_{m} | & = | φ (b_{n}, n + 1) - φ (b_{m}, m + 1) | \\ ⩽ | φ (b_{n}, n + 1) - f (b_{n}) | + | f (b_{n}) - f (b_{m}) | + | f (b_{m}) - φ (b_{m}, m + 1) | \\ < 2^{- (n + 1)} + 2^{- (n + 1)} + 2^{- (m + 1)}, \end{array}$ and so we have $| {(f (x))}_{n} - f (x) | ⩽ 2^{- n}$ . Therefore, for $k = max {n, ν_{n} (n), μ (n)}$ , we have $\begin{array}{l} | {(f (x))}_{n} - {(α (x))}_{n} | \\ = | {(f (x))}_{n} - p_{n} (x) | \\ ⩽ | {(f (x))}_{n} - f (x) | + | f (x) - f (a_{k}) | + | f (a_{k}) - p_{n} (a_{k}) | + | p_{n} (a_{k}) - p_{n} (x) | \\ ⩽ 2^{- n} + 2^{- n} + 2^{- n} + 2^{- n} ⩽ 2^{- n + 2} . \end{array}$ □
Lemma 4.3.
For each $f = {(p_{n})}_{n}$ in $C [0, 1]$ , both of ${sup}_{x \in [0, 1]} | f (x) |$ and ${lim}_{n \to \infty} {sup}_{x \in [0, 1]} | p_{n} (x) |$ exist and satisfy $‖ f ‖ = {sup}_{x \in [0, 1]} | f (x) | = {lim}_{n \to \infty} {sup}_{x \in [0, 1]} | p_{n} (x) |$ .
Proof.
Let $f = {(p_{n})}_{n}$ be in $C [0, 1]$ . Since $‖ f (x) | - | f (y) ‖ ⩽ | f (x) - f (y) |$ , $| f (x) |$ is also an uniformly continuous function on $[0, 1]$ . Let $μ : N \to N$ be a modulus of continuity of $| f (x) |$ and $x_{n} = max {| f (l \cdot 2^{- μ (n)}) | : 0 ⩽ l ⩽ 2^{μ (n)}}$ . Then $x_{m} ⩾ x_{n}$ for each $m ⩾ n$ . For each n, there are j and k such that $x_{n + 1} = | f (j \cdot 2^{- μ (n + 1)}) |$ and $| j \cdot 2^{- μ (n + 1)} - k \cdot 2^{- μ (n)} | ⩽ 2^{- μ (n)}$ . Then $\begin{array}{l} x_{n + 1} & = | f (j \cdot 2^{- μ (n + 1)}) | \\ ⩽ | f (k \cdot 2^{- μ (n)}) | + 2^{- n} \\ ⩽ max {| f (l \cdot 2^{- μ (n)}) | : 0 ⩽ l ⩽ 2^{- μ (n)}} + 2^{- n} \\ ⩽ x_{n} + 2^{- n} . \end{array}$ Therefore ${(x_{n})}_{n}$ is a Cauchy sequence with a modulus $μ^{'} (n) = μ (n + 2)$ , i.e., $m, l ⩾ μ^{'} (n)$ implies $| x_{m} - x_{l} | < 2^{- n}$ . In ${EL}_{0}^{}$ , we can prove that any Cauchy sequence with a modulus converges in the same way to [3, Ch.2, Theorem 2].

We show $z = {lim}_{n \to \infty} {(x_{n})}_{n} = {sup}_{x \in [0, 1]} | f (x) |$ . For contradiction, assume $| f (x) | > z$ for some $x \in [0, 1]$ , and take i, j and k such that $| f (x) | - z > 2^{- i}$ , $| x - j \cdot 2^{- k} | < 2^{- μ (i)}$ and $k = max {μ (i), i + 1}$ . Then $‖ f (x) | - | f (j \cdot 2^{- k}) ‖ < 2^{- i}$ and so $| f (j \cdot 2^{- k}) | > | f (x) | - 2^{- i} > z$ , which contradicts the definition of z. Hence $z ⩾ f (x)$ for each $x \in [0, 1]$ . As we showed above, we have $x_{n + 1} - x_{n} ⩽ 2^{- (n + 1)}$ and so $z - x_{n + 1} = \sum_{j = n + 1}^{\infty} (x_{j + 1} - x_{j}) ⩽ \sum_{j = n + 1}^{\infty} 2^{- j} ⩽ 2^{- n}$ . Therefore $z = {sup}_{x \in [0, 1]} | f (x) |$ .

Next we show $z = {lim}_{n \to \infty} {sup}_{x \in [0, 1]} | p_{n} (x) |$ . Take x and y in $[0, 1]$ such that $| {sup}_{x \in [0, 1]} | f (x) | - | f (x) | | < 2^{- (n + 2)}$ and $| {sup}_{y \in [0, 1]} | p_{n + 2} (y) | - | p_{n + 2} (y) | | < 2^{- (n + 2)}$ . Since $‖ f (y) | - | p_{n + 2} (y) ‖ ⩽ | f (y) - p_{n + 2} (y) | ⩽ 2^{- (n + 2)}$ , we have $| p_{n + 2} (y) | ⩽ | f (y) | + 2^{- (n + 2)} < | f (x) | + 2^{- (n + 1)}$ . Similarly, we have $| f (x) | < | p_{n + 2} (y) | + 2^{- (n + 1)}$ . Hence $‖ f (x) | - | p_{n + 2} (y) ‖ < 2^{- (n + 1)}$ and so $\begin{array}{l} | sup_{x \in [0, 1]} | f (x) | - sup_{y \in [0, 1]} | p_{n + 2} (y) | | \\ ⩽ | sup_{x \in [0, 1]} | f (x) | - | f (x) | | + | | f (x) | - | p_{n + 2} (y) | | + | | p_{n + 2} (y) | - sup_{y \in [0, 1]} | p_{n + 2} (y) | | < 2^{- n} . \end{array}$ Therefore ${lim}_{n \to \infty} {sup}_{x \in [0, 1]} | p_{n} (x) | = {sup}_{x \in [0, 1]} | f (x) | = z$ . □

By the above lemma, we have $\begin{array}{l} ρ (f, g) = lim_{n \to \infty} ρ (p_{n}, q_{n}) = lim_{n \to \infty} sup_{x \in [0, 1]} | p_{n} (x) - q_{n} (x) | = sup_{x \in [0, 1]} | f (x) - g (x) | . \end{array}$ Lemma 4.4.
For each uniformly continuous function f on* $[0, 1]$ and $n \in N$ , there exists $s_{n}$ such that $p_{s_{n}} \in PL [0, 1]$ such that $ρ (f, p_{s_{n}}) < 2^{- n}$ .
Proof.
Assume that f consists of $(φ, ν)$ . Then we have $| f (x) - f (y) | ⩽ 2^{- (n + 3)}$ for all $x, y \in [0, 1]$ such that $| x - y | ⩽ 2^{- μ (n + 3)}$ , where $μ (n) = ν (n + 1) + 1$ . Let $a_{i} = i \cdot 2^{- μ (n + 3)}$ for $i ⩽ 2^{μ (n + 3)}$ and define $s_{n}$ as follows: $\begin{array}{l} s_{n} = ⟨ φ (0, n + 3), φ (a_{1}, n + 3), \dots, φ (a_{2^{- μ (n + 3)} - 1}, n + 3), φ (1, n + 3) ⟩ . \end{array}$ Let $p = ℘_{s_{n}} \in C [0, 1]$ . By $f (a) = {(φ (a, n))}_{n}$ for each $a \in Q$ , we have $| p (a_{i}) - φ (a_{i}, k) | = | φ (a_{i}, n + 3) - φ (a_{i}, k) | < 2^{- (n + 3)} + 2^{- k}$ and so $| p (a_{i}) - f (a_{i}) | ⩽ 2^{- (n + 3)}$ for each $a_{i}$ . By $| f (a_{i}) - f (a_{i + 1}) | ⩽ 2^{- (n + 3)}$ , we have $\begin{array}{l} | p (a_{i + 1}) - p (a_{i}) | & = | p (a_{i + 1}) - f (a_{i + 1}) | + | f (a_{i + 1}) - f (a_{i}) | + | f (a_{i}) - p (a_{i}) | ⩽ 3 \cdot 2^{- (n + 3)} . \end{array}$ Therefore we have $| p (x) - p (a_{i}) | ⩽ 3 \cdot 2^{- (n + 3)}$ for each x such that $| x - a_{i} | < 2^{- μ (n + 3)}$ by the linearity of p on $[a_{j}, a_{j + 1}]$ for each $j < 2^{- μ (n + 3)}$ .

Note that, for each $x \in [0, 1]$ , there is $a_{i}$ such that $| x - a_{i} | < 2^{- μ (n + 3)}$ . For such $a_{i}$ , we have $\begin{array}{l} | p (x) - f (a_{i}) | & ⩽ | p (x) - p (a_{i}) | + | p (a_{i}) - f (a_{i}) | ⩽ 3 \cdot 2^{- (n + 3)} + 2^{- (n + 3)} = 4 \cdot 2^{- (n + 3)} . \end{array}$ Since $| x - a_{i} | < 2^{- μ (n + 3)}$ , we have $| f (x) - f (a_{i}) | < 2^{- (n + 3)}$ , which implies $| p (x) - f (x) | < 5 \cdot 2^{- (n + 3)} < 2^{- n}$ . □
Lemma 4.5.
For each uniformly continuous function f on $[0, 1]$ , there is a point $α \in C [0, 1]$ such that $α (x) = f (x)$ for all $x \in [0, 1]$ .
Proof.
Assume that f consists of $(φ, ν)$ . Then, by $Δ_{0}^{0} - {AC}^{00}$ , we have $α = {(℘_{s_{n}})}_{n}$ , where $s_{n}$ is $\begin{array}{l} s_{n} = ⟨ φ (0, n + 3), φ (2^{- μ (n + 3)}, n + 3), \dots, φ (1 - 2^{- μ (n + 3)}, n + 3), φ (1, n + 3) ⟩, \end{array}$ and where $μ (n) = ν (n + 1) + 1$ . By the proof of Lemma 4.4, we have $\begin{array}{l} ρ (℘_{s_{n}}, ℘_{s_{m}}) & = sup {| ℘_{s_{n}} (x) - ℘_{s_{m}} (x) | : x \in [0, 1]} \\ ⩽ sup {| ℘_{s_{n}} (x) - f (x) | : x \in [0, 1]} + sup {| f (x) - ℘_{s_{m}} (x) | : x \in [0, 1]} \\ < 2^{- n} + 2^{- m}, \end{array}$ and so $α \in C [0, 1]$ . Since $| f (x) - ℘_{s_{n}} (x) | < 2^{- n}$ for each $n \in N$ , we have ${lim}_{n \to \infty} ℘_{s_{n}} (x) = f (x)$ for each $x \in [0, 1]$ . □

5. The main theorem

Definition 5.1.

Let α be a uniformly continuous function on $[0, 1]$ . Then α is differentiable at $x \in [0, 1]$ if for some $z \in R$ , $\begin{array}{l} \forall k \exists l \forall y \in [0, 1] (| x - y | < 2^{- l} \to | z (x - y) - (α (x) - α (y)) | ⩽ 2^{- k} | x - y |) . \end{array}$ We can show that such z is unique if it exists. We call z the derivative at x of α and write $α^{'} (x)$ .

Note that $℘_{s} \in PL [0, 1]$ for $s = ⟨ a_{0}, \dots, a_{n + 1} ⟩$ is differentiable at each $x \in (a_{i}, a_{i + 1})$ for $i ⩽ n$ and at 0 and 1. At $a_{i}$ for $0 < i ⩽ n$ , it is differentiable if and only if $a_{i} = (a_{i - 1} + a_{i + 1}) / 2$ .

Let ${PL}_{n} [0, 1]$ be the set of $p \in PL [0, 1]$ such that $| p^{'} (x) | > n$ at each differentiable $x \in [0, 1]$ , i.e., the set $\begin{array}{l} {PL}_{n} [0, 1] = {℘_{s} \in PL [0, 1] : s \in Q^{< N} \land (\forall i < | s | - 1) (| s (i) - s (i + 1) | > \frac{n}{| s | - 1})} . \end{array}$

Lemma 5.2.

Assume $α \in C [0, 1]$ , $s = ⟨ a_{0}, \dots, a_{k} ⟩$ and $℘_{s} \in {PL}_{n} [0, 1]$ . Then $ρ (α, ℘_{s}) < c_{s, m, n}$ implies $\begin{array}{l} \forall x \in [0, 1] \neg \neg \exists y \in [0, 1] (0 < | x - y | < \frac{1}{m} \land | \frac{α (x) - α (y)}{x - y} | > n), \end{array}$ where $c_{s, m, n} = 2^{- 4} \cdot d_{s, m, n} \cdot d_{s, m, n}^{'}$ , $d_{s, m, n} = min {k^{- 1} | p (a_{i + 1}) - p (a_{i}) | - n : 0 ⩽ i < k}$ and where $d_{s, m, n}^{'} = min {k^{- 1}, m^{- 1}}$ .

Proof.

Take α, s, $℘_{s}$ , $c_{s, m, n}$ , $d_{s, m, n}$ and $d_{s, m, n}^{'}$ as stated. Then $d_{s, m, n} > 0$ , since $| p_{s}^{'} (x) | > n$ at each differentiable $x \in C [0, 1]$ .

For each $x \in [0, 1]$ , we have $\begin{array}{l} min {| x - a_{i} | : 0 ⩽ i ⩽ k} < d_{s, m, n}^{'} / 2 \lor d_{s, m, n}^{'} / 4 ⩽ min {| x - a_{i} | : 0 ⩽ i ⩽ k} . \end{array}$ Case 1. If $min {| x - a_{i} | : 0 ⩽ i ⩽ k} < d_{s, m, n}^{'} / 2$ , take $a_{i}$ such that $| x - a_{i} | < d_{s, m, n}^{'} / 2$ .

If $a_{i} ⩽ x$ , then $℘_{s}$ has the constant slope b at $[x, x + \frac{d_{s, m, n}^{'}}{2}]$ . Since $| b | > n$ , we have $b > n$ or $b < - n$ . If $b > n$ , then $\begin{array}{l} \frac{α (x + \frac{d_{s, m, n}^{'}}{2}) - α (x)}{x + \frac{d_{s, m, n}^{'}}{2} - x} > & \frac{2}{d_{s, m, n}^{'}} (℘_{s} (x + \frac{d_{s, m, n}^{'}}{2}) - c_{s, m, n} - (℘_{s} (x) + c_{s, m, n})) \\ = & \frac{2}{d_{s, m, n}^{'}} ((℘_{s} (x + \frac{d_{s, m, n}^{'}}{2}) - ℘_{s} (x)) - 2 c_{s, m, n}) \\ = & b - \frac{4}{d_{s, m, n}^{'}} c_{s, m, n} \\ ⩾ & d_{s, m, n} + n - \frac{d_{s, m, n}}{4} > n . \end{array}$ Similarly, if $b < - n$ or $x < a_{i}$ , then we can prove $\begin{array}{l} | \frac{α (x + \frac{d_{s, m, n}^{'}}{2}) - α (x)}{x + \frac{d_{s, m, n}^{'}}{2} - x} | > n . \end{array}$

Therefore, we have $\begin{array}{l} a_{i} ⩽ x \lor x < a_{i} \to \exists y \in [0, 1] (0 < | y - x | < \frac{1}{m} \land | \frac{α (y) - α (x)}{y - x} | > n) . \end{array}$ Since $(A \to B) \to (\neg \neg A \to \neg \neg B)$ holds in intuitionistic logic and since $\neg \neg (a_{i} ⩽ x \lor x < a_{i})$ holds, we have $\begin{array}{l} \neg \neg \exists y \in [0, 1] (0 < | y - x | < \frac{1}{m} \land | \frac{α (y) - α (x)}{y - x} | > n) . \end{array}$ Case 2. If $min {| x - a_{i} | : 0 ⩽ i ⩽ k} ⩾ d_{s, m, n}^{'} / 4$ , then $℘_{s}$ has a constant slope b at $[x - \frac{d_{s, m, n}^{'}}{4}, x + \frac{d_{s, m, n}^{'}}{4}]$ . Since $| b | > n$ , we have $b > n$ or $b < - n$ . If $b > n$ , then $\begin{array}{l} \frac{α (x + \frac{d_{s, m, n}^{'}}{4}) - α (x)}{x + \frac{d_{s, m, n}^{'}}{4} - x} > & \frac{4}{d_{s, m, n}^{'}} (℘_{s} (x + \frac{d_{s, m, n}^{'}}{4}) - c_{s, m, n} - (℘_{s} (x) + c_{s, m, n})) \\ = & \frac{4}{d_{s, m, n}^{'}} ((℘_{s} (x + \frac{d_{s, m, n}^{'}}{4}) - ℘_{s} (x)) - 2 c_{s, m, n}) \\ = & b - \frac{8}{d_{s, m, n}^{'}} c_{s, m, n} \\ ⩾ & d_{s, m, n} + n - \frac{d_{s, m, n}}{2} > n . \end{array}$ Similarly, if $b < - n$ we have $\begin{array}{l} \frac{α (x + \frac{d_{s, m, n}^{'}}{4}) - α (x)}{x + \frac{d_{s, m, n}^{'}}{4} - x} < - n . \end{array}$ Therefore, we have $\begin{array}{l} \neg \neg \exists y \in [0, 1] (0 < | x - y | < \frac{1}{m} \land | \frac{α (x) - α (y)}{x - y} | > n) . \end{array}$ □

Let $β_{m, n} : N \to PL [0, 1] \times Q \cup {0}$ defined by $\begin{array}{l} β_{m, n} (i) = \{\begin{matrix} (℘_{s}, c_{s, m, n}) & if i is a code of s such that ℘_{s} \in {PL}_{n} [0, 1]; \\ 0 & otherwise . \end{matrix} \end{array}$ Then $β_{m, n}$ is an open set in $C [0, 1]$ .

Lemma 5.3.

For each m and n, $β_{m, n}$ is dense in $C [0, 1]$ .

Proof.

This proof is essentially the same to the classical well-known proof, e.g., the one in [10, Section 11].

Fix m, n and $a \in Q$ with $a > 0$ and let α be a point of $C [0, 1]$ . Then we can take i such that $2^{- i} < a$ .

Take s and j such that $p = ℘_{s}$ satisfies $ρ (p, α) ⩽ 2^{- (i + 1)}$ and $| s | = 2^{j} + 1$ . Since $p \in PL [0, 1]$ , we can find $k \in N$ such that $| p^{'} (x) | < k$ for all differentiable $x \in [0, 1]$ . Choose l such that $2^{j + l} > 2 (k + n) / a$ .

Let $q \in PL [0, 1]$ be the function satisfying, for each $x \in [0, 1]$ and $j_{0}$ with $0 ⩽ j_{0} ⩽ 2 (j + l)$ , $\begin{array}{l} q (x) = \{\begin{matrix} 2^{j + l} (x - \frac{j_{0}}{2^{j + l}}) & if x \in [\frac{j_{0}}{2^{j + l}}, \frac{j_{0} + 1}{2^{j + l}}] and j_{0} is even; \\ - 2^{j + l} (x - \frac{j_{0} + 1}{2^{j + l}}) & if x \in [\frac{j_{0}}{2^{j + l}}, \frac{j_{0} + 1}{2^{j + l}}] and j_{0} is odd . \end{matrix} \end{array}$ Then $| q (x) | ⩽ 1$ for all $x \in [0, 1]$ and $q^{'} (x) = \pm 2^{j + l}$ for all $x \in [0, 1]$ where $q (x)$ is differentiable. Define $r \in PL [0, 1]$ by $\begin{array}{l} r (x) = p (x) + \frac{a}{2} q (x) . \end{array}$ Then we have $ρ (α, r) < a$ , since $ρ (α, p) < a / 2$ and $ρ (p, r) ⩽ a / 2$ .

For each differentiable $x \in [0, 1]$ , we have $\begin{array}{l} | r^{'} (x) | = | p^{'} (x) + \frac{a}{2} q^{'} (x) | ⩾ | (| p^{'} (x) | - (k + n)) | > n . \end{array}$ Then $r \in β_{m, n}$ by Lemma 5.2. □

Finally, we have the following:

Theorem 5.4.

${EL}_{0}^{*} + Σ_{1}^{0} - IND$ proves that for each $α \in C [0, 1]$ and l, there is $γ \in C [0, 1]$ such that $ρ (α, γ) < 2^{- l}$ and γ is not differentiable at any $x \in [0, 1]$ .

Proof.

By Theorem 3.2, ${EL}_{0}^{*} + Σ_{1}^{0} - IND$ proves $BCT$ . Therefore, for each $α \in C [0, 1]$ and l, there exists $γ \in C [0, 1]$ such that for $ρ (γ, α) < 2^{- l}$ and $γ \in β_{m, n}$ for all $(m, n) \in N \times N$ . If such γ is differentiable at some $x \in C [0, 1]$ , then $γ \notin β_{m, n}$ for some $(m, n)$ by Lemma 5.2. Therefore γ is not differentiable at any $x \in [0, 1]$ . □

Footnotes

Acknowledgements

The author would like to thank Professor Hajime Ishihara for useful discussions. She is grateful to the anonymous referee for his or her many suggestion to improve the earlier version of this paper. She also thanks Professor Michio Seto for his introduction to the topic of this paper and related research. This work was supported by JSPS KAKENHI Grant Number 18K03392.

References

Banach, Über die Baire’sche Kategorie gewisser Funktionenmengen, Studia Mathematica3 (1931), 174–179. doi:10.4064/sm-3-1-174-179.

Berger,

Ishihara,

Kihara and

Nemoto, The binary expansion and the intermediate value theorem in constructive reverse mathematics, Arch. Math. Logic (2018). doi:10.1007/s00153-018-0627-2.

Bishop, Foundations of Constructive Analysis, McGraw-Hill, New York, 1967.

Brattka, Computable versions of Baire’s category theorem, in: Mathematical Foundations of Computer Science 2001. MFCS 2001,

Sgall,

Pultr and

Kolman, eds, Lecture Notes in Computer Science, Vol. 2136, Springer, Berlin, Heidelberg, 2001.

D.K.

Brown and

S.G.

Simpson, The Baire category theorem in weak subsystem of second-order-arithmetic, the Journal of Symbolic Logic58 (1993), 557–578. doi:10.2307/2275219.

Ishihara, Constructive reverse mathematics: Compactness properties, in: From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics,

Schuster and

Crosilla, eds, Oxford University Press, 2005, pp. 245–267. doi:10.1093/acprof:oso/9780198566519.003.0016.

Ishihara and

Schuster, A continuity principle, a version of Baire’s theorem and a boundedness principle, J. Symbolic Logic73 (2008), 1354–1360. doi:10.2178/jsl/1230396924.

Nemoto, Finite sets and infinite sets in weak intuitionistic arithmetic, Arch. Math. Logic (2020). doi:10.1007/s00153-019-00704-8.

Nemoto and

Sato, A marriage of Brouwer’s Intuitionism and Hilbert’s Finitism I: Arithmetic, Journal of Symbolic Logic., to appear.

10.

J.C.

Oxtoby, Measure and Category, Springer-Verlag, New York, 1971.

11.

S.G.

Simpson, Subsystems of Second Order Arithmetic, 2nd edn, Cambridge University Press, 2009.

12.

S.G.

Simpson, Baire categoricity and

Σ_{1}^{0}

-induction, Notre Dame J. Formal Logic55(1) (2014), 75–78. doi:10.1215/00294527-2377887.

13.

A.S.

Troelstra and

van Dalen, Constructivism in Mathematics, Vol. I and II, North-Holland, Amsterdam, 1988.

14.

Yokoyama, On the strength of Ramsey theorem without

Σ_{1}^{0}

-induction, Mathematical Logic Quaterly19 (2013), 108–111. doi:10.1002/malq.201200047.