# Formal definition of “equivalence” between two formalizations of a theory?

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. • @MauroALLEGRANZA Surely the notion of bi-interpretability is more relevant here, since the OP is explicitly asking about theories in different languages? – Alex Kruckman Feb 27 at 14:58 • For your first suggestion, the notion of concrete category could help : for example your two categories are not only isomorphic but concretely isomorphic (in the sense that your isomorphisms commute with forgetful functors). – Arnaud D. Feb 27 at 15:03 • There's also the notion of Morita equivalence of theories, in the sense of having equivalent classifying toposes. This only really works for formalization in the sense of (possibly infinitary) first order axiomatization, so it won't necessarily cover things that aren't first order structures. – Malice Vidrine Feb 27 at 18:45 ## 1 Answer 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. • “I.e. that there is a bijection between the two kinds of structures on a set”. But we don’t just want there to be a bijection$F$, we also want that topological space$X$“contains the same information” as$F(X)$. Certainly not all bijections have this property (e.g. the bijection that maps each topological space to its corresponding neighborhood topological space, except mapping the unit circle to the singleton and the singleton to the neighborhood-unit circle.). I’m assuming that the fact that all continuous functions also have to map properly is the thing that serves this role, but – user56834 Feb 27 at 15:59 • But I don’t find category theory intuitive enough perhaps, however, it seems to me that the categorical isomorphism idea does miss something, even if you also require the forgetful functor to commute with the isomorphism: namely, take a topological space$(X,T)$and a topological space$(X,S)$which has the same set but different topologies, but that are homeomorphic. For example, take$X=\{0,1\}$where$T$has$0$be open and$1$not be open, but$S$has$0$not be open and$1$be open. Then these are not really the same topological spaces in a literal sense, but they are homeomorphic. – user56834 Feb 27 at 16:05 • We CAN distinguish between the neighborhood topologies induced by$(X,T)$and$(X,S)$respectively, and therefore really our notion of “equivalence of axiomatizations” should respect the fact that we can distinguish this, shouldn’t it? But the categorical notion of “there exists an isomorphism of topologies and neighborhood-topologies where the isomorphism commutes with the forgetful functor” does not respect this difference, because functor that maps$(X,T)$to the neighborhood-topology of$(X,S)\$ also satisfies this. – user56834 Feb 27 at 16:08
• @user56834 It depends on what precisely you mean by respect the difference. After all, because the functors are inverses, two distinct but homeomorphic topologies must map to two distinct but homeomorphic neighborhood topologies with the same homeomorphism between them. It's also not obvious that a functor as you've described exists, since it would have to preserve the continuous functions to and from other sets, which means it ought to induce certain permutations on other sets, which aren't obviously compatible. – jgon Feb 27 at 16:25
• Moreover, even if we could define an invertible functor like you've described, I would interpret that as saying that there is a compatible family of permutations for every set such that defining a structure on the permuted set is the same as defining a structure on the unpermuted set. Which seems like a reasonable interpretation. – jgon Feb 27 at 16:25