"Vacuous" quantification

[Jeremy Weissmann]

Dear all,

   Today I had the pleasure of calculating some predicate calculus results which seemed intuitive, but which were previously unknown to me.  Allow me to share them.

   First, let us recall the following slightly-unfamiliar distributivity property:

(0)     (Ax : r.x : t.x => C)   ==   (Ex : r.x : t.x) => C       .

The validity of  (0)  may be seen from the following calculation:

      (Ax : r.x : t.x => C)

==     {  =>  into  ¬  and  \/  }

      (Ax : r.x : ¬t.x \/ C)

==     {  \/  over  A  }

      (Ax : r.x : ¬t.x)  \/  C

==     { de Morgan }

      ¬(Ex : r.x : t.x)  \/  C

==     {  ¬  and  \/  into  =>  }

      (Ex : r.x : t.x)  =>  C     .

* * *

   The formula I was considering today had the shape:

(*)     (Ax,y : r.x.y /\ s.y : t.y)     .

Notice that the quantification is over  x  and  y ,  but the range of quantification is somewhat  “disentangled”  with respect to these variables, and the term does not depend on  x  at all.  It seemed clear to me that under certain conditions, the quantification over  x  could be considered  “vacuous”  and be eliminated.  Intuitively, we would need to at least prove the existence of some  x  satisfying  r.x.y ,  because if we take  r.x.y == false  in  (*) ,  then the whole formula equivales  false  as well.

   I decided to calculate to find the condition in question:

     (Ax,y : r.x.y /\ s.y : t.y)

==     { nesting }

     (Ay :: (Ax : r.x.y /\ s.y : t.y) )

==     { shunting }

     (Ay :: (Ax ::  r.x.y /\ s.y  =>  t.y ) )

==     { distributivity property (0) }

     (Ay :: (Ex :: r.x.y /\ s.y)  =>  t.y )

==     {  /\  over  E  }

     (Ay :: (Ex :: r.x.y) /\ s.y  =>  t.y )

==     { • assuming  s.y  =>  (Ex :: r.x.y)  }

     (Ay :: s.y => t.y)

==     { shunting }

     (Ay : s.y : t.y)       .

And so we have learned that the  “vacuous quantification”  rule:

(1)     (Ax,y : r.x.y /\ s.y : t.y)   ==   (Ay : s.y : t.y)

