Example: Lets say we have two Peano systems (with 2nd order axiomatization). In one system the initial element is 0, and in the other, it is 1. For reference, here are the axioms mentioned in Mendelson's Number Systems and the Foundations of Analysis (he assumes initial element is 1):
These two systems are isomorphic (rename 1 to 0 to obtain theorems in the other system, and vice versa).
Yet, when we extend each system by adding the definition of addition (one that respects intuition), the isomorphism no longer holds. For example, the system with 0 as initial element has an additive inverse, but the system with 1 as initial element does not.
Why should this happen even though the definition of addition is conservatively extending each system? Also, does this phenomenon have a name?
Definition of conservative extension from https://en.wikipedia.org/wiki/Conservative_extension.
a conservative extension is a supertheory of a theory which is often convenient for proving theorems, but proves no new theorems about the language of the original theory.
EDIT: Thanks for the answers and comments. I will try to explain what I think caused my confusion: If a definition is legal, then for every wff $\varphi$ using a defined symbol, there exists a wff $\varphi'$ in the unextended language where the symbol is eliminated, and $\varphi$ and $\varphi'$ are equivalent.
So although addition is defined differently in the two Peano systems above, theorems involving the addition symbol can be reduced to equivalent theorems not involving it, in the unextended language. Since these theorems are in the unextended language, they are contained in both extensions.
I think I was confusing this kind of equivalence of the two Peano systems with the isomorphism of these two systems, which is a different issue. Isomorphism means merely a naming difference but same structure. Elimination of definitions is about logical equivalence regardless of structure.
Perhaps this is hopelessly convoluted thinking, but I'll eventually study this stuff in a proper way, I think I am just jumping ahead too soon.
There is really nothing surprising about this at all. Why should the extended structures be isomorphic, just because they are each models of conservative extensions of the original theory? Conservativity says the new structure and axioms give you no new theorems about the original structure, but there's no reason you couldn't have two different, non-isomorphic new structures with this property.
I think a simpler example is instructive. Let $n$ be your favorite positive integer and consider the first-order theory of a set with $n$ elements, with no functions or relations at all (besides equality). This theory is rather trivially complete, so any consistent extension of it is automatically conservative. But there are tons of possible extensions that have non-isomorphic models: if you introduce just a single relation symbol, then there are multiple interpretations that symbol could have on a set with $n$ elements, and they will not all be isomorphic.