Associative and commutative laws seem to permeate many areas. Hence, a general treatment may be of some use. In order to motivate the theory (which is necessary to even state the question), consider the following statement of a basic associative law:
$$[(a*b)*c] \cong [ a*(b*c)]$$
The specific nature of objects is irrelevant. In order to state the above, one only needs that there is a binary operation $*$ (Binary in the sense it operates on two inputs, however it could be partial binary operation as well) and there is a notion of sameness. Further, one may see that associativity only makes sense if the expression's constituents are the same and in the same order. So in the following, we aim to make these notions explicit.
Primitives
Countable (Possibly infinite) collection of atomic expressions(atoms): $a_1, a_2, ...$
Notion of sameness, an equivalence relation $\cong$
Notion of binary compatibility (a binary predicate) $\psi$
Postulates
P1: Let $e_1, e_2$ be expressions such that $\psi(e_1,e_2)$. Then $(e_1e_2)$ is also an expression. (Expression Construction Mechanism)
P2: Let $(e_1e_2)$ and $(e_3e_4)$ be expressions. If $e_1 \cong e_3$ and $e_2 \cong e_4$, then $(e_1e_2) \cong (e_3e_4)$. (Substitution)
P3: Let $e_1, e_2, e_3$ be expressions. If $\psi(e_1, e_2) \wedge \psi(e_2, e_3)$, then $\psi(e_1, (e_2e_3)) \wedge \psi((e_1e_2),e_3)$. (Conservation of compatibility or two end postulate).
P4: Let $p$ be a predicate defined on expressions. If $p$ holds for all atomic expressions and $p(e_1) \wedge p(e_2) \Rightarrow p((e_1e_2))$ whenever $\psi(e_1, e_2)$, then $p$ holds for all expressions. (Induction Postulate)
P5: Let $e_1$ and $e_2$ be expressions such that $\psi(e_1,e_2)$. It is postulated that for any expression $e_3$ such that $e_2 \cong e_3$, $\psi(e_1, e_3)$ and for any expression $e_4$ such that $e_1 \cong e_4$, $\psi(e_4,e_2)$. (Compatibility respects sameness)
P6: Let $e_1, e_2, e_3$ be expressions such that $\psi(e_1, e_2)$ and $\psi(e_2, e_3)$. It is postulated that $(e_1(e_2e_3)) \cong ((e_1e_2)e_3)$. (Associativity Axiom).
Definitions
D0: Degree of Expression is defined as following - if an expression e is atom, then $D(e) = 0$. Suppose $e_1$ and $e_2$ are expressions of degree $D(e_1)$ and $D(e_2)$ respectively. If $\psi(e_1, e_2)$, then $D((e_1e_2)) = max(D(e_1), D(e_2)) + 1$. By induction, one can show that this defines a degree for each expression.
D1: Atomic sequence of a given expression: For all atomic expressions e, $A(e) = e$ and $len(A(e)) = 1$. Let $e_1$ and $e_2$ be expressions such that $A(e_1)$ and $A(e_2)$ are their respective atomic sequences with lengths $len(A(e_1))$ and $len(A(e_2))$ respectively. If $\psi(e_1,e_2)$, then $A((e_1e_2)) = A(e_1)A(e_2)$ and $len(A((e_1e_2))) = A(e_1) + A(e_2)$. Using expression equality on atomic terms, one is able to define equality on atomic sequences.
D2: Atomically equivalent expressions: Let $e_1, e_2$ be expressions. $e_1$ is said to be atomically equivalent if and only if $A(e_1) = A(e_2)$.
Formulation of General Associativity
Now we can formulate the general associativity as following: Let $e_1$ and $e_2$ be expressions. If $e_1$ is atomically equivalent to $e_2$, then $e_1 \cong e_2$.
Proof Ideas 0
Consider the following atomically equivalent expressions: $e_1 = [((a_1a_2)(a_3a_4))((a_5a_6)(a_7a_8))], e_2 = [a_1(a_2(a_3(a_4(a_5(a_6(a_7a_8))))))]$. In line with our conventional way of proving, we start with $e_1$ and transform it using the basic associativity as follows:
Note that the expression $(a_7a_8)$ occurs in both $e_1$ and $e_2$. So, we can treat it as if it is also atomic.
$$t_1: [((a_1a_2)(a_3a_4))((a_5a_6)(a_7a_8))] \rightarrow [((a_1a_2)(a_3a_4))((a_5(a_6(a_7a_8))))]$$
It is valid transformation for a) from $e_2$ it follows that $\psi(a_6,(a_7a_8))$ and from conservation of compatibility it follows $\psi(a_5,(a_6(a_7a_8)))$; b) From P5 it follows that that $\psi(((a_1a_2)(a_3a_4)), ((a_5(a_6(a_7a_8))))$ as $((a_5a_6)(a_7a_8)) \cong (a_5(a_6(a_7a_8)))$. Similar ideas apply in the following transformations.
$$t_2: [((a_1a_2)(a_3a_4))((a_5(a_6(a_7a_8))))] \rightarrow [(a_1a_2)((a_3a_4)((a_5(a_6(a_7a_8)))))]$$
$$t_3: [(a_1a_2)((a_3a_4)((a_5(a_6(a_7a_8)))))] \rightarrow [(a_1a_2)(a_3(a_4(a_5(a_6(a_7a_8)))))]$$
$$t_5: [(a_1a_2)(a_3(a_4(a_5(a_6(a_7a_8)))))] \rightarrow [a_1(a_2(a_3(a_4(a_5(a_6(a_7a_8))))))]$$
Questions
Note that left-handed expressions such as $(((((((a_1a_2)a_3)a_4)a_5)a_6)a_7)a_8)$ don't always exist. Hence some new ideas are required. Now the goal in which I've been struggling is the following: To distill some general elements from the above transformations which can possibly form the basis of a proof. One idea is that one should start from inside out i.e. one should start by building 1st degree expressions in the target and then second and so on.For example, I started by building the expression $(a_6(a_7a_8))$. But I don't know how to say all of this in a way which can form the basis of a proof.
Secondly, I wonder if there is a better, more natural way to phrase general associativity in general. It will great if somebody can help me.
Thirdly, perhaps most importanly, how can such a general theory apply in specific contexts, for example to show that basic associativity law for morphisms in a category implies the general associativity?
P.S.
- I am not sure if I've tagged this question correctly. I am sorry. Please feel free to suggest appropriate tags.