Dummit and Foote gives the following definition for a free module:
"An $R$-module $F$ is said to be free on the subset $A$ of $F$ if for every nonzero element $x$ of $F$, there exist unique nonzero elements $r_1,r_2,\ldots,r_n$ or $R$ and unique $a_1,a_2,\ldots,a_n$ in $A$ such that $x = r_1a_1 + r_2a_2 + \cdots + r_na_n$, for some $n \in \mathbb{Z}^+$. In this situation we say $A$ is a basis or set of free generators for $F$. If $R$ is a commutative ring the cardinality of $A$ is called the rank of $F$."
This definition seems to imply that the rank of a free module on a commutative ring is unique, but I can't figure out why this must be the case.
Step 1: demonstrate that dimension is unique for vector spaces.
Step 2: consider a ring $R$, and take some maximal ideal $M$. Let $k = R / M$ be the residue field. (Note that this proof doesn’t work for the zero ring - why?).
Suppose we have some isomorphism $R^{\oplus S} \cong R^{\oplus J}$. Consider the extension of scalar functor $F : R-mod \to k-vec$, which is the left adjoint of the restriction of scalars functor $k-vec \to R-mod$. The functor $F$ can be explicitly described as $M \mapsto M \otimes_R k$. Now $F$ takes $R^{\oplus W}$ to $k^{\oplus W}$ for any set $W$, so the functor gives us an isomorphism $k^{\oplus S} \cong k^{\oplus J}$. Thus, we have $|S| = |J|$, since the dimension of a vector space is unique. $\square$
Note that the above proof requires choice. I do not know if a proof without choice is possible, and I do not know whether we can prove this theorem (or some special cases) constructively. It is an interesting exercise.
Edit: for finite ranks, this is provable without choice. We can express “$R^n$ is not isomorphic to $R^m$” as a statement $phi(n, m)$ in the first-order theory of rings. We would like to show that for all $n, m$, we can prove $\phi(n, m)$ from the ring axioms. This can be phrased as a statement $\Phi$ in first-order arithmetic.
Now assuming choice, we know that each $\phi(n, m)$ is true. Thus, completeness shows each $\phi(n, m)$ is provable. So $\Phi$, a statement in first-order arithmetic, follows.
But any first-order arithmetic statement that can be proved with choice can be proved without it by relativising to $L$. So $\Phi$ can be proved without choice.
Then each $\phi(n, m)$ is indeed provable in the theory of rings, and therefore true.
The hard part, of course, is trying to do things for infinite bases or completely constructively.