Whole is greater than the sum of its parts

Stream: Equational

[Hernan Ibarra]

Terence Tao said:

• Explore triple relations of the form "Equation X and Equation Y implies Equation Z". This was for instance proposed by Pace Nielsen in this blog comment, and I think elsewhere as well. This will be harder for several reasons, most notably because 3-SAT is way harder than 2-SAT, but the relations we obtain in this project will help reduce the problem significantly. As Pace suggests, we may have to cut down to just three operations instead of four to obtain a feasible project.

Are there any equations X, Y, Z such that X does not imply Z, and Y does not imply Z, but 'X and Y' implies Z? I fully expect the answer to be yes, so what I'm really asking is for examples to play with (maybe from the subgraph equations).

[Daniel Weber]

x * y = y * x and x * (y * z) = (x * y) * z imply x * (y * z) = (y * x) * z, but neither of them implies it by itself

[Edward van de Meent]

i was about to say, the combination of commutativity with associativity is definitely stronger than their parts...

[Edward van de Meent]

but you beat me to the punch :upside_down:

[Hernan Ibarra]

Thanks to both. I wonder how we can classify the pairs of equations (X,Y) so that this happens (I think the technical term is that they produce a generative effect). If there is no generative effect then we can determine implications in and out of 'X and Y' from the knowledge of the implications of X and Y. Hence more examples would be helpful.

[Daniel Weber]

I'd expect most pairs of nontrivial equations create new implications together

[Hernan Ibarra]

More explanation: let L be the meet-semilattice obtained from the poset of implicaitons by adding 'and'. Apply the Yoneda Lemma to get a contravariant embedding functor Y: L -> P(L), where Y(A) = set of consequences of A. If the Yoneda embedding is continuous (i.e. it preserves limits, i.e. it preserves meets), then Y('A and B') = Y(A) \cup Y(B) (as the functor is contravariant, limits get sent to colimits) and thus we can determine 'A and B' from A and B. Thus the problem only arises when continuity fails, i.e., when there are equations (doesn't have to be two equations but for the sake of simplicity:) A and B such that Y(A) \cup Y(B) != Y('A and B'), and this is what I call a 'generative effect'. Note that it is always the case that Y(A)\cup Y(B) \subseteq Y('A and B').

[Hernan Ibarra]

Maybe I should be asking the opposite question: what are some non-trivial examples of equations A and B such that the set of consequences of 'A and B' is equal to the union of the set of consequences of A and the set of consequences of B.

[Edward van de Meent]

by non-trivial, i expect you mean that A and B both aren't equivalent to x=y, x=x, or eachother?

[Daniel Weber]

I think it just means that neither implies the other

[Edward van de Meent]

ah right

[Hernan Ibarra]

I left 'non-trivial' up to interpretation :)

[Edward van de Meent]

i think this isn't possible? suppose A and B are such, i.e. (A ^ B) -> X implies A -> X or B -> X. using X := (A ^ B) would result in either A -> (A ^ B) or B -> (A ^ B), meaning A -> B or B -> A?

[Daniel Weber]

Doesn't X have to be a single formula?

[Edward van de Meent]

oops, that's fair :upside_down:

[Daniel Weber]

What about (x * x) * (y * z) = (x * x) * (z * y) and (y * z) * (x * x) = (z * y) * (x * x)?

[Daniel Weber]

Ah, no, ((x * x) * (y * z)) * ((y * z) * (x * x)) = ((x * x) * (z * y)) * ((z * y) * (x * x))

[Edward van de Meent]

i imagine it would be easier to prove this isn't a consequence of the parts if you use different variables for the left and right parts? unless you have a clear idea for counterexamples?

[Daniel Weber]

It probably would, yes

[Daniel Weber]

Vampire can construct a counterexample, though

[Edward van de Meent]

not everyone reading this has the knowledge of how to work those programs, though :upside_down:

[Daniel Weber]

I also didn't until yesterday :smile: