A Simple Exercise using the Modular Law

Josh needs a property for which there is an obvious pointwise proof. He wonders whether it is possible to prove it in point-free style. I haven’t practised point-free proofs for a while, so I’d give it a try.

The actual property he needs is that FT . C ⊆ C . FT . C where C is a coreflexive, given T ⊆ ⦇S⦈ and F⦇S⦈ . C ⊆ C . F⦇S⦈ . C. It is sufficient to prove this generalised property:

S ⊆ C . S     ⇐     R ⊆ C . R   ∧   S ⊆ R

Intuitively speaking, if C covers the range of R and S ⊆ R, then C covers the range of S too.

Well, the proof goes:

    C . S
= { since C . C = C }
    C . C . S
{ since X ⊇ X ∩ Y }
     C . ((C . S) ∩ R)
{ modular law X ∩ (Y.Z) ⊆ Y . ((Y˘.X) ∩ Z), and C˘ = C }
     S ∩ (C . R)
{ given: R ⊆ C . R }
     S ∩ R
= { given: S ⊆ R }

It is hard to explain the intuition behind the use of modular law. If we take C as a predicate, the property can be written pointwisely as:

(b S a ⇒ C b ∧ b S a)     ⇐     (b R a ⇒ C b ∧ b R a)   ∧   b S a ⇒ b R a

where a and b are both universally quantified. We may simplify b S a ⇒ C b ∧ b S a to b S a ⇒ C b, but that makes it more difficult to see the connection. Essentially, I was mimicking the following obvious proof:

    C b ∧ b S a
{ strengthening }
    C b ∧ b S a ∧ b R a
{ since b R a ⇒ C b ∧ b R a }
    b S a ∧ b R a
{ since b S a ⇒ b R a }
     b S a

The strengthening step corresponds to the use of X ⊇ X ∩ Y, while the next two steps respectively correspond to the last two steps of the point-free proof. The modular law, implicit in the pointwise proof, was used to group C and R to the right places.

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>