holds, provided we have  (Ay : s.y : (Ex :: r.x.y)) .   Somehow, I feel like I may have proved this before!  (It’s certainly related to JAW66:  http://mathmeth.com/jaw/main/jaw0xx/jaw66.pdf .)

* * *

   Finally, I will reveal the original context of these considerations.  We borrow the basic language of (naive) set theory:  elements, sets, the predicate  ∈ ,  and so forth.  (See Appendix.)  Next, we consider a function  p ,  with which we may form expressions like  p.x ,  where the low dot denotes  ‘application’  of  p  to the element  x .   We extend this notation and allow functions to be applied to sets by the following definition:

(2)     y ∈ p.C  ==  (Ex : x ∈ C : y = p.x)     ,

from which we conclude the basic property:

(2')     x ∈ C  =>  p.x ∈ p.C     .

Additionally, for each element  y  we define a set  p⁻¹.y  by:

(3)     x ∈ p⁻¹.y  ==  p.x = y     .

   Finally, we wish to speak of a set  C  being  ‘saturated’  by  p .   In James Munkres’s book,  Topology ,  he defines this notion by saying that  C  should contain every set  p⁻¹.y  that it intersects.  A colorful description, but not great for calculation!  Let’s see what we can do:

     (Ay ::  C ∩ p⁻¹.y ≠ ø  =>  p⁻¹.y ⊂ C )

==     { rewriting the antecedent, in the language of elements; (3) }

     (Ay ::  (Ez ::  z ∈ C  /\  p.z = y )  =>  p⁻¹.y ⊂ C )

==     { distributive property (0) }

     (Ay,z  :  z ∈ C  /\  p.z = y  :  p⁻¹.y ⊂ C )

==     { one-point rule to eliminate  y  }

     (Az  :  z ∈ C  :  p⁻¹.(p.z) ⊂ C )     .

For my money, this is already a decent simplification!  (I am thinking in particular of the homogenization and disentanglement of the symbols.)  But let’s press further:

     (Az  :  z ∈ C  :  p⁻¹.(p.z) ⊂ C )

==     { expanding the term, in the language of elements; (3) }

     (Az  :  z ∈ C  :  (Ax : p.x = p.z : x ∈ C) )

==     { (un)nesting }

     (Az,x  :  z ∈ C  /\  p.x = p.z  :  x ∈ C )

==     { preparing to eliminate  z ;  (2') and Leibniz }

     (Az,x  :  z ∈ C  /\  p.x = p.z  /\  p.x ∈ p.C  :  x ∈ C )

==     { • vacuous quantification rule (1) ;  see deferred proof obligation below }

     (Ax : p.x ∈ p.C : x ∈ C)     .

And so we may equivalently and simply say that  C  is saturated by  p  if  p.x ∈ p.C  implies  x ∈ C .   Note that this is simply the converse of  (2’)  given above, and constitutes a sort of cancellation property with respect to  ∈ .   Of course, we are only entitled to this simpler definition, provided we address our deferred proof obligation:

     p.x ∈ p.C  =>  (Ez ::  z ∈ C  /\  p.x = p.z )     .

But this is precisely definition  (2)  of  p.C .

* * *

   All best,

+j

APPENDIX

=========

   We consider a universe of mathematical objects which come in two types:  ‘elements’  and  ‘sets’ .   With  x  of type element and  C  of type set we have the predicate  x ∈ C .   We now introduce a new type,  ‘function’ .   With  p  of type function and  x  any mathematical object, we can form the expression  p.x ,  which denotes the  ‘application’  of  p  to  x .   Functions are required to satisfy the  ‘Leibniz’  property:

     x = y  =>  p.x = p.y     (for all  x,y )

which (for example) predicates satisfy as well.  (Indeed, in the final calculation above I used  p.x = p.z  =>  (p.x ∈ C == p.z ∈ C) ,  which is an example of the Leibniz property for predicates.  Accordingly, one might consider predicates to be a sort of function.)   Typically, a function only satisfies the Leibniz property for a collection of mathematical objects specified as the  ‘domain’  of that function, though such specification is not necessary to follow the above discussion.

   It bears mentioning that in certain axiomatic approaches to set theory,  ‘element’ ,  ‘function’ ,  ‘domain’ ,  etc, are all taken to be subtypes of the type  ‘set’ .   For that matter, so is  ‘predicate’ .   Again, I consider all this overspecific and useful primarily for the logical study of (limitations of) set theory.

   Sets satisfy the following axiomatic property:

(0)     C = D  ==  (Ax :: x ∈ C == x ∈ D)     .

We define a relation  ⊂  on sets by:

     C ⊂ D  ==  (Ax :: x ∈ C => x ∈ D)     ,

so that we have a sort of mutual implication property for sets:

     C = D   ==   C ⊂ D  /\  D ⊂ C     .

Note that, thanks to  (0) ,  a property like:

(*)     x ∈ C  ==  f.x

uniquely defines a set  C ,  and we exploit this right away to define the empty set  ø  by:

     x ∈ ø  ==  false     .

It follows that  C ≠ ø  ==  (Ex :: x ∈ C) .   Similarly, we define operators  ∪  and  ∩  on sets by:

     x ∈ C ∪ D   ==   x ∈ C  \/  x ∈ D

     x ∈ C ∩ D   ==   x ∈ C  /\  x ∈ D     .

(End of APPENDIX.)

[Jeremy Weissmann]

In the appendix, I should have written that formula (*) “defines at most one set”, rather than “uniquely defines”. 

On Jan 31, 2022, at 15:14, Jeremy Weissmann <plusj...@gmail.com> wrote:

Dear all,

[alexk]

Hi.

I am not sure if the following makes much (or any) sense, but i feel that the dual approach to the problem is possible.
We can define 'p⁻¹' as dual to the variant of 'p' that maps sets to sets, instead of its lifted version.

Than Munkres’s definition amounts to:

    p is total surjective function from X to Y
=>    
    C is saturated by p  ==  C solves (0)

(0)  x: (Ay :: p⁻¹.(p.(p⁻¹.y ∩ x)) ⊂ x)

Lets explore properties of p and p⁻¹.

(1)     x ⊂ p⁻¹.(p.x)          total
(2)     y ⊂ p.(p⁻¹.y)          surjective
(3)     p.(p⁻¹.y) ⊂ y          function

also we can establish

(4)     p.x ∩ y = ø  ==  x ∩ p⁻¹.y = ø      for all x and y

which means that p and p⁻¹ form Galois algebra from which we can borrow:

(5) p and p⁻¹ are universally disjunctive (hence monotonic)

and

(6)     p.x ∩ y => p.(x ∩ p⁻¹.y)
(7)     p⁻¹.y ∩ x => p⁻¹.(y ∩ p.x)

also known as Dedekind rules.

We can strengthen it to

(8)     p.x ∩ y == p.(x ∩ p⁻¹.y)

by cyclic implication:

    p.x ∩ y
=>      { (6) Dedekind rule }
    p.(x ∩ p⁻¹.y)
=>      { (7) Dedekind rule }
    p.(p⁻¹.(p.C ∩ D))
=>      { (3) p is function }  
    p.C ∩ D
   
now we can simplify (0)

    p⁻¹.(p.(p⁻¹.y ∩ x)) ⊂ x
=       { (8) }
    p⁻¹.(p.x ∩ y)) ⊂ C

or

    p is total surjective function from X to Y
=>    
    C is saturated by p  ==  C solves (9)

(9)  x: (Ay :: p⁻¹.(p.x ∩ y)) ⊂ x)

and at last we can derive definition of saturation from Wikipedia:

    (Ay :: p⁻¹.(p.x ∩ y)) ⊂ x)
=>      { instantiation y := Y }
    p⁻¹.(p.x ∩ Y)) ⊂ x
