The n-Category Café

the physical world we live in is not … a bunch of spacetime points with properties and relations … but … an equivalence class of isomorphic bunches of spacetime points with properties and relations.

I don’t see how that can possibly be true. One of the important features of the world is that we can distinguish between distinct spacetime points, e.g. we can say that a certain event happened here and not there. But it doesn’t make sense to speak of, e.g., the points of an isomorphism class of differentiable manifolds. An individual manifold has points, but an isomorphism class of them doesn’t, because any manifold has automorphisms that interchange some of its points.

John,

You keep saying this. If you have some argument for the claim, presenting it would make this conversation more interesting.

Here are some versions of the formulation of Leibniz equivalence (but there are lots of others):

For any spacetime model $(M, O_1, \dots, O_n)$ and any diffeomorphism $h$ on $M$, Leibniz equivalence asserts that the two models $(M, O_1, \dots, O_n)$ and $(hM, h^{\ast}O_1, \dots, h^{\ast}O_n)$ represent the same physical system. (Norton 2011, note 5.)

and

You will often hear it proclaimed that GR is a “diffeomorphism invariant” theory. What this means is that, if the universe is represented by a manifold M with metric $g_{\mu \nu}$ and matter fields $\psi$, and $\phi :M \to M$ is a diffeomorphism, then the sets $(M,g_{\mu \nu},\psi)$ and $(M,\phi_{\ast}g_{\mu \nu},\phi_{\ast}\psi)$ represent the same physical situation. (Carroll 1997: 138.)

and

Let $\mathcal{M}_1 = \langle M,g,T\rangle$ and $\mathcal{M}_2 = \langle M,d\ast g,d \ast T\rangle$ be two models of GR where $d$ is a non-trivial diffeomorphism, …

(LE) $\mathcal{M}_1$ and $\mathcal{M}_2$ represent the same possible world. (Pooley 2003, Sc. 5.1)

and

… if $\phi : M \rightarrow N$ is a diffeomorphism, then $M$ and $N$ have identical manifold structure. If a theory describes nature in terms of a spacetime manifold $M$ and tensor fields $T^{(i)}$ defined on the manifold, then if $\phi : M \rightarrow N$ is a diffeomorphism, the solutions $(M, T^{(i)})$ and $(N, \phi^{\ast}T^{(i)})$ have physically identical properties. Any physically meaningful statement about $(M, T^{(i)})$ will hold with equal validity for $(N, \phi^{\ast}T^{(i)})$. (Wald 1984: 438)

In these cases, the idea is that the isomorphic models represent the same world.

Cheers,

Jeff

Jeffrey wrote:

Here are some versions of the formulation of Leibniz equivalence (but there are lots of others)…

But these are not arguments that it’s good to treat isomorphic models as models of the same world. They are just further restatements of this claim… or, perhaps, definitions.

I don’t really need more statements of this sort: I’m not a big believer in proof by repetition. What I’d really like would be more precision about what these statements are supposed to mean, and what is their logical status.

Are they claims of the sort we could argue about? Or are they just definitions? If they are claims, is there some evidence for them? What kind of evidence?

If I read this, for example:

For any spacetime model $(M, O_1, \dots, O_n)$ and any diffeomorphism $h$ on $M$, Leibniz equivalence asserts that the two models $(M, O_1, \dots, O_n)$ and $(h M, h^{\ast}O_1, \dots, h^{\ast}O_n)$ represent the same physical system. (Norton 2011, note 5.)

I see a precise mathematical phrase followed by the vaguer phrase ‘represent the same physical system’. So, I’d naturally take the precise phrase as a definition of the vaguer phrase. And then the question is not whether this definition is ‘true’ or not, but merely: when is it a useful definition, and when is it not?

It’s also interesting that you seem to interpret ‘same’ as meaning ‘equal’. But there’s no need to do that: ‘same’ is often used to mean ‘isomorphic’.

For example, if we say “all these sandwiches are the same”, we don’t mean they’re all equal, in the sense of there being just one sandwich. We mean they’re isomorphic in some way.

And if we take this quote by Norton as a definition of ‘the same physical system’, then he’s defining ‘same’ to mean isomorphic!

That would be fine with me.

The most important recent thought on this subject is Voevodsky’s univalence axiom, which is one of the key ideas in homotopy type theory. This axiom asserts that isomorphic mathematical structures (or more generally ‘equivalent’ ones, in a certain precise technical sense) are equal.

The fascinating thing is that this axiom does not cause trouble! You might think it would mess things up to assert that all isomorphic groups are equal. But it doesn’t! Instead, it formalizes common practice in mathematics, where we use ‘the same’ to mean either isomorphic or equal.

So it’s possible that Norton and the other people you’re quoting are secretly believers in the univalence axiom — but perhaps only for ‘worlds’, not mathematical structures!

