2.1. Generalized Definitional Equivalence

The basic idea behind GDE is to count theories as formally equivalent just in case one can define the vocabulary of each theory within the other theory such that this introduction of vocabulary makes the two sides logically equivalent. This idea can be made precise using only weak presuppositions about the structure of theories. All we need is that a theory T comes with a class of models, Mod(T), and that its models are Σ(T)-structures of a signature Σ(T).Footnote ³ A signature is simply a collection of nonlogical symbols. It is not necessary to identify theories with their classes of models. Hence, this requirement is compatible with both the syntactic and the semantic view of theories. Moreover, signatures do not have to be single sorted and first order. They may just as well be many sorted and higher order.Footnote ⁴

In essence, GD-equivalent theories differ only in the choice of primitive vocabulary. Since sort symbols also belong to the vocabulary of a theory, GD-equivalent theories may differ in the sorts of objects they take as primitive. GDE allows that objects of a sort taken as primitive in one theory have to be logically constructed in another theory. Definitional equivalence is the special case of GDE in which theories are required to have the same primitive sorts.

For self-contained expositions of the criterion of GDE, see Andréka et al. (Reference Andréka, Madarász and Németi2008) or Barrett and Halvorson (Reference Barrett and Halvorson2016).Footnote ⁵ Note that Halvorson and Barrett call GDE ‘Morita equivalence’.Footnote ⁶ GDE is also closely related to the criterion of general bi-interpretability as described by Hodges (Reference Hodges1993, sec. 5.4). There is a conjecture that the two criteria are in fact equivalent. Yet, a proof is still missing.

2.2. Choices of Morphisms as Interpretive Choices

GDE works well in many cases. However, there are cases in which the class of models of a formalism is endowed with additional structure that GDE is not designed to take into account but that is relevant when it comes to possible interpretations. As several authors have pointed out, it can be fruitful to endow a class of models with a collection of morphisms when reconstructing the formalism of a theory (e.g., Halvorson Reference Halvorson2016; Weatherall Reference Weatherall2016, Reference Weatherall and Landry2017; Nguyen, Teh, and Wells Reference Nguyen, Teh and Wells2017). Intuitively, morphisms are structure-preserving mappings between models (also called ‘transformations’ or ‘symmetries’ in some contexts).

Among other things, this additional structure on a class of models can be used to encode constraints on possible interpretations. Used in this way, a choice of morphisms reflects which features of models are taken to be meaningful, that is, intended to play a representational role in possible applications.Footnote ⁷ The idea is that only features invariant under the chosen morphisms count as meaningful.Footnote ⁸ For example, Euclidean geometry has the group of Euclidean isometries as morphisms, whereas affine geometry has the larger group of affine transformations as morphisms. So although distance is meaningful in Euclidean geometry, it is not meaningful in affine geometry since it is not invariant under all affine transformations. However, parallelism is still meaningful in affine geometry. Note that even if two formalisms have exactly the same models, they may differ in which morphisms they include. Also note that nonmeaningful (surplus or auxiliary) features of models can be of great practical usefulness, and it may be hard and even undesirable to eliminate them.

Since GDE does not take into account morphisms, it is unable to capture certain cases of equivalence or inequivalence that are due to choices of morphisms between models. Weatherall (Reference Weatherall2016) discusses examples of such equivalences. An example regarding inequivalences will be discussed in section 4.3.

So in order to deal with formalisms that are enriched with morphisms, we need a criterion that takes morphisms into account. CE is such a criterion.

2.3. Categorical Equivalence

In contrast to GDE, the criterion of CE compares classes of models endowed with morphisms rather than bare classes of models of theories. A class of models endowed with morphisms forms what is called a ‘category’. A category C comprises a class of objects, Ob(C); a class of morphisms (arrows) between these objects, Mor(C); an associative composition operation for morphisms; as well as an identity morphism from each object to itself. Category theory provides a rigorous notion of equivalence of categories, on which the criterion of CE is based. In order to define this notion, we need a few important category-theoretic concepts.

A functor from one category to another maps objects to objects and morphisms to morphisms in a way that preserves composition of morphisms and identity morphisms. So functors are morphisms of categories. Natural transformations, however, are morphisms of functors, and natural isomorphisms are invertible natural transformations.Footnote ⁹ Using these concepts, we can define when categories are equivalent. Roughly speaking, categories are equivalent just in case they are related by functors that are quasi-inverse to each other (and hence forget nothing that matters from a categorical perspective).

Definition 2. C₁ and C₂ are equivalent categories iff there are functors

$\begin{array}{cc}F:& {\text{C}}_1\to {\text{C}}_2\\ G:& {\text{C}}_2\to {\text{C}}_1\end{array}$

such that their composition GF is naturally isomorphic to $1_{{\text{C}}_1}$, and FG is naturally isomorphic to $1_{{\text{C}}_2}$ (where $1_{{\text{C}}_i}$ is the identity functor on C_i for $1\le i\le 2$).

A closely related notion is that of duality. Two categories are said to be dual to each other (also dually equivalent or contravariantly equivalent) iff one category is equivalent to the opposite of the other category, where the opposite of a category is the result of reversing all of its arrows.

With these concepts at hand, we can state the criterion of CE for theories that come with an associated category of models. If T is such a theory, let ‘Cat(T)’ denote its category of models.

Philosophers of physics have applied this criterion in several case studies (see Barrett et al. Reference Barrett, Rosenstock and Weatherall2015; Hudetz Reference Hudetz2015; Rosenstock and Weatherall Reference Rosenstock and Weatherall2016; Weatherall Reference Weatherall2016; Barrett Reference Barrett2017; Teh and Tsementzis Reference Teh and Tsementzis2017).

2.4. Internal Structure of Models Matters for Representation

The criterion of CE only takes into account how models are related by morphisms and neglects other properties of models. In particular, it does not take into account how models are internally structured. Yet, the internal constitution of models matters when it comes to establishing representation relations between models and their target systems.

Let me illustrate this point using a simple example. It is well known that the category of finite-dimensional vector spaces with linear mappings as morphisms is equivalent to the category that has natural numbers as objects and real $m\times n$-matrices as morphisms. Up to isomorphism, there is exactly one vector space of dimension n. So one replaces all vector spaces of dimension n with the natural number n and linear mappings with corresponding matrices. Differences in how the objects of two equivalent categories are internally structured are irrelevant from a purely category-theoretic perspective. Nonetheless, such differences are by no means irrelevant for all scientific purposes. Whenever vector spaces are used to model features of real-world systems, we cannot simply replace them with natural numbers. Vector spaces possess internal structure: a set of vectors, the operations of vector addition and scalar multiplication, a zero vector (and an underlying field of scalars). In applications, some of these features serve representational purposes. For example, vectors might be used to represent forces acting on objects, and the net force on an object may be represented by a sum of vectors. It is utterly impossible that a natural number n could serve the same representational purposes as a vector space of dimension n. The number n simply lacks the internal structure necessary for fulfilling such representational roles.

These observations suggest two things. First, a formalism intended to serve representational purposes can only be equivalently replaced by another formalism if their models have the same representational capacities. Second, it is a necessary condition for sameness of representational capacities that the models of each formalism have internal structure that is sufficient for recovering the relevant internal structure of the models of the other formalism.

It is hardly surprising that the fact that CE does not take into account the internal structure of models leads to a trivialization of CE in certain cases. It is easy to see that CE collapses to a mere cardinality comparison of model classes when the theories in question have “very few” morphisms. More precisely, any two theories with categories of models that are rigid groupoids (i.e., when every morphism is an isomorphism and no model has nontrivial automorphisms) are C-equivalent as soon as they have the same number of nonisomorphic models. We will see in section 4.1 that this does not hold for DCE.

4.1. DCE Is Strictly Stronger than CE

There are cases of CE in which equivalence functors trivially exist but mutual reconstruction of models is not possible along these functors. In particular, the criterion of DCE does not collapse to a mere cardinality comparison of model classes when it comes to theories with “very few” morphisms (described at the end of sec. 2.4). I will illustrate this point using two examples. First, let us consider a well-known simple toy example of a pathological C-equivalence due to Barrett and Halvorson (Reference Barrett and Halvorson2016, theorem 5.7). They specify two single-sorted first-order axiom systems: $T_1≔\left\{{\exists }_{{\sigma }_1}!\mathrm{xx}=x\right\}$ and $T_2≔\left\{{\exists }_{{\sigma }_2}!\mathrm{yy}=y\right\}\cup \left\{{\forall }_{{\sigma }_2}y\left(Q_{0}y\to Q_{i}y\right):i\in \mathbb{N}\right\}$ with signatures ${\Sigma }_1≔\left\{{\sigma }_1,P_0,P_1,\dots \right\}$ and ${\Sigma }_2≔\left\{{\sigma }_2,Q_0,Q_1,\dots \right\}$, respectively. Elementary embeddings serve as morphisms in their categories of models. Barrett and Halvorson prove that T ₁ and T ₂ are C-equivalent but not GD-equivalent. Theory T ₂ is stronger than T ₁ in virtue of its additional axioms. The reason why T ₁ and T ₂ are C-equivalent is that they have the same number of nonisomorphic models and their categories of models are rigid groupoids. However, one can show that no functors constituting an equivalence between these categories are reconstruction functors. Hence:

