A generalization of R.S. Bird’s problem

A generalization of R.S. Bird's problem

About function $f$ has been given

(0) $f$ is a function from naturals to naturals (1) ${f}_{n}\left( {P,n}\right) < f\left( {n + 1}\right)$ for all $n \geq 0$

prove that $f$ is the identity function.

A major observation is that it is essential that range and domain of $f$ are natural: had they been integer, $f$ given by $f_{n} = n - 1$ would have satisfied the inequality of (1) for all $n$ . Since the essential difference between the naturals and the integers is that, with respect to $k$ , the former are well-founded and the latter are not, it is a safe bet that we have to use the well-foundedness of the domain and range of $f$ .

A minor observation is that it is essential that (i) is not weakened to $f\left( {p}_{n}\right) \leq f\left( {n + 1}\right)$ , for in that case $f$ given by $f.n =$ constant would have been a solution.

Actually, $f$ can be proved to be the identity function if (i) is replaced by

$$ f ^ {k} \cdot n < f \cdot (n + 1) \quad \mathrm {f o r a l l} \quad n \geqslant 0 $$

with any $k \geq 2$ . We shall prove the case $k = 3$ . That is, given about $f$

$n \geq 0 \Rightarrow f \cdot n \geq 0,$ and (3) $n \geq 0 \Rightarrow f.\left( {f\left( {f.n}\right) }\right) < f.\left( {n + 1}\right)$ ,

we have to prove $\Rightarrow n \geq 0$ $f \cdot n = n$

In view of the inequality signs in (2) and (3) we may expect to demonstrate $\mathbf{f}{\mathbf{n}} \leq \mathbf{n}$ and $n \leq \mathbf{f}{\mathbf{n}}$ more or less independently, but their direct demonstration by mathematical induction over $n$ runs into problems: we have to conclude something about a single $n$ , and in (2) and (3), $n$ (or $n + 1$ ) only occurs with $f$ applied to it.

There are several ways of removing $f$ -

$\left( i\right) f \cdot x \neq f \cdot y \Rightarrow x \neq y$ (ii) ${f}^{x} < {f}^{y} \Rightarrow x < y\;{for}\;{monotonic}\;f$ . (iii) $a \leq f \cdot x \land f \cdot x < b \Rightarrow a < b$ (and other variations on transitivity)

Via (i) we can deduce from (3)

${f}_{1}\left( {p,n}\right) \neq n + 1$

it will not be used in the remainder of this note. (The conclusion is rather weak.)

Technique (ii) looks more promising, and sug.

gests to try to establish first that $f$ is monotonic. There is hope that we can do that: from (2), which states that all $f$ -values are natural, it follows - well-foundedness of the range!- that there exists a minimum $f$ -value, from (3) - the strictness of $< ! -$ it follows that for positive arguments the $f$ -value is not minimal, hence $f.o$ is the minimum $f$ -value. More precisely (A n: 0x n: f.o < f.n)

In order to repeat the argument, we generalize (2) by replacing the constants $0$ by $i$ , and try to prove

(Ai: 0≤i: (Aii: i≤n ⇒ i≤f.o.o.)

by mathematical induction over i . The base $\left( {\underline{A}n : 0 \leq n \Rightarrow 0 \leq f.n}\right)$ is provided by (2). For the induction step we show that for arbitrary $m \geq 0$

$$ (\underline {{A}} n: i \leq n \Rightarrow i \leq f. n) \Rightarrow (i + 1 \leq m \Rightarrow i + 1 \leq f. m). $$

We distinguish two cases

$$ m = 0 \quad W e o b s e r v e f o r a n y n a t u r a l i $$

$$ \begin{array}{r l} & {i + 1 \leq m} \ {=} & {{i \geq 0, m = 0 }} \ & {\mathrm {f a l s e}} \ {\Rightarrow} & {{\mathrm {p r e d . c a l c .} }} \ & {i + 1 \leq f. m} \end{array} $$

$m > 0$ We shall prove for any natural $i$ and positive $m,i + 1 \leq m \Rightarrow i + 1 \leq f\left( m\right)$ under the assumption of

(6) $\left( {A{n}{i} : i \leq n \Rightarrow i \leq f{n}{i}}\right)$

To this end we observe

$$ \begin{array}{l} i + 1 \leq m \ = {\mathrm {a r i t h m e t i c} } \ i \leq m - 1 \ \end{array} $$

$\Rightarrow \;{ (6)$ with $n \mathrel{\text{:=}} m - 1}$

$$ i \leq f (m - 1) $$

$\Rightarrow { (6)$ with $n \mathrel{\text{:=}} f.\left( {m - 1}\right) }$

$$ i \leq f. (f. (m - 1)) $$

$\Rightarrow { 6}$ with $n = f.p\left( {p\left( {m - 1}\right) }\right) }$

$$ i \leq f. (f. (f. (m - 1))) $$

$= \left{ \begin{array}{l} \text{(3) with }n \mathrel{\text{:=}} m - 1;\;m - 1 \geq 0} \end{array}\right.$

$$ i \leq f. (f. (f. (m - 1))) \land f. (f. (f. (m - 1))) < f. m $$