=       { p.x ⊂ Y (Y is range of p)}
    p⁻¹.(p.x) ⊂ x
=       { (1) p is total }
    p⁻¹.(p.x) = x

or

    p is total surjective function from X to Y
=>    
    C is saturated by p  ==  C solves (10)  

(10)  x: (p⁻¹.(p.x) = x)  

alexk

понедельник, 31 января 2022 г. в 23:14:40 UTC+3, Jeremy Weissmann:

[Jeremy Weissmann]

This is fascinating.  I may need it decoded a bit for me.  What is the dual  p⁻¹ ?

--
You received this message because you are subscribed the mathmeth.com mailing list.
To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
---
You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/3028db20-dd95-43cc-8182-5b2c9607781en%40googlegroups.com.

[MS]

Hi Guys,

Can you summarise the discussion in layman's terms, it seems like you had fascinating results.

Regards

Mahesh

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/2613C27C-D9EC-43E1-BE93-C9D0654B2FB3%40gmail.com.

[Jeremy Weissmann]

What is layman’s terms?  I essentially used only predicate calculus in my discussion, plus a very small modicum of set theory which I also explained in an appendix.

+j

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/CAEBVrk8-4Zx2s8nKsnWmt1kyR9m20HChX4H4wrjvumo3HYwd_Q%40mail.gmail.com.

[MS]

Actually what the concept is I didn't understand your formulation. I am seeking an explanation in prose.

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/20C4AEF7-7B17-410D-8C42-A0E1875521C5%40gmail.com.

[alexk]

   As i recall my thought process it was something like this. 

   Initialy there where 'dual' definition op 'p':

-------------------------------------------------

    (2)     y ∈ p.C  ==  (Ex : x ∈ C : y = p.x)     ,