Although this is only a toy example, it shows that, relative to CE, the definability condition built into DCE makes a difference and is therefore not redundant. This observation might seem trivial. Nevertheless, it is important to make in order to address an idea that has recently been put forward in the literature. Feintzeig (Reference Feintzeig2017) claims that an adjunction between two categories of models hints at a sense in which the models in one category are definable from the models in the other category. Since every C-equivalence is an adjunction, the same must hold for CE if Feintzeig’s claim is right. This idea leads to the question whether CE entails that the models in one category are in some sense definable from the models in the other category. If this were so, then adding a definability condition to CE would be redundant. However, it is not so in general. It might be true in special cases in which all the internal structure of models is fully encoded by the morphisms between them.Footnote ¹³ But there are cases in which CE does not capture or even hint at mutual definability in any way. Here is an example that is more general and more robust than the first one.Footnote ¹⁴ There is no reasonable sense of definability according to which any two rigid structures whatsoever are definable from each other. Nevertheless, for any two rigid structures 𝒜₁ and 𝒜₂, there is an equivalence between the categories C₁ and C₂, where C_i has 𝒜_i as its sole object and the trivial identity automorphism of 𝒜₁ as its only arrow. In such cases, CE is trivially satisfied even if 𝒜₁ and 𝒜₂ are not definable from each other in any sense. In contrast, DCE is not necessarily satisfied, as it explicitly takes into account definability.

For instance, take a simple theory describing a social network with an up to isomorphism unique rigid model (a finite graph) and a cosmological model that arises from general relativity by means of conditions singling out a unique space-time manifold with no nontrivial isometries (i.e., where space-time is highly asymmetric). Then these theories are trivially C-equivalent. However, they are not DC-equivalent because a model of general relativity with its rich internal structure is not definable from a finite graph.

Some authors take it as “a definite mark against categorical equivalence as a general standard for equivalence of theories” (Barrett Reference Barrett2018, 636) that C-equivalence does not imply that the models of each theory are somehow definable in terms of the models of the other. From this perspective, DCE can be seen as an amendment of CE not subject to this concern.

4.2. Proving CE Often Yields a Proof of DCE

We have now seen that DCE is a nontrivial strengthening of CE, ruling out several instances of the latter. However, the definability constraint in the criterion of DCE does not constitute an extreme strengthening either. DCE is not very far from CE in the sense that from many proofs of C-equivalences occurring in practice one can extract proofs of DC-equivalences. The reason is that proofs of (dual) equivalences between concrete categories often establish more than the mere existence of (contravariant) equivalence functors. In many cases, one establishes how to define structures of one kind from structures of another kind and vice versa in order to specify functors witnessing the duality or equivalence in question. In such cases, theorems sometimes state a bit less than their proofs establish.

For example, when proving that the category of Boolean algebras is dual to the category of Stone spaces one defines a Stone space from a given Boolean algebra and vice versa. Another example is Gelfand duality, where one defines a compact Hausdorff space from any given unital commutative C*-algebra 𝒜 (i.e., the space of nonvanishing C*-algebra homomorphisms from 𝒜 to ℂ with the spectral topology) and one defines a unital commutative C*-algebra from any given compact Hausdorff space χ (i.e., the algebra of continuous functions from χ to ℂ). Roughly speaking, the definitions involved in specifying the functors constituting Gelfand duality capture a sense in which state spaces and algebras of observables of classical mechanical systems can be reconstructed from each other (Strocchi Reference Strocchi2005, 15).

Actually, finding appropriate definitions is often a crucial step in proofs of (dual) equivalences between categories. It is what enables us to specify functors in the first place, and the fact that the so specified functors constitute a (dual) equivalence between the categories in question depends on the judicious choice of definitions. In this sense, the idea of reconstruction underlying DCE ties in with scientific practice.

