A nice theorem on monotonic predicate sequences

A nice theorem on monotonic predicate sequences

A predicate sequence P_i (i ≥ 0) such that —denoting universal quantification over all states by square brackets— (Ai : i ≥ 0 : [P_i ⇒ P_i+1]) is called weakening; a predicate sequence P_i (i ≥ 0) such that (Ai : 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
  [(Ai : i ≥ 0 : (Ej : j ≥ i : P_j)) = (Ei : i ≥ 0 : (Aj : 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 = (Aj : j ≥ i : P_j)]
(1)  [(Ej : j ≥ i : P_j) = (Ej : j ≥ 0 : P_j)] .
For arbitrary Z we observe

  [Z = (Ai : i ≥ 0 : (Ej : j ≥ i : P_j))]
  = {(1)}
  [Z = (Ai : i ≥ 0 : (Ej : j ≥ 0 : P_j))]
  = {predicate calculus}
  [Z = (Ej : j ≥ 0 : P_j)]
  = {renaming the dummy}
  [Z = (Ei : i ≥ 0 : P_i)]
  = {(0)}
  [Z = (Ei : i ≥ 0 : (Aj : 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
  [(Ai : i ≥ 0 : (Ej : j ≥ i : ¬P_j)) = (Ei : i ≥ 0 : (Aj : j ≥ i : ¬P_j))] .
Negating both sides and applying de Morgan yields
  [(Ei : i ≥ 0 : (Aj : j ≥ i : P_j)) = (Ai : i ≥ 0 : (Ej : 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 (Ei : i ≥ 0 : P_i); for a strengthening predicate sequence P_i (i ≥ 0) they are most simply expressed as (Ai : 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.

---