equivalence of polynomial expressions I like to define a "polynomial expression" in the ring $A$ as any expression involving addition and multiplication of elements of $A$ together with one indeterminate $x$.
Such expression can be manipulated by substituting any operation involving only coefficients in $A$ with the result of such operation, by applying commutative, associative and distributive laws and by identifying $1\cdot x = x$, $0+x=x$ and $0\cdot x = 0$.
We say that two polynomial expressions are equivalent if one can be manipulated to become the other. It is clear that any polynomial expression can be reduced in canonical form: $a_0 + a_1 x + a_2 x^2 + \dots + a_n x^n$, where $x^k$ denotes repeated multiplication.
The question is: how to prove that if two polynomial expression are equivalent then they have the same canonical form?
For example: how to prove that $x\cdot x$ is non equivalent to $x$ as a polynomial expression in the ring $\mathbb Z_2$?
added I think that the example question can be solved by finding a $Z_2$-module where there exists an element $x$ such that $x\neq x^2$.
 A: Generally, when we are discussing "polynomial expressions" over $A$, we are talking about the ring $A[x]$. In this ring, $x$ and $x^2$ are never equal (unless of course $A$ is the zero ring). So even over $\mathbb{F}_2$, $x$ and $x^2$ are not equal.
To be formal, this is the free $A$-algebra on 1 element. It can be shown that this free algebra is given by the free $A$-module on the countably infinite set of "formal terms" $\{1, x, x^2, x^3, ...\}$.
There is, however, another way of approaching this. One may consider the set $S = \{f : A \to A : \exists P \in A[x] \forall a \in A (f(a) = P(a))\}$. In other words, one may consider the set of all functions which can be specified by a polynomial. In this instance, we would have $x = x^2$. This set also forms an $A$-algebra.
Edit: this part of the question goes in-depth into the construction of $A[x]$ as the free $A$-algebra on 1 element.
I'm going to go into more detail about the specifics of the construction of the $A[x]$ algebra. Convention: "ring" means commutative ring with unit. Let $A$ be an arbitrary ring.
Consider the set of "formal terms" $T = \\{x^i : i \in \mathbb{N}\\}$, defined in such a way that $x^i = x^j$ iff $i = j$. This is a "syntactic" definition, if you will. In fact, the proof can proceed just fine by letting $T = \mathbb{N}$ and letting $x^i$ be syntactic sugar for $i$.
Define $A[x]$ to be the free $A$-module over $T$, with universal function $u : T \to A[x]$. This means that for every $A$-module $M$ and every function $g : T \to M$, there exists a unique $A$-module morphism $h : A[x] \to M$ s.t. $g = h \circ u$. There are a number of well-known ways to construct free modules. Clearly (if not clear, then easy exercise), the free $A$-module over a set $S$ is unique up to unique $A$-module isomorphism.
Now, consider the module $M$ of all $A$-module morphisms from $A[x]$ to $A[x]$. We define a function $f : T \to M$ as follows. Suppose given $x^i \in T$. Define a function $f_i : T \to A[x]$ by $f(x^j) = x^{j + i}$. Then $f(x^i)$ is the unique $A$-module morphism $f(x^i) : A[x] \to A[x]$ s.t. $f(x_i) \circ u = f_i$. Clearly $f$ is a function $T \to M$. Then define $\mu$ to be the unique $A$-module map $\mu : A[x] \to M$ s.t. $\mu \circ u = f$. We write $a \cdot b$ for $\mu(a)(b)$.
I claim that $A[x]$, together with $0$ and $+$ inherited from its module structure and $\cdot$ as defined above, form a commutative ring with unit $1 = u(x^0)$. Clearly, $A[x]$ together with $0$ and $+$ form a commutative group since this is part of $A[x]$'s module structure. The axiom of left-distributivity follows from the fact that for all $a \in A[x]$, $g(a)$ is a module homomorphism. The axiom of right distributativity follows from the fact that $g$ itself is a module homomorphism. The more challenging ones are commutativity and associativity. I'll prove a useful lemma.
Consider an arbitrary set $S$, and let $W$ be the free $A$-module on $S$ with $z : S \to W$ the universal morphism. Let $X$ be an arbitrary $A$-module. Define a sequence of $A$-modules by $M_0 = X$, $M_{i + 1} = \\{f : W \to M_i,$ $f$ an $A$ module morphism$\\}$. Informally, $M_i$ is the module of all functions $W^i \to X$ which are linear in each argument independently, all others fixed. I claim that for every $i \in \mathbb{N}$, for all $f, g \in M_i$, we have $f = g$ iff for every $s_1, ..., s_i \in S$, $f(z(s_i))(z(s_{i - 1})) ...(z(s_1)) = g(z(s_i))(z(s_{i - 1})) ... (z(s_1))$. We prove this by induction on $i$.
Base case: $i = 0$. Trivial.
Inductive step: suppose the proposition holds for $i$, and take $f, g \in M_{i + 1}$ s.t. for all $s_1, ..., s_{i + 1} \in S$, we have $f(z(s_{i + 1}))(z(s_{i})) ...(z(s_1)) = g(z(s_{i + 1}))(z(s_{i})) ... (z(s_1))$. Then in for every $x \in S$ and for every $s_1, ..., s_i \in S$, we have $f(z(x))(z(s_i)) ... (z(s_1)) = g(z(x))(z(s_i)) ... (z(s_1))$. Then by the inductive hypothesis, for every $x \in S$, $f(z(x)) = g(z(x))$. That is, $f \circ z = g \circ z$. Then $f = g$. The other direction of the iff is trivial.
In our particular case, we will let $S = T$, $W, X = A[x]$, and $z = u$.
To prove associativity of $\cdot$, it suffices to consider $f, g \in M_3$ defined by $f(x)(y)(z) = (x \cdot y) \cdot z$ and $g(x)(y)(z) = x \cdot (y \cdot z)$ and show that $f = g$. To do this, it suffices to check that $f(x^i)(x^j)(x^k) = g(x^i)(x^j)(x^k)$. This is immediate from the definitions of $f$, $g$, and $\cdot$.
Commutativity is similar (although it relies on the fact that $A$ is a commutative ring). Checking that $1$ is an identity is also similar.
Finally, we define the $A$-algebra structure on $A[x]$ by the ring homomorphism $a \mapsto a1$, where the multiplication is defined by the $A$-module structure on $A[x]$. We also abuse notation by writing $x^i \in A[x]$ instead of the technically more correct $u(x^i)$.
We now demonstrate that $A[x]$ satisfies the following property: for every $A$-algebra $f: A \to B$ and every $b \in B$, there exists a unique $A$-algebra morphism $g : A[x] \to B$ s.t. $f(x) = b$.
Indeed, suppose there is some $A$-algebra morphism $g : A[x] \to B$ s.t. $f(x) = b$. Then $f$ is also an $A$-module morphism. Thus, it suffices to determine what $f(x^i)$ would be for each $i$. But clearly, we have $f(x^i) = f(\prod\limits_{j = 1}^i x) = \prod\limits_{j = 1}^i f(x) = f(x)^i = b^i$. So $f$ would have to be the unique module homomorphism defined by $f(x^i) = b^i$. It is also immediate to show that this module homomorphism is in fact an $A$-algebra homomorphism.
Now, at long last, we may answer OP's original question. We first note that every element of $A[x]$ can be written as $\sum\limits_{i = 0}^\infty a_i x^i$ where each $a_i \in A$ and there exists $N$ s.t. for all $i \geq N$, $a_i = 0$. This can be demonstrated by noting that the set of all $P \in A[x]$ which can be written as $\sum\limits_{i = 0}^\infty a_i x^i$ as above is a sub $A$-module of $A[x]$ which contains all $x^i$; thus, it can be shown by $A[x]$'s properties as a free $A$-module that $A[x]$ equals this submodule.
OP's question amounts to the following: does every element of $A[x]$ have a unique expression $\sum\limits_{i = 0}^\infty a_i x^i$? The answer turns out to be "yes". For consider the $A$-module map $f_i : A[x] \to A$ defined by $f_i(x^j) = 0$ if $i \neq j$ and $1$ if $i = j$. Then we see that $f_i(\sum\limits_{j = 0}^\infty a_j x^j) = a_i$. This means that if we have $\sum\limits_{j = 0}^\infty a_j x^j = \sum\limits_{j = 0}^\infty b_j x^j$, then we have, for every $i$, $a_i = f_i(\sum\limits_{j = 0}^\infty a_j x^j) = f_i(\sum\limits_{j = 0}^\infty b_j x^j) = b_i$.
This demonstrates, for example, that in $\mathbb{Z}_2[x]$, $x \neq x^2$. In fact, the statement $x \neq x^2$ holds in every ring except the zero ring.
Note which doesn't answer OP's question but is very interesting:
How can we define polynomials over an arbitrary set of variables $V$? Simple: we define $T$ to be the free commutative monoid over $V$. We then define the $\cdot$ operation by $u(a) \cdot u(b) = u(ab)$ (where $a$ and $b$ are concatenated using the monoid operation).
A: As a very partial answer, it seems to me that the problem can be reformulated as

If a canonical form is equivalent to zero, it is identically zero

As a first point, it seems easy to prove that if two expressions are equivalent, their formal derivatives are equivalent because of the algebraic rules on the derivatives. As a consequence, if $a_0 + \cdots + a_n x^n$ is equivalent to zero, then $k! a_k = 0$.
This answers the special case of $x+x^2$ not being equivalent to zero in ${\mathbb Z}_2$, but a lot remains to do...
Edit: to address your objection about formal derivation one could define the formal derivation of an expression by the following rules

*

*If the expression is a sum, its derivative is the sum of the derivatives of the terms of the sum

*If the expression is a product, its derivative is the sum of the products obtained by derivating a single factor

*The derivative of $x$ is $1$ and that of a scalar is $0$.

Having defined this, the main usable rule in equivalences is distributivity, that is to say
\begin{equation}
A(B+C) \sim AB + AC
\end{equation}
It is easy to check that the derivatives are equivalent
\begin{equation}
A'(B+C) + A(B'+C') \sim A'B+AB' + A'C+AC'
\end{equation}