It follows from the results in the previous section that not all instances of CE have proofs involving definitions in this way. However, I conjecture that many instances of CE that we encounter in practice do, especially those arising from reconstruction or representation theorems. This conjecture suggests to undertake case studies as a task for future research. For example, is the C-equivalence between formulations of Hamiltonian mechanics and Lagrangian mechanics (Barrett Reference Barrett2017) a case of DCE? Does the Gelfand-Naimark representation theorem (Gelfand and Naimark Reference Gelfand and Naimark1943) allow us to prove that the Hilbert space formalism and the C*-algebra formalism of quantum mechanics are DC-equivalent? Do reconstruction theorems relating different approaches to quantum field theories (e.g., Wightman Reference Wightman1956; Osterwalder and Schrader Reference Osterwalder and Schrader1973, Reference Osterwalder and Schrader1975) give rise to DC-equivalences?

4.3. DCE and GDE Differ in the Presence of Surplus Structure

A major difference between DCE and GDE is that DCE is not overly sensitive to the presence of auxiliary or surplus structure because it takes morphisms into account. This section is devoted to showing that. We put the focus on a particular kind of auxiliary structure, namely, coordinate systems. Although introducing coordinates is an insignificant extension of a formalism as far as representational capacities are concerned, it makes a big difference for GDE: models that are not GD-equivalent can become GD-equivalent when equipped with coordinate systems. The reason is that the presence of a coordinate system allows us to formulate new definitions that could not be formulated otherwise. These newly available definitions can be used to establish GDE even though the definientia involved are not meaningful formulas. This leads to pathological positive cases of GDE. As we will see, DCE is not beset with this problem.

Let us look at an example to illustrate these points. We compare n-dimensional Minkowski geometry (MG_n) and n-dimensional Euclidean geometry (EG_n). The models of MG_n and EG_n are n-dimensional Minkowski spaces and n-dimensional Euclidean spaces, respectively. Both Minkowski spaces and Euclidean spaces are here understood as real vector spaces equipped with generalized inner products (i.e., nondegenerate symmetric bilinear forms).Footnote ¹⁵ This is a slight simplification. Strictly speaking, Minkowski and Euclidean spaces should be treated as affine spaces—rather than vector spaces—equipped with generalized inner products.Footnote ¹⁶ But since this would unnecessarily complicate our presentation without affecting any results, the chosen simplification is unproblematic. It is also common in physics to simplify in this way (see Naber Reference Naber2012).

So we take an n-dimensional Minkowski space (V, η) to consist of an n-dimensional vector space $V=(V,\oplus ,\odot )$ over the field R of real numbers together with a Minkowskian inner product $\eta :V\times V\to ℝ$ of metric signature (1, $n-1$). An n-dimensional Euclidean space (V, 〈·, ·〉) is an n-dimensional real vector space V endowed with a Euclidean inner product $〈\cdot ,\cdot 〉:V\times V\to ℝ$ of metric signature (n, 0). Up to isomorphism, there is only one n-dimensional Minkowski space and only one n-dimensional Euclidean space.

When endowed with a physical interpretation (see Malament Reference Malament2009, sec. 3.2), four-dimensional Minkowski geometry yields the theory of space-time underlying special relativity. Four-dimensional Euclidean geometry, when physically interpreted, ascribes a very different structure to space-time. But more than that these geometries should count as inequivalent irrespective of concrete physical applications because their generalized inner products are very different from a purely mathematical point of view. They encode very different notions of distance and angles. The criteria of GDE and DCE both capture this difference when the models of Euclidean and Minkowski geometry are not endowed with coordinate systems:

However, we will now see that if we endow their models with coordinate systems, the resulting versions of Minkowski and Euclidean geometry become GD-equivalent but not DC-equivalent. Endowing models with coordinate systems can hardly be regarded as an illegitimate step. Although coordinate systems may be dispensable for a characterization of fundamental space-time structure or other foundational issues, they still play an important role in practice. Usually, one cannot apply geometry empirically without choosing a reference frame and an associated coordinate system. For a defense of the legitimacy of a coordinate-based approach for foundational work, see Wallace (Reference Wallace2016).

