JAW114 - Three proofs of multiplication over gcd

[Jeremy Weissmann]

Hello all,

This one’s been rattling around in my head since 2008. I think it brings together a lot of lovely bits of elementary mathematics.

Feedback is warmly encouraged.

Best,

+j

[alexk]

    Hi.
 
    I was not able to find it in the text (probably i will after a closer reading
as it is usually the case) but one line of thought seems to be missing from the
"lattice" section.
   
    First thing that comes to my mind is a statement from WF's tutorial
on lattices that functions, monotonic with respect to the order on the lattice
(in our case "divides"), distribute over meet and join (in our case "gcd" and "lcm").
The example was that addition distribute over "maximum" because it is monotonic with
respect to "greater or equal".

So basically monotonicity of multiplication:
    for all x, y, z : x divides y  =>  z * x divides z * y   (zero included)
is a sufficient condition.

    In context of predicate calculus a function (to be universally disjunctive and
universally conjunctive) supposed to be monotonic and _punctual_, but if we assume
natural numbers to be "scalars", then multiplication is in fact punctual.
   

суббота, 2 марта 2024 г. в 16:52:26 UTC+3, Jeremy Weissmann:

[Jeremy Weissmann]

Are you sure you have this right? Junctivity implies monotonicity but for the converse I believe we would need the order to be total. 

On Mar 3, 2024, at 22:37, alexk <krae...@gmail.com> wrote:

    Hi.

--
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/4f91f4e7-7c10-458a-ad81-9d41f4e03733n%40googlegroups.com.

[alexk]

