I have read in John Corcoran's "Mutual Interpretability is not Definitional Equivalence" (meeting abstract, 1979, p. 430) that the following two "second-order" axiomatizations of Peano arithmetic (I will call them $T$ and $T'$) are mutually interpretable, but not definitionally equivalent. I don't see why. Here are the two formulations ('s' is the successor functor). See also Corcoran's note concerning definitional equivalence.
$T$:
$s(x)\neq 0$;
$s(x) = s(y) \rightarrow x=y$;
$(P0 \land \forall x (Px \rightarrow Ps(x)) \rightarrow \forall yPy $
$T'$:
$x+1 \neq 0$;
$x+1 = y+1 \rightarrow x=y$;
$(P0 \land \forall x (Px \rightarrow Px+1) \rightarrow \forall yPy$
Recall that mutual interpretability is just like definitional equivalence except that the two definitional extensions $T^+$ and $T'^+$ need not be logically equivalent. The only requirement is that $T^+ \vdash T'$ and $T'^+ \vdash T$.