We need a bit of terminology to specify the coordinatized models. A linear coordinate system for an n-dimensional vector space V is an n-tuple of coordinate functions (f ⁰, …, $f^{n-1}$), where $f^i:V\to ℝ$ maps every vector $v\in V$ to a real number serving as the ith coordinate of v ( $0\le i<n$), such that the function $f:V\to {ℝ}^n$ defined by $f\left(v\right)≔\left(f^0\right(v),\dots ,f^{n-1}(v\left)\right)$ is a vector space isomorphism from V to the real coordinate space Rⁿ.Footnote ¹⁷ We say that a linear coordinate system (f ⁰, …, $f^{n-1}$) for V is a Lorentz coordinate system for an n-dimensional Minkowski space $ℳ=(V,\eta )$ iff f is an isometric isomorphism from ℳ to the real coordinate space (Rⁿ, η _std) with the standard Minkowski inner product η _std on Rⁿ, which takes the following form in the standard coordinates xⁱ on ℝⁿ (mapping elements of ℝⁿ to their ith components):

(1) $\begin{array}{}& {\eta }_{\mathrm{std}}(u,v)=x^0\left(u\right)\cdot x^0\left(v\right)-\dots -x^{n-1}\left(u\right)\cdot x^{n-1}\left(v\right).\end{array}$

It immediately follows that all Lorentz coordinate systems for ℳ are related to each other by Lorentz transformations. Analogously, (f ⁰, …, $f^{n-1}$) is a Euclidean coordinate system for an n-dimensional Euclidean space $ℰ=(V,〈\cdot ,\cdot 〉)$ iff f is an isometric isomorphism from ℰ to the real coordinate space (Rⁿ, 〈·, ·〉_std) with the standard Euclidean inner product on Rⁿ, which is given by

(2) $\begin{array}{}& {〈u,v〉}_{\mathrm{std}}=x^0\left(u\right)\cdot x^0\left(v\right)+\dots +x^{n-1}\left(u\right)\cdot x^{n-1}\left(v\right).\end{array}$

Now we can specify the models of Minkowski and Euclidean geometry extended with coordinate systems ( ${\mathrm{MG}}_n^{+}$ and ${\mathrm{EG}}_n^{+}$). The models of ${\mathrm{MG}}_n^{+}$ are those structures (V, f ⁰, …, $f^{n-1}$, η) such that (V, η) is a model of MG_n and (f ⁰, …, $f^{n-1}$) is a Lorentz coordinate system for (V, η). The models of ${\mathrm{EG}}_n^{+}$ are those structures (V, f ⁰, …, $f^{n-1}$, 〈·, ·〉) such that (V, 〈·, ·〉) is a model of EG_n and (f ⁰, …, $f^{n-1}$) is a Euclidean coordinate system for (V, 〈·, ·〉).Footnote ¹⁸ With these specifications at hand, one can prove that

To get an impression of what is going on here, consider a model $ℳ=(V^{+},\eta )$ of ${\mathrm{MG}}_n^{+}$, where $V^{+}=(V,f^0,\dots ,f^{n-1})$. It follows that ℳ is a definitional expansion of V⁺ because (f ⁰, …, $f^{n-1}$) is a Lorentz coordinate system for ℳ, and hence ℳ satisfies

(3) $\begin{array}{}& \eta (u,v)=f^0\left(u\right)\cdot f^0\left(v\right)-\dots -f^{n-1}\left(u\right)\cdot f^{n-1}\left(v\right).\end{array}$

Now define a Euclidean inner product 〈⋅, ⋅〉 over V⁺:

(4) $\begin{array}{}& 〈u,v〉=f^0\left(u\right)\cdot f^0\left(v\right)+\dots +f^{n-1}\left(u\right)\cdot f^{n-1}\left(v\right).\end{array}$

This definition can be formulated in the first-order language of n-dimensional vector spaces with coordinate functions. Then $ℰ≔(V^{+},〈\cdot ,\cdot 〉)$ is a model of ${\mathrm{EG}}_n^{+}$ and also a definitional expansion of V⁺. Hence, ℳ and ℰ are definitional expansions of the same underlying structure V⁺ and, therefore, have a common definitional expansion (V⁺, η, 〈·, ·〉). Thus, ℳ and ℰ are definitionally equivalent.

