__Monotonic demonstranda and dummy introduction__

When we have to prove

[`f`.`exp`]

for some `exp` and some __monotonic__ `f`, it can help to know the following theorem

__Theorem__ For monotonic `f`

(0) [`f`.`exp`] ≡ 〈∀`z `: [`exp` ⇒ `z`]: [`f`.`z`] 〉 and

(1) [`f`.`exp`] ≡ 〈∃`z `: [`z` ⇒ `exp`]: [`f`.`z`] 〉

A reason to use (0) is that [`exp` ⇒ `z`] is the form of expression in which we can manipulate` exp` . An example is given in EWD1118.

A reason to use (1) is that [`z` ⇒ `exp`] is the form of conclusion we can draw about `exp`; if it exists, the strongest `z` satisfying [`f`.`z`] is a good candidate for a witness. An example is given in EWD1116.

This theorem is very simple, very general and probably equally applicable and useful. Why did it take me a lifetime to formulate it?

Austin, 1 December 1991

prof.dr E.W.Dijkstra, CS Dept., UT, Austin TX 78712 - 1188

Transcribed by Guy Haworth.

Last modified