If a theory of everything exists, is it necessarily unique?

I will expand my comment above into an answer:

If you search for a TOE that is a mathematical theory, it has to be at least a logic theory, i.e. you need to define the symbols and statements, and the inference rules to write new (true) sentences from the axioms. Obviously you would need to add mathematical structures by means of additional axioms, symbols, etc. to obtain a sufficient predictive power to answer physically relevant questions.

Then, given two theories, you have the following logical definition of equivalence: let $A$ and $B$ be two theories. Then $A$ is equivalent to $B$ if: for every statement $a$ of both $A$ and $B$, $a$ is provable in $A$ $\Leftrightarrow$ $a$ is provable in $B$.

Obviously you may be able to write statements in $A$ that are not in $B$ or vice-versa, if the objects and symbols of $A$ and $B$ are not the same. But let's suppose (for simplicity) that the symbols of $A$ and $B$ coincide, as the rules of inference, and they only differ for the objects (in the sense that $A$ may contain more objects than $B$ or vice versa) and axioms.

In this context, ZFC and Bernays-Godel set theories are equivalent, when considering statements about sets, even if the axioms are different and the Bernays-Godel theory defines classes as mathematical objects, while ZFC does not.

Let's start to talk about physics, and TOE, following the discussion in the comments. It has been said that two TOEs must differ only in non-physical statements, since they have to be TOEs after all, and thus explain every physical observation in the same way. I agree, and from now on let's consider only theories in which the physical statements are true.

Let $A$ be a TOE. Let $a$ be an axiom that is independent of the axioms of $A$ (that means, roughly speaking, that there are statements undecidable in $A$, that are decidable in $A+a$, but all statements true in $A$ are still true in $A+a$). First of all, such an $a$ exists by Godel's theorem, as there is always an undecidable statement, given a logical theory. Also, $a$ is unphysical, since $A$ is a TOE. Finally, $A$ and $A+a$ are inequivalent (in the sense above), and are TOEs.

One example is, in my opinion, the generalized continuum hypothesis (GCH): without entering into details, it has been shown with the theory of forcing that it is independent of the axioms of ZFC set theory. Thus $ZFC$, $ZFC+GCH$ and $ZFC+\overline{GCH}$ (ZFC plus the negation of GCH) are all inequivalent theories that contain $ZFC$. It is very likely that a TOE must contain set theory, e.g. ZFC. Let $A$ be such a TOE. Also, it is very likely that $GCH$ is not a physically relevant axiom (at least it is not for our present knowledge). Then $A$ and $A+GCH$ would be inequivalent TOEs, then a TOE is not unique.

I have studied a bit of logic just for fun, so I may be wrong...If someone thinks so and can correct me is welcome ;-)

Like yuggib, I have decided to expand my comment(s) into an answer. However, I will be taking a less formal approach. From the comments, it seems that the following might be a satisfactory, workable point of view for the (non-rigorous) physicist:

Two physical theories of everything $A$ & $B$ clearly must predict the same physics in any physical situation, since they must be ToE's. However, we might imagine that two physical theories are (mathematically) inequivalent in the following sense: There is a unphysical situation where the two theories predict something different.

We call a theory unique if there is no inequivalent theory in the above sense.

The most important question is whether it is reasonable for us to expect that - assuming a ToE exists and can be found - a ToE is unique. Given one ToE we can, of course, construct a somewhat trivial and uninteresting example of an inequivalent ToE by adding 'by hand' a new rule which explicitly changes the predictions of the theory in a strictly unphysical way. However, intuitively we know we shouldn't really consider this an inequivalent ToE (though this may be hard to formalize). I think this is similar to the construction outlined in yuggib's answer.

Discounting these "easy" examples, can we still expect an inequivalent ToE to arise in a more nontrivial way? I personally think the answer is yes, but I have no mathematics (or physics) to support my claim. In fact, I'm not sure whether it is possible to consistently reason about these issues. Perhaps, the best way to think about this question is historically.

It is already known that some of our current theories can be formulated in a way which is really mathematically inequivalent in the above sense. One example that I am aware of is Feynman's time-symmetric theory of classical electromagnetism (as compared, of course, to the usual formulation of EM), which predicts that an electron does not radiate if it is alone in the universe. If we can assume that a ToE is not a fundamentally different thing, epistemologically, than the final step in our gradually expanding knowledge of the universe, it might be reasonable to conclude from our experiences with older theories that, indeed, we can expect multiple inequivalent theories to exist.

Caveat: I cannot claim with certainty that the above is reasonable, consistent and/or true.

It is possible to test whether two mathematical formalisms are equivalent

No, it is not possible. Mathematics allows you to talk about things about which you can't determine if they are equivalent. The word problem is a small example and most mathematical systems themselves suffer the same problem.

So now consider the set of all possible formulations of theories predicting the set of all observables

You are now are already using a particular set theory, ZFC and NFU might give you different sets on both levels. If you want to fix a particular version of mathematics you'll run into the problem of nonstandard models. You can try to avoid that by going to second order logic and making a second order theory, but second order logic assumes the exact thing you are discussing so it is classic question begging where you assume the thing you want to show. It's intellectually bankrupt in this context for that reason.

Mathematics as usually practiced is like a game of lets-pretend. The point is that you assume some things and see where you can go from there, leaving the assumptions unquestioned. It does it does. But trying to get more is problematic.

But beyond the mathematics there is some bad physics already too.

For instance there could be a world where 3D Newtonian mechanics is accurate as a TOE. And there could be another world where 2D Newtonian mechanics is accurate as a TOE. But that first theory is fully capable of describing the second world, it just would have all the initial positions and momentums be in some fixed plane.

The first theory allows more observations and more initial conditions. But it works fine for the more restrictive universe.

But we could do the same with GR, just add another coordinate $w$ and say that everything has its coordinate velocity in the $w$ direction be constant but the other four coordinates of an object evolve just as it does in regular GR. Then if the initial conditions have everything at $w=0$ initially and no $w$ velocity then they stay there but this higher dimensional theory has the (unnecessary in our case) freedom to accommodate other initial conditions.

It can be proven that if a ToE exists, it is necessarily not unique

Take any theory T. Add a new parameter. Say that if things have the same parameter value then things behave like they do in T but if they have different values they behave differently, be specific. Say that your value of the new parameter changes in some simple way such that when new stuff is made out of things that had the same value as each other of the parameter that the new thing has the same value and where it is possible for everything to keep having the same value of that new parameter I way independent of everything else. Then you have a new theory N. But you can use N just as easily as T by just specifying initial conditions where everything has the same value of the parameter and starts out the way where that value isn't changing.

But Occam's razor favors the first TOE T because the TOE N is really a theory of too much.

You asked whether it

can be proven that it is impossible to say anything about the uniqueness of a ToE, should it exist (it is impossible to test mathematical equivalence of theories)

And in general you can't test equivalence of theories, but some theories can be tested. So sometimes you can, sometimes you can't. Sometimes you can know that you can't.

Since you said it was a math question, it's not surprising that it all depends on your exact definitions.