Let us now see how a different analysis of the relationship between ${\mathrm{MG}}_n^{+}$ and ${\mathrm{EG}}_n^{+}$ can be achieved by making use of morphisms to wash out auxiliary structure. The crucial point is that choices of coordinates need not be preserved under morphisms. One can change coordinates (e.g., via a Lorentz transformation in the case of ${\mathrm{MG}}_n^{+}$), and the model with the new coordinate system will represent exactly the same physical situation. This suggests specifying the categories of models of ${\mathrm{MG}}_n^{+}$ and ${\mathrm{EG}}_n^{+}$ in such a way that choices of coordinates may vary under morphisms. In particular, we should not take $\Sigma \left({\mathrm{MG}}_n^{+}\right)$-isomorphisms and $\Sigma \left({\mathrm{EG}}_n^{+}\right)$-isomorphisms as the respective morphisms because they preserve all the internal structure of models, including coordinate functions. Furthermore, if we would like to wash out surplus structure that is due to our simplification—that is, the designated origins in Euclidean and Minkowski spaces—now is the opportunity to do so by choosing morphisms that do not preserve origins. This is what we will do. We define $\mathrm{Cat}\left({\mathrm{MG}}_n^{+}\right)$ in such a way that $h:(V,f^0,\dots ,f^{n-1},\eta )\to (V^{\prime },f^{\prime 0},\dots ,f^{\prime n-1},{\eta }^{\prime })$ is a morphism in $\mathrm{Cat}\left({\mathrm{MG}}_n^{+}\right)$ iff h is a bijection from V to V′ that is an affine map from V to V′ preserving Minkowski inner products (i.e., $\eta (u,v)={\eta }^{\prime }\left(h\right(u),h(v\left)\right)$ for all u, $v\in V$), and for technical reasons we also require that h maps each scalar to itself.Footnote ¹⁹ The morphisms in $\mathrm{Cat}\left({\mathrm{EG}}_n^{+}\right)$ are specified analogously.

It follows that the automorphism group of each model in $\mathrm{Cat}\left({\mathrm{MG}}_n^{+}\right)$ is the Poincaré group, whereas the automorphism group of models in $\mathrm{Cat}\left({\mathrm{EG}}_n^{+}\right)$ is the Euclidean group. The fact that the Poincaré group and the Euclidean group are not isomorphic implies that

We can say more when we consider which formulas count as meaningful in ${\mathrm{MG}}_n^{+}$ and ${\mathrm{EG}}_n^{+}$. On a usual interpretation of these formalisms, formulas with free vector variables are only meaningful when they are invariant under morphisms. We call a formula φ over $\Sigma \left({\mathrm{MG}}_n^{+}\right)$ with n free variables invariant under the morphisms of $\mathrm{Cat}\left({\mathrm{MG}}_n^{+}\right)$ just in case for all morphisms $h:ℳ\to {ℳ}^{\prime }$ in $\mathrm{Cat}\left({\mathrm{MG}}_n^{+}\right)$, an n-tuple (a ₁, …, a_n) satisfies φ in ℳ iff (h(a ₁), …, h(a_n)) satisfies φ in ℳ′. It follows that the formula

(5) $\begin{array}{}& z=f^0\left(u\right)\cdot f^0\left(v\right)+\dots +f^{n-1}\left(u\right)\cdot f^{n-1}\left(v\right)\end{array}$

is not invariant under the morphisms of $\mathrm{Cat}\left({\mathrm{MG}}_n^{+}\right)$.Footnote ²⁰ Hence, formula (5) is not meaningful in ${\mathrm{MG}}_n^{+}$. So although formula (5) defines a Euclidean inner product over any given model of ${\mathrm{MG}}_n^{+}$, this inner product will not count as meaningful in ${\mathrm{MG}}_n^{+}$. Thus, any reconstruction manual for $\Sigma \left({\mathrm{EG}}_n^{+}\right)$ in terms of $\Sigma \left({\mathrm{MG}}_n^{+}\right)$ yielding (5) as a translation of $〈u,v〉=z$ does not preserve meaningfulness. An analogous conclusion holds for reconstruction manuals for $\Sigma \left({\mathrm{MG}}_n^{+}\right)$ in terms of $\Sigma \left({\mathrm{EG}}_n^{+}\right)$.

4.4. DCE Is Close to GDE in the Absence of Surplus Structure

We have seen that DCE and GDE sometimes coincide and sometimes do not coincide. This section shows under which conditions the two criteria coincide.

First, one can show that DCE is a generalization of GDE for theories of a certain kind. Barrett and Halvorson (Reference Barrett and Halvorson2016) have shown that GD-equivalent first-order theories with elementary embeddings as morphisms are C-equivalent. Their proof can be generalized for the case of theories with higher-order structures as models. Moreover, one can show that the equivalence functors constructed from a GD-equivalence are indeed reconstruction functors (which is not entirely trivial). So we get the following result.