from which we conclude the basic property:

    (2')    x ∈ C  =>  p.x ∈ p.C     .

-------------------------------------------------

    To distinguish them, we can rename 'unlifted' version 'p' into 'P'

-------------------------------------------------

    (2)     y ∈ P.C  ==  (Ex : x ∈ C : y = p.x)     ,

from which we conclude the basic property:

    (2')    x ∈ C  =>  p.x ∈ P.C     .

-------------------------------------------------    

    What i meant by 'dual' of p⁻¹ is P⁻¹.
    We can define P as

    P.C = (Ux: x ∈ C: p.x)

    and P⁻¹

    P⁻¹.D = (Uy: y ∈ D: p⁻¹.y)

    because inverse of a function is not unique:

        D = P.C  =>  C ⊂  P⁻¹.D

    if C contain just one point {x} and y = p.x
    then p and P are the 'same' (only difference is that an argument of p⁻¹ is an element
    and an argument of P⁻¹ is a set of one element):
   
        p⁻¹.y = P⁻¹.{y}

    and for total surjective function p from X to Y

        P.X = Y and P⁻¹.Y = X

    (whole domain is mapped onto whole image and back)

    With this i interpret 'C intersect p⁻¹.y' as 'P⁻¹.y ∩ C'
   
    and to demonstrate that C contains all p⁻¹.y it intersects we

    - recover y that produce an intersection

        P.(P⁻¹.y ∩ C)
    - recompute preimage of y's
        P⁻¹.(P.(P⁻¹.y ∩ C))

    - and claim it that C contains it

        P⁻¹.(P.(P⁻¹.C ∩ C)) ⊂ C

 

среда, 2 февраля 2022 г. в 05:13:31 UTC+3, Jeremy Weissmann:

[Jeremy Weissmann]

The discussion is about set theory, vacuous quantification (situations where quantification can be “dropped” from a formula), and simplification of a definition from a textbook. 

On Feb 2, 2022, at 01:51, MS <msha...@acm.org> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/CAEBVrk9FM8y4KsD8rgN35VvBKewRxgUzNHAvyh_cQ0%2B59xRWBQ%40mail.gmail.com.

[alexk]

My definition of P was wrong.

Instead of

    P.C = (Ux: x ∈ C: p.x)

it should be

    P.C = {y: x ∈ C  /\  y = p.x}

среда, 2 февраля 2022 г. в 10:01:04 UTC+3, alexk:

[Jeremy Weissmann]

One notation Dijkstra gives for this is:

     P.C = (x : x ∈ C : p.x)     ,

which is very close to what you wrote.  I confess though that I am not familiar with a lot of the properties you invoked so I will have to try to prove them myself.

+j

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/bb445cfb-7cf6-4f27-873a-f8a25244ebefn%40googlegroups.com.

[Diethard Michaelis]

Hi Jeremy,

Some comments.

@(0) (Ax : r.x : t.x => C) == (Ex : r.x : t.x) => C
Your "slightly-unfamiliar" (0) is just the first of the
"two (ugly) formulae" (118),(119) from
Dijkstra, Scholten: Predicate Calculus and Program Semantics,
Ch.5 The calculus of boolean structures.

@(*) (Ax,y : r.x.y /\ s.y : t.y)

"because if we take r.x.y == false in (*) ,
then the whole formula equivales false as well."

No, it equivales true: (Ax : false : ...) = true.

@(1) (Ax,y : r.x.y /\ s.y : t.y) == (Ay : s.y : t.y)
In view of shunting / trading range and term
s becomes redundant { s,t := true,(s => t) }
and (1) becomes
(1') (Ax,y : r.x.y : t.y) == (Ay : true : t.y)
or equivalently using [p] (everywhere) for (Ay::p.y)
(1") [(Ax : r.x : t)] == [t]
<=> { (0)/DS(118) }
[(Ex : r.x : true) => t] == [t]
<=> { trading ; E := (Ex :: r.x) }
[E => t] == [t]
<== { proviso [E] is a bit coarse ... can do better
: range diffusion }
[E\/t => t] == [t]
<== {}
[E\/t]
<=> { shunting / trading if we don't want t in []'s term }
[-t => E] .

@"p saturated subset"
We have an equivalence relation R.p: x(R.p)y == (p.x = p.y) .
Arbitrary unions of R.p's equivalence classes
form just the p saturated subsets of p's domain.

@Appendix
Classes (not sets) form a Boolean algebra ...

Cheers, Diethard.

> holds, provided we have (Ay : s.y : (Ex :: r.x.y)) . Somehow, I feel like I may have proved this before! (It’s certainly related to JAW66: http://mathmeth.com/jaw/main/jaw0xx/jaw66.pdf <http://mathmeth.com/jaw/main/jaw0xx/jaw66.pdf> .)

[Алексей Краевский]

If it helps, I borrowed properties

p is total ~p.(p.X) <= X
p is surjective p.(~p.Y) <= Y
p is functional p.(~p.Y) => Y
p is injective ~p.(p.X) => X

from 'Relational calculus and relational program semantics' by Rutger M. Dijkstra who borrowed them from 'A relational theory of data types' by R.C. Backhouse et al.

Everything related to Galois algebra is taken from 'Temporal algebra' by Burghard von Karger.

You received this message because you are subscribed to a topic in the Google Groups "Calculational Mathematics" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/calculational-mathematics/I2QbMLysYys/unsubscribe.
To unsubscribe from this group and all its topics, send an email to calculational-math...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/B147C90B-7F9F-4753-BC3C-5A38F2FE4246%40gmail.com.

[Jeremy Weissmann]

@(*) (Ax,y : r.x.y /\ s.y : t.y)
"because if we take  r.x.y == false  in  (*) ,
then the whole formula equivales  false  as well."
No, it equivales true: (Ax : false : ...) = true.

Whoops! Thank you!

@(1) (Ax,y : r.x.y /\ s.y : t.y)   ==   (Ay : s.y : t.y)
In view of shunting / trading range and term
s becomes redundant { s,t := true,(s => t) }
and (1) becomes
(1') (Ax,y : r.x.y : t.y)   ==   (Ay : true : t.y)
or equivalently using [p] (everywhere) for (Ay::p.y)
(1") [(Ax : r.x : t)] == [t]
<=> { (0)/DS(118) }
  [(Ex : r.x : true) => t] == [t]
<=> { trading ; E := (Ex :: r.x) }
  [E => t] == [t]
<== { proviso [E] is a bit coarse ... can do better
   : range diffusion }
  [E\/t => t] == [t]
<== {}
  [E\/t]
<=> { shunting / trading if we don't want t in []'s term  }
  [-t => E] .

This is a nice simplification in many ways.

@"p saturated subset"
We have an equivalence relation R.p: x(R.p)y == (p.x = p.y) .
Arbitrary unions of R.p's equivalence classes
form just the p saturated subsets of p's domain.

Yes, this is perhaps a nice answer to Mahesh’s question.  Saturated sets are arbitrary unions of  “fibers”  of  p .

@Appendix
Classes (not sets) form a Boolean algebra ...

Sorry, I’m not sure what you’re referring to, here.

+j

[Diethard Michaelis]

>> @Appendix
>> Classes (not sets) form a Boolean algebra ...
>
> Sorry, I’m not sure what you’re referring to, here.
>

Thus the characteristic predicate of a class "is" the class ...
and I do not need two different calculi/notations
(set and Boolean algebra).
Boolean algebra calculus suffices.

[Jeremy Weissmann]

I don’t take such a monotheistic view of things, but I support all views.

> On Feb 2, 2022, at 11:51, Diethard Michaelis <diethard....@t-online.de> wrote:
>
> 

> --
> You received this message because you are subscribed the mathmeth.com mailing list.
> To unsubscribe from this group, send email to Calculational-Math...@googlegroups.com
> For more options, visit this group at http://groups.google.com/group/Calculational-Mathematics?hl=en
> --- You received this message because you are subscribed to the Google Groups "Calculational Mathematics" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to calculational-math...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/49f4cc73-ffa3-1b63-672f-982d533ea83f%40t-online.de.

[Diethard Michaelis]

Hi Jeremy,

A tiny mono-Boolean :-) demonstration and experiment
to remedy my obviously too sparse
"classes form a boolean algebra" hint.

Let's see what DS predicate calculus can do for
Munkres' definition of "C is p-saturated"
(Ay :: C ∩ p⁻¹.y ≠ ø => p⁻¹.y ⊂ C ) .

. C ∩ p⁻¹.y ≠ ø => p⁻¹.y ⊂ C
<=> { sets as characteristic predicates
. ; transform set operations into boolean operators
. : ∩ -> /\, ø -> false, A ≠ B -> not[A == B], A ⊂ B -> [A => B]
. ; P := p⁻¹.y
. }
. not[(C /\ P) == false] => [P => C]
<=> { pred.calc. (aiming for \/ and symmetry) }
. [P => not C] \/ [P => C]
<=> { or into exclusive or via Golden Rule}
. [P => not C] =/= [P => C] =/= [P => not C] /\ [P => C]
<=>
. { collapse conjunct: [A]/\[B] = [A/\B]
. ; (A=>B)/\(A=>C) == (A=>(B/\C)) ; (A => false) == not A
. }
. [P => not C] =/= [P => C] =/= [not P]
<=>
. { massage "=/= [not P]"
: "=/=" = "== not" ; mutual impl. ; contra-positive
. ; rearrange
. }
. not[not P] => ([P => not C] =/= [P => C])
. /\ [not P] => ([P => not C] == [P => C])
<=>
. { 2nd conjunct vanishes
. : Leibniz: [P == false] => [e.P == e.false]
. ; [false => A] ; [A => true]
. }
. not[not P] => ([P => not C] =/= [P => C])
<=> { back to sets (~ for set complement, universe is p's range) }
. p⁻¹.y ≠ ø => ((p⁻¹.y ⊂ ~C) =/= (p⁻¹.y ⊂ C))

Thus I've re-discovered in great . . . detail
a useful and probably well known
predicate calculus theorem (for arbitrary P and C).

[P => not C] \/ [P => C]
==
(([P => not C] =/= [P => C]) <= not[not P]) ,

and in passing

([P => not C] == [P => C]) <= [not P] .

And as corollary of the 1st theorem
by transcription from predicate to set operators

C is p-saturated
<=>
The preimage of any point in p's image (not range!)
is either contained in C or in C's complement.

Diethard.