Would it be possible / necessary to prove that a math law can be applied to a given formula. Is intuitive recognition of structure similarity enough?

Question

I can apply associativity law to the following formula : [(a+b)+ c] +d

in the following way :

(1) [(a+b)+ c] +d

(2) = (a+b)+ (c +d)

(3) = a + [b+ (c+d)]

I do this so to say intuitively, recognizing intuitively the syntactic structure (A+B) + C in (1) and the structure A+(B+C) in (2).

I say intuitively, for the only reason I could give is that I see that the structure is the same.

In the same way, in logic, it seems there is some intuition involved in the fact of substituting

(A&~B)--> ~ ~ ~(A<-->(CvD)

for ~ [ (A&~B) & ~ ~ ~ ~(A<-->(CvD) ]

on the ground that : ~ [ (A&~B) & ~ ~ ~ ~(A<-->(CvD) ] has the form :

~ (X & ~Y)

and that ~ (X & ~Y) is equivalent to (X --> Y).

My question is : have mathematicians or logicians ever required this structure similarity to be proved ( not just seen) ? would it be possible to get rid of all intuition here?

Answer 1

Suppose you want to prove, say, $(a+b)+(c+d) = a+(b+(c+d))$ from the associativity law.

Recall that this law states : "for all $x,y,z$, $(x+y)+z= x+(y+z)$".

Then you just have to say : let $x=a, y=b, z=(c+d)$. Then $(a+b)+(c+d)=(x+y)+z$, by definition, and $a+(b+(c+d)) = x+(y+z)$, again by definition. The associativity law applied to these specific $x,y,z$ (recall that it holds for all $x,y,z$ !) yields the equality of the two terms : $(a+b)+(c+d) = a+(b+(c+d))$.

I did not have to "see intuitively" anything, I just applied a formal rule that I was allowed to apply because I assumed it.

Of course, all this is very straightforward and obvious, that's why people don't bother justifying it when they write mathematics; but for instance if you wanted a computer to check your proof you would have to tell it how you're using the associativity law (of course a lot of computer proof assistants have the ability built in to detect it from just saying "assoc." or something related, but what's happening is that they're saying "oh right, this works because I can just say $x=a, y=b$ and $z=(c+d)$")

Answer 2

Formally, when associativity holds in some structure closed under addition, we can simply rename $a+b$ to $x$, and then formally apply the associative law to get from (1) to (2). A similar method will get you from (2) to (3).

Answer 3

In everyday arithmetic you just know this.

In any context where that three term associative law holds you can prove by induction that it doesn't matter where you put the parentheses when adding $n$ terms.