Normally, I think of an isomorphism between two structures as requiring they have the same signature. E.g. two structures $(A,\cdot)$ and $(B,+)$ where $\cdot: A\times A\to A$ and $+:B\times B\to B$ can potentially be isomorphic only because they both have a binary operator defined on them. I.e. they have an equivalent type signature.
But we often have two formalizations of a theory that do not have an equivalent type signature. For example, the open set formalization of topology and the neighborhood formalization: The open set formalization has $(X,T)$ where $T\subseteq \mathcal P(X)$ and the neighborhood formalization has $(X,N)$ where $N:X\to\mathcal P \mathcal P(X)$.
Nevertheless, there is an “equivalence” between a topological space such as $(\mathbb R, T_{\mathbb R})$ and $(\mathbb R, N_{\mathbb R})$. (This equivalence is not merely an isomorphism. They actually represent the exact same object in some sense).
Is there a general definition, a set of criteria, for this idea of “equivalence of formalizations of the same structure”?
My thoughts so far are:
We can say something about this from the perspective of category theory, but I find it rather unsatisfactory. If we take the category Top of open-set topological spaces, and the category NTop of neighbourhood topological spaces, then there is an isomorphism functor $F:$Top$\to$ NTop, which maps the topologies to their obvious neighborhood topologies, and maps functions to themselves. Hence Top and NTop are categorically isomorphic. I find this unsatisfactory because it doesn’t directly show that $X$ in Top literally contains the same structure as $F(X)$, only that the continuous functions defined on them are categorically equivalent. This is another way of saying, I’m not sure what categorical definition would be appropriate, or whether category theory is the right framework for doing this.
I’m unsure how we would approach this from the perspective of mathematical logic. In a sense, what we want to say is that “for any proposition $\phi$ about open-set topological spaces, there is an equivalent proposition $\chi$ about neighborhood topological spaces such that $\phi$ holds in $(X,T)$ iff $\chi$ holds in the corresponding $(X,N)”. And we really want a definition of equivalence that we can apply in arbitrary mathematical structures, not just one that works for topological spaces, one that works for groups, etc.
I can't say anything about logic, not being a logician, but I wanted to say a couple things about the category theoretic interpretation.
I have to say, I personally find the isomorphism of categories viewpoint fairly compelling.
The only thing I'd add is that the isomorphism functor commutes with the forgetful functor to $\mathbf{Set}$. This implies that if we think of both categories as sets with extra structure, the isomorphism preserves the set and carries one structure to the other and vice versa, and moreover, this preserves the morphisms. Indeed, this is usually what I've seen proven when people want to prove that they are equivalent definitions. I.e., that there is a bijection between the two kinds of structures on a set. (The morphisms being the same is usually fairly clear).
Note that commuting with the forgetful functor also means that if we think of the morphisms in the two isomorphic categories as being structure preserving functions on the underlying sets (via the forgetful functor) then the isomorphism preserves these functions.