EWD1117

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 : [expz]: [f.z] 〉     and

(1)     [f.exp]    〈∃z : [zexp]: [f.z] 〉

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

A reason to use (1) is that [zexp] 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 Tue, 1 Jan 2008.