ABSTRACT
Ladyman and Presnell have recently argued that the Hole argument is naturally resolved when spacetime is represented within homotopy type theory rather than set theory. The core idea behind their proposal is that the argument does not confront us with any indeterminism, since the set-theoretically different representations of spacetime involved in the argument are homotopy type-theoretically identical. In this article, we will offer a new resolution based on ZFC set theory to the argument. It neither relies on a constructive-intuitionistic form of mathematics, as used by Ladyman and Presnell, nor is foundationally problematic, such as the existing set-theoretic suggestions.
Disclosure statement
No potential conflict of interest was reported by the author(s).
Notes
1 Stachel (Citation2014) has traced the history of the argument.
2 The Hole argument has also a ‘verificationist dilemma’ which is closely related to the problem of underdetermination. For more on this, see footnote 6.
3 More particularly, they hold the isomorphism involved in the Hole argument, which is taken to establish the physical equivalence between the models of general relativity, should be understood in terms of isometry, not diffeomorphism. And also, given a Lorentzian manifold and a proper open subset O of M, there is no ‘isometry that changes things in O but not outside of O’ (Halvorson and Manchak Citation2022, 15).
4 By a ‘linguistic’ framework we mean a mathematical framework within which scientists represent the world or a part of the world. By a ‘meta-linguistic’ framework we mean a logical or mathematical framework within which scientific theories are presented in order to explore philosophical questions. For more on the dichotomy, see French (Citation2012) and Landry (Citation2012).
5 More precisely, M is a 4-dimensional smooth (at least of class ) manifold, and g is a symmetric, non-degenerate -tensor field on M with index 1. For more details, see O'Neill (Citation1983, 54).
6 That these isometric Lorentzian manifolds represent the worlds which are empirically indistinguishable but substantivally distinct presses substantivalists to decide between verificationism and substantivalism. Dubbed ‘verificationist dilemma’ by Earman and Norton (Citation1987), this problem is closely linked to what (Pooley and Read Citation2021) call the ‘underdetermination version of the argument’.
7 Embedding the representation function into Leibniz equivalence and then allowing it to be changed lead to what (Roberts Citation2020) has called ‘Weak Leibniz Equivalence’. Obviously, this meaning of equivalence does not threaten substantivalism.
8 While the relata of the first transition are within the representational framework, a relatum of the second transition belongs to the representational framework and another one belongs to the world.
9 They construe the modality involved in REME as a feature associated with contextual-intentional considerations. Said that, RUMI* states
if two models of a physical theory are mathematically equivalent and if one model is chosen to represent …a particular physical possibility …, then the other model, relative to that choice …, also represents that physical possibility …(Pooley and Read Citation2021, 18)
10 Does the language of general relativity allow us to formulate such a difference? Assuming numerical identity as the best option for cross-model identity (in cases in which the underlying sets are one and the same), Arledge and Rynasiewicz (Citation2019, 10) argue we are allowed to assume different possible worlds which have the same structure. Halvorson and Manchak (Citation2022, 25) disagree with this conclusion, claiming the language of general relativity, as used by physicists, and also any regimentation of it exclude such a possibility. In any case, these discussions shift the debate from mathematical issues to philosophical ones.
11 It is a subspace of , containing all square-integrable functions vanishing on the boundary of Ω, while their weak partial derivatives remain in .
12 For more details, see Brezis (Citation2010, 291).
13 Regarding this consideration, henceforth when we say ‘set’ and ‘set theory’, we mean, respectively, set in ZFC and ZFC set theory.
14 Dougherty (Citation2020) has argued that using HoTT and formalising Lorentzian manifolds in this framework do not resolve both verificationist and indeterminism dilemmas. To solve the latter, he suggested it is needed to consider generally covariant Lorentzian manifolds instead of Lorentzian manifolds as the representations of spacetime.
15 For more on identity in HoTT, see Awodey (Citation2014), Ladyman and Presnell (Citation2015), Ladyman and Presnell (Citation2017), and Ladyman and Presnell (Citation2019b).
16 Let be a universe type and and be two types as elements of . Given the natural function , which is defined by induction, Voevodsky's Univalence Axiom simply states that this function is an equivalence, meaning that it admits an inverse function (Program Citation2013, 89).
17 In a number of papers, Ladyman and Presnell (Citation2015), Ladyman and Presnell (Citation2016) and Ladyman and Presnell (Citation2019b) have proposed HoTT as a foundation for mathematics. To this end, they have tried to represent HoTT independently of homotopy theory which is itself a branch of mathematics. In addition, they have proposed types-as-concepts as a pre-mathematical interpretation of HoTT. Bentzen (Citation2019) believes that Ladyman and Presnell have not fully specified what they mean by concept. He goes on to add while types are considered as extensional objects in Ladyman and Presnell (Citation2019b), conceived of as intentional objects in Ladyman and Presnell (Citation2016), showing their proposal is not consistent. Besides these, their interpretation of HoTT recognises the validity of the Principle of Excluded Middle in its most general form, that this contradicts the incompatibility of HoTT with the principle. All in all, Bentzen (Citation2019) concludes we are still far from being able to say that HoTT is an autonomous foundation for mathematics.
18 In ZFC, each set x has a rank, denoted by , which is the least ordinal α s.t. . Using this, for each proper class C, each and each equivalence relation ≡ on C, one can define In this case, is a set and has all the properties one expects from the equivalence class of x. For more on this, see Jech (Citation2003, Ch. 5). This trick, called ‘Scott's trick’, enables one to define isomorphic types for a given isomorphism over a proper class (e.g. the isomorphic type of groups or Lorentzian manifolds).
19 Here, by a ‘small set’, we mean simply a set, in contrast to a proper class. Formally, a small category is a category where the class of its objects and the class of its morphisms (arrows) are both sets. For more details, see Awodey (Citation2010, 23–25).
20 In fact, -regularity for suffices to have Clrake's results. Nonetheless, in the literature of the theory of general relativity, it is customary to assume that all manifolds are smooth (see, for instance, O'Neill (Citation1983) and also Sachs and Wu (Citation2012)).
21 Besides it, he shows that every ‘spacetime’ of the theory of general relativity can be embedded isometrically in (Clarke Citation1970, 424-425).
22 Let be a subcategory of a category . We say is a ‘full’ subcategory of if for all objects , i.e. every morphism in belongs also to . For more details, see Awodey (Citation2010, 148).