A hint from monotonicity?

A hint from monotonicity?

In EWD832, a one-page note I wrote in 1982, I gave an (obviously short) proof

Theorem An infinite sequence of (real) numbers contains an infinite monotonic subsequence. (End of Theorem.)

Being reminded of it, I looked it up; it had been written on a Monday, and ended with

"I found this proof last Sunday evening; the day before I had heard the theorem together with the rumour that it might require a fancy proof. Quod non."

Well, my proof may not have been "fancy," it definitely contained a rabbit; for a moment I thought that the removal of that rabbit was now a routine matter, but this turned out not to be the case; reason enough to return to the problem.

There are, broadly speaking, two types of monotonic subsequences, viz. ascending ones

and descending ones. It therefore stands to reason to create a dichotomy, i.e. to look for a predicate $P$ on sequences such that for any $x$

${P}_{x} \Rightarrow$ x contains an infinite and ${7P} \cdot x \Rightarrow$ x contains an infinite descending subsequence

But since many sequences contain both types of subsequences, we have consider able freedom in the choice of $P$ . The challenge is to exploit that freedom wisely.

In principle we could take for P.x just "x contains an infinite ascending subsequence". In order to pursue the consequences of this choice, we formal- ize it. With $p,q$ of type "natural" and s of type "predicate on naturals", the existence of an infinite ascending subsequence contained in x boils down to the existence of an s such that

(0) $\left\langle {\exists p : s.p}\right\rangle \land$

$\left\langle {\forall p : s.p. : \left\langle {\exists q : s.q \land p < q : x.p \leq {x.q}}\right\rangle }\right\rangle$

The first conjunct expresses that the ascending subsequence is not empty, the second conjunct expresses that the ascending subsequence has no last element.

But in all its generality, (0) is an unpleasant formula to work with: with s ranging over all predicates on the naturals, (0) is not (anti)monotonically dependent on s. (Given an s that satisfies (0), (0) can in general be falsified both by weakening and by strengthening

Can we restrict the range of $s$ in such a way that (o)'s dependence on s becomes (anti) monotonic? Looking at the second conjunct of (o), we see that it depends antimonotonically on s.p and monotonically on s.q. Hence we can only solve our problem if we can make one of the two ranges independent of s . Predicate calculus tells us that we can simplify the range s.q A p<q for q to p<q provided

${5.9} \sim p < q \Rightarrow {5.9}$ $p < q \Rightarrow \left( {s.p \Rightarrow s.q}\right)$

the general solution of which is

(2) $\;s.p \equiv n \leq p\;$ for some

or

(3) $s.p \equiv f\left( a\right)$ false

The latter solution of (1) is rejected on account of the first conjunct of (0). With choice (2), the existential quantification over $s$ becomes one over $n$ , and we get for $P.x$

$\langle \exists n : \langle \forall p : n \leq p : \langle \exists q : p < q : x.p \leq x.q\rangle \rangle \rangle$

(4) $\langle \forall n : \langle \exists p : n \leq p : \langle \forall q : p < q : x.p > x.q\rangle \rangle \rangle$

With s defined by

(5) $s.p \equiv \left\langle {\forall t : p < t : x.p > x.t}\right\rangle$

we derive

(6) $\mathrm{s}.\mathrm{p} \land \mathrm{p} < \mathrm{q} \Rightarrow \mathrm{x}.\mathrm{p} > \mathrm{x}.\mathrm{q}$ , and rewrite (4) as (7) $\langle \forall n : \langle \exists p : n \leq p : s.p. \rangle$ ,

(8) $\langle \exists p : {s.p} \rangle$

Finally, in order to establish the existence of an infinite decreasing sub sequence, we observe for any $p$

[\text{S.p.} \Rightarrow \left\langle {\exists q : S,q \land p < q : x.p > x.q}\right\rangle ] $\Leftrightarrow$ {pred. calc.; arithmetic} $\Leftrightarrow \;\left{ \begin{array}{l} { \left( 7\right) \text{ with }n,p \mathrel{\text{:=}} p + 1,q} \ \end{array}\right.$

Without any introduction, EWD832 gave a definition like (5), and then made a case analysis on whether the number of p-values satisfying s.p was finite or not. Some rabbits, I think, have been successfully removed.

Austin, 23 February 1996

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

USA