Tuesday, February 11, 2020

Larry Wos's Recent Newsletter

In the most recent newsletter of the Association for Automated Reasoning, Dr. Larry Wos presents us with a collection of axioms, with labels for them.
" f(e,x) = x. % left identity
 f(x,e) = x. % right identity
 f(g(x),x) = e. % left inverse
 f(x,g(x)) = e. % right inverse
 f(f(x,y),z) = f(x,f(y,z)). % associativity
 h(x,y) = f(x,f(y,f(g(x),g(y)))). % definition of commutator"

I'll call the relevant set of axioms G.

Then he presents three properties:

"h(h(x,y),z = h(x,h(y,z)), commutator is associative, property 1
f(h(x,y),z) = f(z,h(x,y)), commutator has the property of nilpotent class 2, 
property 3
f(h(x,z),h(y,z)) = h(f(x,y),z), commutator distributes over product, property 2"

He then asks us prove that property 1 follows from property 2, property 1 from 3,
2 from 1, 2 from 3, 3 from 1, and 3 from 2.

And then a careful reader is either confused or laughing, 
since if your only axiom has only one function like 'h', 
it's impossible to correctly get to a property with a function like 'f' 
(or I don't understand the term 'property' correctly). 

What I suspect Dr. Wos means to ask is about relationships between theories.

The theories are G supplemented with property 1 (G1), 
G supplemented with property 2 (G2), and G supplemented with property 3 (G3).

Thus, more precisely, Dr. Wos's first challenge is to prove that G2 follows from G3,
G2 from G1, G1 from G3, G1 from G2, G3 from G2, and G3 from G1.

Edit: That's not the intended challenge either.

Property 1 should be h(h(x,y),z) = h(x,h(y,z)). or h(h(x,y),z) = h(x,h(y,z)), .  
Also, the termination symbol for the supplementary axioms need to match those in G 
(the commas need to get replaced by periods 
or the periods have to get replaced by commas).

If anything is incorrect in the above, hopefully it gets corrected.
    

No comments:

Post a Comment