数理解析研究所講究録1096 巻 1999 年 25-34

25

Reverse Mathematics and weak second-order systemsof 0-1 strings
Takeshi Yamazaki$(\lfloor l_{\mathrm{I}}\mathrm{L}\S \mathrm{f}\mathrm{f}\mathrm{i})$Mathematical Institute, Tohoku University
Abstract. Rom a standpoint congenial to$\mathrm{R}\mathrm{e}\mathrm{v}\mathrm{e}\mathrm{r}\circ.\mathrm{e}$Mathematics, we develop a basic part ofreal analysis within weak second-order systems of 0-1 strings, e.g., BTFA. Among others, weshow within BTFA that a version of the maximum principle is equivalent to$\Sigma_{1}^{b_{-}}\mathrm{C}\mathrm{A}$.

\S 1. Introduction.
The purpose of Reverse Mathematics is to determine which set existence axioms areneeded to prove a popular theorem of mathematics. For the main-stream researches ofthis program, the system$\mathrm{R}\mathrm{C}\mathrm{A}_{0}$is presupposed as a base theory in which most of basic

concepts of ordinary mathematics (e.g., reals, continuous functions) are defined. However,it has been claimed by several people that the phenomena of Reverse Mathematics dependon the base theory, so that necessary axioms for a theorem may be changing if one replaces$\mathrm{R}\mathrm{C}\mathrm{A}_{\mathrm{O}}$by a weaker system. Actually, Simpson and Smith [6] already studied Reverse

Mathematics over$\mathrm{R}\mathrm{C}\mathrm{A}_{0}^{*}$, which is roughly$\mathrm{R}\mathrm{C}\mathrm{A}_{0}$minus$\Sigma_{1}^{0}$-induction plus$\Sigma_{0}^{0}$-induction

plus exponentiation. F.Ferreira [2] proposed to do Reverse Mathematics over BTFA (or$\mathrm{B}\mathrm{T}\mathrm{F}\mathrm{A}+\Sigma_{\infty}^{b}$-WKL), a second-order systems of 0-1 strings whose provably total functions

are the polynomial time computable functions.

26

In this paper, we carry out Ferreira’s plan and show, for instance, that the intermediate

value theorem on $[0,1]$ is provable in BTFA, and a version of the maximum principle isequivalent to$\Sigma_{1}^{b_{-}}\mathrm{C}\mathrm{A}$within BTFA.

In the rest of this section, we quickly review the basic concepts about second-ordersystems of 0-1 strings following [2]. Then in \S 2, we develop real analysis within such
systems, and in \S 3, we prove our main results.

The language of second-order systems of 0-1 strings consists of three constant symbols$\epsilon,$$0$, and 1, two binary function symbols $-$ (for concatenation) and

word

$x$

concatenated with itself the length of$y$$\cross(x\cross y$means thetimes) and a binary relation symbol$\subseteq$(for initial subwordness). The class of s.w.q. formulae (where s.w.q. stands for “subword
quantification”) is the smallest class of formulae containing the atomic formulae and closed

under the Boolean operations and quantifications of the form
$x\subseteq*y$means$\exists z\subseteq y(z^{-}X\subseteq y)$

The relation $x\leq y$ is defined

and

$t$

$y$

form

$\exists x\leq t\varphi$

where$\varphi$

not occur. The class of

is a term in which the variable$\mathrm{b}\mathrm{y},1\cross x\subseteq 1\cross y$than or equal to the length of . We$\tilde{\mathrm{w}}$

rite

$t$

or
$x$

$\exists x\subseteq*t$.

$\Sigma_{1}^{b}$

where

does not occur.

to express that the length of$1\cross x\dot{\mathrm{f}}\mathrm{o}\mathrm{r}|x|$is a s.w.q. formula and$\Sigma_{\infty}^{b}$$\forall x\subseteq*t$$x$is less-formula is a formula of theis a term in which the variable

$x$

does

-formulas is the smallest class containing the s.w.q. formulasand closed under Boolean operations and bounded quantification, i.e., quantification of

the form$\exists x\leq t(\ldots)$or$\forall x\leq t(\ldots)$, where the variable$x$

does not occur in the term .
$t$Definition 1 i) ($)-CA is the set of universal closures of formulas of the form$\forall x(\exists y\varphi(x, y)rightarrow\forall z\neg\psi(x, z))arrow\exists X\forall x(x\in Xrightarrow\exists y\varphi(x, y))$where$\varphi$and$\psi$

are$\Sigma_{1}^{b}$-formulae$X$does not occur in$\varphi$

.

,

27

ii)

$\Sigma_{1}^{b_{-}}\mathrm{C}\mathrm{A}$is the set of universal closures of formulas of the form,$\exists X\forall x(x\in Xrightarrow\varphi(x))$

where
iii)

is

$\varphi$$\Sigma_{1}^{b}$-formulae and(notation induction) is the$\Sigma_{1^{-}}^{b}\mathrm{N}\mathrm{I}$$\varphi(\epsilon)$

where
iv)

$\mathrm{B}\Sigma_{\infty}^{b}$$Xdoe\mathit{8}$is$\varphi$$\Sigma_{1}^{b}$A$\mathit{8}et$

not occur in$\varphi$.

of universal closures of$formula\mathit{8}$$\forall x(\varphi(x)arrow\varphi(x\mathrm{O})\wedge\varphi(x1))arrow\forall x\varphi(x)$$formula\mathit{8}$:$\forall x\leq a\exists y\varphi(x, y)arrow\exists z\forall x\leq a\exists y\leq z\varphi(x, y)$$\varphi i_{\mathit{8}}\Sigma_{\infty}^{b}$$ba\mathit{8}ic$ii) BTFA isword operators $-,$$\cross$, etc. plus$\Sigma_{1}^{b_{- \mathrm{N}\mathrm{I}\mathrm{A}+\mathrm{B}}}\Sigma^{b}\infty+(-\mathrm{c}\mathrm{A}$We notice that$\Sigma_{1}^{b}$,-formula.

Definition 2 (See [2] for a complete statement) i)for,-formula.

is the set of universal closures of

where

:

-NIA and Buss’$S_{2}^{1}$$\Sigma_{1^{-}}^{b}\mathrm{N}\mathrm{I}$$\Sigma_{1}^{b}$-NIA$con\mathit{8}i\mathit{8}t_{S}$of the axioms.

.

are mutually interpretable. Originally, BTFA,

which stands for base theory for feasible analysis, is introduced by F. Ferreira [2] toanswer Sieg’s problem: find a mathematically significant subsystem of analysis whoseclass of provably recursive functions consists only of the computationally “feasible” ones.

It is obvious that the smallest model of BTFA isor not ($)-CA implies
systems$\Sigma_{1}^{b}$$\Sigma_{1}^{b_{-\mathrm{C}\mathrm{A}}}$$(2^{\omega}, \Delta^{0})1$’

though it is unknown whether. The following theorem is a major characterization of-NIA and BTFA.

Theorem 1 i)$\Sigma_{1}^{b_{-}}\mathrm{N}\mathrm{I}\mathrm{A}+\mathrm{B}\Sigma_{\infty}^{b}$is conservative over$\Sigma_{1}^{b}$-NIA with respect to$\Pi_{2}^{0}$-formulas.

28ii) BTFA is conservative over$\Sigma_{1}^{b_{- \mathrm{N}\mathrm{I}\mathrm{A}+\mathrm{B}\Sigma_{\infty}}}b$with$re\mathit{8}pect$to.

$\Pi_{1}^{1_{-}}f_{\mathit{0}}rmulaS$

For a proof of this theorem and other related results, see Ferreira [2].

\S 2. Basics of real analysis.
We begin with defining a real number and a (uniformly) continuous function on thereals in BTFA. We here have two sorts of natural numbers, i.e., tally natural numbers

and dyadic natural numbers. A tally natural number is defined by a string of l’s, i.e.,
11,$\epsilon,$$\ldots$$\subseteq,$

. Let

$-$

be the set of tally natural numbers. We can define$\mathrm{N}$and$\cross$, respectively. Then it is easy to show in BTFA thatring. We use $n,$ $m,$

$k,$

$l,$

$\ldots$$\sigma=1\tau$$\mathrm{N}$$\leq_{\mathrm{N}},$$+_{\mathrm{N}}$and$\cdot \mathrm{N}$

$1$

,

by

is an ordered semi-

as variables over N. A tally natural number is used to express

the length of a string or the index of a sequence. A stringif$0_{\mathrm{N}},$$\epsilon,$

for some , or $\sigma=0$ . In the standard model,$\tau$$\sigma$$\sigma$

is a dyadic natural number

can be seen as the ordinary

dyadic notation of a natural number. The set of all dyadic natural numbers is denotedby$\mathrm{N}_{2}$. Also we can defineand show in BTFA thata natural embedding ofomit subscripts

A 3-tupleor 1 andnumb$e\mathrm{r}\mathrm{s}$$(i, n, \sigma)$$\sigma(j)$To$\mathrm{N}_{2}$$\leq_{\mathrm{N}_{2}}$$\mathrm{N}_{2}$, but not vice versa. Without misunderstanding, we, etc.

$j’ \mathrm{t}\mathrm{h}$element ( or 1) of$0$$=_{D’},$$+_{D’},$$\leq_{D’},$$\cdot D’$$\sigma$

. Let

$D’$

be the set of dyadic rational, etc. in the usual way. We have a natural

into $D’/=_{D^{l}}$ . Let $D$ be the set of $D’\cap[0,1]$ .

of $D$ where the length of$\mathrm{s}\mathrm{i}\mathrm{m}\mathrm{p}\mathrm{l}\mathrm{i}\Phi$in the usual way (cf. Ferreira [3]),denotes a dyadic rational number $(-1)^{i}2^{n} \sum\sigma(j)2^{-j}-1$ where $i=0$

is the$\mathrm{N}_{2}$$+_{\mathrm{N}_{2}}\mathrm{a}\mathrm{n}\mathrm{d}.\mathrm{N}_{2}$$\leq_{\mathrm{N}_{2}},$is an ordered semi-ring. We should notice that there exists

into$\mathrm{N}$. Then we define

embedding of$(0, m, \sigma)$$\mathrm{o}\mathrm{f}+_{\mathrm{N}},$$0_{\mathrm{N}_{2}},$$\sigma$is the set of all elements

is $m+n$ .

the notation, we write$\sigma$whose length is . Moreover, we write
$f$

for

$2^{-n}$$n$Definition 3 (BTFA) A function$D_{n}$:$(0, n, \mathrm{o}^{n}\sigma)\in D$, where$0^{n}$

is the string of$\mathrm{O}’ \mathrm{s}$for $0^{n-1}1$ .

$\mathrm{N}arrow D’i\mathit{8}$a real number $if|f(n)-f(m)|\leq 2^{-n}$29for each $n\leq m$ . Two real$2^{-n+1})$

that $=,$$\Pi_{1}^{b}$

and

$g$

are said to be equal if $\forall n\in \mathrm{N}(|f(n)-g(n)|\leq$.

The relations $<,$

is$number\mathit{8}f$$\leq$

and basic operations on the real numbers are defined as usual. Notethe real numbers can be defined by a formula of the form$\leq \mathrm{o}\mathrm{n}$$\forall\sigma\varphi(\sigma)$

where$\varphi$.

Definition 4 (BTFA) $F=(\{f_{n}\}, m)$ is a (code for a) (uniformly)

from $[0,1]$ to $[0,1]$ if
1.

$m:\mathrm{N}arrow \mathrm{N}$2.

$\{f_{n}\}$is a$D_{m(n)}$$Fsati\mathit{8}fies$offunction

the following conditions:is an increasing functionf called a$\mathit{8}equenCe$$continuou\mathit{8}$$piecewi_{\mathit{8}}e$$modulu\mathit{8}$linear functions$f_{n}$

function for .
$F$: $Darrow D$ whose break points are in,

3. $|f_{n}(d)-fn(d+2^{-m(n)})|\leq 2^{-n}$ for each

4. $|f_{n}(d)-fn+m(d)|\leq 2^{-n}$ for each
We define$F(x)=\langle r_{n}\rangle$$n\in \mathrm{N}$$n,$ $m\in \mathrm{N}$and $d\in D$ ,and $d\in D$ .

for each $x\in[0,1]$ by ($)-CA. Namely, if

to any $\sigma\in D$ , then we define $r_{n}=f_{n+1}(\sigma)$ where$|x-\sigma|\leq 2^{-m(+1)-}n1\wedge\sigma\in D_{m(n+1)}$. If $x=\tau$ for some$\sigma$is not equal$x$is the unique string such that$\tau\in D,$$r_{n}=f_{|\tau|+n}(\mathcal{T})$.

Remark 1. It is easy to extend the above definition to define a continuous function fromany bounded closed interval to any bounded closed interval. Also a multi-dimensional
continuous function can be defined in an obvious way. The identity function, the constantfunction, $+,$

$x^{n}$$\cdot,$, etc. are all continuous. The continuous functions are closed under thecomposition.

Remark 2. We could adopt another definition of continuous functions such as given in
Simpson [5]. However, with such a definition, we may not compute $F(x)$ even if $F$ has amodulus function (except for a polynomial.)

30

The following lemma can be used to show that functions defined by power series, e.g.,$e\mathrm{x}\mathrm{p}(x)$and $\sin(x)$ , are continuous on $[0,1]$ .

Lemma 2 (BTFA) Let$\{F_{n}\}$with the modulus function$m_{n}$$m(k+n)$ for each $n,$ $k\in$ N.

be a$\mathit{8}equence$of continuous $function\mathit{8}Fn:[0,1]arrow[0,2^{-n}]$. Suppose that there

Then$F=\Sigma_{k\in \mathrm{N}}F_{k}$$exist\mathit{8}m:\mathrm{N}arrow \mathrm{N}\mathit{8}uch$

is continuous.

Proof. We reason in BTFA. Let $F_{n}=(\{f_{m}^{n}\}, m_{n})$ . Letof a whose length isfunction$n$. Since we can compute$F=(\{\Sigma_{k=}^{n}0f_{2}^{k}n\lceil 2n\}, m)$.

that $m_{n}(k)\leq$$\sigma\lceil n$$\sum_{k=0^{\sigma}k}^{m}\lceil n$denote the initial segment, then we have a continuous$\square$\S 3. The intermediate value theorem and the maximum principle.
Before proving the intermediate value theorem, we show a useful lemma.
Lemma 3 (BTFA) Leta term$t’\mathit{8}uch$$g,$$h_{0}$

and$h_{1}$

be functions and be a term. Assume that there is$t$that $g(\tau)\leq t’(\tau)$ for each . Then, there$\tau$$exi\mathit{8}tsf$

such that$f(\epsilon, \tau)=g(\tau)$$f(\sigma 0, \tau)=h0(f(\sigma, \tau),$$\sigma,$$\tau)\mathrm{r}t(\sigma 0, \mathcal{T})$$f(\sigma 1, \tau)=h_{1}(f(\sigma, \mathcal{T}),$ $\sigma,$ $\tau)\mathrm{r}t(\sigma 1, \tau)$

Proof. By modifying the proof of proposition 7 in Ferreira [1],formula of the form($)-CA,$f$exists.

$\exists y\varphi$

with$\varphi\in\Sigma_{1}^{b}$$f$

is obtained by a

, which just describes the course of values. By$\square$

Theorem 4 (BTFA) Let $F$ be a $continuou\mathit{8}$ function from $[0,1]$ to$1/2<F(1)$ . Then, there exists a real$x\in(\mathrm{O}, 1)\mathit{8}uch$

Proof. We may assume that $F(\sigma)\neq 0$ for alla set $X$ consisting of all$\sigma\in D$$[0,1]_{\mathit{8}}uch$that$F(\mathrm{O})<$

that $F(x)=1/2$ .

$\sigma\in D$. Then by ($)-CA there exists

such that $F(\sigma)>0$ . By the above lemma, we define

31

$g$

:

$\mathrm{N}arrow D$by$0$$g(n)=\{$ $g(n-1)0$$\Sigma_{1^{-}}^{b}\mathrm{N}\mathrm{I}$$n=\epsilon$

if$n\neq\epsilon$,
and $g(n-1)1\in X$ ,otherwise$g(n-1)1$

By

if

,
$\forall n\in \mathrm{N}\forall m\in \mathrm{N}[n\leq marrow g(n)\subseteq g(m)\wedge g(n)\equiv n+1]$

Thus

$g$

is a real. By$\Sigma_{1^{-}}^{b}\mathrm{N}\mathrm{I}$$F(x)=1/2$ where $x=g$ .

.

again, $\forall n\in \mathrm{N}[F(g(n))<1/2<F(g(n)+2^{-n})]$ . Therefore,$\square$If the modulus function for a continuous function $F$ is of the form$|t|$where is a term,$t$then we say that $F$ has a polynomial modulus function.

We now prove a lemma saying that a weak version of the maximum principle can beshown in BTFA adding a very weak comprehension scheme.
Lemma 5$(\mathrm{B}\mathrm{T}\mathrm{F}\mathrm{A}+\Sigma_{1^{-}}^{b}\mathrm{C}\mathrm{A})$For each continuous function $F$ on $[0,1]$ with a polynomial

modulus function, then there exists $\sup_{0\leq y\leq}1(Fy)$ .
Proof. Let $F=(\{f_{n}\}, m)$ . By

We define$\varphi(l, n, \sigma)$$\varphi$is$\Pi_{1}^{b}$, there is$X_{n}^{l}=\{\tau\lceil l:\exists\sigma\in D_{m(n)}f_{n}(\sigma)=\tau\}$.

by$\sigma\in X_{n}^{l}$

Since$\Sigma_{1}^{b_{-}}\mathrm{C}\mathrm{A}$A$\sigma\equiv l$, we can show that

A$\forall\sigma’\equiv l(\sigma/<\sigmaarrow\sigma’\not\in X_{n}^{l})$$\forall n\in \mathrm{N}\forall l\in \mathrm{N}\exists!\sigma\varphi(l, n, \sigma)$such that $\varphi(n+2, n+2, \sigma)$ . Then, for each$n\in \mathrm{N}$$f_{n+2}(d)\leq g(n)+2^{-n-2}$

for each $d\in D_{m(n+2)}$ .

$f_{n+2}(d’)\lceil(n+2)=g(n)$for some $d’\in D_{m(n+2)}$ .

Therefore, we can show that$g$is a real and that

$g$

by

.

$\Pi_{1^{-}}^{b}\mathrm{N}\mathrm{I}$on . Let $g(n)=\sigma$$l$,is the least upper bound.

$\square$32

Corollary 6$(\mathrm{B}\mathrm{T}\mathrm{F}\mathrm{A}+\Sigma_{1}b_{-}\mathrm{C}\mathrm{A})$For each continuous function $F$ on $[0,1]\mathrm{x}[0,1]$ with apolynomial modulus function, then there exists a continuous function $G(x)= \sup 0\leq y\leq 1F(x, y)$ .

Proof. It is straightforward from the proof of the above lemma.
Corollary 7$(\mathrm{B}\mathrm{T}\mathrm{F}\mathrm{A}+\Sigma_{1^{-}}^{b}\mathrm{C}\mathrm{A})$$\square$For each continuous function $F$ on $[0,1]$ with a polyno-

mial modulus function, then there$exi_{\mathit{8}}t_{S}$a$continuou\mathit{8}$function $G(x)= \sup 0\leq y\leq xF(y)$ .

Proof. We define a continuous function $F’$ on $[0,1]\cross[0,1]$ by$F(0)$

if $x<y$ ,$F(x-y)$

if $y\leq x$ .

$F’(x)=\{$

Then $F’$ has a polynomial modulus function. By the above lemma, we can obtain acontinuous function $G(x)= \sup_{0\leq}y\leq xF(y)$ .

$\square$

Theorem 8 (BTFA) The following are equivalent:

1.

$\Sigma_{1}^{b_{-}}\mathrm{C}\mathrm{A}$.

2. For each continuous function $F$ on $[0,1]$ with a polynomial
there$exi\mathit{8}t\mathit{8}$$modulu\mathit{8}$function, thena continuous function $G(x)= \sup_{0\leq}y\leq xF(y)$ .

Proof. The implication from 1 to 2 is Corollary 7. It remains to prove that 2 implies 1.
We reason in BTFA.

Let$\varphi(\sigma)$$\psi(\sigma, \tau)$be$\Sigma_{1}^{b}$. For simplicity, we assume$\varphi(\sigma)$

is of the form$\exists\tau\equiv t(\sigma)\psi(\sigma, \mathcal{T})$whereis a s.w.q. formula. (It is a routine to extend the following argument to the generalcase.)For each$n\in \mathrm{N}$, let $a_{n}=1-2^{-n}\in D$ . (Namely, $a_{n}=n$ in the sense of strings.) If

is the length of , then let $u_{\sigma}=a_{n}+0^{n+1}s$ and$n$$|t(n)|,$$y_{\sigma},\mathcal{T}=u_{\sigma}+0^{2n+2}\tau$and$v_{\sigma}=u_{\sigma}+2^{-2n-1}$$z_{\sigma,\tau}=y_{\sigma,\tau}+2^{-2n-2-|}t(n)|$

.

. If

$\tau$$\sigma$is the length of

33

Define a function $H:[0,1]arrow[0,1]$ by$2x$

if $0\leq x\leq 1/2$ ,$2-2x$

if $1/2\leq x$ .

$H(x)=\{$

Now we define a continuous function $F=(\{f_{n}\}, m)$ . Let $m(n)=|t(n)|+2n+3$ . Let$f_{n}(\sigma)=f_{n-}1(\sigma)$for$\sigma\leq a_{n},$$f(\sigma)=a_{n+1}$

for$\sigma\geq a_{n+1}$, and for$2\sigma-v_{\sigma}$$f_{n}(\sigma)=\{$$u_{\sigma}$$u_{\sigma}+2^{-|t(n})|-2n-2h(2|t(n)|+2n+2.

(\sigma-y\sigma,\mathcal{T}))$

If $G(x)= \sup_{0\leq y\leq}x(Fy)$ , then it is easy to see that$2^{-|t(\sigma)|}-2\cdot|\sigma|-3>u_{\sigma}$existsiff$X=\{\sigma:\varphi(\sigma)\}$$g|t( \sigma)|+2\cdot|\sigma|+5(\frac{u_{\sigma}+v_{\sigma}}{2})>u_{\sigma}$.

$\sigma\in[a_{n}, a_{n+1}]$

,

,

if

$\sigma\in[\frac{u+v_{\sigma}}{2}, v_{\sigma}]$if$\sigma\in[y_{\sigma,\tau}, Z_{\sigma,\mathcal{T}}]$and$\neg\psi(\sigma, \mathcal{T})$if$\sigma\in[y_{\sigma T})’ z_{\sigma,\mathcal{T}}]$and$\psi(\sigma, \tau)$$\exists\tau\leq t(\sigma)\psi(\sigma, \mathcal{T})$,.

iff $G( \frac{u+v}{2})-$, where $G=(\{g_{n}\}, m’)$ . Therefore, there$\square$Note. The above theorem can be viewed as a formalized version of theorem 3.7 in Ko’s

book [4].

参考文献[1] F. Ferreira, Polynomial time computable arithmetic, Contemporary Mathematics,

Vol. 106, 1990, 137-156.
[2] F. Ferreira, A feasible theory for analysis, J. Symb. Logic, Vol. 59, No. 3, 1994,

1001-1011.
[3] F. Ferreira, Some notes on subword quantification and induction thereof, Lo

algebra, Lecture notes in pure and appl. math., Vol. 180, No1996, 477-489.
[4] K. Ko, Complexity Theory of Real Functions, Birkh\"auser, 1991.

$g\mathrm{i}\mathrm{c}$

and

34

[5] S. G. Simpson, Subsystems of Second Order Arithmetic, Springer-Verlag, 1998.

[6] S. G. Simpson and R. Smith, Factorization of polynomials andof Pure and Appl. Logic,$\mathrm{v}\mathrm{o}\mathrm{l}$31,1986, 289-306.

$\Sigma_{1}^{0}$

induction, Annals