A predicate sequence `P`_{i} (`i` ≥
0) such that —denoting universal quantification over all states by
square brackets— (A`i` :
`i` ≥ 0 : [`P`_{i} ⇒
`P`_{i+1}]) is called *weakening*; a predicate sequence
`P`_{i} (`i` ≥ 0) such that (A`i` : `i` ≥ 0 :
[`P`_{i+1} ⇒
`P`_{i}]) is called *strengthening*. A predicate sequence
`P`_{i} (`i` ≥ 0) that is
weakening or strengthening is called *monotonic*.

**Theorem** For any monotonic predicate
sequence `P`_{i} (`i` ≥ 0) we have

[(A`i` : `i`
≥ 0 : (E`j` : `j`
≥ `i` : `P`_{j})) = (E`i` : `i` ≥ 0 : (A`j` : `j` ≥ `i` :
`P`_{j}))] .

**Proof** Let
`P`_{i} (`i` ≥ 0) be a weakening
predicate sequence; we then have for all natural `i`

(0) [`P`_{i} = (A`j` : `j` ≥ `i` :
`P`_{j})]

(1) [(E`j` : `j`
≥ `i` : `P`_{j}) = (E`j` : `j` ≥ 0 :
`P`_{j})] .

For arbitrary `Z` we observe

[`Z` = (A`i` :
`i` ≥ 0 : (E`j` :
`j` ≥ `i` : `P`_{j}))]

= {(1)}

[`Z` = (A`i` :
`i` ≥ 0 : (E`j` :
`j` ≥ 0 : `P`_{j}))]

= {predicate calculus}

[`Z` = (E`j` :
`j` ≥ 0 : `P`_{j})]

= {renaming the dummy}

[`Z` = (E`i` :
`i` ≥ 0 : `P`_{i})]

= {(0)}

[`Z` = (E`i` :
`i` ≥ 0 : (A`j` :
`j` ≥ i : `P`_{j}))]

which proves the theorem for weakening

`P`

_{i}(

`i`≥ 0).

Let `P`_{i} (`i` ≥ 0) be a
strengthening predicate sequence; then the sequence of predicates
¬`P`_{i} is weakening and we conclude
from the above

[(A`i` : `i`
≥ 0 : (E`j` : `j`
≥ `i` : ¬`P`_{j})) =
(E`i` : `i` ≥ 0 :
(A`j` : `j` ≥
`i` : ¬`P`_{j}))] .

Negating both sides and applying de Morgan yields

[(E`i` : `i`
≥ 0 : (A`j` : `j`
≥ `i` : `P`_{j})) = (A`i` : `i` ≥ 0 : (E`j` : `j` ≥ `i`
: `P`_{j}))] .

(End of Proof.)

As we see from the proof, the two equal expressions mentioned in the
Theorem are for a weakening predicate sequence
`P`_{i} (`i` ≥ 0) most simply
expressed as (E`i` : `i`
≥ 0 : `P`_{i}); for a strengthening
predicate sequence `P`_{i} (`i`
≥ 0) they are most simply expressed as (A`i` : `i` ≥ 0 :
`P`_{i}). These are the forms in which these
limits are best known.

* *

*

C.S. Scholten and I discovered this theorem while working on EWD816. We were slightly amazed that in its full generality the Theorem was new for us, the more so because monotonic predicate sequences occur so frequently and its proof is so simple. (The Theorem, though nice and in a way striking, is definitely not deep.) Hence this note.