Definable Categorical Equivalence Abstract This paper aims to provide a new criterion of formal equivalence of the- ories that is suitable for being supplemented with preservation conditions concerning interpretation. I argue that both the internal structure of mod- els and choices of morphisms between models are aspects of formalisms that are relevant when it comes to their interpretations. So an adequate crite- rion should take these aspects into account. The two most important cri- teria presently discussed in philosophy of science—generalised definitional equivalence (Morita equivalence) and categorical equivalence—are not opti- mal in this respect. Generalised definitional equivalence neglects choices of morphisms, whereas categorical equivalence neglects the internal structure of models. I put forward the new criterion of definable categorical equivalence which takes into account both aspects and connects the category-theoretic approach and the definability-theoretic approach to formal equivalence. Manuscript Contents 1 Introduction 1 2 Two criteria, morphisms and internal structure 2 2.1 Generalised definitional equivalence . . . . . . . . . . . . . . . . . . 2 2.2 Choices of morphisms as interpretive choices . . . . . . . . . . . . . 3 2.3 Categorical equivalence . . . . . . . . . . . . . . . . . . . . . . . . 4 2.4 Internal structure of models matters for representation . . . . . . . 5 3 Definable categorical equivalence 6 4 Properties of the new criterion 10 4.1 DCE is strictly stronger than CE . . . . . . . . . . . . . . . . . . . 10 4.2 Proving CE often yields a proof of DCE . . . . . . . . . . . . . . . 11 4.3 DCE and GDE di↵er in the presence of surplus structure . . . . . 12 4.4 DCE is close to GDE in the absence of surplus structure . . . . . . 16 5 Conclusions 18 Appendix A GD-expansions 20 Appendix B Proofs 20 1 Introduction This paper puts forward a new criterion of formal equivalence of theories. Roughly speaking, theories are formally equivalent when their formalisms are intertrans- latable in the sense that they can be logically or mathematically recovered from each other. There are various explications of this idea. The criterion of definitional equivalence is one of the oldest and most well-known ones. Recently, increasing e↵ort has been devoted to finding criteria of formal equivalence that improve on definitional equivalence: the most important proposals are direct generalisations of definitional equivalence (Andréka, Madarász, and Németi, 2008; Barrett and Halvorson, 2016) and category-theoretic criteria (Halvorson, 2016; Halvorson and Tsementzis, 2017; Weatherall, 2016a). These new criteria have been applied in several case studies.1 A well-known criticism of this project is that no criterion that focuses exclu- sively on formalisms is able to capture full equivalence of theories and full equiva- lence is what ultimately matters (cf. Co↵ey, 2014). Whether two theories are fully equivalent depends on how their formalisms are empirically and ontologically in- terpreted. Di↵erent interpretations lead to di↵erent equivalence judgements. Co↵ey is right that one should not neglect interpretation when addressing the problem of full theoretical equivalence. However, this point is by no means a valid objection against the project of explicating formal equivalence. This project is not committed to the assumption that formal equivalence is necessary and su�cient for full equivalence of theories. Instead, one can view the formal project as laying the groundwork for (su�cient) criteria of full theoretical equivalence. According to this view, full theoretical equivalence is to formal equivalence what interpreted formalisms are to uninterpreted ones. The idea is that full equivalence of theories (qua interpreted formalisms) obtains if there is a way of translating between their formalisms that preserves empirical content as well as theoretical content beyond the empirical (if there is any). This idea has been put forward, e.g., by Putnam (1983, pp. 38–39).2 In order to turn this idea into a rigorous account, we need (1) a criterion of formal equivalence that is suitable for being supplemented with preservation conditions regarding interpretation, (2) an explication of what it is to endow a formalism with an interpretation and (3) a rigorous formulation of preservation conditions. This paper addresses the first point (but work devoted to the second and third point is already in progress). In Section 2, I highlight two aspects of formalisms that are relevant when it comes to interpreting a formalism. I briefly present the two currently most important criteria of formal equivalence—generalised defini- 1See for example Andréka and Németi (2014), Barrett (2017), Barrett and Halvorson (2017), Barrett, Rosenstock, and Weatherall (2015), Hudetz (2015), Lefever and Székely (2018), Rosen- stock and Weatherall (2016), Teh and Tsementzis (2017) and Weatherall (2016a). 2Putnam (1983, p. 40) argues that formal equivalence is even necessary for full equivalence. 1 tional equivalence (GDE) and categorical equivalence (CE)—and point out that each of them takes into account one such aspect while neglecting the other. In Sec- tion 3, I introduce the criterion of definable categorical equivalence (DCE), which takes into account both relevant aspects. Section 4 investigates the properties of DCE and how it is related to GDE and CE. Section 4 contains results suggesting that DCE can also be of interest indepen- dently of the motivations concerning interpretation described above. For example, these results shed new light on GDE and answer a technical question about the relationship between CE and GDE posed by Barrett (2018). There is a sense in which DCE builds a bridge between CE and GDE. Thereby, it connects two main strands of research about formal equivalence criteria: the category-theoretic approach and the definability-theoretic approach. DCE might be of interest for anyone engage with either of these approaches. 2 Two criteria, morphisms and internal structure To understand the new criterion, we first examine the criteria of GDE and CE. These two criteria focus on di↵erent aspects of formalisms. GDE focuses on the internal constitution of models, whereas CE focuses on relationships between mod- els. I argue that both of these aspects are relevant when it comes to interpreting a formalism. An adequate criterion should take both into account. 2.1 Generalised 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).3 A signature is simply a collection of non-logical 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.4 Definition 1. T1 is GD-equivalent to T2 i↵ their classes of models Mod(T1) and Mod(T2) have stepwise GD-expansions E1 and E2 such that E1 = E2. (For a definition of ‘GD-expansion’ see Appendix A.) 3So models are taken to be structures in the model-theoretic sense (see Hodges, 1993). 4For details about higher-order signatures see Hudetz (2017), Johnstone (2002, Section D4.1) or Awodey (1997, Chapter I, Section 1). 2 In essence, GD-equivalent theories di↵er only in the choice of primitive vocabu- lary. Since sort symbols also belong to the vocabulary of a theory, GD-equivalent theories may di↵er 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 con- structed in another theory. Definitional equivalence is the special case of GDE where theories are required to have the same primitive sorts. For self-contained expositions of the criterion of GDE see Barrett and Halvor- son (2016) or Andréka, Madarász, and Németi (2008). Note that Halvorson and Barrett call GDE ‘Morita equivalence’. 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 (cf. Halvorson, 2016; Weatherall, 2016a,b; Nguyen, Teh, and Wells, 2017). 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 mor- phisms reflects which features of models are taken to be meaningful, i.e. intended to play a representational role in possible applications.5 The idea is that only fea- tures invariant under the chosen morphisms count as meaningful.6 For example, Euclidean geometry has the group of Euclidean isometries as morphisms, whereas a�ne geometry has the larger group of a�ne transformations as morphisms. So although distance is meaningful in Euclidean geometry, it is not meaningful in a�ne geometry since it is not invariant under all a�ne transformations. However, parallelism is still meaningful in a�ne geometry. Note that even if two formalisms have exactly the same models, they may di↵er in which morphisms they include. Also note that non-meaningful (surplus or auxiliary) features of models can be of great practical usefulness and it may be hard and even undesirable to eliminate them. 5Of course, choosing morphisms in not su�cient for interpreting a formalisms. It only sets an upper bound on meaningfulness. Formalisms that include morphisms and in which certain formulas are designated as meaningful may be described as ‘pre-interpreted formalisms’. They are prepared for being interpreted but not endowed with a particular interpretation. 6I only assume that the choice of morphisms is coupled with interpretive decisions. This implies neither a commitment to a morphisms first approach, according to which morphisms are prior to the identification of surplus structure (cf. Ismael and van Fraassen, 2003), nor to an interpretation first approach, according to which the interpretive identification of surplus structure is prior to the choice of morphisms. 3 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 (2016a) 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 mor- phisms to morphisms in a way that preserves composition of morphisms and identity morphisms. So functors are morphisms of categories. Natural transfor- mations, on the other hand, are morphisms of functors and natural isomorphisms are invertible natural transformations.7 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. C1 and C2 are equivalent categories i↵ there are functors F : C1 ! C2, G : C2 ! C1 such that their composition GF is naturally isomorphic to 1C1 and FG is naturally isomorphic to 1C2 (where 1Ci is the identity functor on Ci for 1  i  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) i↵ 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. 7For details about these notions see any textbook on category theory, e.g. MacLane (1998) or Awodey (2006). 4 Definition 3. T1 is C-equivalent to T2 i↵ Cat(T1) and Cat(T2) are equivalent or dually equivalent categories. Philosophers of physics have applied this criterion in several case studies (cf. Barrett, 2017; Barrett et al., 2015; Hudetz, 2015; Rosenstock and Weatherall, 2016; Teh and Tsementzis, 2017; Weatherall, 2016a). 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 ⇥ 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. Di↵erences in how the objects of two equivalent categories are internally structured are irrelevant from a purely category-theoretic perspective. Nonetheless, such di↵erences 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 posses 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 upon 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 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 for- malism have internal structure that is su�cient 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 trivialisation 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 5 two theories with categories of models that are rigid groupoids (i.e. where every morphism is an isomorphism and no model has non-trivial automorphisms) are C-equivalent as soon as they have the same number of non-isomorphic models. We will see in Section 4.1 that this does not hold for DCE. 3 Definable categorical equivalence The upshot so far is this: Both choices of morphisms and the internal structure of models are aspects of formalisms that are relevant when it comes to their possible interpretations. Hence, a criterion that is suitable for being supplemented with preservation conditions concerning interpretation should take these aspects into account. GDE and CE are not optimal in this respect because GDE does not take into account choices of morphisms and CE does not take into account the internal structure of models.8 In this section, I propose a criterion that is designed to take into account both morphisms and the internal structure of models. The basic idea is to strengthen CE by imposing a definability constraint on equivalence functors. For this reason, the new criterion is called ‘definable categorical equivalence’. The definability con- straint serves to capture the above-mentioned idea that, if theories are formally equivalent, the models in each formalism should have su�cient internal structure to recover the internal structure of the other formalism’s models. Before laying down the definition of DCE, some preliminary remarks are in order. We consider theories T that come with an associated category Cat(T) having the models of T as objects. We use the same assumptions about Mod(T) as in the case of GDE (see Section 2.1). So models are assumed to be higher-order structures.9 Construing models of scientific theories as higher-order structures does not lead to a relevant loss of generality (see Hudetz, 2017). Models such as dynamical systems, di↵erentiable manifolds, stochastic processes, causal graphs or games (in normal or extensive form) can all be seen as higher-order structures. Moreover, theories with first-order structures as models are subsumed as a special case. The essential idea of DCE does not depend on this particular choice of rep- resenting formalisms of theories. DCE could in principle also be explicated in a di↵erent framework in which we can rigorously talk about definability and mod- els. I use the model-theoretic framework because it is very general, comparatively 8To be fair, GDE and CE were not designed to take these aspects into account. So their lack of doing so is by no means an objection against these criteria per se. It just speaks against using them for certain purposes. 9One could easily lift the requirement that the objects are higher-order structures in the usual sense, i.e. structures consisting of a set (or element) for each symbol of a higher-order signature: they could also be higher-order models in other topoi than the topos of sets. But let us keep things simple and classical for now. 6 simple, close to mathematical practice and many philosophers are familiar with it. Moreover, it makes a comparison with GDE possible, which is also naturally explicated in this framework. There is only a mild requirement concerning morphisms in Cat(T) since the type of structures used as models does not necessarily determine what the relevant notion of morphism is (cf. Awodey, 1997, p. 18; Landry, 2007). The only require- ment is that ⌃(T)-isomorphic models of T should also be isomorphic in Cat(T). The idea is that being ⌃(T)-isomorphic is the strictest notion of isomorphism for ⌃(T)-structures. ⌃(T)-isomorphisms preserve all features of structures expressible in terms of the symbols in ⌃(T). The notion of ⌃(T)-isomorphism is the standard notion of isomorphism in model theory.10 It is crucial that the above requirement allows that there are invertible morphisms in Cat(T), i.e. Cat(T)-isomorphisms, that are not ⌃(T)-isomorphisms. For example, gauge transformations serving as extra isomorphisms in the category of models of a potential-based formulation of classical electromagnetism are isomorphisms of this kind (cf. Weatherall, 2016a). Moreover, Cat(T) may also contain non-invertible morphisms such as homomor- phisms or embeddings. I will now define DCE and then unpack the definition step by step. Definition 4. T1 is DC-equivalent to T2 i↵ there are reconstruction functors F : Cat (T1) ! Cat (T2) G : Cat (T2) ! Cat(T1) constituting a (dual) equivalence between the categories Cat (T1) and Cat (T2). So in contrast to CE, the existence of arbitrary functors constituting a (dual) equivalence between categories of models is not su�cient for DCE. Roughly speak- ing, a reconstruction functor is a functor such that for every model A of the source theory, the corresponding model F(A) of the target theory can be reconstructed up to isomorphism from A. To reconstruct F(A) from A is to define F(A) on the basis of A. The reconstruction has to be uniform in the sense that the same definitions are used for all models. More precisely: Definition 5. A functor F : Cat(T1) ! Cat(T2) is a reconstruction functor i↵ there is a reconstruction manual � for ⌃(T2) in terms of ⌃(T1) such that for every object A in Cat(T1), F(A) is defined by � over A or a ⌃(T2)-isomorphic copy of F(A) is defined by � over A. The rest of this section is devoted to clarifying what reconstruction manuals are and what it means that a structure is defined over another structure by a recon- struction manual. 10For a definition of ⌃-isomorphism, see any model theory textbook, e.g. Hodges (1993, p. 5). 7 Reconstruction manuals tell us how to reconstruct structures of one signature from structures of another signature. They can be viewed as functions mapping the non-logical symbols of one signature to open formulas over the other signature. The free variables of these associated formulas need to be of the right type, of course. So a reconstruction manual presupposes an association between the types of the two signatures in question. In the general case of higher-order signatures, this can be made precise as follows. Definition 6. Let ⌃1 and ⌃2 be higher-order signatures. ↵ is an association of ⌃1-types with ⌃2-types i↵ ↵ maps every type of ⌃1 to a type of ⌃2 such that: (1) ↵ commutes with the product type constructor: ↵(⌧1 ⇥ ⌧2) = ↵(⌧1) ⇥ ↵(⌧2). (2) ↵ commutes with the power type constructor: ↵(}(⌧)) = }(↵(⌧)). Using this auxiliary notion, we can make precise what reconstruction manuals are. Definition 7. Let ⌃1 and ⌃2 be higher-order signatures. � is a reconstruction manual for ⌃1 in terms of ⌃2 i↵ there is an association ↵ of ⌃1-types with ⌃2-types such that: (1) � maps every basic sort � of ⌃1 to a ⌃2-formula �� with one free variable of type ↵(�). (2) � maps every predicate P in ⌃1 with simple type }(⌧) to a ⌃2-formula �P with a free variable of type ↵(⌧). (3) � maps every function symbol f in ⌃1 with input-type ⌧1 and output-type ⌧2 to a ⌃2-formula � f with two free variables of types ↵(⌧1), ↵(⌧2). (4) � maps every individual constant c in ⌃1 of basic sort � to a ⌃2-formula �c with a free variable of type ↵(�). With reconstruction manuals at hand, we can make precise what it means that the models of one theory can be defined from corresponding models of another theory. Definability of models is explained in terms of definability of their components. The latter notion is understood as usual: Suppose A is a ⌃-structure and ' an open formula over ⌃. Then a set X is defined by ' over A just in case X contains exactly those (tuples of) objects that satisfy ' in A, i.e. X = {a : A ✏ ' [a]}. The set defined by ' in A, i.e. the extension of ' in A, is denoted by ‘'A’. Similarly, the extension of a symbol S of ⌃ in A is denoted by ‘SA’. Using these notations, then next definition explicates when a model is defined over another model by means of a reconstruction manual. 8 Definition 8. Suppose A1 is a ⌃1-structure and A2 is a ⌃2-structure. A2 is defined by � over A1 i↵ � is a reconstruction manual for ⌃2 in terms of ⌃1 such that the following conditions hold: (1) for every symbol S of ⌃2 that is not an individual constant, S A2 is defined by � S over A1 (i.e. SA2 = �A1 S ). (2) for every individual constant c of ⌃2, {cA2} is defined by �c over A1 (i.e. {cA2} = �A1 c ). This completes the explication of DCE. Before investigating the properties of DCE, three remarks about possible modification are in order. First, using formu- las of higher-order languages in reconstruction manuals reflects a liberal attitude about which kinds of logico-mathematical constructions are admissible to recon- struct models. This liberality ties in with scientific practice. Working scientists do not restrict themselves to first-order constructions. For example, defining states over a C⇤-algebra is a higher-order construction: states are defined as certain functions from a C⇤-algebra to its underlying field C. However, using higher- order languages is not essential to the idea of DCE. So if one wishes to take a less liberal stance on admissible logical constructions for philosophical reasons, one can impose constraints on which kinds of formulas are allowed in reconstruction manuals (e.g. only first-order formulas). This will lead to stricter versions of DCE. Second, to go beyond formal equivalence, one can impose admissibility con- straints on reconstruction manuals and functors that take into consideration how formalisms are interpreted. A natural constraint would be to allow only recon- struction manuals that preserve meaningfulness in the sense that they map mean- ingful symbols of one theory to meaningful formulas of another theory. Also con- straints regarding empirical content or theoretical content beyond the empirical can be brought in at this stage. However, putting forward concrete formulations of preservation conditions for reconstruction functors falls outside the scope of this paper. But work devoted to this issue is already in progress. Third, there are cases in which it is not necessary to reconstruct the entire internal structure of models. It may su�ce to reconstruct only those parts of models that play a representational role. Such cases can be captured using the notion of partial reconstruction manuals. Roughly speaking, a partial reconstruc- tion manual maps the meaningful formulas of one theory to meaningful formulas of another theory. Explicating DCE with partial reconstruction manuals raises ques- tions about meaningfulness and interpretation that would lead us too far afield. Therefore, we will restrict our attention to the simpler case of full reconstruction manuals in this paper. 9 4 Properties of the new criterion To understand the new criterion better, it is useful to examine in which ways it di↵ers from CE and GDE and in which ways it is close them. 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 cri- terion 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 Section 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 (2016, Theorem 5.7). They specify two single-sorted first-order axiom systems: T1 := {9�1!xx = x} and T2 := {9�2!yy = y}[{8�2y (Q0y ! Qiy) : i 2 N} with signatures ⌃1 := {�1, P0, P1, . . .} and ⌃2 := {�2, Q0, Q1, . . .}, respectively. Elementary embeddings serve as morphisms in their categories of models. Barrett and Halvorson prove that T1 and T2 are C-equivalent but not GD-equivalent. T2 is stronger than T1 in virtue of its additional axioms. The reason why T1 and T2 are C-equivalent is that they have the same number of non-isomorphic 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: Proposition 1. The theories T1 and T2 are not DC-equivalent. Although this is only a toy example, it shows that, relative to CE, the definability condition built into DCE makes a di↵erence 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 (2017) 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 CE is stronger than 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.11 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 11In such cases, it would seem plausible that CE should be su�cient for DCE. Yet, it is not clear at all what it exactly means that morphisms fully encode the internal structure of models. However, to explicate this idea seems to be an interesting project. 10 general and more robust12 than the first one. 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 A1 and A2, there is an equivalence between the categories C1 and C2, where Ci has Ai as its sole object and the trivial identity automorphism of A i as its only arrow. In such cases, CE is trivially satisfied even if A1 and A2 are not definable from each other in any sense. In contrast, DCE is not necessarily satisfied as it explicitly takes into account definability. Proposition 2. There are theories with an up to isomorphism unique rigid model that are C-equivalent but not DC-equivalent. For instance, take a simple theory describing a social network with an up to iso- morphism unique rigid model (a finite graph) and a cosmological model that arises from general relativity by means of conditions singling out a unique spacetime manifold with no non-trivial isometries (i.e. where spacetime is highly asymmet- ric). 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, 2018, p. 13) 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 non-trivial strengthening of CE, ruling out sev- eral 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 prac- tice one can extract proofs of DC-equivalences. The reason is that proofs of (dual) equivalences between concrete categories often establish more than the mere exis- tence 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 Stones space from a given Boolean 12The example by Barrett and Halvorson (2016) is not very robust in the following sense. Although T1 and T2 are not GD-equivalent in classical first-order logic, it turns out that they are GD-equivalent when infinitely long formulas with countable conjunctions and disjunctions are allowed in definitions. Thanks to Hajnal Andréka and István Németi for sharing their proof. 11 algebra and vice versa. Another example is Gelfand duality, where one defines a compact Hausdor↵ space from any given unital commutative C⇤-algebra A (namely the space of non-vanishing C⇤-algebra homomorphisms from A to C with the spectral topology) and one defines a unital commutative C⇤-algebra from any given compact Hausdor↵ space X (namely the algebra of continuous functions from X to C). 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, 2005, p. 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 be- tween formulations of Hamiltonian mechanics and Lagrangian mechanics (Barrett, 2017) a case of DCE? Does the Gelfand-Naimark representation theorem (Gelfand and Naimark, 1943) allow us to prove that the Hilbert space formalism and the C⇤- algebra formalism of quantum mechanics are DC-equivalent? Do reconstruction theorems relating di↵erent approaches to quantum field theories (e.g. Wightman, 1956; Osterwalder and Schrader, 1973, 1975) give rise to DC-equivalences? 4.3 DCE and GDE di↵er in the presence of surplus structure A major di↵erence 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 a particular kind of auxiliary structure, namely coordinate systems. Although introducing co- ordinates is an insignificant extension of a formalism as far as representational capacities are concerned, it makes a big di↵erence for GDE: models that are not GD-equivalent can become GD-equivalent when equipped with coordinate sys- tems. The reason is that the presence of a coordinate system allows 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 12 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 generalised inner products (i.e. non-degenerate symmetric bilinear forms).13 This is a slight simplification. Strictly speaking, Minkowski and Euclidean spaces should be treated as a�ne spaces—rather than vector spaces—equipped with generalised inner products.14 But since this would unnecessarily complicate our presentation without a↵ect- ing any results, the chosen simplification is unproblematic. It is also common in physics to simplify in this way (cf. Naber, 2012). So we take an n-dimensional Minkowski space (V, ⌘) to consist of an n- dimensional vector space V = (V, �, �) over the field R of real numbers together with a Minkowskian inner product ⌘ : V ⇥ V ! R of metric signature (1, n � 1). An n-dimensional Euclidean space (V, h·, ·i) is an n-dimensional real vector space V endowed with a Euclidean inner product h·, ·i : V ⇥ V ! R 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 (cf. Malament, 2009, Section 3.2), 4-dimensional Minkowski geometry yields the theory of spacetime underlying spe- cial relativity. 4-dimensional Euclidean geometry, when physically interpreted, as- cribes a very di↵erent structure to spacetime. But more than that: these geome- tries should count as inequivalent irrespective of concrete physical applications because their generalised inner products are very di↵erent from a mathematical point of view. They encode very di↵erent notions of distance and angles. The cri- teria of GDE and DCE both capture this di↵erence when the models of Euclidean and Minkowski geometry are not endowed with coordinate systems: Proposition 3. (1) MG n and EG n are not DC-equivalent. (2) MG n and EG n are not GD-equivalent. However, we will now see that if we endow their models with coordinate sys- tems, 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 characterisation of fundamental spacetime structure or other 13So Minkowski spaces have a first-order signature comprising two basic sort symbols (for scalars and vectors) as well as various operation symbols (for the field operations, the vector space operations and the generalised inner product). The signature of Euclidean spaces only di↵ers from that of Minkowski spaces in having a di↵erent symbol for the inner product. 14For a detailed exposition of Minkowski and Euclidean spaces as metric a�ne spaces see Malament (2009, Section 2). 13 foundational issues, they still play an important role in practice. Usually, one cannot apply geometry empirically without choosing a reference frame and an as- sociated coordinate system. For a defence of the legitimacy of a coordinate-based approach for foundational work see Wallace (2016). We need a bit of terminology to specify the coordinatised models. A linear coordinate system for an n-dimensional vector space V is an n-tuple of coordinate functions (f0, . . . , fn�1), where fi : V ! R maps every vector v 2 V to a real number serving as the i-th coordinate of v (0  i < n), such that the function f : V ! Rn defined by f(v) := (f0(v), . . . , fn�1(v)) is a vector space isomor- phism from V to the real coordinate space Rn.15 We say that a linear coordinate system (f0, . . . , fn�1) for V is a Lorentz coordinate system for an n-dimensional Minkowski space M = (V, ⌘) i↵ f is an isometric isomorphism from M to the real coordinate space (Rn, ⌘ std ) with the standard Minkowski inner product ⌘ std on R n, which takes the following form in the standard coordinates xi on Rn (mapping elements of Rn to their i-th components): ⌘ std (u, v) = x0(u) · x0(v) � . . . � xn�1(u) · xn�1(v). (1) It immediately follows that all Lorentz coordinate systems for M are related to each other by Lorentz transformations. Analogously, (f0, . . . , fn�1) is a Euclidean coordinate systems for an n-dimensional Euclidean space E = (V, h·, ·i) i↵ f is an isometric isomorphism from E to the real coordinate space (Rn, h·, ·i std ) with the standard Euclidean inner product on Rn, which is given by: hu, vi std = x0(u) · x0(v) + . . . + xn�1(u) · xn�1(v). (2) Now we can specify the models of Minkowski and Euclidean geometry extended with coordinate systems (MG+ n and EG+ n ). The models of MG+ n are those struc- tures (V, f0, . . . , fn�1, ⌘) such that (V, ⌘) is a model of MG n and (f0, . . . , fn�1) is a Lorentz coordinate system for (V, ⌘). The models of EG+ n are those structures (V, f0, . . . , fn�1, h·, ·i) such that (V, h·, ·i) is a model of EG n and (f0, . . . , fn�1) is a Euclidean coordinate system for (V, h·, ·i).16 With these specifications at hand, one can prove that: Proposition 4. MG+ n and EG+ n are GD-equivalent (for n � 2). To get an impression of what is going on here, consider a model M = (V+, ⌘) of MG+ n , where V+ = (V, f0, . . . , fn�1). It follows that M is a definitional expansion of V+ because (f0, . . . , fn�1) is a Lorentz coordinate system for M and hence M satisfies: ⌘(u, v) = f0(u) · f0(v) � . . . � fn�1(u) · fn�1(v). (3) 15Note that choosing a linear coordinate system for a vector space amounts to the same as choosing an ordered basis. Hence, coordinate systems are often simply defined as ordered bases. 16Note that for every model of MGn there are infinitely many models of MG + n . The same holds for EGn and EG + n . 14 Now define a Euclidean inner product h·, ·i over V+: hu, vi = f0(u) · f0(v) + . . . + fn�1(u) · fn�1(v). (4) This definition can be formulated in the first-order language of n-dimensional vector spaces with coordinate functions. Then E := (V+, h·, ·i) is a model of EG+ n and also a definitional expansion of V+. Hence, M and E are definitional expansions of the same underlying structure V+ and, therefore, have a common definitional expansion (V+, ⌘, h·, ·i). Thus, M and E are definitionally equivalent. Let us now see how a di↵erent analysis of the relationship between MG+ n and 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 MG+ n ) and the model with the new coordinate system will represent exactly the same physical situation. This suggests to specify the categories of models of MG+ n and EG+ n in such a way that choices of coordinates may vary under morphisms. In particular, we should not take ⌃(MG+ n )-isomorphisms and ⌃(EG+ n )-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—i.e. 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 Cat(MG+ n ) in such a way that h : (V, f0, . . . , fn�1, ⌘) ! (V0, f 00, . . . , f 0n�1, ⌘0) is a morphism in Cat(MG+ n ) i↵ h is a bijection from V to V 0 that is an a�ne map17 from V to V0 preserving Minkowski inner products (i.e. ⌘(u, v) = ⌘0(h(u), h(v)) for all u, v 2 V ) and for technical reasons we also require that h maps each scalar to itself. The morphisms in Cat(EG+ n ) are specified analogously. It follows that, the automorphism group of each model in Cat(MG+ n ) is the Poincaré group, whereas the automorphism group of models in Cat(EG+ n ) is the Euclidean group. The fact that the Poincaré group and the Euclidean group are not isomorphic implies that: Proposition 5. MG+ n and EG+ n are not DC-equivalent (for n � 2). We can say more when we consider which formulas count as meaningful in MG+ n and 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 ⌃(MG+ n ) with n free variables invariant under the morphisms of Cat(MG+ n ) just in case for all morphisms h : M ! M0 in Cat(MG+ n ), an n-tuple 17h is an a�ne map from a vector space V = (V, �, �) to another V0 = (V 0, �0, �0) i↵ there is a vector space isomorphism H from V to V0 and a w 2 V such that for all v 2 V : h(v) = H(v)�0w. 15 (a1, . . . , an) satisfies ' in M i↵ (h(a1), . . . , h(an)) satisfies ' in M0. It follows that the formula z = f0(u) · f0(v) + . . . + fn�1(u) · fn�1(v) (5) is not invariant under the morphisms of Cat(MG+ n ).18 Hence, formula (5) is not meaningful in MG+ n . So although formula (5) defines a Euclidean inner product over any given model of MG+ n , this inner products will not count as meaningful in MG+ n . Thus, any reconstruction manual for ⌃(EG+ n ) in terms of ⌃(MG+ n ) yielding (5) as a translation of hu, vi = z does not preserve meaningfulness. An analogous conclusions holds for reconstruction manuals for ⌃(MG+ n ) in terms of ⌃(EG+ n ). 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 generalisation of GDE for theories of a certain kind. Barrett and Halvorson (2016) have shown that GD-equivalent first- order theories with elementary embeddings as morphisms are C-equivalent. Their proof can be generalised 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. Theorem 1. Suppose T1 and T2 are theories with disjoint signatures and suppose the morphisms in Cat(T i ) are precisely elementary embeddings (1  i  2). If T1 and T2 GD-equivalent, then T1 and T2 are DC-equivalent. 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 struc- ture. This idea furthermore suggests that DCE should also not be much wider 18In contrast, the formula z = f 0 (u) · f0(v) � . . . � fn�1(u) · fn�1(v) is invariant under the morphisms of Cat(MG+n ) although coordinate functions vary from model to model. This formula is meaningful in MG+n . So a formula may be meaningful even if the terms and function symbols occurring in it are not meaningful. 16 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 paper. Theorem 2. Suppose T1 and T2 are theories with disjoint signatures and suppose the isomorphisms in Cat(T i ) are precisely the ⌃(T i )-isomorphisms (1  i  2). If T1 and T2 are DC-equivalent, then T1 and T2 are GD-equivalent up to external auxiliaries. The qualification ‘up to external auxiliaries’ concerns auxiliary vocabulary intro- duced in GD-expansions rather than auxiliary vocabulary of the theories them- selves. Every GD-expansion to a signature with new sorts also introduces aux- iliary 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” auxil- iary vocabulary to be recovered. More precisely, T1 and T2 are GD-equivalent up to external auxiliaries i↵ they have stepwise GD-expansions E1 and E2 that coincide insofar as one ignores external auxiliary vocabulary on both sides, i.e. E1|⌃(T1)[⌃(T2) = E2|⌃(T1)[⌃(T2). 19 So for theories with standard model-theoretic isomorphisms, DCE di↵ers from GDE only in not requiring that auxiliary symbols used for reconstructing the sorts of one theory from 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’. Definition 9. T1 and T2 are DC-equivalent with definable inner isomor- phisms i↵ there are functors F : Cat (T1) ! Cat (T2), G : Cat (T2) ! Cat(T1) and reconstruction manuals � for ⌃(T2) in terms of ⌃(T1) and for ⌃(T1) in terms of ⌃(T2) establishing a DCE between T1 and T2 such that (1) there is a family of ⌃(T1)-formulas defining a ⌃(T1)-isomorphism from A1 to GF(A1) for all A1 2 Mod(T1) and (2) there is a family of ⌃(T2)-formulas defining a ⌃(T2)-isomorphism from A2 to FG(A2) for all A2 2 Mod(T2) such that (3) these isomorphisms are compatible with each other and with � and . 19E|⌃ := {A|⌃ : A 2 E}, where A|⌃ is the reduct of A to ⌃ (cf. Hodges, 1993, p. 9). 17 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 (1986). For a more detailed formulation of this condition see Definition B.8, Ap- pendix B. Theorem 3. Suppose T1 and T2 are theories with disjoint signatures and suppose the isomorphisms in Cat(T i ) are precisely the ⌃(T i )-isomorphisms (1  i  2). If T1 and T2 are DC-equivalent with definable inner isomorphisms, then T1 and T2 are GD-equivalent. 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 (cf. 2018, p. 14). 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 su�ce. 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 con- dition 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 (2016a) examples, di↵erent potential-based models A1, A2 that are related by a gauge transformation will be mapped to the same model A by the composite auto-equivalence functor. How- ever, the gauge transformations from A1 to A and from A2 to A are not induced by uniformly defined bijections in the way the many-sorted Ahlbrandt-Ziegler condition would require (cf. Definition B.8, Appendix 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. 5 Conclusions Let me sum up the core results of this paper. I have argued that choices of mor- phisms and the internal structure of models both matter when it comes to pos- sible interpretations of a formalism. I have pointed out that GDE does not take into account morphisms and CE does not take into account the internal struc- ture of models. I have presented a new criterion, namely DCE, which connects the category-theoretic approach and the definability-theoretic approach to for- mal equivalence. DCE is a strengthening of CE with a definability constraint on 18 equivalence functors. It is also closely related to GDE in cases where morphisms preserve all definable features of models. DCE takes into account the internal structure of models as well as choices of morphisms. Thereby, it allows a more nuanced analysis of scientific theories. An important task for future research is to supplement DCE with preservation conditions concerning interpretation by imposing constraints on which reconstruc- tion manuals and functors are admissible. One can specify preservation conditions corresponding to di↵erent levels of interpretation: (1) preservation of meaning- fulness for pre-interpreted formalisms, (2) preservation of empirical content for empirically interpreted formalisms and (3) preservation of theoretical content for formalisms that are endowed with a full-blown interpretation going beyond the empirical. Furthermore, one can weaken the notion of reconstruction functor by al- lowing partial reconstruction manuals, in which non-meaningful features of models do not need to be reconstructed. Working out these ideas in detail and exploring their consequences seems to be a promising direction for future research. 19 Appendix A GD-expansions Suppose ⌃ and ⌃+ are higher-order signatures with ⌃ ⇢ ⌃+ and C and E are classes of ⌃-structures and ⌃+-structures, respectively. Definition A.1. E is a GD-expansion of C to ⌃+ by � i↵ � is a set of explicit definitions and sort-definitions of the symbols in ⌃+ \ ⌃ in terms of ⌃ such that (1) all A 2 C satisfy the admissibility conditions of the definitions in �; (2) all A+ 2 E satisfy �; (3) C = {A+|⌃ : A+ 2 E}. For the form of sort-definitions see Barrett and Halvorson (2016, Section 4.1). Definition A.2. E is a stepwise GD-expansion of C to ⌃+ by (�1, . . . ,�n) i↵ there is a sequence (E0, E1, . . . , En) of classes of structures of signatures ⌃0 ⇢ ⌃1 ⇢ . . . ⇢ ⌃n such that (1) ⌃0 = ⌃ and ⌃n = ⌃ +; (2) E0 = C and En = E and (3) E i is a GD-expansion of E i�1 to ⌃i by �i (for 1  i  n). Appendix B Proofs Proposition 1. The theories T1 and T2 are not DC-equivalent. Proof. Note that, up to ⌃2-isomorphism, there is only one model A⇤2 of T2 such that the predicate Q0 has a non-empty extension. Suppose for reductio that there are reconstruction functors F : Cat (T1) ! Cat (T2) and G : Cat (T2) ! Cat(T1) constituting a (dual) equivalence. Then for every A1 ✏ T1 there is an A2 ✏ T2 such that A2 is ⌃2-isomorphic to F (A1) and A2 is definable from A1 by some reconstruction manual �. It follows that (*) there can only be one model A⇤1 ✏ T1 up to ⌃1-isomorphism such that � A⇤1 Q0 6= ;, namely A⇤1 ⇠= G (A ⇤ 2). The formula � Q0 contains only finitely many of the predicates P0, P1, . . . of ⌃1. Therefore, we get many models A of T1 such that A is not ⌃1-isomorphic to G (A⇤2) but � A Q0 6= ;. We achieve this by varying the extensions of those P i not contained in the formula � Q0, while using the same extension as in G (A⇤2) for the predicates contained in � Q0. Thus we get a contradiction to (*). 20 Proposition 2. There are theories with an up to isomorphism unique rigid model that are C-equivalent but not DC-equivalent. Proof. Let T1 be a theory with an up to isomorphism unique finite rigid model (e.g. an asymmetric graph) and let T2 be a theory with an up to isomorphism unique infinite rigid model (e.g. a spacetime manifold without non-trivial isome- tries). Then T1 and T2 are trivially C-equivalent. But they are not DC-equivalent. It is su�cient to show that no infinite structure is definable over a finite structure. Let A be a structure such that every basic type has a finite extension. Note that if ⌧1 and ⌧2 are types with finite extensions, then so are the product type ⌧1 ⇥ ⌧2 and the power types } (⌧ i ). Thus, every type has a finite extension. Therefore, every ⌃(A)-formula can only have a finite extension under A. Hence, no infinite set is definable over A. Proposition 3. (1) MG n and EG n are not DC-equivalent. (2) MG n and EG n are not GD-equivalent. Proof. The ⌃(MG n )-automorphism group of the models of MG n is not isomorphic to the ⌃(EG n )-automorphism group of the models of EG n . Since GDE preserves automorphism groups, MG n and EG n cannot be GD-equivalent. For analogous reasons, they cannot be DC-equivalent either. Proposition 4. MG+ n and EG+ n are GD-equivalent (for n � 2). Proof. Let VEC+ be the set of all structures (V, f0, . . . , fn�1) such that V is an n-dimensional vector space and (f0, . . . , fn�1) is a linear coordinate system for V. It su�ces to show that both Mod(MG+ n ) and Mod(EG+ n ) are GD-expansions of VEC+. Let M = (V+, ⌘) be a model of MG+ n , where V+ = (V, f0, . . . , fn�1). Then (f0, . . . , fn�1) is a Lorentz coordinate system for M. This implies that M satisfies the definition: ⌘(u, v) = f0(u) · f0(v) � . . . � fn�1(u) · fn�1(v). Moreover, it follows that V+ 2 VEC+. Conversely, if V+ 2 VEC+, one can define a Minkowskian inner product ⌘ over V+ using the equation above. Then (V+, ⌘) 2 Mod(MG+ n ). Hence, Mod(MG+ n ) is a GD-expansion of VEC+. Analogously, one shows that Mod(EG+ n ) is a GD-expansion of VEC+. Proposition 5. MG+ n and EG+ n are not DC-equivalent (for n � 2). Proof. There cannot be reconstruction functors establishing a (dual) equivalence between Cat(MG+ n ) and Cat(EG+ n ) because the Poincaré group is not isomorphic to the Euclidean group. 21 Definition B.1. A stepwise GD-expansion E of C to ⌃+ by (�1, . . . ,�n) uses only subsorts i↵ all basic sorts of ⌃+ are introduced as subsorts of types of ⌃ by (�1, . . . ,�n). Lemma B.1. If T1 and T2 are GD-equivalent, there are stepwise GD-expansions E1 and E2 of Mod(T1) and Mod(T2) using only subsorts such that E1 = E2. Theorem 1. Suppose T1 and T2 are theories with disjoint signatures and suppose the morphisms in Cat(T i ) are precisely elementary embeddings (1  i  2). If T1 and T2 are GD-equivalent, then T1 and T2 are DC-equivalent. Proof. By Lemma B.1, Mod(T1) and Mod(T2) have stepwise GD-expansions E1 and E2 to some signature ⌃ + by (�11, . . . ,� 1 n ) and (�21, . . . ,� 2 m ) using only sub- sorts such that E1 = E2. This gives rise to reconstruction manuals. Let � map ev- ery symbol S of ⌃(T2) to the open ⌃(T1)-formula used to define S in (� 1 1, . . . ,� 1 n ). Then � is a reconstruction manual for ⌃(T2) in terms of ⌃(T1). Analogously, we get a reconstruction manual for ⌃(T1) in terms of ⌃(T2). Let Cat(E i ) be the category having the structures of E i as objects and ele- mentary embeddings between them as morphisms (1  i  2). Then the reduct functors P1 : Cat(E1) ! Cat(T1) and P2 : Cat(E2) ! Cat(T2) are equivalence functors, as described in Barrett and Halvorson (2016, Section 5). By the axiom of choice, there are functors P �11 and P �1 2 essentially inverse to P1 and P2. Since Cat(E1) = Cat(E2), we can define functors F := P2P �1 1 : Cat(T1) ! Cat(T2) and G := P1P �1 2 : Cat(T2) ! Cat(T1). F and G constitute an equivalence of cat- egories between. It is a matter of routine to check that F and G are reconstruction functors w.r.t. the reconstruction manuals � and . In order to prove Theorem 2, we need several lemmata and definitions. Lemma B.2. Suppose ↵ and ↵0 both are associations of ⌃1-types with ⌃2-types satisfying (1) in Definition 7 with respect to the same reconstruction manual � for ⌃1 in terms of ⌃2. Then for every type ⌧ of ⌃1: ↵(⌧) = ↵ 0(⌧). So given a type ⌧ of ⌃1, a reconstruction manual � for ⌃1 in terms of ⌃2 associates a unique type �(⌧) of ⌃2 with ⌧. Definition B.2. Let � be a reconstruction manual for ⌃⇤ in terms of ⌃ and let T be a theory with signature ⌃. Then we say that � is formally admissible w.r.t. T2 i↵ for every model A of T : (1) for every basic sort � of ⌃⇤, � � defines a non-empty set over A. (2) for every function symbol f of ⌃⇤, � f defines a function over A. (3) for every individual constant c of ⌃⇤, � c defines a singleton over A. 22 From now on suppose that (a) T and T ⇤ have disjoint signatures ⌃ and ⌃⇤ and (b) � is a reconstruction manual for ⌃⇤ in terms of ⌃ that is formally admissible w.r.t. T . Definition B.3. ⌃+ is a �-extension of ⌃ by external auxiliaries i↵ ⌃+ contains the symbols of ⌃ as well as ⌃⇤ and (1) for every basic sort � in ⌃⇤, ⌃+ contains exactly one new function symbol i � with � as input-type and �(�) as output-type. (2) for every types ⌧ of ⌃⇤, ⌃+ contains exactly one new function symbol j ⌧ with ⌧ as input-type and �(⌧) as output-type. From now on let ⌃+ be a �-extension of ⌃ by external auxiliaries. Definition B.4. Let A 2 Mod(T). Then we call the ⌃+-structure A+ with the following properties the canonical expansion of A to ⌃+ induced by �: (1) A+|⌃ = A. (2) For every symbol S in ⌃⇤ that is not an individual constant: SA + = �A S . (3) For every individual constant c in ⌃⇤: {cA + } = �A c . (4) For every basic sort � in ⌃⇤: iA + � is the identity on �A � . (5) For every type ⌧ over ⌃⇤: jA + ⌧ is the identity on D ⌧ , where D ⌧ is defined as follows: (a) if ⌧ is a basic sort of ⌃⇤, then D ⌧ = �A ⌧ . (b) if ⌧ = ⌧1 ⇥ ⌧2 is a product type of ⌃⇤, then D⌧ = D⌧1 ⇥ D⌧2. (c) if ⌧ = }(⌧ 0) is a power type of ⌃⇤, then D ⌧ = P(D ⌧ 0). Definition B.5. The canonical expansion of Mod(T) to ⌃+ induced by � is the isomorphic closure of {A+ : A 2 Mod(T)}, where A+ is the canonical expansion of A to ⌃+ induced by � for A 2 Mod(T). Notation. In the following it is useful to write variables with their type as super- script (e.g. ‘x⌧ ’) to avoid confusions. Lemma B.3. The canonical expansion of Mod(T) to ⌃+ induced by � is a step- wise GD-expansion of Mod(T) to ⌃+ by (�sorts� ,� inj � ,� const � ), where (1) �sorts� consists of subsort-definitions for all basic sorts � of ⌃ ⇤: 8x�(�)(� � (x�(�)) $ 9y� i � (y�) = x�(�)) ^ 8y�1 8y � 2 (i�(y � 1 ) = i�(y � 2 ) ! y � 1 = y � 2 ), 23 (2) � inj � consists of definitions of the injection symbols j⌧ for types ⌧ of ⌃ ⇤: 8x⌧ 8z�(⌧)(j ⌧ (x⌧ ) = z�(⌧) $ ' ⌧ (x⌧ , z�(⌧))), where the definiens ' ⌧ (x⌧ , z�(⌧)) is a ⌃ [ ⌃(�sorts� )-formula for every type ⌧ of ⌃⇤, recursively defined as follows: (a) if ⌧ is a basic sort of ⌃⇤, then ' ⌧ (x⌧ , z�(⌧)) is the formula z�(⌧) = i ⌧ (x⌧ ). (b) if ⌧ = ⌧1 ⇥ ⌧2 is a product type of ⌃⇤, then '⌧ (x⌧ , z�(⌧)) is the formula 9x⌧11 9x ⌧2 2 (x ⌧ = hx⌧11 , x ⌧2 2 i^9z �(⌧1) 1 9z �(⌧2) 2 ('⌧1(x ⌧1 1 , z �(⌧1) 1 )^'⌧2(x ⌧2 2 , z �(⌧2) 2 )^ z�(⌧) = hz�(⌧1)1 , z �(⌧2) 2 i)). (c) if ⌧ = }(⌧ 0) is a power type of ⌃⇤, then ' ⌧ (x⌧ , z�(⌧)) is the formula z�(⌧) = {u�(⌧ 0) : 9v⌧ 0 (x⌧ (v⌧ 0 ) ^ ' ⌧ 0(v⌧ 0 , u�(⌧ 0)))}. (3) �const� consists of the following definitions: (a) 8x⌧ (P(x⌧ ) $ � P (j ⌧ (x⌧ ))), for every predicate P in ⌃⇤ of type ⌧. (b) 8x⌧18y⌧2(f(x⌧1) = y⌧2 $ � f (j ⌧1(x ⌧1), j ⌧2(y ⌧2))), for every function symbol f in ⌃⇤ with input-type ⌧1 and output-type ⌧2. (c) 8x�(c = x� $ � c (j ⌧ (x⌧ ))), for every individual constant c of basic sort � in ⌃⇤. Lemma B.4. Suppose the following: H : Cat(T) ! Cat(T ⇤) is a reconstruction functor with reconstruction manual �; the isomorphisms in Cat(T ⇤) are precisely the ⌃⇤-isomorphisms; A is a model of T; A+ is the canonical expansion of A to ⌃+ induced by �. Then H(A) is ⌃⇤-isomorphic to A+|⌃⇤. Lemma B.5. Suppose E is the canonical expansion of Mod(T) to ⌃+ induced by �, A 2 E and (A|⌃)+ is the canonical expansion of A|⌃ to ⌃+ induced by �. Then A is ⌃+-isomorphic to (A|⌃)+. Theorem 2. Suppose T1 and T2 are theories with disjoint signatures and suppose the isomorphisms in Cat(T i ) are precisely the ⌃(T i )-isomorphisms (1  i  2). If T1 and T2 are DC-equivalent, then T1 and T2 are GD-equivalent up to external auxiliaries. Proof. Suppose T1 and T2 are DC-equivalent. Let ⌃1 and ⌃2 be their signa- tures. Then there are reconstruction functors F : Cat (T1) ! Cat (T2) and G : Cat (T2) ! Cat(T1) constituting a (dual) equivalence accompanied by recon- struction manuals � for ⌃2 over ⌃1 and for ⌃1 over ⌃2. It follows that � and are formally admissible w.r.t. T1 and T2, respectively. Let ⌃ + 1 and ⌃ + 2 be �- and -extensions of ⌃1 and ⌃2 by external auxiliaries, respectively. Now let E1 and E2 24 be the canonical expansions of Mod(T1) and Mod(T2) to ⌃ + 1 and ⌃ + 2 induced by � and . We know from Lemma B.3 that E1 and E2 are stepwise GD-expansions of Mod(T1) and Mod(T2), respectively. We show that E1|⌃1[⌃2 = E2|⌃1[⌃2. Suppose A 2 E1|⌃1[⌃2. Then there is a B 2 E1 such that A = B|⌃1[⌃2. Moreover, A|⌃1 2 Mod(T1). Let (A|⌃1) + be the canonical expansion of A|⌃1 to ⌃+1 induced by �. Check that the following statements hold. (1) B is ⌃+1 -isomorphic to (A|⌃1) + (by Lemma B.5 and B|⌃1 = A|⌃1). (2) F(A|⌃1) is ⌃2-isomorphic to (A|⌃1) +|⌃2 (Lemma B.4). (3) A|⌃2 is ⌃2-isomorphic to F(A|⌃1) (by 1, 2 and B|⌃2 = A|⌃2). (4) A|⌃1 is ⌃1-isomorphic to GF(A|⌃1) (because F and G constitute a (dual) equivalence and isomorphisms in Cat(T i ) are ⌃(T i )-isomorphisms). (5) GF(A|⌃1) is ⌃1-isomorphic to F(A|⌃1)+|⌃1, where F(A|⌃1) + is the canon- ical expansion of F(A|⌃1) induced by (Lemma B.4). (6) A|⌃1 is ⌃1-isomorphic to F(A|⌃1) +|⌃1 (by 4 and 5). (7) A is ⌃1 [ ⌃2-isomorphic to F(A|⌃1)+|⌃1[⌃2 (by 3 and 6). Since F(A|⌃1) 2 Mod(T2), its canonical expansion F(A|⌃1)+ by is in E2. This implies F(A|⌃1)+|⌃1[⌃2 2 E2|⌃1[⌃2. E2|⌃1[⌃2 is closed under ⌃1[⌃2-isomorphism because E2 is closed under ⌃ + 2 -isomorphism. Hence, A 2 E2|⌃1[⌃2. The proof for the other direction is analogous. Definition B.6. We say that � is a family of formulas defining inner iso- morphisms of T1-models w.r.t. F,� and G, i↵ (1) � maps every basic sort �1 of ⌃(T1) to a ⌃(T1)-formula ��1(x �1, y� (�1)). (2) for every basic sort �1 of ⌃(T1) and every A1 2 Mod(T1), �A1 �1 is a bijection from �A11 to � GF(A1) 1 ; and these bijections constitute a ⌃(T1)-isomorphism from A1 to GF(A1). Definition B.7. Let ⌃(T1) + be a �-extension of ⌃(T1) by external auxiliaries, let E1 be the canonical expansion of Mod(T1) to ⌃(T1) + induced by � and let � be a family of formulas defining inner isomorphisms of T1-models w.r.t. F,� and G, . Then the �-expansion of Mod(T1) to ⌃(T1) + [ ⌃(T2)+ induced by � and is the stepwise GD-expansion of E1 to ⌃(T1) + [ ⌃(T2)+ by (�i ,� inj ), where � inj is as in Lemma B.3 and � i comprises definitions of the following form for all basic sorts �1 of ⌃(T1): 8x�18y (�1)(i �1(x �1) = y (�1) $ � �1(x �1, j (�1)(y (�1)))) (Def-i �1) 25 Definition B.8. T1 and T2 are DC-equivalent with definable inner isomor- phisms i↵ there are functors F : Cat (T1) ! Cat (T2), G : Cat (T2) ! Cat(T1) and reconstruction manuals � for ⌃(T2) in terms of ⌃(T1) and for ⌃(T1) in terms of ⌃(T2) establishing a DCE between T1 and T2 such that the many-sorted Ahlbrandt-Ziegler condition holds: (1) there is a family of formulas � defining inner isomorphisms of T1-models w.r.t. F,� and G, and (2) there is a family of formulas �̃ defining inner isomorphisms of T2-models w.r.t. G, and F,� such that (3) these isomorphisms are compatible with each other and with � and in the following sense: (a) for every model B1 of the �-expansion of Mod(T1) to ⌃(T1)+ [⌃(T2)+ induced by � and and all basic sorts �2 of ⌃(T2): j B1 �(�2) � iB1 �2 = �̃B1 �2 . (b) for every model B2 of the �̃-expansion of Mod(T2) to ⌃(T2)+ [⌃(T1)+ induced by � and and all basic sorts �1 of ⌃(T1): j B2 (�1) � iB2 �1 = �B2 �1 . Theorem 3. Suppose T1 and T2 are theories with disjoint signatures and suppose the isomorphisms in Cat(T i ) are precisely the ⌃ i -isomorphisms (1  i  2). If T1 and T2 are DC-equivalent with definable inner isomorphisms, then T1 and T2 are GD-equivalent. Proof. Let ⌃1,⌃2 be the signatures of T1, T2. There are functors F, G, reconstruc- tion manuals �, and stepwise GD-expansions E1, E2 to extended signatures ⌃+1 ,⌃ + 2 as in the proof of Theorem 2 and we know that E1|⌃1[⌃2 = E2|⌃1[⌃2. Moreover, there are families of formulas � and �̃ defining inner isomorphisms of T1-models and T2-models, respectively. Note that, for every basic sort �1 and every type ⌧1 of ⌃1, the auxiliary function symbols i �1 and j⌧1 are in ⌃ + 2 but not in ⌃ + 1 . Analogously, for every basic sort �2 and every type ⌧2 of ⌃2, the auxiliary function symbols i�2 and j⌧2 are in ⌃ + 1 but not in ⌃+2 . Moreover, that is the only di↵erence between ⌃ + 1 and ⌃ + 2 . Let E+1 be the �-expansion of Mod(T1) to ⌃ + 1 [ ⌃ + 2 induced by � and and let E+2 be the �̃-expansion of Mod(T2) to the same signature. By definition, E + i is a stepwise GD-expansion of E i (1  i  2). We have to show that E+1 = E + 2 . It is su�cient if E+2 ✏ Def-i�1 for �1 in ⌃1 and E + 1 ✏ Def-i�2 for �2 in ⌃2 because the definitions of j ⌧1 and j⌧2 are the same for E + 1 and E + 2 . That E + 2 ✏ Def-i�1 and E + 1 ✏ Def-i �2 follows directly from the many-sorted Ahlbrandt-Ziegler condition. 26 References Ahlbrandt, G. and M. Ziegler (1986). Quasi-finitely axiomatizable totally cate- gorical theories. Annals of Pure and Applied Logic 30, 63–83. Andréka, H., J. Madarász, and I. Németi (2008). Defining new universes in many- sorted logic. Manuscript. Andréka, H. and I. Németi (2014). Comparing theories: The dynamics of changing vocabulary. In S. Smets and A. Baltag (Eds.), Johan van Benthem on Logic and Information Dynamics, pp. 143–172. Cham: Springer. Awodey, S. (1997). Logic in Topoi: Functorial Semantics for Higher-Order Logic. Chicago. PhD Dissertation. Awodey, S. (2006). Category theory. Oxford: Oxford University Press. Barrett, T. (2017). Equivalent and Inequivalent Formulations of Classical Me- chanics. British Journal for the Philosophy of Science. Forthcoming. Barrett, T. (2018). What do symmetries tell us about structure? Manuscript. Barrett, T. and H. Halvorson (2016). Morita equivalence. The Review of Symbolic Logic 9(3), 556–582. Barrett, T. and H. Halvorson (2017). From geometry to conceptual relativity. 82, 1043–1063. Barrett, T., S. Rosenstock, and J. Weatherall (2015). On Einstein Algebras and Relativistic Spacetimes. Studies in History and Philosophy of Modern Physics 52B, 309–316. Co↵ey, K. (2014). Theoretical Equivalence as Interpretive Equivalence. British Journal for the Philosophy of Science 65(4), 821–844. Feintzeig, B. (2017). Deduction and definability in infinite statistical systems. Synthese. Gelfand, I. and M. Naimark (1943). On the imbedding of normed rings into the ring of operators in hilbert space. Matematiceskij sbornik 54(2), 197–217. Halvorson, H. (2016). Scientific Theories. In Oxford Handbook of the Philosophy of Science. Oxford University Press. Halvorson, H. and D. Tsementzis (2017). Categories of Scientific Theories. In E. Landry (Ed.), Categories for the Working Philosopher. Oxford: Oxford Uni- versity Press. 27 Hodges, W. (1993). Model Theory. Cambridge: Cambridge University Press. Hudetz, L. (2015). Linear Structures, Causal Sets and Topology. Studies in History and Philosophy of Modern Physics. Hudetz, L. (2017). The semantic view of theories and higher-order languages. Synthese. Ismael, J. and B. C. van Fraassen (2003). Symmetry as a guide to superfluous theoretical structure. In K. Brading and E. Castellani (Eds.), Symmetries in Physics: Philosophical Reflections., pp. 371–92. Cambridge: Cambridge Univer- sity Press. Johnstone, P. (2002). Sketches of an Elephant: A Topos Theory Compendium. Volumes I, II. Oxford: Oxford University Press. Landry, E. (2007). Shared structure need not be shared set-structure. Syn- these 158(1), 1–17. Lefever, K. and G. Székely (2018). Comparing classical and relativistic kinematics in first-order logic. Logique et Analyse 61(241), 57–117. MacLane, S. (1998). Categories for the working mathematician (2 ed.). New York: Springer. Malament, D. (2009). Geometry and spacetime. Lecture notes. Naber, G. L. (2012). The Geometry of Minkowski Spacetime. An Introduction to the Mathematics of the Special Theory of Relativity. New York: Springer. Nguyen, J., N. J. Teh, and L. Wells (2017). Why surplus structure is not super- fluous. British Journal for the Philosophy of Science. forthcoming. Osterwalder, K. and R. Schrader (1973). Axioms for Euclidean Green’s functions. Communications in Mathematical Physics 31(2), 83–112. Osterwalder, K. and R. Schrader (1975). Axioms for Euclidean Green’s functions. Communications in Mathematical Physics 42, 281–305. Putnam, H. (1983). Equivalence. In H. Putnam (Ed.), Philosophical Papers. Volume 3. Realism and Reason., pp. 26–45. Cambridge: Cambridge University Press. Rosenstock, S. and J. O. Weatherall (2016). A categorical equivalence between generalized holonomy maps on a connected manifold and principal connections on bundles over that manifold. Journal of Mathematical Physics 57, 102902. 28 Strocchi, F. (2005). An Introduction to the Mathematical Structure of Quantum Mechanics: A Short Course for Mathematicians. Singapore: World Scientific. Teh, N. and D. Tsementzis (2017). Theoretical equivalence in classical mechanics and its relationship to duality. Studies in History and Philosophy of Science Part B: Studies in History and Philosophy of Modern Physics 59, 44–54. Wallace, D. (2016). Studies in the History and Philosophy of Modern Physics. Weatherall, J. (2016a). Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent? Erkenntnis 81(5), 1073–1091. Weatherall, J. O. (2016b). Categories and the Foundations of Classical Field Theories. In E. Landry (Ed.), Categories for the Working Philosopher. Oxford: Oxford University Press. Wightman, A. S. (1956). Quantum field theory in terms of vacuum expectation values. Physical Review 101, 860–866. 29