$\Rightarrow {$ transitivity,see (iii) $}$

$$ i < f, m $$

[\left{ \begin{array}{ll} \text{arithmetic} \ \end{array}\right} ]

$$ i + 1 \leq f. m $$

This completes the proof of (5) which, by an interchange of quantifications, can be written as

$$ (\underline {{A}} n: (\underline {{A}} i: 0 \leq i: i \leq n \Rightarrow i \leq p _ {n})) $$

Remembering that

$$ (\underline {{A}} i: 0 \leq i: i \leq n \Rightarrow i \leq f _ {n}) \equiv n \leq f _ {n} \quad \mathrm {f o r} 0 \leq n $$

we have inadvertently established

(7) $n \leq f.n\;$ for $\;0 \leq n$

We shall now use (5) and (3) to prove

(A i: 0.5 i: f.i < f.(i+1))

i.e., to prove that $f$ is increasing. To this end we observe of an arbitrary natural i the following. Let min satisfy

(9) $i \leq {min}$ and (10) $\left( {\underline{A}k : i \leq k : f\min \leq f,k}\right)$

Because the f.k for is $k$ are natural, there exists among them a minimum value, and therefore it is possible to satisfy (9) and (10). Next we observe for any $n$

$$ i \leq n $$

$$ \begin{array}{l} \Rightarrow {(\overline {{5}}) } \ i \leq f. n \ \Rightarrow \quad {(5) \mathrm {w i t h} n := f _ {n} } \ i \leqslant f ^ {2}. n \ \Rightarrow \quad {(1 0) \mathrm {w i t h} k := f ^ {2} n } \ f. m i n \leq f ^ {3}. n \ = {3 } \ p. m i n < p. (n + 1) \quad *) \ = {\mathrm {a r i t h m e h i c} } \ f. \min \neq f. (n + 1) \ = {\mathrm {L e i n i z} } \ \min \neq n + 1 \ \end{array} $$

Thus we have established

$$ (\mathrm {A n}: i \leq n: \min \neq n + 1) $$

from which we derive by trading

$$ \begin{array}{l} = (\mathrm {A n}: \min = n + 1: i > n) \ = {\mathrm {a r i t h m e t i c} } \ (\mathrm {A n}: \min - 1 = n: i > n) \ = {\mathrm {o n e - p o i n t r u l e} } \ i > \min - 1 \ = {\mathrm {a r i t h m e h i c} } \ \min \leq i. \ \end{array} $$

from this and (9) we conclude min = i

hence from the line marked in the previous proof $i \leq n \Rightarrow {f}{i} < f\left( {n + 1}\right)$ ,in particular ${f}{i} < f\left( {i + 1}\right)$ . Thus (8) has been established

Finally we observe for any natural $n$

true

$$ \begin{array}{l} = {n \mathrm {i s n a t u r a l a n d} (3) } \ f. (f. (f. n)) < f. (n + 1) \ \Rightarrow \quad {f i s m o m o t u m i c } \ f _ {1} (f _ {n}) < n + 1 \ = {(\eta) \mathrm {w i t h} n := n + 1 } \ p. (p, n) < n + 1 \land n + 1 \leq f. (n + 1) \ \Rightarrow {t r a n s i t i v i t y } \ f. (f. n) < f. (n + 1) \ \Rightarrow \quad {f i s m o n o t o n i c } \ f \cdot n < n + 1 \ \end{array} $$

$$ \begin{array}{l} = {\mathrm {a r i t h m e t i c} } \ f \cdot n \leq n \ \end{array} $$

which in combination with (7) establishes (4),

our original demonstrum.

The above owes a lot to J. Misra and J. L. A. van de Sneepscheut. J. Misra proved (8) using (7) and (3) by observing for any natural $i$

$$ \begin{array}{l} p, i \ \leq {(\gamma) \mathrm {w i t h} n := p _ {i} } \ f. (f. i) \ \leq {(7) \mathrm {w i t h} n := f _ {\cdot} (f _ {\cdot} i) } \ f. (f. (f. i)) \ < {3) \mathrm {w i t h} n := i } \ f: (i + 1) \ \end{array} $$

which is a much shorter argument than

mine.

In my treatment of this problem I have tried to avoid pulling rabbits out of the mathematical magician's hat. Formula (5) is an obvious generalization of (2), and it was by that generalization indeed that I constructed (5) as a worthy goal to prove. Please note that (5) may have been much harder to come up with had we not

bothered to formulate (2) and but been content with (0). The description " $f$ is a function from naturals to naturals" is not an invita-tion to manipulation; formula (2) is.

Confession Not having seen that with (2) (5) is equivalent to (7), I originally derived - with one more mathematical induction over $n - \left( 7\right)$ from (2) and (8), (the statement that $f$ is increasing). (End of Confession.)

I did not attempt the other generaliza tion -it was suggested by Misra- to replace the natural numbers with $<$ by a general well-founded set.

Austin, 12 February 1990

Prof. dr. Edsger W. Dgksta Department of Computer Sciences The University of Texas at Austin Austin, TX 78712 - 1188 USA