I have no problem with the univalence axiom: it shocked me at first, but now I see it’s a great idea. However, it seems to me that if you adopt this idea for one kind of thing (‘worlds’), it makes a mess if you don’t also adopt this idea for another related thing (‘models’). It creates a false puzzle, which is why worlds act differently than models.

It works more smoothly to either adopt univalence in a uniform way, or not at all.

What does the applicability of mathematics have to do with Steve’s observation, which is a statement about mathematics in its own right?

Thanks, Mike -

Does this mean, for any predicate $P(x)$ applied to non-mathematical entities, we always have a corresponding type? E.g., in set theory with urelements, $ZFU$, in a language $L$, we assert the existence of a set $U$ of all urelements (all satisfying “$x$ is an urelement”), we state that urelements have no members, and we restrict extensionality to sets,

$\forall x \notin U \forall y \notin U (\forall z(z \in x \leftrightarrow z \in y) \to x = y)$

Then, for any formula $\phi(x)$ whatsoever in $L$ (e.g., applying to urelements or not), we have by separation, the existence of the set $\{x \in U \mid \phi(x)\}$ by applying separation,

$\exists z\forall x(x \in z \leftrightarrow (\phi(x) \wedge x \in U))$

It’s this comprehension principle which allows us to assert the existence of sets of physical things: e.g., sets of spacetime points, regions, and so on.

But in type theory this works somewhat differently: what is the comprehension principle stating what types exist?

Jeff

Yes, it’s correct that in type theory, for every predicate $P(x)$ the variable $x$ has a specified type, so that $P$ can only be applied to objects of that type. Types in type theory are not “cut out” of a universe of everything by a comprehension principle. Rather, they are “built up” using rules of type construction. For instance, one of the rules says that we have a type $\mathbb{N}$ of natural numbers. Another of the rules says that if $A$ and $B$ are types, then we have a type $A\to B$ of functions from $A$ to $B$. Thus, we have types such as $\mathbb{N}\to\mathbb{N}$ of functions from naturals to naturals, or $(\mathbb{N}\to\mathbb{N}) \to (\mathbb{N}\to\mathbb{N})$ of functionals acting on such functions, etc.

I would personally shy away from making any claims about predicates applied to non-mathematical entities, since type theory is a mathematical theory (as is set theory, for that matter) and so all objects involved are mathematical. But I could imagine that in type theory used to model, say, natural language or human reasoning, you would have (say) a type of people, and a type of boulders, and a type of houses, and so on, and in a predicate like $P(x)=$ “$x$ is friendly” the variable $x$ would have type $Person$, since saying that a boulder is friendly is not very sensical. I’m sure there are people who’ve thought about this a lot more, like David here.

Mike, I agree with all of that - but that’s the classicist’s attitude!

Intuitionism places constraints on truth and proof, e.g., “each truth is knowable”,

If $\phi$, then it’s knowable that $\phi$

and on how proof relates to the connectives (BHK: roughly “proof commutes with logical connectives”). From these, we get that non-constructive proofs are somehow illegitimate (and the model theory - e.g., using Kripke models - shows how to give counter-examples to LEM).

The classicist responds to this by saying, e.g., that LEM is legitimate, but non-constructive. So the classicist has a liberal view, and the intuitionist imposes restrictions - “don’t use LEM!”. So, e.g., Douglas Bridges in his SEP on “Constructive Mathematics”, writes,

Thus just as mathematicians will assert $P$ only when they have decided that $P$ holds by proving it, they may assert $P \vee Q$ only when they either can produce a proof of $P$ or else produce one of $Q$. (First section)

But maybe that’s not what you mean by intuitionism; then I can’t quite figure out what you mean by classicism about logic. The classicist says you can choose to use LEM, or not. The intuitionist (e.g., Dummett, Bridges, others) says you cannot use LEM, because - on their philosophical view abut “proof” - to assert $A \vee \neg A$, you must have already proved either $A$ or $\neg A$.

Cheers,

Jeff

The statement “HoTT logic is intuitionist” is a mathematical statement, and therefore does not say anything about an attitude. It merely states that the default logic of HoTT lacks LEM. One can approach this mathematical fact from the philosophical perspective of an intuitionist, saying “excellent, this is the One True Way to do mathematics”; or from the philosophical perspective that I would call “classical”, saying “that’s dumb, but fortunately we can just add in LEM”; or from the philosophical perspective I advocate and call “pluralist” or “relativist”, saying “that’s good, so we can put in LEM or not, as needed or appropriate for the particular application”. The point I’m making is that there’s nothing intrinsic about the mathematics of HoTT that mandates approaching it with an intuitionist philosophy.

David,

It was partly through the recognition that set theory is inadequate as a language for mathematics.

Isn’t set theory simply a theory of sui generis mathematical entities, $\varnothing, \mathcal{P}(\varnothing), \dots$, forming a very large structure $(V, \in)$, the cumulative hierarchy of pure well-founded sets?

