Predicate transformers implied by their dual

[Diethard Michaelis]

Recently [while studying properties of punctual predicate transformers],
I stumbled over the following property of predicate transformer  f 

(as it was simply missing in my list of properties) :

    [ f.(¬X) ⋁ f.X ]  for all X

which by predicate calculus equivales

    [ ¬f.(¬X)  ⇒ f.X ] for all X    i.e.  "the (dual of  f )  implies   f  ".

Together with its converse (equally missing in my list) it yields self-duality.

Can anyone tell, if this property (or its converse) is of some importance
in program semantics, boolean algebra, or whatever subject else?
Has this property a name?

 

I could not figure out.

Diethard.

[Diethard Michaelis]

Just seen the created e-mail ... a bit ugly in plain text ... so here once more w/o formatting (bold etc.)

----

Recently [while studying properties of punctual predicate transformers], I stumbled over the following* property of predicate transformer f *

(as it was simply missing in my list of properties) :

[f.(¬X) ⋁ f.X] for all X

which by predicate calculus equivales

[¬f.(¬X) ⇒ f.X] for all X i.e. "the (dual of f ) implies f ".

Together with its converse (equally missing in my list) it yields self-duality.

Can anyone tell, if this property (or its converse) is of some importance in program semantics, boolean algebra, or whatever subject else?
Has this property a name?
I could not figure out.

Diethard.