Let us briefly pause here and reflect on what the choice of elementary embeddings as morphisms means for a theory. Elementary embeddings are injective mappings between models that preserve all relations definable in the theory’s language. This choice of morphisms reflects the idea that all definable features of models may be taken to be meaningful. (The same holds for Σ(T)-isomorphisms, which form a subclass of elementary embeddings.) So taking precisely elementary embeddings (or precisely Σ(T)-isomorphisms) as the morphisms of a theory T means viewing the models of T as not exhibiting any auxiliary or surplus structure.

Under this reading, theorem 1 partially captures the idea that morphisms need to be taken into account only in the presence of auxiliary or surplus structure. This idea furthermore suggests that DCE should not be much wider than GDE when it comes to theories without auxiliary or surplus structure. The following theorem captures a sense in which this is indeed the case. This theorem is one of the main technical results of this article.

The qualification ‘up to external auxiliaries’ concerns auxiliary vocabulary introduced in GD-expansions rather than auxiliary vocabulary of the theories themselves. Every GD-expansion to a signature with new sorts also introduces auxiliary function symbols relating the new sorts to old sorts. GDE up to external auxiliaries is like GDE except that it does not require such “external” auxiliary vocabulary to be recovered. More precisely, T ₁ and T ₂ are GD-equivalent up to external auxiliaries iff they have stepwise GD-expansions E ₁ and E ₂ that coincide insofar as one ignores external auxiliary vocabulary on both sides; that is, $E_1{|}_{\Sigma \left(T_1\right)\cup \Sigma \left(T_2\right)}=E_2{|}_{\Sigma \left(T_1\right)\cup \Sigma \left(T_2\right)}$.Footnote ²¹

So for theories with standard model-theoretic isomorphisms, DCE differs from GDE only in not requiring that auxiliary symbols used for reconstructing the sorts of one theory from the sorts of another theory have to be recovered as well. Hence, DCE is slightly more liberal than GDE in these cases. This raises the question whether and when we should regard recovering external auxiliaries as necessary. I am not aware of any published arguments concerning this question. To shed light on what the requirement of recovering external auxiliaries amounts to, it is useful to find a corresponding strengthening of DCE. It turns out that to obtain GDE simpliciter instead of GDE up to auxiliaries, one only needs to strengthen DCE by adding an extra definability condition regarding isomorphisms between models and their inner models given by composition of reconstruction functors. Call such isomorphisms ‘inner isomorphisms’.

Call 1–3 the ‘many-sorted Ahlbrandt-Ziegler condition’. Its underlying idea is closely related to the concept of bi-interpretability due to Ahlbrandt and Ziegler (Reference Ahlbrandt and Ziegler1986). For a more detailed formulation of this condition, see definition B8, appendix B.

This shows that the requirement to recover external auxiliaries contained in GDE is closely related to the requirement that inner isomorphisms are definable in a certain way. Moreover, this theorem answers a question posed by Barrett (Reference Barrett2018, 637). The question is whether there is a special property $P$ of functors such that the existence of a C-equivalence that is constituted by functors having property $P$ entails GDE (given the theories in question have precisely elementary embeddings as morphisms). The property of being a reconstruction functor comes close. But to achieve GDE, a monadic property of functors is unlikely to suffice. However, a binary relation between functors works, namely, the relation of being reconstruction functors that jointly satisfy the Ahlbrandt-Ziegler condition.

There are good reasons not to include the many-sorted Ahlbrandt-Ziegler condition as a regular component of the criterion of DCE. When strengthened with this extra condition, it would not be able to capture formal equivalences between theories with categories of models that do not (only) contain standard model-theoretic isomorphisms. For instance, in Weatherall’s (Reference Weatherall2016) examples, different potential-based models 𝒜₁, 𝒜₂ that are related by a gauge transformation will be mapped to the same model 𝒜 by the composite auto-equivalence functor. However, the gauge transformations from 𝒜₁ to 𝒜 and from 𝒜₂ to 𝒜 are not induced by uniformly defined bijections in the way the many-sorted Ahlbrandt-Ziegler condition would require (cf. definition B8, app. B). So if we seek to capture equivalences between theories that do not (only) have standard model-theoretic isomorphisms, we should not impose the many-sorted Ahlbrandt-Ziegler condition as necessary.