The foundational point, which became clear during the crucial foundational period from Frege (1879) to von Neumann (1925), say, is that all mathematical structures of interest can be interpreted in $V$. That is, there is a translation that maps all the axioms of one’s favourite theory into $L_{\in}$ so that they become theorems of $ZFC$, say.

Is something wrong with this mathematical discovery?

Cheers,

Jeff

Perhaps rather than “inadequate” it would be better to say “inconvenient”. I think it’s still true, as far as we know, that all mathematics can be interpreted into set theory (although some of the boundaries of HoTT might push that close to debate). But there are some problems with making practical use of this interpretation, such as:

• The distance between the foundational set theory and some parts of mathematics built on it is large. In other words, the translation is a lot of work. This is a problem when trying to formalize math in a computer, which has to be taught every detail of the translation into whatever foundational system you use.

• Set theory is not natively computational, which makes it less convenient to use for formalizing correctness proofs of computer programs, and other related things.

• The translation into set theory introduces new meaningless or undesirable statements and truths. Benacerraf’s complaints fall under this heading, but more recently and relevantly, we have the issue that in category theory we avoid distinguishing between isomorphic objects, whereas when we translate into set theory, it always becomes possible to distinguish between them in some way.

• The construction of new models of mathematics from old ones is more artificial in set theory. For instance, new toposes arise naturally from old ones by constructions of sheaves and realizability, and we can interpret all of mathematics in any topos. But if this interpretation is to go by way of set theory, then we have to go through a laborious process of constructing a model of set theory with its intricate $\in$-structure out of the objects of any topos — only to mostly discard that structure when we start interpreting the rest of mathematics! Type theory (and “structural” or “categorical” set theory) avoid this detour.

• Not all models of mathematics can be regarded as models of set theory. Higher toposes do contain models of set theory, but not all objects therein can be built out of the resulting sets. It’s still true that the higher topos itself can be built out of the sets in the ground model, so that ultimately everything can be reduced to set theory, but restricting ourselves to set theory as the foundation prevents us from working inside the higher topos as a world of mathematics in its own right.

But (as pointed out on that page) for the physics to work we need the smooth structure in place. You’re not going to be able to reimpose it after the quotienting process of forming the action groupoid.

John,

I think maybe you took it that the entity $\Phi_{\mathcal{A}}(\vec{X})$ that I mentioned above is a set or an equivalence class? No, these entities are formulas of infinitary logic: omitting the reference to the sequence $\vec{X}$ of free second-order variables, $\Phi_{\mathcal{A}}$ is a kind of linguistic diagram of $\mathcal{A}$, analogous to the notion of a diagram in model theory. Its most important property is its categoricity:

$\mathcal{B} \models \Phi_{\mathcal{A}}$ iff $\mathcal{B} \cong \mathcal{A}$.

So, yes, moving to an equivalence class is “decategorification”, just as in the example of moving from FinSet to $\mathbb{N}$.

But this isn’t decategorification. For example, the formula $\Phi_{\mathcal{A}}$ (omitting the reference to the free variables) can be “skolemized”, written $sk_{\alpha}\Phi_{\mathcal{A}}$, where the map $\alpha$ replaces each bound variable in the formula by some new constant. Any pair of skolemizations $\alpha, \beta$ corresponds to a permutation $\pi: A \to A$ of the carrier set of $\mathcal{A}$. Then one can show that:

$\pi \in Aut(\mathcal{A})$ iff $sk_{\alpha}\Phi_{\mathcal{A}} \equiv sk_{\beta}\Phi_{\mathcal{A}}$.

This shows how automorphisms of $\mathcal{A}$ correspond to logical equivalence, under linguistic relabellings of the formulas that describe $\mathcal{A}$.

The formula $\Phi_{\mathcal{A}}$ isn’t an equivalence class; it’s a formula which encodes all the structural information about $\mathcal{A}$, but throws away its carrier set. This idea isn’t decategorification; it’s decarriersetification!

The propositional content of the formula $\Phi_{\mathcal{A}}$ is called $\hat{\Phi}_{\mathcal{A}}$; and then, with some mild assumptions about propositional content, one can prove, rather than decree, that

$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A} \cong \mathcal{B}$.

Jeff

John,

Isomorphic models will describe isomorphic universes, and everything will make sense.

This sort of view was defended about 20 years ago (e.g., Maudlin 1990 and Butterfield 1989).

But I think it’s fair to say that no one defends it anymore. Your distinct-but-isomorphic-universes would be physically indistinguishable (like Leibniz’s original “shifted worlds”, in Leibniz’s argument against Newton’s absolute space), but the physical principle involved suggests that there cannot be such distinct, isomorphic universes. The isomorphic models are representations of the same universe!

Cheers,

Jeff