An interesting problem to think about:

[Jeremy Weissmann]

Given f is conjunctive, meaning:

[ f.(x /\ y) == f.x /\ f.y ] for all x,y .

Show that f is disjunctive if and only if:

(*) (∀x :: f.x == (∀y : f.y : < x /\ y > )) ,

where < > is the somewhere operator.

——

Some observations: f being conjunctive already gives us one direction of disjunctivity, namely monotonicity in the form:

[ f.x \/ f.y => f.(x \/ y) ] for all x,y ,

so for proving disjunctivity we only need to prove the converse

Also, given conjunctivity, the “ => “ direction of (*) reduces to f.false == false , for whatever that’s worth, and the “ <= “ direction can be written:

(**) (∀x :: (∃y : f.y : < x /\ y > => f.x)) .

——

+j

[Wolfram Kahl]

On Fri, Oct 17, 2025 at 10:20:39PM -0400, Jeremy Weissmann wrote:
> Given f is conjunctive, meaning:
>
> [ f.(x /\ y) == f.x /\ f.y ] for all x,y .
>
> Show that f is disjunctive if and only if:
>
> (*) (∀x :: f.x == (∀y : f.y : < x /\ y > )) ,
>
> where < > is the somewhere operator.

What is that ``somewhere operator'' and
how is it interacting with the variable bindings here?

The intention appears to be that `y` in the `< x /\ y >`
here refers to the `y` bound by `∀y`,
but that `x` does NOT refer to the `x` bound by `∀x`.
Is that the case?
If yes, then why would that operator behave differently for the two variables?
(If both `x` and `y` were encapsulated in `< x /\ y >`,
that would be trivially true.)


(By the way, the statement is not terribly interesting,
since there are only four candidates for `f`
(being a function from Booleans to Booleans),
and exactly those besides negation are conjunctive,
and exactly those besides negation are disjunctive.
)


Wolfram


P.S.:

> ——
>
> Some observations: f being conjunctive already gives us one direction of disjunctivity, namely monotonicity in the form:
>
> [ f.x \/ f.y => f.(x \/ y) ] for all x,y ,

Assuming that `[ ... ]` is ``the everywhere operator'',
isn't the explicit `for all x,y` rather superfluous?

> so for proving disjunctivity we only need to prove the converse
>
> Also, given conjunctivity, the “ => “ direction of (*) reduces to f.false == false , for whatever that’s worth, and the “ <= “ direction can be written:
>
> (**) (∀x :: (∃y : f.y : < x /\ y > => f.x)) .
>
> ——
>
> +j
>

> --
> 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 visit https://groups.google.com/d/msgid/calculational-mathematics/21401899-66FA-469B-85A5-B976D13A2EEB%40gmail.com.
>
>
> !DSPAM:68f2f98581681804284693!

[Jeremy Weissmann]

Variables  x  and  y  are of type  ’structure’ .   If you like, you could interpret structures as predicates on a  ‘universe’ ,  and the everywhere and somewhere operators —  [ ]  and  < > ,  respectively — denote universal and existential quantification over that universe.  ‘f’  is a predicate transformer, meaning a map from predicates to predicates, though in the original context I found this problem, it should be said that  f  was scalar valued, and I have no idea if that is relevant here.  I suspect it isn’t, however.

The axioms of  [ ]  are I believe encapsulated entirely in:  [ ]  is identity on scalars, that is:

   [ true ] == true   and   [ false ] == false

and  “universal conjunctivity” :  that is, for any bag  V  of predicates, we have:

  [ (Ax : x ∈ V : x) ]  ==  (Ax : x ∈ V : [x] )      .

(Universal conjuctivity gives us  [ true ] == true ,  so that is a bit redundant I suppose.)

The somewhere operator  < >  is defined by  < x > == ¬[¬x] ,  and its properties are dual:

   < true > == true  and  < false > == false

and  “universal disjunctivity” :  for any bag  V  of predicates:

   < (Ex : x ∈ V : x) >  ==  (Ex : x ∈ V : <x> )    .

* * *

   If you are thinking of  x  and  y  as sets (or their characteristic predicates), then  < x >  means  x ≠ ∅ ,  and  < x /\ y >  means that  x  and  y  have nonempty intersection.

+j

To view this discussion visit https://groups.google.com/d/msgid/calculational-mathematics/20251018181821.GR2550%40ritchie.cas.mcmaster.ca.

[Diethard Michaelis]

Hi Wolfram and Jeremy,

I felt Wolfram's questions need some more explatation ...

Jeremy uses the notational conventions 
from the Dijkstra/Scholten book "Predicate Calculus  and Program Semantics" 
or equivalently from EWD1300 " The notational conventions I adopted, and why" 
https://www.cs.utexas.edu/~EWD/ewd13xx/EWD1300.PDF>.

Wolfram seems to understand notation 
as e.g. used by Gries/Schneider in their "A Logical Approach to Discrete Math".

The most important notational difference is: 

Gries/Schneider convention names (sub-)expressions as in (∀x | R : T) 
and this way hides the dependency of R and T on dummy x.

Dijkstra/Scholten convention, however, names functions as in (∀x : r.x : t.x)

and never hides dependency on dummy x.

So for  Dijkstra/Scholten in stating that

(∀x : r.x : t.x \/ Q) ==  (∀x : r.x : t.x) \/ Q

there is no need to tell that Q does not depend on x.

Gries/Schneider must write for the same theorem

(∀x | R : T \/ Q) ==  (∀x | R : T) \/ Q , provided Q does not depend on x.

Consequently the "Dijkstra/Scholten" everywhere operator [] does not bind any visible dummy.

For me the most easy definition of [x] is (x = true) i.e. "x equals true" (*),

which works in every Boolean Algebra.

Equality of x and y then becomes  [x == y] as desired.

(It's a simple exercise to derive "my" [] definition from "Dijkstra/Scholten" book's definition.)

Equality of x and y then becomes  [x == y].

----

(*) unfortunately the  "Dijkstra/Scholten" book redefines = as "pointwise" equality ... 
(see the end of EWD1300 commenting on the resulting dilemma).

Hope this is helpful.

Diethard.

[Jeremy Weissmann]

Thanks for clarifying!

On Oct 23, 2025, at 07:09, Diethard Michaelis <diethard....@t-online.de> wrote:



To view this discussion visit https://groups.google.com/d/msgid/calculational-mathematics/eceb0af2-6ad3-446e-92dd-ecd230aa8eb2n%40googlegroups.com.