For Once and for All

I think I've finally discovered how to explain the difference between functional requirements of a system and requirements of an instance of data produced by that system.  The distinction is based on the different between the logical qualifiers ∀ and ∃.  Given that we (IHE, HL7 and others), express requirements on content of the document (or message);

To express a constraint that is true for all instances of every document,
 ∀ documents: X shall/should/may Y.

And to express a constraint that must be true for at least one instance of a document,
 ∃ document: X shall/should/may Y.

This is fairly clear to engineers who have not been trained in "standards terminology" such as the distinctions between mandatory and required.  For a document X and data element Y: To say that Y is mandatory in X is the same as saying: ∀ documents X: X SHALL contain Y.  To say that Y is required in X is the same as saying ∃ document X: X SHALL contain Y.  To test the system for the first case, you must verify that Y is present in all cases.  To test the system for the second, you must verify that Y is present in at least one case.

In both cases, the system MUST be able to produce Y, the distinction is whether is must do so all the time, or just some of the time.

If I'm right, then I've managed to explain it for once ∃ and for all ∀. [ouch]

   Keith