No, i am not... in fact i have checked and it is only for total order. Sorry :(

понедельник, 4 марта 2024 г. в 07:13:28 UTC+3, Jeremy Weissmann:

[Diethard Michaelis]

Hi Jeremy,

had an extremely short look into the JAW114 paper.
My eye got stuck on p.7, proof of Lemma:

[...]
<E q :: [#x + #q = #y] >
= ??? { quantifier exchange } ???
[ <E q :: #x + #q = #y> ]
[...]

Universal and existential quantifiers usually do not commute.
So what is this "quantifier exchange"?

Cheers, Diethard.

[Jeremy Weissmann]

Wow! I’ll have to take a look at that nonsense! I wrote that part some five years ago and I never bothered to check it.

Thank you for catching that horrendous error!

> On Mar 4, 2024, at 03:34, Diethard Michaelis <diethard....@t-online.de> wrote:
>
> Hi Jeremy,

[Jeremy Weissmann]

On a bit of reflection it seems like

> <E q :: [#x + #q = #y] >

is all I need: it is equivalent to [ #x ≤ #y ] . Let me think more.

Thanks again for catching this.

[Jeremy Weissmann]

On a bit more reflection, I see conceptually that there is indeed a quantifier exchange rule:

Ex Ay

where x,y are structures, should be equivalent to

Ay Ec

where c is scalar. I believe this is a sort of Skolemization, although my logic is a bit far in the past to help me.

Let me ponder more and see if I can’t find a nice way to capture/prove this calculationally.

> On Mar 4, 2024, at 08:05, Jeremy Weissmann <plusj...@gmail.com> wrote:
>
> On a bit of reflection it seems like

[alexk]

Actually it isn't (only for total order).

There are 2 versions of the junctivity theorem , scalar and lifted.

Scalar (requires total order):

(0) [ x =< y ] or [ y =< x ]        --  =< - is a total order

(1) [ x =< y ] => [ f.x =< f.y ]   -- f is monotonic with respect to =<

Lifted (requires weaker form of order):

(2) [ (x =< y) or (y =< x) ]       --  =< - is 'punctually' total order

(3) [ (x =< y) =>  (f.x =< f.y) ] -- f is punctual and monotonic with respect to =<

For example (0) and (1) holds for boolean with implication or natural numbers

with "greater or equal"

(2) and (3) holds for predicates and bags

понедельник, 4 марта 2024 г. в 07:40:10 UTC+3, alexk:

[Jeremy Weissmann]

Haven’t gotten anywhere significant yet.

Let

x: structure of some type
c: scalar of that type
U: predicate on that type

then we want:

(Ex :: [U.x]) == [ (Ec :: U.c) ] .

Is this perhaps the definition of scalarity?

In the Boolean domain we have [ x == [x] ] as a definition of scalarity but this doesn’t work in other domains.

> On Mar 4, 2024, at 08:30, Jeremy Weissmann <plusj...@gmail.com> wrote:
>
> On a bit more reflection, I see conceptually that there is indeed a quantifier exchange rule:

[alexk]

Can we introduce existential quantifier constructively? After all we know, what "q" is.

    [ #x ≤ #y ]
=>   { (#y - #x) is non negative }
    [ #x + (#y - #x) = #y ]
=    { # over - }
    [ #x + #(y / x) = #y ]    
=>   { instantiate y / x with q }
    (E q :: [ #x + #q = #y ])
=
    same as before

понедельник, 4 марта 2024 г. в 20:23:57 UTC+3, Jeremy Weissmann:

[Jeremy Weissmann]

I suppose the definition of “c scalar” should be, for all x:

[ x = c == [x = c] ] .

I still haven’t managed to prove:

(*) (Ex :: [U.x]) == [ (Ec :: U.c) ]

The direction “<=“ follows from predicate calculus, but the direction “=>” I haven’t been able to prove without referring to the underlying state space.

I would be quite pleased if someone could come up with a point-free proof of the forward direction! Perhaps another axiom is needed.

> On Mar 4, 2024, at 12:23, Jeremy Weissmann <plusj...@gmail.com> wrote:
>
> Haven’t gotten anywhere significant yet.

[alexk]

I am not sure that [ x = c == [x = c] ] is definition of a scalar. For example "true" is a scalar. For "c = true" 

  [ x = c == [x = c] ]

=

  [ x = true == [x = true] ]

=

 [ x == [x] ]

which is not the case for all x.

About  (Ex :: [U.x]) == [ (Ec :: U.c) ]

Can you elaborate the properties of U ? For example if "c" is a scalar, is "U.c" scalar as well?

вторник, 5 марта 2024 г. в 19:35:06 UTC+3, Jeremy Weissmann:

[Jeremy Weissmann]

As to the first part, you are right.

As to the second part, which also relates to the first part, I think scalarity as a concept needs to be pinned down more. My own understanding of it is flimsy at best!

But absolutely, a function of scalars should be scalar as well. 

On Mar 5, 2024, at 12:44, alexk <krae...@gmail.com> 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/fa384bfe-8529-489a-9ba2-2b87ddd8bd4cn%40googlegroups.com.

[alexk]

i found similar definition from Lex Bijlsma's AB36

x is a scalar iff (∀c :: [x = c ≡ [x = c]])

but it define scalarbility of x in term of that of c's.

вторник, 5 марта 2024 г. в 21:33:00 UTC+3, Jeremy Weissmann:

[alexk]

The other thing that is bothering me, that in context of prime factorization we have the only scalar, namely 1 (one).

We can define scalar in terms of # operator:

n is a scalar == (E c:: (A p:: #n.p = c))

but the only possible choice for 'c' is zero or 'n' will be infinite.

So i don't see what use the only scalar have there. 

вторник, 5 марта 2024 г. в 21:35:57 UTC+3, alexk:

[Jeremy Weissmann]

This is not a problem, many natural structures don’t correspond to characteristics of natural numbers. Structures here are functions from the primes to natural numbers, and scalars are constant functions. 

On Mar 5, 2024, at 13:43, alexk <krae...@gmail.com> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/a31d6951-4a7c-485f-853e-cdcb9b769703n%40googlegroups.com.

[alexk]

Do i understand correctly, you a trying to replace:
⟨ ∃q :: [ #x + #q = #y ] ⟩
≡
[ ⟨ ∃q :: #x + #q = #y ⟩ ]
≡

[ #x ≤ #y ]

with

⟨ ∃q :: [ #x + #q = #y ] ⟩
≡
[ ⟨ ∃c :: #x + #c = #y ⟩ ]
≡

[ #x ≤ #y ]

where #c is some scalar?

if in fact there is only one (#1) scalar, it won't work, it will imply [#x = #y]

вторник, 5 марта 2024 г. в 23:16:25 UTC+3, Jeremy Weissmann:

[Jeremy Weissmann]



Hm well actually I was proposing to replace the structure #q with the scalar c. 

But either way there is not just one scalar. There are many scalar functions from primes to natural numbers — one for each natural number. 

On Mar 5, 2024, at 15:30, alexk <krae...@gmail.com> wrote:

Do i understand correctly, you a trying to replace:

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/76b5c018-bb50-47e1-81a8-5d2e7d12ab9an%40googlegroups.com.

[alexk]

or it should be

⟨ ∃q :: [ #x + #q = #y ] ⟩
≡

[ ⟨ ∃c :: #x + c = #y ⟩ ]      (i replaced "#c" with "c", where "c" is just a number that we add to the value of the function at any point)
≡

[ #x ≤ #y ]

?

it looks somewhat correct. Here we lost one "#" while exchanging quantifiers.

вторник, 5 марта 2024 г. в 23:30:16 UTC+3, alexk:

[Jeremy Weissmann]

The problem is that the original quantification over q is not over structures. The dummy is of type natural; #q is the structure. But it could have been a quantification over structures s where s = #q for some q. The plot thickens.

Amazing what we’ve uncovered in this one step that is completely irrelevant to the point of the paper. Nevertheless, this must be addressed (or sidestepped). 

On Mar 5, 2024, at 15:41, alexk <krae...@gmail.com> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/3cd3a240-acd1-4067-94e4-1f4c60984eabn%40googlegroups.com.

[alexk]

sorry, another clarification.

[QUOTE]:

(*) (Ex :: [U.x]) == [ (Ec :: U.c) ]

The direction “<=“ follows from predicate calculus, but the direction “=>” I haven’t been able to prove without referring to the underlying state space.

[END OF QUOTE]

are arrows in the correct direction? for me it is the opposite:

     (Ex :: [U.x])

=> {EA => AE)

    [(Ex :: U.x)]

= {for punctual U [(Ex :: U.x) == (Ec :: U.c)]}

    [(Ec :: U.c)]

вторник, 5 марта 2024 г. в 23:51:52 UTC+3, Jeremy Weissmann:

[alexk]

disregard previous message please...

среда, 6 марта 2024 г. в 00:02:45 UTC+3, alexk:

[Jeremy Weissmann]

I’ve said perhaps 10 wrong things for every right thing so I’ll stop now. Perhaps someone who has been more thoughtful about this can help sort it out. 

On Mar 5, 2024, at 16:04, alexk <krae...@gmail.com> wrote:

disregard previous message please...

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/8e22a9a5-0ec6-4d5c-a18a-2013c9259a69n%40googlegroups.com.

[alexk]

    I feel the same, regretted the absence of the "delete message" button couple of times.

    But over all the article and the discussion were quite interesting and i got a lot insights from it.
   
    Few final remarks:

(0)  [ (Ec :: U.c) ] => (Ex :: [U.x])

    It can't be proved in general, because it amounts to the Axiom of Choice. Operationally speaking, from assumption that for each, implicit, point 'p' we have a scalar (or several of them) 'c', satisfying U.c we conclude the existence of function 'x' that for each 'p'  "chooses" one of the appropriate  scalars.

   
(1)  (Ex :: [U.x]) => [ (Ec :: U.c) ]

     My prove from above seems to be correct after all.
     It uses the theorem

     
     for punctual U: [(Ex :: U.x) == (Ec :: U.c)]
     

     which is dual to the theorem (7) from EWD1184-3.

    Initially i just assumed it to be true, but wasn't able to prove it right away and panicked. My problem was that the prove requires a different (from original) version of Leibniz rule:
    [ (x = c) ^ f.x == (x = c) ^ f.c ]
    instead of
    [ (x = c) => f.x == (x = c) => f.c ]
   
(2) Appealing to monotonicity

    Argument

      multiplication is monotonic with respect to 'divides'
      =>

      multiplication distribute over 'gcd'

    is appealing, because it can be easily reused, for example exponentiation as also monotonic.
    The objection is that 'divides' is not a total order.

    But, assuming prime factorization, it is as total as '=<':

    (Ap :: p ** x divides p ** y  ==  x =< y )

    where ** is exponentiation ( 2 ** 3 = 8 )

    To exploit this local, or punctual, totality, the monotonic functions have to distribute over factorization, i.e. be punctual.

    Luckily they do:

    (Px:: f.x) * (Px:: g.x) = (P.x:: f.x * g.x)

    (Px:: f.x) ** y = (P.x:: f.x ** y)

    where (P::) is a "product" quantifier.
   
    And that is about it.    
       
   
   

среда, 6 марта 2024 г. в 00:53:49 UTC+3, Jeremy Weissmann:

[Jeremy Weissmann]

Hm okay I will have to go through the details of punctual linearity implies (monotonic iff junctive). 

Nevertheless I do find my proof using the prime factorization approach more “lo-tech”. But it relies on + over max, which as you point out follows from the same general theorem above!

On Mar 6, 2024, at 10:49, alexk <krae...@gmail.com> wrote:

    I feel the same, regretted the absence of the "delete message" button couple of times.

To view this discussion on the web visit https://groups.google.com/d/msgid/calculational-mathematics/45b9fdde-c5a9-40a4-bdd6-83633b20c2b6n%40googlegroups.com.

[alexk]

Well, I was only able to formulate "Appealing to monotonicity" due to "lo-tech" nature of the prime factorization approach.

I was struggling with logarithmic nature of # operator:

     #(x * y) = #x + #y    

     log.p.(x * y) = log.p.x  +  log.p.y

 and decided to exponentiate it. So i came up with & operator:

    &n.p = p ** #n.p

    #n.p = log.p.&n

It have few nice properties, for example there is no need to define bag and distribution over bag and product quantifier can be used instead:

    n = (Px:: &n.x)

But important thing is that now, having two operators side by side, it became clear how prime factorization induce totality on 'divides' relation:

   (Ap:: &n.p divides &m.p  ==  #n.p =< #m.p)  

and i managed to buff the general theorem from above by introducing "punctually total order" concept.

четверг, 7 марта 2024 г. в 07:23:20 UTC+3, Jeremy Weissmann: