66 views

Skip to first unread message

Jan 31, 2022, 3:14:40 PM1/31/22

to mathmeth, Tom Verhoeff, Wim Feijen

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.)

Jan 31, 2022, 3:46:41 PM1/31/22

to mathmeth, Tom Verhoeff, Wim Feijen

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,

Feb 1, 2022, 3:30:15 PM2/1/22

to Calculational Mathematics

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)

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:

Feb 1, 2022, 9:13:31 PM2/1/22

to mathmeth

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.

Feb 1, 2022, 10:15:51 PM2/1/22

to calculationa...@googlegroups.com

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.

Feb 1, 2022, 10:27:53 PM2/1/22

to mathmeth

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.

Feb 2, 2022, 1:51:41 AM2/2/22

to calculationa...@googlegroups.com

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.

Feb 2, 2022, 2:01:04 AM2/2/22

to Calculational Mathematics

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) ,

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

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

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))

- 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:

Feb 2, 2022, 7:25:12 AM2/2/22

to calculationa...@googlegroups.com

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.

Feb 2, 2022, 10:22:06 AM2/2/22

to Calculational Mathematics

My definition of P was wrong.

Instead of

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

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

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

Feb 2, 2022, 11:16:07 AM2/2/22

to mathmeth

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.

Feb 2, 2022, 11:32:29 AM2/2/22

to calculationa...@googlegroups.com

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)

@(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> .)

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.
then the whole formula equivales false as well."

@(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.

Feb 2, 2022, 11:33:05 AM2/2/22

to calculationa...@googlegroups.com

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.

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.

Feb 2, 2022, 11:39:50 AM2/2/22

to mathmeth

@(*) (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

Feb 2, 2022, 11:51:14 AM2/2/22

to calculationa...@googlegroups.com

>> @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 ...
>> Classes (not sets) form a Boolean algebra ...

>

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

>

and I do not need two different calculi/notations

(set and Boolean algebra).

Boolean algebra calculus suffices.

Feb 2, 2022, 11:54:04 AM2/2/22

to calculationa...@googlegroups.com

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:

>

>

> 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.
> 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.

Feb 7, 2022, 8:33:35 AM2/7/22

to calculationa...@googlegroups.com

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.

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.

Reply all

Reply to author

Forward

0 new messages