Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

November 19, 2013

The Covariance of Coloured Balls

Posted by David Corfield

When you reach over 150 messages in response to a post, it’s probably time to start a new one, especially for those with inefficient browsers. In this post I want to see if I can make sense of discussions we were having there about general relativity, covariance, groupoids and sameness in a much more intuitively clear setting, though perhaps it will introduce its own problems.

OK, so say I have a set, BB, of 5 indiscernible balls in a box, each of which can be coloured in 3 ways. Then I might take the state space to be [B,3][B, 3], of cardinality 243. But perhaps while doing physics on these balls, I come to see that nothing about them matters aside from their colour. Since I can’t tell the difference between any two versions of 2 reds, 2 greens and a blue, I decide to reduce my state space to [B,3]/Sym(B)[B, 3]/Sym(B), a set of equivalence classes of cardinality 21.

However, after a time this starts to strike me as odd. I have represented the fact that any colouring of 2 reds, 2 greens and a blue are equal, and yet were someone to swap a green and a red I’d notice in a way that I wouldn’t notice a swap of two reds. Any swaps in a state of 5 red balls would also go unnoticed. At the very least, there seems to be a difference between a monochrome state and a tricoloured state.

So I decide to change my state space to the action groupoid [B,3]//Sym(B)[B, 3]//Sym(B). This has 21 connected components, but an object in the all red component has 120 automorphisms, where an object in the 2 reds, 2 greens and a blue component has 4 automorphisms. The groupoid as a whole has cardinality 243/120.

Hopefully the analogy with general covariance, where we consider [Σ,Fields]//Diff(Σ)[\Sigma, \mathbf{Fields}]//Diff(\Sigma), is clear. So what is it legitimate to ask, and what illegitimate?

Well, I shouldn’t ask how many worlds there are. Nor should I ask how many worlds there are in which there are 2 reds, 2 greens and a blue, but I can ask how many automorphisms there are on that world. I can also ask how many distinguishable kinds of world there are (21).

Can I even ask how many balls there are? If I model the space of balls as B//Sym(B)B//Sym(B), then ‘No’, all I have is its cardinality, 1/24.

On the other hand, so long as I know the symmetry group, I can reconstruct the number of balls. This is reflected by the magic of dependent type theory.

B:BSym(B)B:Type B : \mathbf{B} Sym(B) \vdash B : Type

denotes a dependent type, which we interpret externally as the balls with the action of their symmetry group. Now I can ask things like “Sym(B)Sym(B)-equivariantly, is BB a set, and if so what cardinality does it have?”, and be told “Yes, 5.”

So you hand me a groupoid and I may be able to reconstruct it as an action groupoid of a group acting on a set, but I won’t be able to do this uniquely. I can’t tell the difference between 1\mathbf{1} and 2//Sym(2)\mathbf{2}//Sym(\mathbf{2}). If you tell me that every object I see has a double residing within it, which is identical to it in a canonical way, I should say that’s equivalent to my ordinary view of the world. However, once we agree on the action group, you can say things like “Sym(2)Sym(\mathbf{2})-equivariantly there are two cups in front of me.” But I shouldn’t ask you “Which is in front of you now?”

In the analogy between the coloured balls and the case of general covariance, something like the following seems to be going on. I see two reds, two greens and a blue. I agree there’s no difference between this and the situation where the two reds are swapped. Since I can’t tell the difference, I take the two cases to represent the same state of affairs. However, once I’ve done this, I seem to have given up any way of conceiving of there to be 5 balls. Hopefully, we can agree, that via the action groupoid understood in a certain equivariant context, we can still say there are 5 balls, while agreeing that we can’t tell the two coloured worlds apart.

Posted at November 19, 2013 12:35 PM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2672

136 Comments & 0 Trackbacks

Re: The Covariance of Coloured Balls

This is a very nice way of thinking about it.

I do think we shouldn’t use the same letter BB for the set of balls, for a variable of type BSym(B)\mathbf{B} Sym(B), and for the type in that context whose fiber is the set of balls. It’s even worse because we’re using B\mathbf{B} for delooping! So despite the fact that “balls” begins with B, I suggest using a different letter like SS for the set of balls. Then the set SS is acted on by the group Sym(S)Sym(S):

Sym(S)×SS Sym(S) \times S \to S

and this action can be encoded by a dependent type

x:BSym(S)T(x):Type x : \mathbf{B} Sym(S) \;\vdash\; T(x) : Type

with the property that T(*)=ST(\ast) = S, where *:BSym(S)\ast:\mathbf{B} Sym(S) is the canonical basepoint.

Now it’s true that if we define BSym(S)\mathbf{B} Sym(S) to be the image of (λu.S):1Type(\lambda u . S) : \mathbf{1} \to Type, i.e.

BSym(S): X:TypeX=S \mathbf{B} Sym(S) :\equiv \sum_{X:Type} {\Vert X = S\Vert}

then its canonical basepoint is (S,refl S)(S,refl_S) and the dependent type TT is pr 1:( X:TypeX=S)Typepr_1 : \big(\sum_{X:Type} {\Vert X = S\Vert}\big) \to Type. So if we decided not to notate the second components of elements of this image (which is not unreasonable, since they are hprops), then TT would be the identity and the basepoint would be SS; thus we would write

x:BSym(S)x:Type x : \mathbf{B} Sym(S) \;\vdash\; x : Type

and upon substituting SS for xx we would get S:TypeS:Type as the fiber over the basepoint SS. However, one might argue that this is more confusing rather than less.

What we shouldn’t do is use the same letter for the fixed set SS and for a variable of type BSym(S)\mathbf{B} Sym(S). Indeed, the whole point is that T(x)T(x) is defined over that whole type rather than just at the basepoint, and that definition encodes the action of Sym(S)Sym(S) on SS.

The intuition does argue for using the same letter for TT and for SS, since TT is “SS equipped with its action by Sym(S)Sym(S)”. That seems okay as long as we find a way to notate the dependence on xx, such as writing

x:BSym(S)S x:Type x : \mathbf{B} Sym(S) \;\vdash\; S_x : Type

so that we could then say S *=SS_\ast = S (or, I suppose, S S=SS_S = S; ugh). It may also be tempting to write S//Sym(S)S//Sym(S) for TT, but properly that notation belongs rather to the dependent sum x:BSym(S)T(x)\sum_{x:\mathbf{B}Sym(S)} T(x), so I think that confusion could arise there as well.

Posted by: Mike Shulman on November 19, 2013 8:20 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Thanks! I guess Urs is the one to convince about notation.

Posted by: David Corfield on November 22, 2013 7:09 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

If I understand this setup right, each model has the form of a partition

=(B,C 1,C 2,C 3)\mathcal{M} = (B, C_1, C_2, C_3),

where B={b 1,,b 5}B = \{b_1, \dots, b_5\} (with b ib jb_i \neq b_j for iji \neq j), C iBC_i \subseteq B, and C iC j=C_i \cap C_j = \varnothing (with iji \neq j), and B= iC iB = \bigcup_i C_i.

Let n i=|C i|n_i = |C_i|. So, each n i5n_i \leq 5 and n 1+n 2+n 3=5n_1 + n_2 + n_3 = 5.

Because Nature doesn’t care about the “identity” of the b ib_i, Nature counts isomorphic models as representing to the same world. Equivalence classes of isomorphic models are labelled by the cardinalities (n 1,n 2,n 3)(n_1, n_2, n_3). So, the worlds are of the form W n 1,n 2,n 3W_{n_1,n_2,n_3}.

In Nature, there are (in reality) no balls! There are only three properties C 1,C 2,C 3C_1, C_2, C_3, with occupation numbers that must sum to 55.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 20, 2013 8:37 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I think Nature has balls.

Posted by: John Baez on November 20, 2013 4:49 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

On the connection between the notion of indiscernibility in the models and the automorphisms of that model: the indiscernibility relations of the balls will in general vary from model to model. Let =(B,C 1,C 2,C 3)\mathcal{M} = (B,C_1,C_2,C_3) be such a model and define the indiscernibility relation \sim_{\mathcal{M}} on \mathcal{M} like this: for a,bBa,b \in B,

a ba \sim_{\mathcal{M}} b if and only if, for each C iC_i, we have aC ibC ia \in C_i \leftrightarrow b\in C_i.

(This is the Hilbert-Bernays-Quine “first-order indiscernibility predicate” for this monadic structure. It says that a,ba,b cannot be distinguished by colour in that particular model.)

Then one can prove:

a ba \sim_{\mathcal{M}} b if and only if π abAut()\pi_{ab} \in Aut(\mathcal{M})

where π ab:BB\pi_{ab} : B \to B is the transposition swapping a,bBa,b \in B.

This is Theorem 3.23 of “Identity and Indiscernibility” (applied to monadic structures: in general, only the left-to-right direction holds for arbitrary relational structures).

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 20, 2013 9:10 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Given what I just wrote in the other thread, my example is precisely not a good one to challenge your formulation. I’ve even taken the smoothness out of the situation, not that we discussed it over there.

What I think will make you uncomfortable are situations where our worlds are modelled (a) as forming a smooth groupoid and (b) as forming a higher groupoid. I’ll see if I can think up some simple cases.

I’m not so sure I’d say

In Nature, there are (in reality) no balls!

I can say the situation may be conceived as though there are 5 indiscernible balls, in the sense that this gives rise to a groupoid equivalent to my groupoid of states.

I suppose there could be a simplest reconstruction of a groupoid as an action groupoid of a group acting on a set. Given my groupoid 1\mathbf{1} above (one object, one identity morphism), I can reconstruct it in different ways, e.g., a set with one element, or a set with 2 elements under permutations. You would wonder why I bothered to do the latter, unless I had reason to think that in the future the two copies of my cup revealed themselves as somehow different, i.e., that in fact a better model will be seen to have 2 objects and no nontrivial morphisms.

We could track the history of physics in terms of how it modifies its model of spacetime and its gauge fields. It seems we may need to depart from models which can be constructed in terms of sets (manifolds) and groups.

Posted by: David Corfield on November 20, 2013 10:54 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

About that last point, one advantage to the construction of the configuration space in terms of a manifold, is that I can present the addition of gauge fields in a simple way. E.g., in the Einstein-Yang-Mills-Dirac-Higgs theory, I just successively expanded what I took to be Fields\mathbf{Fields}.

On the other hand, this shouldn’t blind us to the need to rethink spacetime as in the D’Auria-Fre formulation of supergravity, where we turn to a higher Cartan geometry to represent spacetime.

Posted by: David Corfield on November 20, 2013 11:20 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

But note that the formulation I use is from Wald 1984, Carroll 1997 and Rovelli 2004. This is why I’m worried that the category-theory approach may be in conflict with what physicists themselves think about the interpretation of diffeomorphism invariance.

(Physical spacetime mightn’t be smooth though. It’s convenient, and our best theory (!), to have models (M,g,T)(M, g, T), with MM a manifold, g,Tg,T tensor fields, satisfying Einstein’s equations; but we might consider discrete approaches, say (X,)(X, \preceq), a “causal set” model in the sense of Sorkin. Again, causal seets (X 1, 1)(X_1,\preceq_1) and (X 2, 2)(X_2,\preceq_2) would count as representing the same physical world just when isomorphic.)

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 20, 2013 11:52 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

There’s no commitment to smoothness, but still it’s pleasing cohesive HoTT handles it well, since almost all physics today is done in terms of differential equations.

The concept of cohesion is broader than the smoothness of the reals. It’s being spotted even in arithmetic in the guise of differential K-theory.

It arises from a simple chain of adjunctions, so feels like it ought to good for many things. But still, maybe physics takes us somewhere that we need a different concept to add onto HoTT. So be it.

Posted by: David Corfield on November 20, 2013 12:38 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

There’s no guarantee that the physicists have it right! Isomorphism invariance is a tricky concept which it took mathematicians many years to really understand, so I’m not at all surprised if physicists haven’t really internalized it correctly yet.

Posted by: Mike Shulman on November 20, 2013 11:03 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David, John and Mike,

Suppose we have two indistinguishable “particles” and two physical properties, Left\mathbf{Left} and Right\mathbf{Right}. Then, calling the particles 0 and 1, let P={0,1}P = \{0,1\}. Let the models have the form =(P,L,R)\mathcal{M} = (P, L,R), where L,RPL,R \subseteq P and LR=L \cap R = \varnothing and P=LRP = L \cup R. LL is what the model “thinks” is the set of Left\mathbf{Left} things, and RR is what the model “thinks” is the set of of Right\mathbf{Right} things.

There are 4 models,

1=(P,{0,1},)\mathcal{M}_1 = (P, \{0,1\},\varnothing)

2=(P,{0},{1})\mathcal{M}_2 = (P, \{0\},\{1\})

3=(P,{1},{0})\mathcal{M}_3 = (P, \{1\},\{0\})

4=(P,,{0,1})\mathcal{M}_4 = (P, \varnothing,\{0,1\})

but only 3 worlds (physical states), labelled by occupation numbers,

W 2,0W_{2,0} (represented by 1\mathcal{M}_1)

W 1,1W_{1,1} (represented by 2\mathcal{M}_2 and 3\mathcal{M}_3)

W 0,2W_{0,2} (represented by 4\mathcal{M}_4)

This is because 2 3\mathcal{M}_2 \cong \mathcal{M}_3. So, they both represent the same state (world), W 1,1W_{1,1}.

This is how I make sense of this.

W 2,0W_{2,0} is the world in which x,y(xyL(x)L(y)¬R(x)¬R(y)z(z=xz=y))\exists x,y(x \neq y \wedge \mathbf{L}(x) \wedge \mathbf{L}(y) \wedge \neg \mathbf{R}(x) \wedge \neg \mathbf{R}(y) \wedge \forall z(z = x \vee z = y)).

W 1,1W_{1,1} is the world in which x,y(xyL(x)¬L(y)¬R(x)R(y)z(z=xz=y))\exists x,y(x \neq y \wedge \mathbf{L}(x) \wedge \neg \mathbf{L}(y) \wedge \neg \mathbf{R}(x) \wedge \mathbf{R}(y) \wedge \forall z(z = x \vee z = y)).

W 0,2W_{0,2} is the world in which x,y(xy¬L(x)¬L(y)R(x)R(y)z(z=xz=y))\exists x,y(x \neq y \wedge \neg \mathbf{L}(x) \wedge \neg \mathbf{L}(y) \wedge \mathbf{R}(x) \wedge \mathbf{R}(y) \wedge \forall z(z = x \vee z = y)).

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 21, 2013 12:59 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

OK. At first I think we took you as just having taken equivalence classes, but as I understand it you want your formalism to recognise that, say, W 2,0W_{2,0} and W 1,1W_{1,1} have different symmetry groups.

I’ve then pointed out that we would typically think of configuration space as a groupoid [Worlds,2]//Sym(Worlds)[Worlds, 2]//Sym(Worlds) with four objects, two of which have a nontrivial isomorphism between them, and the other two of which each has a nontrivial automorphism.

We then note that our groupoid is equivalent (in our technical sense) to how we would represent your system as a groupoid, i.e., three objects, two of which each has a nontrivial automorphism. We can say nothing that tells these groupoids apart.

You, on the other hand, presumably think you’ve done something more or other than form a groupoid, that, say, to comprehend the situation as having either three or four things (worlds, or whatever we decide to call them) makes a difference.

We don’t agree. The number of objects in a groupoid is not invariant under equivalence.

How could we settle such a disagreement? Clearly, if you could do something with your system that we should want, but can’t do with our system.

Two things I’ve said in favour of our system are that we can cope: (a) In other situations, such as general relativity, when these worlds don’t just form a groupoid but a smooth groupoid; (b) In other situations, such as the Kalb-Ramond field, where we need our worlds to form a higher groupoid.

I’m not sure your logical representation will work in these cases.

I also suggested that it’s a little odd in your approach that when new information emerges, you end up radically revising what you take there to be.

For example, in the situation you describe, you say there are no balls in the ordinary sense. We say that we can construe the situation as though there are two balls. We can construe it in other ways too, but we note that this is an especially simple way.

Information may emerge which allows what, after the event, we might both describe as the distinguishing of the balls. You’ll now form four worlds. We’ll modify to an equivalent four object groupoid. We’ll still say that we can construe the situation as there being two balls. You’ll say now there are two balls.

On the other hand, new information may emerge that we can now detect that both of the balls in fact has a double that agrees as to Left or Right, but can agree or disagree as to a new property Up or Down. You’ll form your worlds, we our groupoid. Depending on the set-up, you may well be forced to say again there are no balls. We will say, we can construe the situation as though there are four balls in two pairs…

My point is that you seem to be more definite as to what there is, and are forced to change your mind as new information emerges, where we just talk of possible ways to construe the situation.

But I can see that someone might not like our lack of definiteness, and think it a good thing that new information should radically change what we take there to be.

Posted by: David Corfield on November 21, 2013 9:20 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

At first I think we took you as just having taken equivalence classes …

Right - worlds are not equivalence classes. (Neither is the abstract structure of a model.)

You, on the other hand, presumably think you’ve done something more or other than form a groupoid, that, say, to comprehend the situation as having either three or four things (worlds, or whatever we decide to call them) makes a difference. We don’t agree.

Yes, looks so. Whether there is a groupoid or a schmoupoid, here, I don’t know. But it seems like the disagreement is about physics. Nature says that there is one world, not two, corresponding to the isomorphic models 2\mathcal{M}_2 and 3\mathcal{M}_3. The swap 010 \leftrightarrow 1 makes no physical difference. “Labelling” the “particles” as 00 and 11 is a representational act: both models correspond to a single world, W 1,1W_{1,1}. So, for example, when one works out a partition function in statistical physics involving indistinguishable particles, one must not overcount the physical states.

The models involve “unphysical labellings”. So, one needs to distinguish the models (representations) from the worlds.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 21, 2013 12:25 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I dare say the ‘we’ I’ve been using may break down at the point where the passage is made from modelling to saying how things really are.

Let me think of some options:

1) There is an answer but we don’t need to know it, and couldn’t find it out anyway. I can do my work as a physicist without answering such questions. I can calculate things, make predictions and test them using any equivalent mathematical representation of the relevant configuration space.

2) There is no answer. To the extent that the configuration space is modelled as well as it can be for the purposes of doing physics (predicting, etc.) in terms of a groupoid, asking how many states there really are is meaningless.

Of course, we need to put in some proviso about having reached a state of maximal knowledge. Many things can happen that will make us change our space of models. It’s possible that ideas about what’s ‘really’ happening might play a role in helping or hindering our devising of new models.

Regarding (2), which I favour, to the extent that I can construe the groupoid in an obviously most simple way as the action groupoid of a group on a set, I may be inclined to say there’s that set of states. So I might say in your case that it’s as though there are four states two of which are indiscernible, with relevant symmetries. But then I’m really just saying I have a neat way to convey the groupoid. On the other hand, the original description of the set-up lends itself to this representation.

Similarly, asked to say whether my coffee cup just is in its own unique state or is in one of two indiscernible states, I’d opt for the former, even though the latter represents an identical groupoid to the component of the two indiscernible models of your example, where I opted for the two state representation. But since the description of the situation was as it was, this option seems to better represent my expectations.

Posted by: David Corfield on November 21, 2013 5:57 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

I can do my work as a physicist without answering such questions. I can calculate things, make predictions and test them using any equivalent mathematical representation of the relevant configuration space.

You cannot do it your way, not as a physicist. You’re not counting states correctly. When you compute physical quantities, you must do it my way, and count the isomorphic copies as labelled representations of the same physical state – this is the standard method in physics. From the point of view of the quantum physics of indistinguishable particles, it’s crucial that there are three physical states, not four. Otherwise, you double count the statistics. There are four models, yes; and this is because the models are “labelled mathematical representations”. But to get the physical states, you must “remove the labelling”. Same thing happens with Feynman diagrams.

There’s some nice explanations in this 2010 online textbook, The Joy of Quantum Physics, (Ch 8., “Identical particles, indistinguishability, and interchange invariance”), by Michael Morrison.

To the extent that the configuration space is modelled as well as it can be for the purposes of doing physics (predicting, etc.) in terms of a groupoid, asking how many states there really are is meaningless.

As I said, this gives the wrong physical answer and it’s because it seems to be mixing up the number of mathematical models with the number of distinct physical states. How many physical states there are is what the physicist is interested in!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 21, 2013 8:26 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

You cannot do it your way, not as a physicist. You’re not counting states correctly. When you compute physical quantities, you must do it my way, and count the isomorphic copies as labelled representations of the same physical state – this is the standard method in physics.

These are bold statements. They seem to be saying that a physics based on the HoTT framework can’t work. After nearly 800 pages, Urs won’t like that. If we must do it your way, you owe us a very long book.

I could see you might believe there’s an extra layer of interpretative work to be done which makes no difference to calculations, but you seem to be saying that this extra physical interpretation does matter for calculations. But this can only be because it gives rise to different mathematical representations in the models.

Of course, we have different understandings of what count as ‘different mathematical representations’.

…this gives the wrong physical answer and it’s because it seems to be mixing up the number of mathematical models with the number of distinct physical states. How many physical states there are is what the physicist is interested in!

I still can’t tell whether you’re talking about something beyond calculation of something measurable. My claim is that as far as calculation goes, no distinction that is meaningless to HoTT will make a difference.

Posted by: David Corfield on November 22, 2013 9:05 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

After nearly 800 pages, Urs won’t like that. If we must do it your way, you owe us a very long book.

Crikey, hope not! :)

But taking the 2 particle/2 properties setup, the physical answer surely has to be 3 distinct physical states, and not 4. So (see the same question below), there must be some way of extracting the number 3 from the action groupoid you’re considering.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 9:49 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Jeffrey wrote:

You’re not counting states correctly. When you compute physical quantities, you must do it my way, and count the isomorphic copies as labelled representations of the same physical state – this is the standard method in physics. […] Same thing happens with Feynman diagrams.

Oh, goodie. Let’s take the case of Feynman diagrams, since I’ve written a paper about exactly that case.

If you do a calculation that involves summing up Feynman diagrams, and you do it by simply counting isomorphic ones as the same and ignoring the isomorphisms, you’ll get the physically incorrect answer!

Instead, you have to sum over Feynman diagrams where each one is weighted by the reciprocal of the size of its symmetry group.

All physicists know this, but they don’t all know the reason why. It’s because you should not work with the set of isomorphism classes of Feynman diagrams. Instead, you should work with the groupoid of Feynman diagrams and isomorphisms between these! There’s a generalization of summing over a finite set that works for finite groupoids. And when you use this, you get the right answers.

Here’s a nice paper that goes into more detail than mine:

Jeffrey Morton, Categorified algebra and quantum mechanics.

Posted by: John Baez on November 22, 2013 2:13 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John,

What I’m describing is definitely the usual way of counting states for “identical particles” in statistical physics and gives the physically correct answer! E.g., here is a quick online explanation:

Consider first the simplest case, of two particles and two energy levels. If the particles are distinguishable, as in the upper picture below, there are four states, two of which have energy ε\varepsilon , ….

If the particles are indistinguishable, however, there are only three states, as in the lower picture…

So, on the 2-particle, 2-properties case again: you agree that there are four models, but three physical possibilities? We can’t be disagreeing on that …

John:

If you do a calculation that involves summing up Feynman diagrams, and you do it by simply counting isomorphic ones as the same and ignoring the isomorphisms, you’ll get the physically incorrect answer! Instead, you have to sum over Feynman diagrams where each one is weighted by the reciprocal of the size of its symmetry group.

Right - but surely what I’m saying is don’t ignore the isomorphisms of the labelled diagram to itself, because that overcounts, and the symmetry factor comes from this. “Counting” Feynman diagrams seem to be analogous to the case in statistical physics, and the symmetry factor is analogous too, isn’t it? There is something I’m not understanding though about what you’re saying, about the automorphisms of the models to themselves.

Many thanks for linking to the Morton paper – actually, I read it a while ago (a year ago, maybe), as it mentioned “structure types”, and it seems to be extremely interesting; but, unfortunately, too much category theory for me to absorb at the time. I’m going to read it again, and your earlier paper too!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 4:41 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Of course the two situations at that page are represented differently by us.

In the case of the indiscernible particles, we too have a ‘3’ available to us as the cardinality of the connected components of the groupoid of states. We could understand what you mean by saying that there are three states.

We would say that by taking the skeleton of the groupoid, the number of objects is made equal to the number of its components. If you identify states with objects in the skeleton, then obviously there will be as many states as there are objects.

But we’d also say there’s no advantage to the skeleton. So long as you retained the automorphism information to go along with the equivalence classes, we’ll both proceed in the same way with our calculations.

Posted by: David Corfield on November 22, 2013 9:40 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

Does this mean that, on your approach, when you count physical states, you count the number of connected components in your skeleton?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 9:55 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

It seems to me that the partition function cannot be physically observable.

Suppose I am red-blue colour blind, but I have a friend who is not. Surely we would deduce different partition functions for the same system. Am I right, or just confused about how statistical mechanics works?

Posted by: Tom Ellis on November 22, 2013 11:00 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Say, we put a little time variation into the situation, where repetitively on a periodic basis, 00 and 11 change places.

We represent time as a circle, and fibred above it we have our four object groupoid. The configuration space is what we would call a stack of groupoids.

One passage around the circle will generate morphisms between our worlds (or an autoequivalence of the whole groupoid), the nontrivial automorphism on the all left and all right worlds, and the isomorphism each way between the other two worlds.

How would you deal with this situation?

Posted by: David Corfield on November 21, 2013 11:48 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I’m not sure how to think of the relevant models. Maybe

𝒜=(S 1,Σ)\mathcal{A} = (S^1, \Sigma)

where S 1S^1 is the circle, and

Σ:S 1Π\Sigma : S^1 \to \Pi

is a function specifying the partition at any tS 1t \in S^1, and where

Π={ 1, 2, 3, 4}\Pi = \{\mathcal{M}_1, \mathcal{M}_2, \mathcal{M}_3, \mathcal{M}_4\}

is set of models given before.

Let G=Sym({0,1})G = Sym(\{0,1\}). Models 𝒜=(S 1,Σ)\mathcal{A} = (S^1, \Sigma) and 𝒜 =(S 1,Σ )\mathcal{A}^{\prime} = (S^1, \Sigma^{\prime}) count as physically equivalent if there is some some πG\pi \in G such that Σ =π *Σ\Sigma^{\prime} = \pi_{\ast} \Sigma.

Such physically equivalent models correspond to the same physical world.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 21, 2013 1:24 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Jeffrey wrote:

But note that the formulation I use is from Wald 1984, Carroll 1997 and Rovelli 2004. This is why I’m worried that the category-theory approach may be in conflict with what physicists themselves think about the interpretation of diffeomorphism invariance.

I know these guys, and while they know a lot of physics, I know a certain amount myself… and probably more math. So I am unintimidated by their names, much as I respect them.

For example, let’s talk about gauge theory.

It’s quite possible that these guys think the space of connection modulo gauge transformations is the right kind of thing to think about when doing gauge theory. That seems to be what you’d advocate… and for a while everyone thought that was true. But these days, if you talk to more mathematically minded physicists, they’ll tell that ain’t so!

You shouldn’t take connections and impose an equivalence relation saying they’re equal if there’s a gauge transformation mapping one to the other. You should instead form a groupoid where you say two connections are isomorphic if there’s a gauge transformation carrying one to the other.

In modern jargon: don’t look at the moduli space of connections. Look at the moduli stack.

You need to do this to get the right answers to concrete questions. The simplest example is computing the partition function of a gauge theory in 2 dimensions where the gauge group is a finite group; here you can compute everything explicitly, and the partition function is the cardinality of the moduli stack. But the moduli stack is not a finite set: it’s a finite groupoid. So, you need to use a generalization of cardinality to groupoids!

If you don’t, you get wrong answers that just don’t work.

Another great example comes from string theory. To get the right answers, you’ve got to use things like moduli stacks of elliptic curves, not moduli spaces.

(To a zeroth approximation, ‘stack’ means ‘groupoid, equipped with a smooth structure’.)

Posted by: John Baez on November 22, 2013 2:03 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

When Edward Witten gives a talk at a conference with ‘higher-dimensonal categories’ in the title, you know you’ve won :)

Posted by: David Corfield on November 22, 2013 9:26 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David wrote:

What I think will make you uncomfortable are situations where our worlds are modelled (a) as forming a smooth groupoid and (b) as forming a higher groupoid.

You’re ceding too much ground here. If you act like distinguishing between equality and isomorphism only matters much when we get into such ‘fancy’ situations, most philosophers will never get the point.

Be bold! It’s better to stick to your guns and argue that even when dealing with a finite set XX acted on by a finite group GG, the weak quotient X//GX//G is better than the ordinary quotient X/GX/G.

After all, it’s true! In this discussion thread I’ve pointed to two examples: summing over Feynman diagrams, and doing path integrals in gauge theories with finite gauge group. In both cases you need to use groupoid cardinality of X//GX//G instead of the ordinary cardinality of X/GX/G, to get the right answers!

And ‘the covariance of colored balls’ is really very close to what Jim Dolan and I were doing, when we connected Feynman diagrams to stuff types and groupoid cardinality. These simple combinatorial examples are great for explaining issues that also show up later in more ‘fancy’ examples.

Posted by: John Baez on November 22, 2013 2:56 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John,

You’re ceding too much ground here. If you act like distinguishing between equality and isomorphism only matters much when we get into such ‘fancy’ situations, most philosophers will never get the point.

Hey - philosophers invented some of this stuff!! I think the thing you call the “decategorifcation” of FinSetFinSet was invented by Frege, who wrote down the axiom,

c(X)=c(Y)XYc(X) = c(Y) \leftrightarrow X \sim Y

and gave the detailed interpretation of arithmetic into the resulting (second-order) theory. The notions x=yx = y and xyx \cong y are clearly distinguished and matter very much!! The notion xyx \cong y was quite important for Russell, Wittgenstein and Carnap, and used by Russell (e.g., in Introduction to Mathematical Philosophy (1919), Analysis of Matter (1927)) and by Carnap (Logical Structure of the World (1928)) to try and explain representation; and later by Carnap to begin to develop modal logic (state descriptions; structure descriptions) and confirmation theory. The isomorphism type of a relation was called a “relation-number” by Russell. Large amounts of stuff has been written on notions of indiscernibility - e.g., by Quine and many others.

So, I think you’re just being a bit too strong in your condemnations–because you’re frustrated and want people to take up not just category theory qua branch of mathematics, but “category-ism” as a “philosophy”.

It’s not simply true that philosophers don’t either pay attention to this stuff (many do, and write about it: e.g., Hellman a while back; Linnebo and Pettigrew in a 2011 paper; John Burgess in his forthcoming book) or that there aren’t philosophers (or logicians in philosophy depts) who work in this kind of area. I personally know many examples. Steve Awodey is a visitor, and his student Hans-Christoph is a PhD student, at MCMP, Munich.

I don’t know if you know any of the philosophers of physics in either Oxford or Munich (MCMP)? You should go and give a talk there - they don’t bite! (The new Math Institute here is 10 yards away from the Phil Faculty.)

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 5:35 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I wasn’t ‘condemning’ anyone, and I’m sorry if it sounded like that. I like philosophers, some of my best friends are philosophers — I’m even married to one! I’ve published a few papers in books edited by philosophers, and I like giving talks in philosophy departments.

However, I believe that most philosophers of mathematics don’t know much about smooth groupoids and higher groupoids. Certainly most mathematicians and physicists don’t! So when David wrote:

What I think will make you uncomfortable are situations where our worlds are modelled (a) as forming a smooth groupoid and (b) as forming a higher groupoid.

I feared that this would sound to most people as if he was ‘backing off’ into esoteric and obscure topics. I felt the key points can be made in simpler examples… like the example he started out with.

But maybe I was wrong. He would certainly need to go up to smooth groupoids to make certain points, e.g. the inadequacy of working with a skeleton.

Posted by: John Baez on November 22, 2013 6:25 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John wrote

Be bold! It’s better to stick to your guns and argue that even when dealing with a finite set XX acted on by a finite group GG, the weak quotient X//GX//G is better than the ordinary quotient X/GX/G.

But we established that this wasn’t what Jeff was doing. He is forming the set of equivalence classes, but he retains the symmetry groups on each member (encoded by a logical formula). As I keep saying, from our perspective he’s forming the skeleton.

As such, from our perspective it won’t be any surprise in these cases (involving discrete groupoids) that we end up being able to do the same things because the skeleton is equivalent. Hence my interest in “fancy situations” (which are really not so very fancy).

Posted by: David Corfield on November 22, 2013 8:34 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

If we stick with the simplified 2 indistinguishable particles/2 properties setup, are the objects in relevant action groupoid still the four models i\mathcal{M}_i I listed? (with the morphisms being the isomorphisms between them). It’s this “4-ness” that I’m saying needs to go down to 3! Because, physically, two of the models, 2\mathcal{M}_2 and 3\mathcal{M}_3, are isomorphic and count as representing the same state/world.

Is there some way of extracting the number 3 from the action groupoid?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 9:39 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Simultaneously messaging! As I just said above, yes there is a three there in the action groupoid. There are three components, or if you like, three objects in the skeleton.

The worry you keep hearing from those who haven’t understood that you’ve retained automorphism information, is that the ‘three’ by itself is not enough information to reconstruct the groupoid.

Up to equivalence, a groupoid is a multiset of groups. That ‘three’ would be counting the number of members in the multiset.

Posted by: David Corfield on November 22, 2013 9:46 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Ah - ok: so, on the groupoid approach, the three physical states come from the skeleton of the action groupoid.

On the other issue, yes. It’s because I tend to think about this kind of thing model-theoretically; I’ve got the models–the mathematical representations, if you like. The models come with their automorphism groups, and the groupoid is definable given the models. Admittedly, if I didn’t know what the models are, I’d be lost.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 10:14 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

the three physical states come from the skeleton of the action groupoid.

It’s better to say that they come from the connected components of the action groupoid, since skeleta are, as John said, gauche.

Posted by: Mike Shulman on November 22, 2013 7:40 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

Thanks and sure, yes – but the debate here comes from a question about the mathematical representation of physical reality. We know from the last 100 years of physics that there is some kind of equivalence relation, p\equiv_p, of “representing the same world/situation/state” amongst mathematical representations used in physics. E.g., we know this from three cases: GR, from gauge symmetries and from permutation symmetry of indistinguishable particles. But I‘m not saying whether p\equiv_p should be understood in terms of S/GS/G, or S//GS//G, or skeletons, or decategorification, or anything.

The physics literature has, in many cases,

if XYX \cong Y, then X pYX \equiv_p Y?

So, the category-theory formulation of this idea then is:

if X,YX,Y are in connected components of the action groupoid, then X pYX \equiv_p Y?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 11:30 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John wrote:

It’s better to stick to your guns and argue that even when dealing with a finite set XX acted on by a finite group GG, the weak quotient X//GX//G is better than the ordinary quotient X/GX/G.

David wrote:

But we established that this wasn’t what Jeff was doing. He is forming the set of equivalence classes, but he retains the symmetry groups on each member (encoded by a logical formula). As I keep saying, from our perspective he’s forming the skeleton.

Okay, sorry—I wasn’t following the conversation in detail; I just noticed Jeffrey making remarks like this:

You cannot do it your way, not as a physicist. You’re not counting states correctly. When you compute physical quantities, you must do it my way, and count the isomorphic copies as labelled representations of the same physical state – this is the standard method in physics.

I took that as him insisting that you had to use X/GX/G. I see now it could be him insisting that you had to use a skeleton of X//GX//G, instead of the standard construction of X//GX//G, or any other groupoid equivalent to X//GX//G.

If so, I would be tempted to argue that anything you can do with a category, you can do with an equivalent category. So, while working with a skeleton is acceptable, it’s misguided to insist that anyone else must work with a skeleton, as Jeffrey may be doing above. It would be like a philosopher insisting you have to use Roman numerals in order to correctly add 7 and 2.

It’s possible that persuading someone that equivalent categories are equally good is no easier than persuading them that isomorphic objects in a category are equally good. They’re closely interlinked points, both part of what I’d call “relaxing our attitude toward sameness”.

Alternatively, I agree that switching to a situation where you cannot take a skeleton might be convincing. There are examples involving manifolds XX and Lie groups GG.

Posted by: John Baez on November 22, 2013 6:05 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

In the higher groupoid direction, there must be a nice simple, small, discrete case we could talk about. Any ideas?

As for higher differential geometry, we’re spoilt for choice. Let’s take something from the nLab on fields:

“A field configuration of the electromagnetic field is a circle bundle with connection and a gauge transformation of the EM field is an equivalence of such connections.

Let therefore

BU(1) connΩ 1//U(1)DK(U(1)dlogΩ 1) \mathbf{B}U(1)_{conn} \coloneqq \Omega^1//U(1) \simeq DK(U(1) \stackrel{d log}{\to} \Omega^1)

be the quotient stack of the action of U(1)U(1) on the sheaf of differential 1-forms, equivalently the image under the Dold-Kan correspondence of the sheaf of chain complexes given by the Deligne complex for degree-2 ordinary differential cohomology, as indicated.”

Posted by: David Corfield on November 22, 2013 7:07 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Is there a reason that going to higher groupoids prevents us from forming skeleta?

Posted by: Mike Shulman on November 22, 2013 7:42 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Not in principle, but do you think it’s possible using Jeff’s logical technique?

Wouldn’t we expect to have to use higher pieces of HoTT than predicate logic to represent in a single expression a component of a higher groupoids?

Posted by: David Corfield on November 22, 2013 8:01 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David, yes, the idea is that for any model 𝒜\mathcal{A}, we can fix it up to isomorphism by a single “diagram formula”—called Φ 𝒜\Phi_{\mathcal{A}}–in the language L κ +,κ +L_{\kappa^{+},\kappa^{+}}, such that, for any \mathcal{B}, we have:

Φ 𝒜\mathcal{B} \models \Phi_{\mathcal{A}} iff 𝒜\mathcal{B} \cong \mathcal{A}

This has the further property that, for any permutation π:AA\pi : A \to A and skolem mapping α\alpha (which maps variables to constants), we get a corresponding skolem mapping β\beta such that,

πAut(𝒜)\pi \in Aut(\mathcal{A}) iff sk α(Φ 𝒜)sk β(Φ 𝒜)sk_{\alpha}(\Phi_{\mathcal{A}}) \equiv sk_{\beta}(\Phi_{\mathcal{A}})

So, in a slogan:

automorphic relabellings correspond to logically equivalent skolemizations.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 11:56 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

No, I don’t think so, not if we’re only talking about components. In HoTT, a predicate on a type AA is a map APropA\to Prop, and since PropProp is a set, any such map factors through the 0-truncation A 0{\Vert A \Vert}_0, i.e. the set of components. That’s true regardless of how truncated or not AA might be. Of course, the “automorphism group” at each component of an nn-type will be an nn-group rather than an ordinary group.

That reminds me of another issue, which might or might not be relevant. An automorphism group is not actually canonically associated to a component of a groupoid. Each object of that component has an automorphism group, and different objects in the same component have isomorphic automorphism groups, but the isomorphism is not unique or canonical. The best you can say is that each component has an associated “band”, where the category of “bands” is the quotient of the category of groups in which conjugate homomorphisms are identified. I’m not sure whether or not this is relevant to the discussion, however.

Posted by: Mike Shulman on November 23, 2013 1:00 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike and David,

So, if I understand this, we represent the world mathematically using a space Σ\Sigma of models (simple setups with indistinguishable thingies, like David described; or principal bundles from gauge theory; or spacetime models in GR), and we have a group GG acting on Σ\Sigma. This yields an action groupoid Σ//G\Sigma//G.

Then what David said is that the physical equivalence relation p\equiv_p for objects in Σ//G\Sigma//G then is defined by:

X pYX \equiv_p Y if and only if X,YX,Y are in the same component of Σ//G\Sigma//G.

Is that right? In the case we’re considering, each model has the form X=(S,)X = (S, \dots), where SS is the underlying carrier set, and G=Sym(S)G = Sym(S). So,

X pYX \equiv_p Y if and only if X,YX,Y are in the same component of Σ//Sym(S)\Sigma//Sym(S).

If I understand correctly, XX and YY are in the same component of Σ//Sym(S)\Sigma//Sym(S) if and only if Y=π *XY = \pi_{\ast}X, for some πSym(S)\pi \in Sym(S). But this just means, XX and YY are in the same component of Σ//Sym(S)\Sigma//Sym(S) if and only if XYX \cong Y. So, in other words,

X pYX \equiv_p Y if and only if XYX \cong Y.

But this quite literally is the Wald-Carroll-Rovelli explanation of physical equivalence! (And mine too …). It’s just Leibniz equivalence. But I thought you were all disputing this. Now it seems you’re agreeing with it! So I am now completely confused about what the debate is about.

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 2:08 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

…what David said is that the physical equivalence relation…

I was just showing you how we would understand what you call the physical equivalence relation, hoping to reassure you that we can make sense of your 3 states. This 3 is an invariant of the way we’ve modelled the situation. But this doesn’t mean I must subscribe to a particular physical or metaphysical gloss of how the world really is.

I can do good work keeping the right number of kids together on a school trip by treating them as indiscernible, just lining them up anyhow and counting, but it doesn’t mean I’m committed to their being clones.

This works well despite their individual charming properties because for my purposes they do behave as non-vanishing, non-merging entities.

As I said in my post, for any particular modelling of a physical situation, there may be a simple description of it in terms of entities and their properties under invariance of some kind. But no description is unique.

Once the modelling is done and we have some candidate mathematical representations, then any two mathematically equivalent representations will yield the same predictions.

Of course, our job is never finished. There are always inadequacies in any piece of real physics. It might happen that one of a collection of mathematically equivalent descriptions lends itself better to fruitful modification.

Posted by: David Corfield on November 23, 2013 10:19 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

Ok, but I think that this

I can do good work keeping the right number of kids together on a school trip by treating them as indiscernible, just lining them up anyhow and counting, but it doesn’t mean I’m committed to their being clones. This works well despite their individual charming properties because for my purposes they do behave as non-vanishing, non-merging entities.

isn’t a good analogy—as what you’re describing is a convenient abstraction, with respect to some useful equivalence relation:

x tripyx \equiv_{trip} y iff xx is a child on the trip and yy is a child on the trip

And clearly “x tripyx \equiv_{trip} y” does not imply “xx is a clone of yy”.

But, in the case of physics, the physical equivalence relation p\equiv_p (on the models used to represent the physical situations) is not a convenient choice. The choice of models is a matter of convenience; once that is fixed, the physical equivalence of the models is not a matter of convenience.

(Cf., the choice of a co-ordinate system ϕ\phi and measurement scale is a matter of convenience. Once that is fixed, the distance between two points is not a matter of convenience.)

It’s a feature of reality that there really are only three states, if the particles are indistinguishable! E.g., quoting again from the earlier online explanation,

Consider first the simplest case, of two particles and two energy levels. If the particles are distinguishable, as in the upper picture below, there are four states, two of which have energy , …. If the particles are indistinguishable, however, there are only three states, as in the lower picture…

And, e.g., from these online notes,

As before, the instantaneous state of the system is specified by the complex wave-function ψ(x 1,x 2,t)\psi(x_1,x_2,t). However, the only thing which this wave-function tells us is that the probability of finding the first particle between x 1x_1 and x 1+dx 1x_1+dx_1, and the second between x 2x_2 and x 2+dx 2x_2+dx_2, at time tt is |ψ(x 1,x 2,t)| 2dx 1dx 2\vert\psi(x_1,x_2,t)\vert^2\,dx_1\,dx_2. However, since the particles are identical, this must be the same as the probability of finding the first particle between x 2x_2 and x 2+dx 2x_2+dx_2, and the second between x 1x_1 and x 1+dx 1x_1+dx_1, at time tt (since, in both cases, the physical outcome of the measurement is exactly the same).

And from here too:

QM teaches us to think about the states. A lot of people get themselves tangled trying identify the particles instead of the states.

Specifically: It makes no sense whatsoever to talk about two states that differ by exchange of identical particles.

To illustrate the right way to think about things, consider the following states, for particles in two boxes:

[diagrams omitted]

For indistinguishable bosons, these count as three states, and they are equiprobable, assuming the boxes and the setup procedure etc. are symmetric. That is, the probabilities are in the ratio a:b:c = 1:1:1.

So, the mathematical representation used to model the world needs to count the physical states, and this involves counting some mathematical representations as describing the same physical situation.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 11:42 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike wrote

No, I don’t think so, not if we’re only talking about components.

I don’t think we are. The issue is whether we can reconstruct an nn-groupoid, from some logical formula which stands for a component.

Of course, the “automorphism group” at each component of an nn-type will be an nn-group rather than an ordinary group.

Right. But can that nn-group be recovered from the corresponding logical formula.

In the case of discrete 1-groupoids this is plausible. E.g., were we talking about finite sets, I could take the famous formula for there are exactly nn elements, and then consider permutations on the variables, or better on the constants in the skolemization.

I’m expressing doubt that something similar is possible for 2-groupoids. I guess an easy test is to try to do it for finite groupoids.

Posted by: David Corfield on November 23, 2013 10:28 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

I’m expressing doubt that something similar is possible for 2-groupoids. I guess an easy test is to try to do it for finite groupies.

I think there’s a generic response to this generic kind of “it’s impossible to do X …” line of argument, which is this: presumably any nn-category CC can be interpreted as a class/set-theoretic object C *C^{\ast}?

If so, then take the corresponding L ,L_{\infty,\infty}-formula Φ C *\Phi_{C^{\ast}} (the “carrier set dependence” has been eliminated by construction).

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 12:44 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike wrote:

Is there a reason that going to higher groupoids prevents us from forming skeleta?

Not that I know of. So if that’s the point — if David is battling against the pro-skeleton faction — I think he should drag out the smooth or topological groupoids.

Posted by: John Baez on November 22, 2013 7:49 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David and John,

In what sense does the map,

𝒜Φ 𝒜\mathcal{A} \mapsto \Phi_{\mathcal{A}}

from relational models (of cardinality κ\kappa), to formulas in the (typically) infinitary language L κ +,κ +L_{\kappa^{+},\kappa^{+}}, correspond to a “skeleton”?

Could you give me the exact definition of how one corresponds to the other?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 12:03 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Jeffrey wrote:

In what sense does the map,

𝒜Φ 𝒜\mathcal{A} \mapsto \Phi_{\mathcal{A}}

[…] correspond to a “skeleton”?

I’ve left out some stuff because it’s unimportant for answering this question. All that’s important is something I think you said earlier, using somewhat different notation:

𝒜Φ 𝒜=Φ \mathcal{A} \cong \mathcal{B} \iff \Phi_{\mathcal{A}} = \Phi_{\mathcal{B}}

I’ll assume this is true; if it’s not I apologize because I’m misunderstanding you.

When we write

𝒜\mathcal{A} \cong \mathcal{B}

we are assuming, explicitly or implicitly, that the things called 𝒜,\mathcal{A}, \mathcal{B} are objects in a groupoid GG, with

𝒜 \mathcal{A} \cong \mathcal{B}

asserting that there exists an isomorphism between them.

When we then say

𝒜Φ 𝒜=Φ \mathcal{A} \cong \mathcal{B} \iff \Phi_{\mathcal{A}} = \Phi_{\mathcal{B}}

it follows that the things called 𝒜,\mathcal{A}, \mathcal{B} are elements of a set that is in 1-1 correspondence with the set SS of isomorphism classes of GG.

This set SS, the set of isomorphism classes [x][x] of objects xx in the groupoid GG, is called the decategorification of the groupoid GG. Note that

xy[x]=[y] x \cong y \iff [x] = [y]

We can however create a groupoid having one object for each element of SS, with all morphisms being automorphisms, such that the group of automorphisms of any object xx is is the group of automorphisms of [x][x]. This groupoid is called a skeleton of the groupoid GG. Let’s denote it by Sk(G)\mathrm{Sk}(G).

It’s a famous fact that the groupoid Sk(G)\mathrm{Sk}(G) is equivalent to GG. However, by how we’ve created it, it has the additional property that whenever two objects in Sk(G)\mathrm{Sk}(G) are isomorphic, they are equal.

So, people who believe isomorphic things should be equal are naturally drawn to using the decategorification, or the skeleton.

The skeleton is better, since it contains more information. But those who believe that equivalent groupoids are ‘the same in every important respect’ will argue — and in my opinion, correctly — that anything you might want to do with the skeleton Sk(G)\mathrm{Sk}(G), you can do with the original groupoid GG.

Posted by: John Baez on November 23, 2013 6:19 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John, thanks - that’s close; there are two mappings; Φ\Phi (which takes isomorphic models to logical equivalent things) and Φ^\hat{\Phi} which takes isomorphic models to the same thing. So,

Φ^ 𝒜=Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}} \Leftrightarrow \mathcal{A} \cong \mathcal{B}

These things Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} are not defined to be equivalence classes, but that’s the structural effect, yes. So, this amounts, categorically speaking, to decategorifcation.

But it is extremely important that Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} is not an equivalence class. For it is a functional entity, which can be applied to some physical relations R,SR,S (e.g., say Red,Green,\mathbf{Red},\mathbf{Green},\dots). Then Φ^ 𝒜[R,S]\hat{\Phi}_{\mathcal{A}}[R,S] is a proposition. And this proposition Φ^ 𝒜[R,S]\hat{\Phi}_{\mathcal{A}}[R,S] is identical to Φ^ [R,S]\hat{\Phi}_{\mathcal{B}}[R,S] exactly if 𝒜\mathcal{A} \cong \mathcal{B}.

Going back to the “indiscernible balls/particles” setup that David described, the crucial issue is how to count the physically different worlds/states to accord with what statistical physics tells us. So, I suggest that we identify (physical) worlds with things like Φ^ [Red,Green,Blue]\hat{\Phi}_{\mathcal{M}}[\mathbf{Red},\mathbf{Green}, \mathbf{Blue}]. So, the conclusion is then that,

If 𝒩\mathcal{M} \cong \mathcal{N}, then Φ^ [Red,Green,Blue]=Φ^ 𝒩[Red,Green,Blue]\hat{\Phi}_{\mathcal{M}}[\mathbf{Red},\mathbf{Green}, \mathbf{Blue}] = \hat{\Phi}_{\mathcal{N}}[\mathbf{Red},\mathbf{Green}, \mathbf{Blue}].

So, the four models, i\mathcal{M}_i, of my simplified version of David’s setup give three worlds, as required. We can think of the distinct but isomorphic models 2, 3\mathcal{M}_2,\mathcal{M}_3 as distinct but isomorphic (unphysical) “labellings” of the same (physical) world. The same physical world, but “labelled” in two distinct, isomorphic, ways.

And now we’re back to the Leibnizian “isomorphic models represent the same physical world/situation” point, that we began discussing a couple of weeks ago!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 7:17 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David wrote:

In the higher groupoid direction, there must be a nice simple, small, discrete case we could talk about. Any ideas?

Here’s an idea. The following example is discrete. It’s not small. But since philosophers of mathematics tend to be fond of set theory and don’t mind ‘big’ mathematical entities, maybe that’s not a problem.

The 2-groupoid of all groupoids!

Like I said, it’s not small. This may be distracting to some, but it can be dealt with in various standard ways (e.g. the axiom of universes). So let me not worry about this, and get to the actual point.

For someone to realize that working with the skeleton of a groupoid is ‘just the same’ as working with the groupoid itself, they need to understand:

1) any groupoid is equivalent to its skeleton,

2) any ‘legitimate’ statement about a groupoid GG is true iff it is true of any equivalent groupoid HH. (Examples of illegitimate statements, and explanations of why such statements are useless, are required here. This really takes time; it can’t be understood overnight.)

Then, ultimately,

3) equivalence is the right generalization of equality for objects in 2-groupoids. In 1) and 2), where we are talking about equivalence of groupoids, that’s just an example: the 2-groupoid of all groupoids.

Maybe this is too steep a road for most. But for someone interested in foundations of mathematics, this steep road leads to truly magnificent vistas.

Posted by: John Baez on November 22, 2013 7:46 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John,

The question we’re been discussing is, when 𝒜,\mathcal{A},\mathcal{B} are mathematical representations of some kind, what does

𝒜\mathcal{A} represents the same physical world as \mathcal{B} does

mean. Write this equivalence relation as

𝒜 p\mathcal{A} \equiv_p \mathcal{B}

This is why the standard method in statistical physics seems highly relevant, because in that case, we have guidance about physical equivalence. In that case, we have

If 1 2\mathcal{M}_1 \cong \mathcal{M}_2 then 1 p 2\mathcal{M}_1 \equiv_p \mathcal{M}_2

Similarly, for spacetime models, the formulations from Wald-Carroll-Rovelli give us,

If 1 2\mathcal{M}_1 \cong \mathcal{M}_2 then 1 p 2\mathcal{M}_1 \equiv_p \mathcal{M}_2

Everything that’s been said (at least by me) concerns the notion p\equiv_p physical equivalence.

It’s possible that persuading someone that equivalent categories are equally good is no easier than persuading them that isomorphic objects in a category are equally good. They’re closely interlinked points, both part of what I’d call “relaxing our attitude toward sameness”.

This is not what is happening. No one disputes any of this. The discussion concerns physical equivalence. There is a notion of “sameness” here. The notion p\equiv_p above. How is it to be understood?

I now think I see how David’s suggestion works now: it’s “connected components of the action groupoid”. Is that the right answer, in general?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 22, 2013 11:08 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John,

It would be like a philosopher insisting you have to use Roman numerals in order to correctly add 7 and 2.

It was a philosopher/mathematician, Frege (1892, “On Sense and Reference”, and later) who explained why this is mistaken—i.e., use/mention confusion—and other philosophers, like Carnap and Quine (Mathematical Logic), etc., who have made a big point about it since. Eventually, it became clear that,

An atomic formula (t=u)(t = u) is true in 𝒜\mathcal{A} if and only if t 𝒜=u 𝒜t^{\mathcal{A}} = u^{\mathcal{A}}.

On the use of roman numerals, suppose L 0,s,+,×L_{0,s,+,\times} is the language of arithmetic in its usual signature, and L rn,+,×L_{rn, +, \times} uses roman numerals.

How would a logician characterize the relationship between arithmetic T 1T_1 formulated in L 0,s,+,×L_{0,s,+,\times} and arithmetic T 2T_2 formulated in L rn,+,×L_{rn,+,\times}? For example, which mapping would you consider? What has to be preserved?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 12:48 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Oops, wrong URL. The URL for Quine’s discussion of use vs. mention should be this:

Quine, 1940, Mathematical Logic, Sc. 4, “Use Versus Mention”.

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 2:22 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Jeffrey wrote:

It was a philosopher/mathematician, Frege (1892, “On Sense and Reference”, and later) who explained why this is mistaken—i.e., use/mention confusion—and other philosophers, like Carnap and Quine, etc., who have made a big point about it since.

Right. You seem to feel I’m attacking philosophers, but I’m not. I will stop using the word ‘philosopher’ in any future comments on this thread, to prevent this misunderstanding.

I was just saying: just as it would ill behoove a philosopher to argue that we can only add numbers using Roman numerals, it would ill behoove them to argue that we can only work with a groupoid by passing to its skeleton.

My point was: in each case we can do this, but it’s often an inconvenient way of describing the data we’re working with, and it would be a major mistake to claim it’s necessary.

Posted by: John Baez on November 23, 2013 5:50 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John, good!

it would ill behoove them to argue that we can only work with a groupoid by passing to its skeleton.

Sure, so suppose Mod(σ)Mod(\sigma) is the class of models of signature σ\sigma. Then I’m considering a certain mapping,

Φ:Mod(σ)L ,(σ)\Phi : Mod(\sigma) \to L_{\infty,\infty}(\sigma)

where L ,(σ)L_{\infty,\infty}(\sigma) is the vast infinitary language based on signature σ\sigma. This mapping has three nice properties:

  1. Φ 𝒜\mathcal{B} \models \Phi_{\mathcal{A}} iff 𝒜\mathcal{B} \cong \mathcal{A}.

  2. 𝒜\mathcal{A} \cong \mathcal{B} iff Φ 𝒜Φ \Phi_{\mathcal{A}} \equiv \Phi_{\mathcal{B}}.

  3. πAut(𝒜)\pi \in Aut(\mathcal{A}) iff sk α(Φ 𝒜)sk β(Φ 𝒜)sk_{\alpha}(\Phi_{\mathcal{A}}) \equiv sk_{\beta}(\Phi_{\mathcal{A}}).

(where, here 𝒜=(A,)\mathcal{A} = (A, \dots) and =(B,)\mathcal{B} = (B, \dots) are models of signature σ\sigma; and, in the last one, π:AA\pi : A \to A is a permutation and sk α(),sk β()sk_{\alpha}(-), sk_{\beta}(-) involve “skolemizations” that I don’t want to go into.)

David says this involves a “skeleton”. How is this demonstrated?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 6:28 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Let me pop out of all these comment nestings and try to say in a different way what I now think the confusion is. I think that David, John, and I are taking issue with the idea that physical equivalence should — in general — be thought of as a mere relation. What sticks in our throat is saying that “𝒜\mathcal{A} represents the same physical world as \mathcal{B} does” without specifying in what way they represent the same physical world, i.e. by specifying a particular isomorphism between them.

To a category theorist, the fact that one shouldn’t do this is implicit in the idea that the mathematical models in use are the objects of a groupoid rather than the elements of a set. We don’t (in polite company) talk about whether two elements of a groupoid are equal, only about whether they are isomorphic. So we should not talk about whether two mathematical structures “are physically equivalent”, we should talk instead about particular “physical equivalences” between them.

Now having established the fact that these things form a groupoid, we can consider the question of how to “count” them. It seems quite possible to me that the answer may be different in different contexts. I think it’s well-established by now that in the context of Feynman diagrams, the appropriate way to “count” a groupoid is given by “groupoid cardinality” which takes account of the size of the automorphism groups. But it may be that in some other context (statistical physics?), the appropriate way to “count” a groupoid is given by just counting the number of isomorphism classes, and if so, there’s nothing wrong with that.

There is an equivalence relation on objects of a groupoid defined by the mere existence of an (unspecified) isomorphism between them, and this equivalence relation can be important and interesting. We may even want to count the number of equivalence classes of this equivalence relation. And I agree that this is the equivalence relation that you’re calling “physical equivalence”. But I think we are bothered by calling it “physical equivalence”, not because we think that “physical equivalence” should be a different equivalence relation, but because we think that “physical equivalence” should not be a mere equivalence relation.

Posted by: Mike Shulman on November 23, 2013 6:18 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike wrote:

Let me pop out of all these comment nestings and try to say in a different way what I now think the confusion is. I think that David, John, and I are taking issue with the idea that physical equivalence should — in general — be thought of as a mere relation. What sticks in our throat is saying that “𝒜 represents the same physical world as ℬ does” without specifying in what way they represent the same physical world, i.e. by specifying a particular isomorphism between them.

Good, you said it better than I was going to. I was going to quote this passage of Jeffrey’s:

The question we’re been discussing is, when 𝒜,ℬ are mathematical representations of some kind, what does

𝒜 represents the same physical world as ℬ does

mean. Write this equivalence relation as…

And I was going to say Whoa! That’s where the problem starts!

The problem starts with treating sameness as a mere relation, instead of keeping track of the ways that two things can be the same. The ‘ways’ are the morphisms in your category, and they’re just as important as the ‘things’ (the objects).

For example, a cube has 48 symmetries generated by reflections and rotations. Each of these is a ‘way for the cube to be the same as itself’. Saying that the cube has 48 ways of being the same as itself is interesting! Merely saying that the cube is the same as itself, while true, contains a lot less information.

But I think we are bothered by calling it “physical equivalence”, not because we think that “physical equivalence” should be a different equivalence relation, but because we think that “physical equivalence” should not be a mere equivalence relation.

Agreed, that’s exactly what’s bugging me.

Of course, it took mathematicians a long time to reach the viewpoint you and I share, and I don’t think any amount of persuasion was sufficient to do the job: it may just be that there were lots of problems we couldn’t easily solve until we took this viewpoint. In some ways switching from sets to groupoids and then general homotopy types was a very pragmatic decision. It’s hard to say that the old ways of thinking were ‘false’—it’s just that we became more powerful when we acquired the new ones.

Posted by: John Baez on November 23, 2013 6:47 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike and John,

Right, I get the point. That explains it well. (I have to take back my Feynman diagram comment: it’s ages since I did a scattering calculation, and I forgot the complexities of the symmetry factor; and now, reading up on it, yes, I see: the symmetry factor involves |Aut(G)||Aut(G)|. I’m not sure how to relate that to what I say.)

Let me go back though. My suggestion is that physical worlds are things like:

W=Φ^ [R 1,]W = \hat{\Phi}_{\mathcal{M}}[\mathbf{R}_1,\dots]

where R i\mathbf{R}_i are physical properties & relations. With that definition, I get the conclusion that isomorphic models ,𝒩\mathcal{M},\mathcal{N} represent the same world.

This implements the basic Leibnizian intuition, that “spacetime points have no independent meaning” (roughly how Rovelli phrases it). But all that has been thrown away is the carrier set of any particular model.

So, let me choose a world, W=Φ^ [R 1,]W = \hat{\Phi}_{\mathcal{M}}[\mathbf{R}_1,\dots]. So, I now have a model, \mathcal{M}, which represents WW (relative to the relations R 1,\mathbf{R}_1,\dots). One could call this a “gauge choice”: models are like co-ordinate systems. And so, I have Aut()Aut(\mathcal{M}) too. And this is the symmetry group of the physical world WW!

Suppose the world WW has a cube somewhere inside it. This means that any model \mathcal{M} of WW will also have a mathematical representation, 𝒩\mathcal{N}, of the cube somewhere “inside” it. And then I will have the 48 symmetries that John mentions as Aut(𝒩)Aut(\mathcal{N}). So I don’t think I’ve lost, or ignored, the symmetries of the world WW. I’ve simply encoded what a world is, in order to get the right way to “count physical equivalences”. I know that the world WW has a symmetry group, and I can even define it!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 7:49 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Great! I think we’re getting closer to seeing eye-to-eye.

But before we get too happy, let me say how a category theorist would think about this.

What you’ve done here is described an equivalence

Φ^:ModelsWorlds \hat{\Phi} : Models \to Worlds

from a groupoid with ‘models’ like 𝒜\mathcal{A} as objects to another groupoid with ‘worlds’ like W=Φ^ 𝒜W = \hat{\Phi}_{\mathcal{A}} as objects.

The latter groupoid is skeletal, meaning that isomorphic objects are equal. Because it is also equivalent to the former groupoid, we call it a skeleton of the first.

As any functor must, Φ^\hat{\Phi} sends each object and each morphism of ModelsModels to one of WorldsWorlds. At first you hadn’t defined Φ^\hat{\Phi} on morphisms, so I complained that you were decategorifying. But now I see you’re constructing a skeleton in a certain interesting way.

From the viewpoint of a category theorist, the fact that the latter groupoid is skeletal is not the interesting thing here. The interesting thing is that we’ve got an equivalence between groupoids, one defined in a ‘semantic’ way in terms of models of a logical theory, and another defined in a ‘syntactic’ way.

This equivalence of groupoids is probably one of the syntax-semantics relationships that category-theoretic logicians like to study. There are lots of these, for many different forms of logic. You seem to be using infinitary first order logic with relations. You’re saying that the groupoid of models of a theory formulated in this language is equivalent to a groupoid that can be described syntactically.

I hope a category-theoretic logician could go a bit further and tell me what they call this equivalence of groupoids! My best guess is that it’s related to this:

• Michael Makkai, Stone duality for first order logic, Advances in Mathematics 65, (1987), 97-170.

Here’s how the paper starts:

The most interesting phenomena in model theory are conclusions concerning the syntactical structure of a first order theory drawn from the examination of the models of the theory. With these phenomena in mind, it is natural to ask if it is possible to endow the collection of models of the theory with a natural abstract structure so that from the resulting entity one can fully recover the theory as a syntactical structure. We report here on results intended to constitute a positive answer to this question.

Consider a first order theory TT. The models of TT form a category ModTMod T with morphisms the elementary embeddings. One observes that every formula ϕ\phi of the theory, say with one free variable, gives rise to a functor [ϕ][\phi] from ModTMod T to SETSET, the category of sets.

He shows nicely how this construction, which goes further, is a generalization to first-order logic of Stone duality for Boolean algebras (or in other words, propositional logic).

(Note that his ModTMod T has noninvertible morphisms, but if we restrict attention to the isomorphisms I’m hoping we get the groupoid I was calling ModelsModels above.)

Posted by: John Baez on November 23, 2013 6:05 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John

The interesting thing is that we’ve got an equivalence between groupoids, one defined in a ‘semantic’ way in terms of models of a logical theory, and another defined in a ‘syntactic’ way.

Yes, in FOL, the language is too weak to get a “balance” between syntax and semantics—at least if one wants strong definability/categoricity results. E.g., ZFCZFC (if consistent) has countable models. To get things to match, you need to use much stronger syntax: infinitely long conjunctions/disjunctions and infinitely long quantifier prefixes. What I’m doing is very basic, and not fancy at all; in fact, it seems to be mathematically uninteresting. There are many interesting results in this field (famously, Scott’s Isomorphism Theorem). The method I use is really a simple generalization to infinitary languages of the Diagram Lemma in model theory. The reason I think it’s philosophically interesting is because it allows one to “throw away” the carrier sets of isomorphic models, and this has applications to structuralism in both philosophy of maths and philosophy of physics.

Thanks for the link to Makkai’s paper!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 24, 2013 2:34 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I think there’s another aspect to the confusion, which is that we category theorists tend to treat objects of a category (such as these mathematical models \mathcal{M}) categorically, which is to say, we study them only with respect to the category in which they sit. Jeff, however, is “looking inside” these objects, saying that they are constructed as models of some logical theory, and using that construction of them to do something else. This took me a bit of time to understand.

For instance, I think when David asked whether we can “logically” extract the automorphism nn-groups from an nn-groupoid, he was thinking of the nn-groupoid categorically. But Jeff’s response

presumably any nn-category CC can be interpreted as a class/set-theoretic object C *C^\ast? If so, then take the corresponding L ,L_{\infty,\infty}-formula Φ C *\Phi_{C^\ast}

seems to assume that the nn-groupoid is concrete, i.e. that its objects are models of some theory, in the classical sense of sets equipped with structure satisfying axioms. Am I hearing that right? If not, please explain. But if so, then I think I would respond that our nn-groupoid might not be concrete. In the case n=1n=1, it might be that our 1-groupoids are usually concrete or can be regarded as concrete, but for n2n\ge 2 I don’t see how to make any sense of that, since sets equipped with any sort of structure can only form a 1-groupoid.

I also don’t quite see yet how Jeff is constructing a skeleton, rather than (something bijective to) the set of isomorphism classes. For one thing, I don’t see what the morphisms of the groupoid WorldsWorlds are, or how the functor Φ^\widehat{\Phi} is defined on morphisms. Probably that was said in some comment that I missed, but maybe someone could say it again?

Part of what’s bothering me is the issue of “bands” I mentioned above. For instance, when Jeff says

So, let me choose a world WW… I now have a model \mathcal{M}, which represents WW… And so, I have Aut()Aut(\mathcal{M}) too. And this is the symmetry group of the physical world WW!

What do you mean by “have” and “is”? Given WW, there exists some model \mathcal{M} which represents it, but there is no canonical choice of such an \mathcal{M}, is there? And thus, the symmetry group Aut()Aut(\mathcal{M}) is not canonically determined either. So when you say that this “is” the symmetry group of WW, if you’re trying to use that as a definition of “the symmetry group of WW”, it doesn’t work, unless you’re willing to make an arbitrary choice of one such \mathcal{M} for every world WW. Or you could be saying that there is an independent definition of “the symmetry group of WW” (which is what?) and that this group turns out to be isomorphic to Aut()Aut(\mathcal{M}) for any \mathcal{M} representing WW. Which is it?

Posted by: Mike Shulman on November 23, 2013 7:03 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike, thanks. I probably have to try and answer these separately. Yes, you’re right that I’m thinking of the 𝒜\mathcal{A}s as models in the model-theory sense; i.e., as “structured-sets”, of the form 𝒜=(A,)\mathcal{A} = (A, \dots), with a carrier set AA, and some distinguished relations. So, collections of them, with morphisms being say isomorphisms or elementary embeddings, form concrete categories, yes.

But, if I understand right, any category (concrete or not) can be thought of as a 2-sorted model:

𝒞=(Ob,Mor;s,t,m)\mathcal{C} = (Ob,Mor; s,t,m)

where s:MorObs: Mor \to Ob is the “source mapping”, t:MorObt: Mor \to Ob is the target mapping, and mMor 3m \subseteq Mor^3 is the composition: these satisfy certain uniqueness and associativity conditions.

If that’s right, then there is a formula Φ 𝒞\Phi_{\mathcal{C}} that defines 𝒞\mathcal{C} up to isomorphism. It’s easiest to see in a finite case. For example, if GG is the Klein 4-group, let 𝒞=(Ob,Mor;s,t,m)\mathcal{C} = (Ob,Mor; s,t,m) be the corresponding groupoid with one element and four morphisms. I can write down a formula Φ 𝒞\Phi_{\mathcal{C}} defining 𝒞\mathcal{C} up to isomorphism. (It’s complicated, and I’d have to think about it for a while.)

In general, concrete or not, a category 𝒞\mathcal{C} should have a categorical (in the logical sense) syntactic description in L ,L_{\infty,\infty}. It is required that ObOb be of definite cardinality.

But is this all still true for nn-categories? I’d need to see how to describe, e.g., a 2-category as a many-sorted model (3-sorted?) satisfying certain conditions. I think this can be done. I’m not sure.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 7:49 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

What do you mean by “have” and “is”? Given W, there exists some model ℳ which represents it, but there is no canonical choice of such an ℳ, is there?

Yes, that’s right. Given WW, the choice of some \mathcal{M} that represents WW is analogous to a “gauge choice”, a bit like choosing a co-ordinate system; in fact, a like choosing a global co-ordinate system. There is no “canonical model” for a world, much as there is no “canonical co-ordinate system” for a manifold.

Hence my semi-joke that “in reality, there are no balls”; cf., Rovelli’s interpretation of diffeomorphism invariance (= LE)—that “spacetime points have no independent meaning”. I am in a sense “deleting” the underlying carrier set of a spacetime model (M,g,T,)(M,g,T,\dots), while retaining its abstract structure (up to isomorphism).

And thus, the symmetry group Aut(ℳ) is not canonically determined either.

Right, but if ,𝒩\mathcal{M},\mathcal{N} are isomorphic gauge choices for WW, then Aut()Aut(𝒩)Aut(\mathcal{M}) \cong Aut(\mathcal{N}). Strictu dictu, Aut()Sym(M)Aut(\mathcal{M}) \subseteq Sym(M), where MM is the carrier set of \mathcal{M}, and Aut(𝒩)Sym(N)Aut(\mathcal{N}) \subseteq Sym(N), where NN is the carrier set of \mathcal{M}, and since, typically MNM \neq N, we have that Sym(M)Sym(N)Sym(M) \neq Sym(N). But this is ok. If that worries you, then let G 1=Aut()G_1 = Aut(\mathcal{M}) and let G 2=Aut(𝒩)G_2 = Aut(\mathcal{N}). Since G 1G 2G_1 \cong G_2, we get:

Φ^ G 1=Φ^ G 2\hat{\Phi}_{G_1} = \hat{\Phi}_{G_2}.

I.e., G 1G_1 and G 2G_2 have the same “abstract structure”.

So when you say that this “is” the symmetry group of W, if you’re trying to use that as a definition of “the symmetry group of W”, it doesn’t work, unless you’re willing to make an arbitrary choice of one such ℳ for every world W.

Right: like a global co-ordinate system. The groupoid of models for a world WW is like a maximal atlas, and the isomorphisms between the models are like transition maps.

So, the definition of the (abstract) automorphism group of a world WW is given by:

If W=Φ^ [R 1,]W = \hat{\Phi}_{\mathcal{M}}[\mathbf{R}_1,\dots], then Aut(W):=Φ^ Aut()Aut(W) := \hat{\Phi}_{Aut(\mathcal{M})}.

As an application, I listed the three (physical) worlds W 2,0,W 1,1,W 0,2W_{2,0}, W_{1,1}, W_{0,2} for the simplified 2-particle/2-properties setup, which has four models 1,, 4\mathcal{M}_1, \dots, \mathcal{M}_4. Then, say, we get:

Aut(W 2,0)=Φ^ Aut( 1)Aut(W_{2,0}) = \hat{\Phi}_{Aut(\mathcal{M}_1)}

which is in fact the (abstract) symmetric group S 2S_2 on 2 elements.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 8:29 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Right, but if ,𝒩\mathcal{M},\mathcal{N} are isomorphic gauge choices for W, then Aut()Aut(𝒩)Aut(\mathcal{M})\cong Aut(\mathcal{N})

Indeed, but there is no specified such isomorphism. The isomorphism depends on the choice of an isomorphism 𝒩\mathcal{M}\cong\mathcal{N}, which is not determined by knowing only that \mathcal{M} and 𝒩\mathcal{N} are in the same isomorphism class (WW). So the automorphism group “Aut()Aut(\mathcal{M})” is determined by WW only up to non-unique isomorphism, which generally in mathematics is not enough.

For instance, suppose you wanted to say that the symmetry group of WW acts on some object XX, which after all is what groups are for. You might do this by specifying how Aut()Aut(\mathcal{M}) acts on XX for some model \mathcal{M} representing WW. But if you then want to transfer this to an action by Aut(𝒩)Aut(\mathcal{N}) for some other model 𝒩\mathcal{N} representing WW, you’ll have to choose an isomorphism 𝒩\mathcal{M}\cong\mathcal{N}, and different isomorphisms will yield different actions by Aut(𝒩)Aut(\mathcal{N}). So it isn’t possible to give a meaning to “the symmetry group of WW”, for a meaning of “the” that would let you do the things that mathematicians and physicists need to do with groups, unless you’re willing to arbitrarily choose a particular model \mathcal{M} as a “preferred” representative of WW.

This is different from the situation with coordinate systems, because two coordinate systems on the same manifold are related by a unique isomorphism.

Posted by: Mike Shulman on November 23, 2013 9:18 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

It’s true that categories (as defined in set theory) are the models of a 2-sorted theory (even a 1-sorted theory if you are clever). Similarly, nn-categories are the models of an (n+1)(n+1)-sorted theory. But that’s happening at a different level from saying that the objects of a category are the models of a theory, so I don’t understand why it’s relevant?

Posted by: Mike Shulman on November 23, 2013 8:34 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

Similarly, nn-categories are the models of an (n+1)(n+1)-sorted theory. But that’s happening at a different level from saying that the objects of a category are the models of a theory, so I don’t understand why it’s relevant?

Right, but I don’t think that, in general, the objects have to be models in the model-theoretic sense. In the case of physics, I think they are models in the model-theoretic sense: a carrier set of “spacetime points”, or “particles”, etc., with some distinguished relations.

I think when David asked whether we can “logically” extract the automorphism nn-groups from an nn-groupoid, he was thinking of the nn-groupoid categorically. But Jeff’s response “presumably any nn-category CC can be interpreted as a class/set-theoretic object C *C^{\ast}? …” seems to assume that the nn-groupoid is concrete

In the purely mathematical case, I was thinking that perhaps this doesn’t follow. If an nn-category CC is interpreted as a class/set-theoretic object C *C^{\ast}, then C *C^{\ast} is a model of an n+1n+1-sorted theory. But the objects in C *C^{\ast} needn’t be structured sets/models. They could, e.g., be ordinals. Maybe I’m misunderstanding this question though!

So, is the question: how does one logically extract the automorphism 22-groups from a 22-groupoid CC? My answer was to interpret CC as a 3-sorted set-theoretical model C *C^{\ast}, and then define the formula Φ C *\Phi_{C^{\ast}}, and does this not yield (implicitly define) the automorphism 22-groups?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 10:01 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

But in your construction of the Φ\Phi’s, you are using that the objects are concrete models of some theory. I thought the question was whether that method could be generalized to extract information about the automorphism (nn-)groups.

Posted by: Mike Shulman on November 23, 2013 11:21 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Yes, because I’m mainly thinking about the physical case, where we have a concrete groupoid, or something like that, with structured sets/models \mathcal{M} representing physical worlds (the carrier sets of which have “particles”, “spacetime points”, etc). My goal is to eliminate the carrier set, while retaining all the “structure”, which is now understood as “logical relationships amongst relations”. Call this view Physical Leibnizianism: it’s a metaphysical view about possible (physical) worlds. If you read the section in Rovelli’s 2004 book on QG, about the interpretation of diffemorphism invariance, he says that one doesn’t have fields living on a carrier set of “spacetime points”; rather, the spacetime points have “no independent physical meaning”, and one just has “fields on fields”, as it were. (I’m quoting from memory.) That’s what I’m doing; or at least, trying to do.

But, in the purely mathematical case, I think the question is: given an nn-groupoid 𝒞\mathcal{C}, can we apply this “infinitary diagram” method to give a complicated formula Φ 𝒞\Phi_{\mathcal{C}} from which the nn-groups can be extracted somehow? I think so. But I am very unsure. I think your point about not being unique-up-to-unique isomorphism will apply. Because 𝒞\mathcal{C} is turned into a n+1n+1-sorted structure, and one only gets a model-class, I think. (I.e., a class of \mathcal{M} satisfying some formula ϕ\phi or theory TT.) But this last point is still very confusing to me.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 24, 2013 1:04 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

My goal is to eliminate the carrier set, while retaining all the “structure”, which is now understood as “logical relationships amongst relations”.

That’s a funny way of understanding “structure”. I would say that the way to eliminate the carrier set while retaining all the structure would be to simply regard a structure as an object of a category, without “peeking inside it”.

Posted by: Mike Shulman on November 24, 2013 5:34 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

I would say that the way to eliminate the carrier set while retaining all the structure would be to simply regard a structure as an object of a category, without “peeking inside it”.

Ok, but doesn’t this require an “ambient category” that the objects live inside? My proposed definition of the “abstract structure of 𝒜\mathcal{A}” doesn’t involve anything extraneous to 𝒜\mathcal{A} at all; certainly no other models, or morphisms, and whatnot. It’s intrinsic to 𝒜\mathcal{A}, if you like. It is more like a “purely logical picture” of 𝒜\mathcal{A}, where the “nodes” lack labels.

So, in a bit more detail, given 𝒜=(A,)\mathcal{A} = (A, \dots) in the usual model-theoretic sense, first one gives the (categorical) diagram formula Φ 𝒜\Phi_{\mathcal{A}}, which has all its first-order variables existentially quantified, and it has free second-order variables (which are labels of the distinguished relations). If AA is infinite, one has to use infinitary logic. But that’s ok. Everything works. Then the abstract structure Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} is defined to be the second-order propositional function expressed by this formula. One needs to use the assumption that logically equivalent formulas express the same propositional content (and the converse). With this assumption, one can prove the required abstraction principle,

Φ^ 𝒜=Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}} \Leftrightarrow \mathcal{A} \cong \mathcal{B}

I.e., the structure of 𝒜\mathcal{A} is identical to the structure of \mathcal{B} if and only if 𝒜\mathcal{A} \cong \mathcal{B}.

If one thinks about this a bit more carefully, one sees that “labelling the nodes” corresponds (roughly) to skolemization of the formula Φ 𝒜\Phi_{\mathcal{A}}, and it turns out that automorphisms of 𝒜\mathcal{A} correspond to logically equivalent skolemizations.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 24, 2013 8:07 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Yes, of course there has to be an ambient category, but there is no such thing as a mathematical structure that doesn’t live in some ambient category. This is one of the insights of category theory. In particular, a first-order structure lives in the ambient category of all structures of the same signature. This signature is the same information that you have to use in order to introduce logical formulas. So it is not at all extraneous, but rather intrinsic to what type of thing 𝒜\mathcal{A} is.

Posted by: Mike Shulman on November 24, 2013 9:31 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

… but there is no such thing as a mathematical structure that doesn’t live in some ambient category. This is one of the insights of category theory. In particular, a first-order structure lives in the ambient category of all structures of the same signature. This signature is the same information that you have to use in order to introduce logical formulas. So it is not at all extraneous, but rather intrinsic to what type of thing 𝒜 is.

Yes, but this may in fact be a conceptual sticking point between the category-theoretic view and a non-category-theoretic view of mathematical objects. Yes, I agree that, given 𝒜\mathcal{A} of signature σ\sigma, say, then we consider the class, call it Mod(σ)Mod(\sigma), of all models of same signature σ\sigma. I guess this, with elementary maps say, is a category, say 𝒞 σ\mathcal{C}_{\sigma}. But suppose we consider expansions σ\sigma too. Let σ +\sigma^{+} be an expansion. Consider Mod(σσ +)Mod(\sigma \cup \sigma^{+}), and correspondingly, and 𝒞 σσ +\mathcal{C}_{\sigma \cup \sigma^{+}}, I guess. Is one of these the “correct” category for 𝒜\mathcal{A}? Does changing the signature (to a more inclusive one), and so changing the ambient category, change what 𝒜\mathcal{A} “is”, as it were?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 24, 2013 10:03 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Does changing the signature (to a more inclusive one), and so changing the ambient category, change what 𝒜\mathcal{A} “is”, as it were?

Yes. The integers qua monoid are a different mathematical object from the integers qua group or qua commutative ring. I agree that this is not a priori obvious, and it’s actually something that we’ve had long discussions about here before. But it’s what experience with abstract mathematics over the last 100 years or so has taught us. Category-theoretic language just codifies that lesson.

Posted by: Mike Shulman on November 25, 2013 12:32 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

I also don’t quite see yet how Jeff is constructing a skeleton, rather than (something bijective to) the set of isomorphism classes. For one thing, I don’t see what the morphisms of the groupoid Worlds are, or how the functor Φˆ is defined on morphisms. Probably that was said in some comment that I missed, but maybe someone could say it again?

Right, good point. There are two mappings I’ve tried to define:

Φ:ModL ,\Phi : Mod \to L_{\infty,\infty}

Φ^:ModPropFuncs\hat{\Phi} : Mod \to PropFuncs

The first of these take a model 𝒜Mod\mathcal{A} \in Mod, and outputs a formula Φ 𝒜L ,\Phi_{\mathcal{A}} \in L_{\infty,\infty}. This has the equivalence property:

𝒜Φ 𝒜Φ \mathcal{A} \cong \mathcal{B} \Leftrightarrow \Phi_{\mathcal{A}} \equiv \Phi_{\mathcal{B}}.

where Φ 𝒜Φ \Phi_{\mathcal{A}} \equiv \Phi_{\mathcal{B}} means logical equivalence (in L ,L_{\infty,\infty}). In some sense, this seems to take us from the groupoid of models, to a groupoid of formulas. This, however, I’m not sure of.

If one wants to “track” the particular isomorphism f:𝒜f : \mathcal{A} \to \mathcal{B}, then this can be done too, but it is quite complicated, and requires going into how the carrier sets A,BA,B are “labelled” in L ,L_{\infty,\infty} using variables as “names” of elements of A,BA,B; and “skolemizations” of the corresponding formulas. With these “labellings” fixed, an isomorphism f:𝒜f : \mathcal{A} \to \mathcal{B} corresponds more or less exactly to a permutation of variables (or skolem constants) in the language L ,L_{\infty,\infty} which leaves the formulas logically equivalent.

This is some sort of groupoid equivalence, I think, but I’m not sure how to describe it category-theoretically. It’s not a skeleton, I think. The mapping Φ\Phi is a functor which gives an equivalence.

The other map Φ^\hat{\Phi} takes models to “abstract propositional functions” (in the philosopher’s sense of proposition: i.e., not a syntactical entity at all). As John suggested, this seems to be decategorification, much as the “Frege functor”,

card(.):FinSet 0card(.) : FinSet_0 \to \mathbb{N}

or the “Cantor functor”,

ord(.):WOOrdord(.) : WO \to Ord

or the “Dedekind functor”,

r(.):DedSec (,)r(.) : DedSec_{(\mathbb{Q},\leq)} \to \mathbb{R}

are examples of decategorification.

These are, more or less, what philosophers and logicians call “abstraction principles” (following Frege), and have the generic form

α(X)=α(Y)XY\alpha(X) = \alpha(Y) \Leftrightarrow X \equiv Y

The first person to identify and study such things was Frege, who unfortunately made an error - but one that this is totally unexpected and very deep. Quantifiying over second-order things (concepts/classes), he tried to assign an object, a set (he called it an “extension”), satisfying,

ϵ(X)=ϵ(Y)x(X(x)Y(x))\epsilon(X) = \epsilon(Y) \Leftrightarrow \forall x(X(x) \leftrightarrow Y(x))

But this is inconsistent, as can be seen by considering the Russell formula,

R(x):=X(x=ϵ(X)¬X(x))R(x) : = \exists X(x = \epsilon(X) \wedge \neg X(x))

For let a=ϵ(R)a = \epsilon(R). Then suppose R(a)R(a). It follows that X(a=ϵ(X)¬X(a))\exists X(a = \epsilon(X) \wedge \neg X(a)). Let AA be some XX such that a=ϵ(X)¬X(a))a = \epsilon(X) \wedge \neg X(a)). So, ϵ(R)=ϵ(A)\epsilon(R) = \epsilon(A) and ¬A(a)\neg A(a). But by the abstraction principle, x(R(x)A(x))\forall x(R(x) \leftrightarrow A(x)), and so R(a)A(a)R(a) \leftrightarrow A(a), and so ¬R(a)\neg R(a). Contradiction.

So, ¬R(a)\neg R(a). So, X(a=ϵ(X)X(a))\forall X(a = \epsilon(X) \rightarrow X(a)). So, a=ϵ(R)R(a)a = \epsilon(R) \rightarrow R(a). So, R(a)R(a). Contradiction.

So, Russell’s paradox arises from an inconsistent decategorification!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 23, 2013 9:22 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Okay. So there is some complicated way to define a functor Φ\Phi which is an equivalence. So category-theoretically, nothing is gained or lost by all of that work. (-: Then there is also a decategorifying operation Φ^\widehat{\Phi}, which does lose information.

So to recap, what we’re saying is that “physical equivalence” shouldn’t be defined as equality under Φ^\widehat{\Phi}, because of the information it loses. Sometimes we might want to count the equivalence classes, or equivalently the images of Φ^\widehat{\Phi}, but other times it’s important to remember the whole groupoid. In particular, an automorphism group is not associated (canonically) to a thing in the image of Φ^\widehat{\Phi}. So it’s not a good idea to call those things “physical worlds”.

Posted by: Mike Shulman on November 23, 2013 11:32 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

In particular, an automorphism group is not associated (canonically) to a thing in the image of Φˆ. So it’s not a good idea to call those things “physical worlds”.

Strictly speaking, the things in the image are “abstract structures”, and not worlds: they’re (categorical, second-order) propositional functions. Worlds arise when you apply these to some specific physical properties and relations R i\mathbf{R}_i. The reason for calling them “physical worlds” is because of the requirement that “isomorphic models represent the same world”, i.e.,

𝒩Φ^ [R 1,]=Φ^ 𝒩[R 1,]\mathcal{M} \cong \mathcal{N} \Rightarrow \hat{\Phi}_{\mathcal{M}}[\mathbf{R}_1,\dots] = \hat{\Phi}_{\mathcal{N}}[\mathbf{R}_1,\dots]

So, to count the physical worlds/states in the 2 particle/2 properties setup, I have to count the things Φ^ [Left,Right]\hat{\Phi}_{\mathcal{M}}[\mathbf{Left},\mathbf{Right}]. Because we have 2 3\mathcal{M}_2 \cong \mathcal{M}_3, we get Φ^ 2[Left,Right]=Φ^ 3[Left,Right]\hat{\Phi}_{\mathcal{M}_2}[\mathbf{Left},\mathbf{Right}] = \hat{\Phi}_{\mathcal{M}_3}[\mathbf{Left},\mathbf{Right}], so we count correctly. To count the physical worlds/states in David’s 5 ball/3 colour properties setup, I have to count the things Φ^ [Red,Blue,Green]\hat{\Phi}_{\mathcal{M}}[\mathbf{Red},\mathbf{Blue},\mathbf{Green}]. This generalizes, I believe, to the case of GR and gauge theory too.

[John pointed out that I’m counting equivalence classes, which is true; and disagreed on this way of defining physical equivalent models; but I don’t think the symmetry group of a world is related to the individuation criteria for worlds. But having said that, I have to think about the examples John mentioned: Feynman graphs and, I’ve semi-forgotten, a 2-D TQFT with finite gauge group, I think.]

But: I still need to think about your point about Aut(W)Aut(W). I’m not sure I get it—probably my fault for misunderstanding. By “automorphism group” do you mean some specific (G,)(G, \circ), with a particular carrier set GG? Or do you mean the something like the “abstract automorphism group”—that all isomorphic copies of (G,)(G, \circ) have in common? For a particular choice =(M,)\mathcal{M} = (M,\dots), the automorphism group of WW, relative to \mathcal{M}, is Aut()Sym(M)Aut(\mathcal{M}) \subseteq Sym(M). So, its carrier set is a subset of the permutations of MM. So, I suspect that there cannot be a canonical group Aut(W)=(G,)Aut(W) = (G,\circ) in that sense, because the world WW has no carrier set! The whole point of the construction is to implement the idea that the world WW doesn’t have a carrier set. Rather, on this Leibnizian view, the world WW is a system of logically-related relations.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 24, 2013 12:40 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

By definition, a group consists of a set together with a binary operation on it satisfying certain axioms. Since this is an abstract group, the elements of the set don’t have to literally be automorphisms of anything, but the set has to be specified in some way. And so the point that

there cannot be a canonical group Aut(W)=(G,)Aut(W)=(G,\circ)

is exactly the point that I was making. Your “world” WW does not have an automorphism group. Rather, it has an automorphism isomorphism-class-of-groups, which is different.

Posted by: Mike Shulman on November 24, 2013 5:33 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

Right, the worlds have lost their carrier set … That’s the point of the mapping

𝒜Φ^ 𝒜\mathcal{A} \mapsto \hat{\Phi}_{\mathcal{A}}.

The object Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} is the “abstract structure” of 𝒜=(A,)\mathcal{A} = (A, \dots). When you discard the (arbitrary) carrier set AA, you’re left with the pure relational structure as it were. This is why it satisfies the Leibniz abstraction principle,

Φ^ 𝒜=Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}} \Leftrightarrow \mathcal{A} \cong \mathcal{B}

Cf., conceptually speaking, this is also what Steve Awodey does in his paper, “Univalence, Invariance and Structuralism”, page 3,

But it is not the definition of isomorphism, because it presumes the notion of structure and an identity criterion for it, and that is putting the cart before the horse. Structure is like color or the direction of a line or number: it is an abstract concept. And as Frege wisely taught us, it is determined by an abstraction principle, in this case:

str(A)=str(B)ABstr(A) = str(B) \Leftrightarrow A \cong B. (DS)

The structure of A is the same as the structure of B just in case A and B are isomorphic.

So, I’m defining something to play the role of str(A)str(A), the “abstract structure of AA”, to fulfil what I call Leibniz Abstraction and what Steve calls (DS). The thing I define is Φ^ 𝒜\hat{\Phi}_{\mathcal{A}}. But my approach is model-theoretic, and not category/type-theoretic.

Steve then goes on to say (UA) yields the conclusion that “isomorphic structures are equal”, which I don’t think is right, unless one does some redefining of what “equal” means. Rather, I’d rather say “isomorphic models have the same abstract structure”, where “the same” really does mean “the same”. So, for example, if G 1,G 2G_1, G_2 are isomorphic graphs, then Φ^ G 1=Φ^ G 2\hat{\Phi}_{G_1} = \hat{\Phi}_{G_2}.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 24, 2013 7:43 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

You’re saying a lot of stuff that you’ve said before already, but it doesn’t have any bearing on the point I was making, namely that the automorphism group can’t be recovered from Φ^ 𝒜\widehat{\Phi}_{\mathcal{A}}, making it a problematic thing to call a “world” or an “abstract structure”.

Steve then goes on to say (UA) yields the conclusion that “isomorphic structures are equal”, which I don’t think is right, unless one does some redefining of what “equal” means.

That (redefining of what “equal” means) is in fact exactly what (UA) does. Steve also says this (p10):

Rather than viewing [(UA)] as identifying equivalent objects, and thus collapsing distinct objects, it is more useful to regard it as expanding the notion of identity to that of equivalence.

Posted by: Mike Shulman on November 24, 2013 9:29 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

namely that the automorphism group can’t be recovered from Φˆ𝒜, making it a problematic thing to call a “world” or an “abstract structure”.

But we all–you, me, Steve, Frege, everyone!–agree that the definition of “abstract structure” is given by an abstraction principle,

Str(𝒜)=Str()𝒜Str(\mathcal{A}) = Str(\mathcal{B}) \Leftrightarrow \mathcal{A} \cong \mathcal{B}

So, calling Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} the abstract structure does seem to be the right thing to do, because it satisfies the abstraction principle,

Φ^ 𝒜=Φ^ 𝒜\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}} \Leftrightarrow \mathcal{A} \cong \mathcal{B}

But … then, on the (UA) issue, I want to add that if one redefines what “=” means here, then it seems to me that we’re not talking about “abstract structure”. I think the abstraction principle has to contain “=”, and not a surrogate. Otherwise, this is an example of equivocation: changing meanings mid-argument!

Maybe this is an analogy: take the abstraction principle for wellorders,

ord (X, X)=ord (Y, Y)(X, X)(Y, Y)ord_{(X,\leq_X)} = ord_{(Y,\leq_Y)} \Leftrightarrow (X,\leq_X) \cong (Y,\leq_Y)

where (X, X),(Y, Y)(X,\leq_X), (Y,\leq_Y) are well ordered sets. We want to say that isomorphic wellorders have identical ordinals, because that’s what “ordinal” means!

Yes, I agree with the earlier point you made: there is no unique automorphism group for the thing I call the abstract structure Φ^ 𝒜\hat{\Phi}_{\mathcal{A}}. However, it is unique up to isomorphism. That is, “isomorphic copies have the same automorphism group up to isomorphism”. I’m not sure why the lack of a unique representative is a problem, though. If f:ABf : A \to B is an isomorphism from 𝒜\mathcal{A} to \mathcal{B} and gSym(A)g \in Sym(A) is an automorphism of 𝒜\mathcal{A}, then fgf 1:BBf \circ g \circ f^{-1} : B \to B is at least a corresponding automorphism of \mathcal{B}. So, given any isomorphism f:𝒜f: \mathcal{A} \to \mathcal{B} and gAut(𝒜)g \in Aut(\mathcal{A}), we get a g fAut()g^{f} \in Aut(\mathcal{B}). If gg acts on subsets XAX \subseteq A, then g fg^{f} acts on their images f[X]Bf[X] \subseteq B. For example, suppose WW is a spacetime world, and has two isomorphic models (M,g ab),(N,h ab)(M,g_{ab}), (N,h_{ab}) representing WW. Suppose f:(M,g ab)(N,h ab)f : (M,g_{ab}) \to (N,h_{ab}) is an isomorphism. If XMX \subseteq M is some set of points of some interest. Its image in NN is f[X]f[X]. When an automorphism gg of (M,g ab)(M,g_{ab}) takes the set XX to Y=g[X]Y = g[X], then the corresponding automorphism g fg^f takes f[X]f[X] to (fgf 1)[f[X]]=(fg)[X]=f[g[X]]=f[Y](f \circ g \circ f^{-1})[f[X]] = (f \circ g)[X] = f[g[X]] = f[Y]. Does that help? I could be misunderstanding.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 24, 2013 11:19 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

But we all—you, me, Steve, Frege, everyone!—agree that the definition of “abstract structure” is given by an abstraction principle,

When did I agree with that?

“isomorphic copies have the same automorphism group up to isomorphism”

But not up to unique isomorphism. The problem is that your definition of g fg^f depends on ff, whereas if you are given only (M,g ab)(M,g_{a b}) and (N,h ab)(N,h_{a b}) “representing WW” there is no specified ff. You can pick one at random, but if I pick a different one at random, then we’ll get different automorphisms g fg^f of (N,h ab)(N,h_{a b}).

Posted by: Mike Shulman on November 25, 2013 12:35 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

The problem is that your definition of g fg^f depends on ff, whereas if you are given only (M,g ab)(M,g_{ab}) and (N,h ab)(N,h_{ab}) “representing WW” there is no specified ff. You can pick one at random, but if I pick a different one at random, then we’ll get different automorphisms g fg^f of (N,h ab)(N,h_{ab}).

Right, yes. (Let me change notation a bit and use G ab,H abG_{ab}, H_{ab} for the two metrics, as I want to use h,gh,g to mean something else.)

Thinking through this, given two isomorphisms f 1,f 2:(M,G ab)(N,H ab)f_1,f_2 :(M,G_{ab}) \to (N,H_{ab}), and some gAut((M,G ab))g \in Aut((M,G_{ab})), then g f 1g^{f_1} and g f 2g^{f_2} will be conjugate. I.e., let h 12=f 2(f 1) 1h_{12} = f_2 \circ (f_1)^{-1} be the automorphism of (N,H ab)(N,H_{ab}) induced by f 1,f 2f_1,f_2. Then

g f 2=h 12g f 1(h 12) 1g^{f_2} = h_{12} \circ g^{f_1} \circ (h_{12})^{-1}.

So, any pair of gauge transformations f 1,f 2f_1, f_2 moves automorphisms around inside a conjugacy class. Is that a problem?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 25, 2013 3:14 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Well, it means that as I said up here, instead of a “group” you have a “band”, i.e. an object of the quotient category of groups in which conjugate homomorphisms have been identified. A band is is a perfectly good object, but it’s not a group; for instance, it can’t act on things. So your WW has an “automorphism band” but not an automorphism group.

Posted by: Mike Shulman on November 25, 2013 5:31 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike, yes, thanks - I see now. A band …

Jeff

Posted by: Jeffrey Ketland on November 25, 2013 7:28 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

When did I agree with that?

Oh, ok; apologies. I had thought you did agree with Steve’s point about (implicitly) defining the notion of “abstract structure” via the abstraction principle:

Str(A)=Str(B)ABStr(A) = Str(B) \Leftrightarrow A \cong B

I think this would be common to anyone thinking about what “the structure of AA” means.

You don’t?

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 25, 2013 3:58 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I actually have no idea what “the structure of AA” is supposed to mean; it’s not something that it would occur to me to think about. AA is a structure; it’s not as if it’s made up of a structure together with some other stuff that you could discard. Saying “the structure of AA” sounds like saying “the person of Mike”.

Posted by: Mike Shulman on November 25, 2013 4:51 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

I actually have no idea what “the structure of A” is supposed to mean; it’s not something that it would occur to me to think about. A is a structure; it’s not as if it’s made up of a structure together with some other stuff that you could discard.

The intuitive idea is that, say, the directed graphs,

G 1=(V 1,E 1)G_1 = (V_1,E_1), where V 1={0,1}V_1 = \{0,1\} and E 1={(0,1)}E_1 = \{(0,1)\}

G 2=(V 2,E 2)G_2 = (V_2, E_2), where V 2={2,3}V_2 = \{2,3\} and E 1={(2,3)}E_1 = \{(2,3)\}

have “the same structure”, because they’re isomorphic. This is the standard view in the philosophy of mathematics: isomorphic models have the same structure. (This is why I’m trying to keep distinct my use of the words “model”–i.e.. structured sets, that the model theorist studies—and “the structure of 𝒜\mathcal{A}”, as that which isomorphic copies have in common.) When we say that, e.g., second-order arithmetic PA 2PA_2 characterises “the standard model”, we mean that all models (X,e,f)PA 2(X,e,f) \models PA_2 are isomorphic, and what they all “have in common” is this structure. When a structuralist (e.g., Resnik, Hellman, Shapiro) says that mathematics is only concerned with structure, they mean that they are not concerned with individual choices of models, but only with what holds in all isomorphic copies. This is the fairly standard structuralist way of thinking about the notion of structure. So, similarly, Steve (Awodey) explains “structure” informally like this:

But it is not the definition of isomorphism, because it presumes the notion of structure and an identity criterion for it, and that is putting the cart before the horse. Structure is like color or the direction of a line or number: it is an abstract concept. And as Frege wisely taught us, it is determined by an abstraction principle, in this case:

str(A)=str(B)⇔A≅B. (DS)

The structure of A is the same as the structure of B just in case A and B are isomorphic.

Steve’s essay is a way of aiming to clarify category-theoretic structuralism, using insights from type theory, homotopy theory and (UA).

(There are, roughly, two other versions of structuralism. Hellman’s eliminative structuralism and Shapiro’s ante rem structuralism. See, e.g., Shapiro’s online survey.)

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 25, 2013 7:33 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

That sounds to me like a instance of the same mistake. The notion of “having the same structure” should not be considered a mere relation: it’s not sensible to say that AA has the same structure as BB without specifying in what way their structures are identified.

Certainly in some contexts we may be interested in isomorphism classes. But it doesn’t make sense to me to call its isomorphism class “the structure” of an object; it loses too much information.

I don’t think I’m disagreeing with Steve, either. Notice that he ends up by deriving the “principle of structuralism” from the univalence axiom, and the latter expands the meaning of “equality” to include the data of a specific isomorphism. So I think he’s really making the same point, that it doesn’t make sense to say that two objects have the same structure without remembering the isomorphism between them which witnesses that fact.

Posted by: Mike Shulman on November 25, 2013 9:01 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike, yes, it’s this point - essentially a conceptual or philosophical point - that we disagree about. For each model (= structured set) AA, I’m trying to define a unique Φ^ A\hat{\Phi}_A which is “the abstract structure of AA”. Maybe a comparison is: for each wellorder (X,<)(X,&lt;) one defines a unique o(X,<)o(X,&lt;) which is its ordinal.

Throwing away the information is not accidental; though; It’s deliberate! However, the only information I’m throwing away is the carrier set.

So, e.g., for wellorders (X,< 1),(Y,< 2)(X,&lt;_1), (Y,&lt;_2), one defines unique objects o(X,< 1),o(Y,< 2)o(X,&lt;_1), o(Y,&lt;_2) such that

Ordinal abstraction: o(X,< 1)=o(Y,< 2)(X,< 1)(Y,< 2)o(X,&lt;_1) = o(Y,&lt;_2) \Leftrightarrow (X,&lt;_1) \cong (Y,&lt;_2)

holds. The only thing that has been “thrown away” are the carrier sets, X,YX,Y, which are like local carriers on which the same ordinal structure has been placed.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 26, 2013 4:27 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

…essentially a conceptual or philosophical point…

Is that a rewording ‘or’ (Huguenots, or French protestants) or an ‘or’ providing alternatives, with or without potential overlap? I hope Mike is allowed to partake in discussions of the point, that a lack of philosophical training doesn’t preclude such participation.

But then what determines what should be said here? If Mike says it’s generally wrong to throw away the witness to an isomorphism, what can you appeal to? What can philosophy bring to the debate that goes against what mathematicians have decided is right for their practice, especially if they can give a reasoned account of why they’ve adopted their practice.

In this case, you may feel that HoTT is the young pretender, and that the onus is on it to establish itself, and that you yourself are best capturing explicitly what goes on largely implicitly in the working mathematical community.

If this is so, we can get down to arguing about whether or not you really have captured a sizeable portion of actual practice, and then whether or not this is best practice.

Otherwise, what’s there left for Mike to do to persuade you to his position? And how do you imagine you will persuade Mike’s to yours?

Posted by: David Corfield on November 26, 2013 9:10 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David,

If Mike says it’s generally wrong to throw away the witness to an isomorphism, what can you appeal to?

Why should one throw away a witness? I don’t think that is under dispute. The question I’m trying to understand is whether an abstraction principle,

α(X)=α(Y)XY\alpha(X) = \alpha(Y) \Leftrightarrow X \cong Y

is “wrong” somehow–but I’m not sure why it is “wrong”. The rhs is synonymous with,

“there exists an isomorphism f:XYf : X \to Y

which is existentially quantified. So, it’s possible the question becomes: is there something “wrong” with existential quantifiers?

I suspect that the underlying idea might be this: given a construction of an isomorphism f:XYf : X \to Y, there is a corresponding proof, depending on ff, of α(X)=α(Y)\alpha(X) = \alpha(Y). That is, the conditional \Leftrightarrow is being understood in a BHK manner. (I.e., a proof of ABA \to B is a construction that maps a proof of AA to a proof of BB.)

Otherwise, what’s there left for Mike to do to persuade you to his position? And how do you imagine you will persuade Mike’s to yours?

I think Mike’s idea is that the phrase “the structure of AA” is somehow meaningless. That’s a quite interesting view, and so I’m very interested to know why that might be.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 26, 2013 10:51 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I think what you suspect is right.

Passing from isomorphisms between AA and BB to the mere existence of an isomorphism is to truncate the type of equivalences between AA and BB into the proposition (i.e., type of hlevel -1) that there is one.

It’s like the difference between telling me it’s possible to do something and telling me the different ways I could do that thing.

This is what the HoTT people call the bracket type. Mike has a great post on the subject here. In particular, this passage;

in everyday mathematics, not all the “propositions” we prove are naturally (-1)-truncated! Once my eyes were opened to this, I started to see it everywhere. Most classical mathematicians are deeply programmed to think of proofs as containing no content, in the sense that once you prove a theorem it doesn’t matter what the proof was (a type theorist calls this “proof irrelevance”). But actually, in doing ordinary mathematics it happens to me all the time that I end up writing “by the proof of Lemma 9.3”, because what matters is not just the statement of Lemma 9.3 but the particular proof of it that I gave.

This is especially common for statements such as “ABA \cong B”. In practice, (1) to prove that two things are isomorphic, almost without exception we construct a particular isomorphism, and (2) very often in order to use the fact that two things are isomorphic, we need a particular isomorphism, and it often matters what that isomorphism is. In other words, when we “prove” a statement of the form ABA \cong B, almost always we are not constructing a term in some (-1)-type (which would have to be the (-1)-truncation of the type of isomorphisms from AA to BB), but rather constructing a term in the type of isomorphisms from AA to BB. Therefore, why not allow “ABA \cong B” to denote the type of isomorphisms?

Posted by: David Corfield on November 26, 2013 11:48 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I’m not saying that it’s wrong to throw away information sometimes. What I was saying is that the result of throwing this information away should not be called “the structure of AA”. You can call it “the isomorphism class of AA”, but I already explained why I don’t see any sense in saying “the structure of AA” to refer to anything less than AA itself. In particular, you can’t “throw away the carrier set” and still say that you have a “structure”, because the carrier set is the most basic part of the structure.

However, after thinking more carefully about your construction, I think I should actually be making a different point, which is that you aren’t throwing anything away! Not even the carrier set. This is easiest to see in the infinitary case. Let’s take your example of directed simple graphs and let (V,E)(V,E) be an infinite such. The most straightforward way to label the variables is by the vertices themselves, so that ν(a)=x a\nu(a) = x_a. Then our formula is

aVx a( a,bVabx ax b (a,b)EX(x a,x b)) \underset{a\in V}{\exists} x_a (\bigwedge_{a,b\in V\atop a\neq b} x_a \neq x_b \wedge \bigwedge_{(a,b)\in E} X(x_a,x_b) \wedge \cdots )

and clearly we haven’t thrown away the sets VV and EE, since they’re right there in the formula! Now you might choose a different labeling by some set V^\widehat{V} of variables with a bijection ν:VV^\nu:V\to \widehat{V}, but in that case all you’ve done is transfer the structure of your graph along a bijection of carrier sets, which is quite a different thing from “throwing away the carrier set”. From a category-theoretic point of view, it’s doing nothing at all.

Posted by: Mike Shulman on November 26, 2013 4:44 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Oh, wait, I think I got confused between Φ\Phi and Φ^\widehat{\Phi} again, because in this thread we’re talking about Φ^\widehat{\Phi} and in the other (functoriality) one we’re talking about Φ\Phi. The first paragraph of that comment applies to Φ^\widehat{\Phi}, and the second to Φ\Phi (and hence is probably not surprising to you).

Posted by: Mike Shulman on November 26, 2013 5:11 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike, yes, the Φ^ A\hat{\Phi}_A thing is being identified as the “abstract structure” of AA. Apologies for waffling on – I appreciate the discussion and feedback from you, David and John (and in any case, it overlaps quite a bit with interesting conceptual and philosophical points connected to HoTT, category-theoretic structuralism (e.g., Steve’s paper) and so on).

The Φ^ A\hat{\Phi}_A thing an abstract second-order propositional function expressed by the diagram formula Φ A\Phi_A. This is precisely what perked my interest in Steve’s stuff when he told me about it in Munich either in 2011 or 2012. On the other hand, the Φ A\Phi_A thing is a syntactic formula, the diagram formula for AA, and it has various labels built into it (e.g., a variable v(a)v(a) labelling each element aAa \in A, as you say), which “disappear” as it were when we consider the purely propositional content. It’s main property is its categoricity: any pair of models satisfying a diagram formula are isomorphic. Indeed, the diagram formula “throws nothing away”! (as you say). It is a detailed labelled syntactic picture of our starting model AA, and has a label v(a)v(a) for each element adom(A)a \in dom(A) (where dom(A)dom(A) is the carrier set of AA). But these labels are quantified, which is a sense in which the specific nature of the elements of the carrier dom(A)dom(A) no longer matters.

E.g., for the two isomorphic graphs G 1,G 2G_1, G_2 I mentioned before, that we might picture like this,

00 121 - 2

and

33 454 - 5

with carrier sets {0,1,2}\{0,1,2\} and {3,4,5}\{3,4,5\}, then I want to find something which I can identify with the “abstract structure” that both G 1,G 2G_1, G_2 “have in common”, which is usually pictured like this,

\cdot \cdot - \cdot

and often called an “unlabelled graph”, or “the abstract graph”. There are various reasons why I definitely do not want this something to be the equivalence class [G 1][G_1] under isomorphism. I need something that has propositional content, so that I can apply it to the case in physics. This something is then, I suggest, Φ^ G 1\hat{\Phi}_{G_1}. So, in particular,

Φ^ G 1=Φ^ G 2\hat{\Phi}_{G_1} = \hat{\Phi}_{G_2}

A philosopher will usually be ok to consider the purely abstract propositional function expressed by the English string of letters,

xx is happy

What is expressed is a propositional function, which I might call ϕ^\hat{\phi}, which maps an object (or, as Carnap would say, probably rightly, the individual concept of an object) to a proposition. It maps Bill to the proposition that Bill is happy. But the Spanish string of letters,

xx es feliz

expresses the same propositional function, ϕ^\hat{\phi}, despite the two strings being syntactically distinct.

This is of course very controversial, as many philosophers and some in semantics think the relevant notions (“synonymy”, “expressing”, “propositional function”) are ill-defined or badly behaved (e.g., under substitution). Very famously, W.V. Quine!

But, in a sense, I can somewhat sidestep those objections, because diagram formulas Φ A\Phi_A belong to “pure (infinitary, higher-order) logic”, and only contain: first-order variables, connectives, identity predicate, second-order variables, quantifiers.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 27, 2013 8:08 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

But these labels are quantified, which is a sense in which the specific nature of the elements of the carrier dom(A)dom(A) no longer matters.

Hmm, I don’t agree. As I said, in Φ A\Phi_A the elements of the carrier set are right there in the variables appearing in the formula. Their “specific nature”, whatever that means, matters neither more nor less than it does in the structure AA itself.

Can you say again how Φ^ A\widehat{\Phi}_A is defined mathematically? I don’t see how Φ A\Phi_A defines a propositional function, since it has no free variables.

Posted by: Mike Shulman on November 27, 2013 6:20 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I suspect Jeff is in the habit of considering α-equivalent formulae as being identical, which most logicians seem to do on an unconscious basis.

Posted by: Zhen Lin on November 27, 2013 7:12 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Zhen

I suspect Jeff is in the habit of considering α-equivalent formulae as being identical, which most logicians seem to do on an unconscious basis.

No, it is absolutely crucial to treat distinct syntactical entities as distinct, even if equivalent under relabelling of bound variables. One cannot begin to teach the incompleteness theorems without being ultra-precise about syntax. For example, the syntactical strings

x¬(sx=0)\forall x \neg(sx = 0)

y¬(sy=0)\forall y \neg(sy = 0)

have different codes. Recently, there has been much interesting work on the formalized theory of syntax; e.g., by Albert Visser.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 27, 2013 9:56 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

As I said, in Φ A\Phi_A the elements of the carrier set are right there in the variables appearing in the formula. Their “specific nature”, whatever that means, matters neither more nor less than it does in the structure A itself.

Agreed: that’s exactly the definition used. Note, though, that when labelling distinct carrier sets A,BA,B using some bijections v 1:dom(A)V 1v_1 : dom(A) \to V_1, v 2:dom(A)V 2v_2 : dom(A) \to V_2 to sets of variables, and then applying existential quantification, the elements of AA (or BB) do not matter; all that matters is that there is a bijection. When we move to the proposition expressed, then the distinct syntactical entities

There is an xx such that F(x)F(x)

There is a yy such that F(y)F(y)

Es gibt ein xx mit F(x)F(x)

There is an FF

F\exists F

all express the same (abstract) proposition.

(On a very closely related theme, there’s Quine’s “Variables Explained Away”. It’s really combinatory logic. Quine called his version “Predicate Functor Logic”. But Quine was a sceptic about propositions.)

Mike:

Can you say again how Φ^ A\hat{\Phi}_A is defined mathematically? I don’t see how Φ A\Phi_A defines a propositional function, since it has no free variables.

By “propositional function”, I don’t mean a syntactic entity (a string of symbols)–I’d call that a formula. Propositional functions therefore do not contain free variables, or indeed any variables! Propositions are what syntactic entities express. They’re intensional entities. The formula Φ A\Phi_A has free second-order variables, and Φ^ A\hat{\Phi}_A is then the (second-order) propositional function it expresses. But Φ^ A\hat{\Phi}_A is not defined mathematically in a way that would be considered routinely acceptable. To accept this, one has to accept some version of intensional logic and all that goes with it. For example, treating “xyx \leq y” as interpreted, the distinct strings,

(xA)(yA)(xy)(\forall x \in A)(\exists y \in A)(x \leq y)

(yA)(xA)(yx)(\forall y \in A)(\exists x \in A)(y \leq x)

express the same proposition. A proposition is the semantic content of a (certain kind of) linguistic string.

Some may, for philosophical reasons, reject propositions as strange or peculiar or ill-individuated and so on (Quine did). But the cost is that one cannot then say that Goldbach’s Conjecture expressed using an Spanish string is the same proposition as Goldbach’s Conjecture expressed using an English string. You cannot say that when John believes Goldbach’s conjecture, while Juan disagrees with Goldbach’s Conjecture, then they disagree. For they disagree when there is a single proposition that one believes and the other disbelieves.

E.g., consider the graph G=(V,E)G = (V,E), with V={0,1,2}V = \{0,1,2\} and E={(1,2)}E = \{(1,2)\}. Then the proposal is that the abstract structure of the graph GG is the propositional function Φ^ G\hat{\Phi}_G expressed by Φ G\Phi_G. This is the propositional function whose value on a property XX and a binary relation YY is the proposition that there exactly three things with property XX, and the first is YY-related to no other, and the second is YY-related to the third and nothing else, and the third is YY-related to nothing.

If we consider an isomorphic copy, e.g., G =(V ,E )G^{\prime} = (V^{\prime},E^{\prime}), with V ={3,4,5}V^{\prime} = \{3,4,5\} and E ={(4,5)}E^{\prime} = \{(4,5)\}, then

the abstract structure of G G^{\prime} = the abstract structure of GG.

So, what is “the abstract structure of GG”? Well, my answer is that both have categorical diagram formulas Φ G\Phi_G, Φ G \Phi_{G^{\prime}}, and, because GG G \cong G^{\prime}, these are logically equivalent; and so, the propositional function Φ^ G \hat{\Phi}_{G^{\prime}} is identical to Φ^ G\hat{\Phi}_G. Its value on a property XX and a binary relation YY is the proposition that there exactly three things with property XX, and the first is YY-related to no other, and the second is YY-related to the third and nothing else, and the third is YY-related to nothing. This is the sense in which “the carrier set has been thrown away”, but the abstract structure has been left intact.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 27, 2013 9:28 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

It seems to me you’re just saying that Φ^ A\widehat{\Phi}_A is the property of structures in the language of graphs that they satisfy the formula Φ A\Phi_A. That’s a perfectly fine mathematical definition. Of course, it’s the same as the property of “being isomorphic to AA”, which is easily definable without going through all the logical shenanigans, so I must be missing something.

Posted by: Mike Shulman on November 27, 2013 11:29 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

It seems to me you’re just saying that Φ^ A\hat{\Phi}_A is the property of structures in the language of graphs that they satisfy the formula Φ A\Phi_A.

Yes, so one might define it using a λ\lambda-abstraction as:

Φ^ A:=λ X(XA)\hat{\Phi}_A := \lambda_X(X \cong A)

A smart graduate student made this point to me after a talk earlier this year.

Mike:

Of course, it’s the same as the property of “being isomorphic to A”, which is easily definable without going through all the logical shenanigans, so I must be missing something.

Agreed - so, why the logical shenanigans …. why the detour via the “diagram formula” Φ A\Phi_A? Good question.

The reasons are connected to debates in phil maths and debates in phil physics.

  1. Phil maths: various people are interested in making sense of the notion of “the abstract structure of AA”. Shapiro, for example, thinks that arithmetic should be understood as being “about” the abstract structure of (ω,, +)(\omega, \varnothing, ^{+}), where (ω,, +)(\omega, \varnothing, ^{+}) is the von Neumann model for arithmetic. But then this is the same as the abstract structure of Zermelo’s model, and this resolves Benacerraf’s problem about what the topic of arithmetic is. Shapiro calls “the abstract structure of (ω,, +)(\omega, \varnothing, ^{+})” an ante rem structure. But this view has been criticised as being mystical, because if this abstract structure is a common-or-garden structured set, then its carrier set contains mysterious “abstract nodes” (like the dots in the picture of an “unlabelled graph”). What then are these “abstract nodes” of the “abstract structure of AA”? Like the critics, I agree that there aren’t any “abstract nodes”, forming a mysterious carrier set. But there are “ersatz nodes”, which turn out to be the existentially quantified variables in the diagram formula Φ A\Phi_A. So, relative to a labelling, one has a bunch of “ersatz nodes”. And then one sees that Φ A\Phi_A has some other nice properties, including the connection between automorphisms of AA and equivalent skolemizations of Φ A\Phi_A.

  2. Phil physics: here, people have noticed a connection between debates about gauge equivalence & permutation symmetry (e.g., David’s example, statistical physics, GR and gauge theory), traditional debates about “haecceities”, and debates about the metaphysics of possible worlds and modal logic. This is a long complicated story, but given that Φ^ A\hat{\Phi}_A is a propositional function (say, with implicit unary argument and a binary one), then I can define Φ^ A[P,R]\hat{\Phi}_A[P,R], the result of applying the function to the property PP and the relation RR. Then, when ABA \cong B, it follows that Φ^ A[P,R]=Φ^ B[P,R]\hat{\Phi}_A[P,R] = \hat{\Phi}_B[P,R].

So, … if I define

WW is a possible (physical) world if and only if W=Φ^ A[R 1,]W = \hat{\Phi}_A[R_1, \dots] for some AA, and physical relations R iR_i.

and

AA represents WW with respect to R 1,R_1, \dots if and only if W=Φ^ A[R 1,]W = \hat{\Phi}_A[R_1,\dots],

then I can show that

(LE) If ABA \cong B, then AA represents WW with respect to R 1,R_1, \dots iff BB represents WW with respect to R 1,R_1, \dots

and that is the principle called “Leibniz equivalence” that we were discussing in the thread for David’s previous blog, and that corresponds to the Wald-Carroll-Rovelli formulation of diffeomorphism invariance for GR.

So, cutting a long story short, the logical shenanigans via the diagram formula Φ A\Phi_A gets me a theory of “abstract structure” (implementing the abstraction principle that isomorphic models have the same abstract structure), and of “possible worlds” (including what “represents” means), and implements (LE) as a consequence.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 28, 2013 6:20 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Undoubtedly there are these ongoing debates in philosophy, but what if they revolve around questions relying on presuppositions that we shouldn’t accept? Collingwood was surely right that to take a question seriously, one must have accepted certain presuppositions, e.g., Have you left off beating you wife?

Isn’t it rather common for questions to fade away rather than be answered? If Newton came back today he might ask whether we now know if space really is the sensorium of God. The passage of time reveals many such things.

In the philosophy of maths debate you mention, there seems to be a presupposition that there’s something different from AA that its abstract structure could be, so that whatever ‘the abstract structure of AA’ really is, it’s not AA. Some genuine work has been done in the abstracting.

Something I very much like about dependent type theory is that it’s good at revealing presuppositions. Mike used Coq to show us those going on in Collingwood’s example.

Even the use of ‘the’ turns out to involve a presupposition, as we saw here. To form a term ‘the AA’ for a type AA, you must first establish that the type is contractible. For a set (i.e., hlevel 0 type) this means it’s a singleton. But we can also use it to understand why we say the product of two objects in a category. Unique up to canonical isomorphism is enough.

If we take this point of view, then to form the term ‘the abstract structure of AA’ you must first form the dependent type of ‘abstract structures of AA’, and then establish that this is contractible.

Contractible is defined as follows:

isContr(X) x:X y:X(y=x). isContr(X) \coloneqq \sum_{x\colon X} \prod_{y\colon X} (y=x).

I provide a term and for any other term (in a continuous way) a term in their identity type.

I suppose we could take AA along with anything canonically isomorphic to it to be the type of things with the abstract structure of AA. I can’t think of what else we could choose. But now the obvious choice of witness to the contractibility of this type is

AA : Type of things canonically isomorphic to AA,

along with those canonical isomorphisms to the other objects.

So we can say

AA is the thing which is canonically isomorphic to AA,

which seems close to Mike’s

I don’t see any sense in saying ‘the structure of AA’ to refer to anything less than AA itself.

It turns out that no work is being done by forming from AA ‘the abstract structure of AA’.

The point is that if one adopts this type theoretic language, along with its presuppositions, because you cannot include extraneous details in your definitions, there’s nothing more to the abstract structure of a type than that type itself. The use of the usual predicate logic-set theoretic apparatus that philosophers prefer comes with a range of presuppositions that it may be time to give up.

Posted by: David Corfield on November 28, 2013 9:51 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Well put, David.

Posted by: Mike Shulman on November 28, 2013 5:53 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

often called an “unlabelled graph”, or “the abstract graph”

Perhaps another way to phrase the point I’m making is that there’s no such thing as a truly “unlabelled graph”. You can decline to label the points by numbers, but they’ll still have to be labeled by the elements of some set. For instance, when you drew that picture with dots, you had a set of dots on the page that one could consider to “label” the vertices of the graph.

Posted by: Mike Shulman on November 27, 2013 9:49 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike remarked

I already explained why I don’t see any sense in saying “the structure of AA” to refer to anything less than AA itself.

What do you think of this phrasing by Pelayo and Warren in Homotopy type theory and Voevodsky’s univalent foundations:

…in the presence of the Univalence Axiom, any structure on a type AA which is type theoretically definable can be transferred along a weak equivalence ABA \to B to give a corresponding structure on BB. (ArXiv, p. 10))

Clearly what’s intended are things such as were we to have p:IsSet(A)p : IsSet(A), we could transfer this along an equivalence ff to give a term f(p):IsSet(B)f(p): IsSet(B).

It might sound like we could form the collection of all the things I can say about AA such that this is identical to all the things I can say about an equivalent BB. But Pelayo and Warren do say corresponding structures.

Could we rephrase your remark that the structure of AA refers to AA as saying that whatever can be said about AA in the type theory follows from the way AA is introduced as a type?

Posted by: David Corfield on November 27, 2013 9:09 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Could we rephrase your remark that the structure of AA refers to AA as saying that whatever can be said about AA in the type theory follows from the way AA is introduced as a type?

Hmm… could you explain why the latter is a rephrasing of the former?

Posted by: Mike Shulman on November 27, 2013 6:25 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Bit vague wasn’t it? I guess I’m trying to see how you’re pouring cold water on the idea that we can abstract out a ‘structure of AA’ from AA itself.

One might consider ‘all that can be said in the type theory about AA’ as if one could only say structural things. But this can’t be done without reference to the way AA was introduced, which in a sense is all AA is.

Hmm, not much better.

Posted by: David Corfield on November 27, 2013 8:10 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Here’s another way to put it that might make more sense to you. From the point of view of stuff, structure, property, “structure” on an object XX of a category CC is “what is forgotten” by a faithful functor U:DCU:D\to C. Thus the possible DD-structures on XX are the elements of the preorder U 1(X)U^{-1}(X). Those are the only thing I can think of calling “the structure of” an object ADA\in D, since to “equip XX with DD-structure” we have exactly to choose an object of U 1(X)U^{-1}(X). But we can’t define the preorder U 1(X)U^{-1}(X) until we know the carrier set XX! So we can’t “forget the carrier set” XX and still talk about “the structure” of AA.

Posted by: Mike Shulman on November 27, 2013 9:16 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

“structure” on an object XX of a category CC is “what is forgotten” by a faithful functor U:DCU : D \to C. Thus the possible DD-structures on XX are the elements of the preorder U 1(X)U^{-1}(X). Those are the only thing I can think of calling “the structure of” an object ADA \in D, since to “equip XX with DD-structure” we have exactly to choose an object of U 1(X)U^{-1}(X).

So, in model theory lingo, that’s a reduct? And in reverse, in model theory lingo, possible expansions.

But we can’t define the preorder U 1(X)U^{-1}(X) until we know the carrier set XX! So we can’t “forget the carrier set” XX and still talk about “the structure” of AA.

As you pointed out, the formula Φ A v,r\Phi^{v,r}_A does have the carrier set of AA “built-in” to it, via the labelling vv of domain elements by variables. But the propositional function Φ^ A\hat{\Phi}_A doesn’t have any carrier set at all! That’s been abstracted away. So, (the idea is that) then Φ^ A[R 1,]\hat{\Phi}_A[R_1, \dots] = the proposition that there are some κ\kappa many things, and they bear relations R iR_i, in some structural way, given, up-to-isomorphism, by AA. (κ\kappa is the cardinality of AA.) Or, as you put it in the other comment, it’s the proposition that the R iR_i together are isomorphic to AA.

To go back to David’s original example, “covariance of coloured balls”, suppose MM is one of the models representing the physical situations, and Ball is the property of being a ball, Red is the property of being red, etc. Then Φ^ M[Ball,Red,Green,Blue]\hat{\Phi}_{M}[Ball, Red, Green, Blue] = the proposition that the properties Ball,Red,Green,BlueBall,Red, Green, Blue together are isomorphic to MM. Let XX be the carrier set of MM. This can be anything you like, so long as |X|=5|X| = 5. XX can be {0,1,2,3,4}\{0,1,2,3,4\}, or XX could be {David,John,Mike,Zhen,Jeff}\{David, John, Mike, Zhen, Jeff\}, or … It doesn’t matter: it’s been abstracted away! What this means is a very structuralist view of possible worlds. Possible worlds are not a bunch of “things”, connected by relations. Rather, possible worlds are relations connected by logic

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 28, 2013 11:33 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

At this point I feel like we’re just arguing about how words should be defined, and repeating ourselves over and over again. So I propose we each make our point one more time and then call it quits. I’ll start.

To me — and also to others who’ve written about it from a categorical point of view, e.g. Awodey and McLarty — “structuralism” does not mean forgetting about the “things” that make up a structure. Rather, it means forgetting about any internal properties that those things may have (e.g. is 22\in\mathbb{N} defined as {,{}}\{\emptyset,\{\emptyset\}\} or {{}}\{\{\emptyset\}\}, or is your carrier set XX defined as {0,1,2,3,4}\{0,1,2,3,4\} or {David,John,Mike,Zhen,Jeff}\{David, John, Mike, Zhen, Jeff\}?). Instead we regard these things merely as abstract points, whose only interest is in the operations and relations that connect them (e.g. the successor s:s:\mathbb{N}\to \mathbb{N}), making up the structure. But the points are still there.

This point of view is not based in a philosophical a priori predilection, or in any appeal to historical authority, so it is unlikely to be refuted by either. Instead, it is based on actual practical experience of doing mathematics, which teaches us that isomorphism classes are not very useful. For instance, as we’ve seen, an isomorphism class does not have an automorphism group. So if a “structure” is to be something that you can do mathematics with, then it cannot be an isomorphism class — or anything isomorphic to an isomorphism class, such as a propositional function.

This perspective was not originally obvious to mathematicians! We’ve only come to it through long and bitter experience (and by “we” I really mean “they”, since I didn’t join up until close to the end of the journey). For instance, a “representation” of a group GG used to mean an isomorphism class of vector spaces with a GG-action. But eventually we decided that that’s not a good definition, for the reasons mentioned above, and now a “representation” usually means a particular vector space with a GG-action. Even Wikipedia, which is often behind the times on such things, agrees.

Posted by: Mike Shulman on November 28, 2013 6:56 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

a “representation” of a group GG used to mean an isomorphism class of vector spaces with a GG-action

This sounds like a curious notion to me. What exactly is “an isomorphism class of vector spaces with a GG-action”? I can’t imagine anyone ever thinking that was a sensible thing to study, but perhaps I’m spoiled by the vantage point I occupy.

Posted by: Tom on November 28, 2013 8:21 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Sorry, I meant “an isomorphism class of (vector spaces with a GG-action)”.

Posted by: Mike Shulman on November 28, 2013 9:49 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

is 22 \in \mathbb{N} defined as {,{}}\{&#8709;,\{&#8709;\}\} or {{}}\{\{&#8709;\}\}?

22 is defined as |{0,1}||\{0,1\}|, the cardinal of any 2-element set. On the other hand, the set {,{}}\{\varnothing,\{\varnothing\}\} is a representation (implementation, etc.) of 22. Arithmetic is multiply interpretable into ZFCZFC. None is especially privileged, aside from convenience. (The finite von Neumann ordinals, ω\omega, are quite convenient, though.)

Instead we regard these things merely as abstract points, whose only interest is in the operations and relations that connect them (e.g. the successor s:ℕ→ℕ), making up the structure. But the points are still there.

Yes, I know - this philosophical belief in “abstract points” is what motivates Shapiro’s ante rem structuralism (and is what Dummett called “mysticism”). The idea is that the abstract structure of AA has a carrier set of “abstract points”, and isomorphic copies of AA somehow “instantiate” it. But a major problem is that it faces Benacerraf’s objection, as explained in Geoffrey Hellman’s 2007 article “Structuralism”.

In fact, SGS, seems ultimately subject to the very objection of Benacerraf [“What Numbers Could Not Be”] that helped inspire recent structuralist approaches to number systems in the first place. Suppose we had the ante rem structure for the natural numbers, call it ⟨N,φ,1⟩, where φ is the privileged successor function, and 1 the initial place. Obviously, there are indefinitely many other progressions, explicitly definable in terms of this one, which qualify equally well as referents for our numerals and are just as “free from irrelevant features”; simply permute any (for simplicity, say finite) number of places, obtaining a system ⟨N,φ′,1′⟩, made up of the same items but “set in order” by an adjusted transformation, φ′. Why should this not have been called “the archetypical ante rem progression”, or “the result of Dedekind abstraction”? We cannot say, e.g., “because 1 is really first”, since the very notion “first” is relative to an ordering; relative to φ′, 1′, not 1, is “first”. Indeed, Benacerraf, in his original paper, generalized his argument that numbers cannot really be sets to the conclusion that they cannot really be objects at all, and here, with purported ante rem structures, we can see again why not, as multiple, equally valid identifications compete with one another as “uniquely correct”. Hyperplatonist abstraction, far from transcending the problem, leads straight back to it. (Hellman, “Structuralism”, pp. 11-12 in the preprint).

As a workable philosophical view, the category-theoretic foundationalist has to explain what an “abstract point” is, in a way that avoids the Benacerraf objection.

We’ll stop there though!

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 28, 2013 8:25 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Augh, you said something new in that last comment! (-: Now I can’t help replying, but I’ll confine myself to remarking that evidently Hellman has not understood the generalized the.

Posted by: Mike Shulman on November 28, 2013 9:53 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

:)

Ok - maybe the debate about the concept of “the abstract structure of AA” can continue another time.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 29, 2013 11:29 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Okay. Since I took an extra comment, you can have the last word if you want; I promise to keep my mouth shut this time. (-:

Posted by: Mike Shulman on November 29, 2013 5:40 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike – thanks - this thread is already beyond huge! Maybe, at some point, if you, David and John are interested in continuing the underlying conceptual debate about structuralism (the topic of Steve Awodey’s new paper; and the other literature on this - e.g., Resnik, Shapiro, Hellman, Parsons, McLarty, Burgess and … er even others), you might think of another post on the concepts of “abstract structure”, “abstract points”, “evil”, “category-theoretic sameness” (morphic indisernibility), the generalized “the” (“the permutation group S nS_n”, etc.), and so on.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 29, 2013 10:59 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

Your explanation of the construction is exactly right.

Now you might choose a different labeling by some set Vˆ of variables with a bijection ν:V→Vˆ, but in that case all you’ve done is transfer the structure of your graph along a bijection of carrier sets, which is quite a different thing from “throwing away the carrier set”.

Right, indeed. Let me change notation a bit and stop using squiggly “𝒜\mathcal{A}” to refer to models. Let A=(dom(A),)A = (dom(A), \dots) be our model, where dom(A)dom(A) is the carrier set, and “\dots” means some relations, operations, etc, on dom(A)dom(A). Let v 1:dom(A)V 1v_1 : dom(A) \to V_1 and v 2:dom(A)V 2v_2 : dom(A) \to V_2 be labellings of dom(A)dom(A) by sets V 1,V 2V_1, V_2 of variables. Then we have that the resulting diagram formulas Φ A v 1\Phi^{v_1}_A and Φ A v 2\Phi^{v_2}_A are logically equivalent.

Suppose further that V 1=V 2V_1 = V_2. Then we have an induced permutation

π(v 1,v 2):dom(A)dom(A)\pi(v_1,v_2) : dom(A) \to dom(A)

of the domain of AA (i.e., carrier set of AA) defined by:

π(v 1,v 2)=(v 2) 1v 1\pi(v_1,v_2) = (v_2)^{-1} \circ v_1

Also, if one removes the initial existential quantifier prefix in Φ A v\Phi^{v}_A, call the formula ϕ A v\phi^{v}_A. Then one can show that:

Labelling-Automorphism Lemma:

π(v 1,v 2)Aut(A)ϕ A v 1ϕ A v 2\pi(v_1,v_2) \in Aut(A) \Leftrightarrow \phi^{v_1}_A \equiv \phi^{v_2}_A

This corresponds I guess to “transferring the structure” on dom(A)dom(A) along the bijection π(v 1,v 2)\pi(v_1,v_2)–a pushforward. So, slightly more suggestively,

π(v 1,v 2) *[A]=Aϕ A v 1ϕ A v 2\pi(v_1,v_2)_{\ast}[A] = A \Leftrightarrow \phi^{v_1}_A \equiv \phi^{v_2}_A

And I guess that the logical equivalence ϕ A v 1ϕ A v 2\phi^{v_1}_A \equiv \phi^{v_2}_A could be understood to mean a pair of proofs, rather than as meaning “true in all the same models”. The proof sort of “shuffles” all the conjuncts of literals in the diagram of AA under the permutation of variables, and shows that the result of “shuffling” the literals in ϕ A v 1\phi^{v_1}_A leads to ϕ A v 2\phi^{v_2}_A.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 27, 2013 10:57 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John optimistically wrote:

What you’ve done here is described an equivalence

Φ^:ModelsWorlds \hat{&#934;}:Models \to Worlds

Mike more carefully replied:

I also don’t quite see yet how Jeff is constructing a skeleton, rather than (something bijective to) the set of isomorphism classes. For one thing, I don’t see what the morphisms of the groupoid Worlds are, or how the functor Φ^\hat{\Phi} is defined on morphisms. Probably that was said in some comment that I missed, but maybe someone could say it again?

Whoops! I was assuming, from things Jeffrey and David wrote, that Jeffrey had (implicitly) defined automorphisms of worlds, thus (implicitly) defining a groupoid Worlds, which was isomorphic to a skeleton of Models.

But from your subsequent discussion, it looks like I was being optimistic. So, my whole remark now switches from an attempted summary of what Jeffrey has done, to an outline of what I wish someone would do.

Namely, in a version of first-order logic that has a nice ‘balance’ between syntax and semantics, I’d hope there would be some purely syntactic way to think about elementary embeddings of models (also known as structures). Then we could have, for any theory TT in this version of logic, a category ModTMod T of models and elementary embeddings, as discussed by Makkai, but also some syntactically defined category which I’ll call WorldTWorld T, and an equivalence

F:ModTWorldT F: Mod T \to World T

Unfortunately I don’t enough model theory to quickly carry out this program, or show it can’t be done. I would need to learn some stuff like what Jeffrey was talking about here:

Yes, in FOL, the language is too weak to get a “balance” between syntax and semantics—at least if one wants strong definability/categoricity results. E.g., ZFC (if consistent) has countable models. To get things to match, you need to use much stronger syntax: infinitely long conjunctions/disjunctions and infinitely long quantifier prefixes. What I’m doing is very basic, and not fancy at all; in fact, it seems to be mathematically uninteresting. There are many interesting results in this field (famously, Scott’s Isomorphism Theorem). The method I use is really a simple generalization to infinitary languages of the Diagram Lemma in model theory.

Someday maybe I’ll learn this stuff! I’m happy with infinitary languages of the sort described, and I see why they’re needed to get the ‘categoricity’ required for the kind of result I’m thinking about. But I don’t know Scott’s Isomorphism Theorem, or the Diagram Lemma, or… lots of other stuff, I’m sure.

Posted by: John Baez on November 25, 2013 12:25 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John,

The Diagram Lemma is briefly explained in Wilfrid Hodges’ article on first-order model theory at Stanford Encyclopedia of Philosophy (SEP).

Suppose we have a structure 𝒜=(A,R)\mathcal{A} = (A, R), with carrier setAA and a single (binary, say) relation RR. We introduce a first-order language LL with a binary predicate PP which denotes RR. We add a set CC of constants a̲A\underline{a} \in A, one for every element of AA, and interpret them to denote what they label, so that (a̲) 𝒜=a(\underline{a})^{\mathcal{A}} = a.

A literal in this language L CL_C is something that is either an atomic sentence, or a negation of an atomic sentence. The literals will be of the form: (a̲=b̲)(\underline{a} = \underline{b}), (a̲b̲)(\underline{a} \neq \underline{b}), P(a̲,b̲)P(\underline{a},\underline{b}), or ¬P(a̲,b̲)\neg P(\underline{a},\underline{b}), with a,bAa,b \in A.

The (Robinson) diagram of 𝒜\mathcal{A} is defined to be the set of literals true in 𝒜\mathcal{A}.

So, for a simple finite example, suppose A={0,1,2}A = \{0,1,2\}, so |A|=3|A| = 3, and suppose the constants are {c 0,c 1,c 2}\{c_0,c_1,c_2\}, with denotations (c i) 𝒜=i(c_i)^{\mathcal{A}} = i. Suppose R={(0,1),(1,1)}R = \{(0,1),(1,1)\}. The set of true literals, diag(𝒜)diag(\mathcal{A}) is then

{(c 0c 1),(c 0c 2),(c 1c 2),P(c 0,c 1),P(c 1,c 1),¬P(c 0,c 0),¬P(c 0,c 2),\{(c_0 \neq c_1),(c_0 \neq c_2),(c_1 \neq c_2), P(c_0,c_1),P(c_1,c_1), \neg P(c_0,c_0), \neg P(c_0,c_2),

¬P(c 1,c 0),¬P(c 1,c 2),¬P(c 2,c 0),¬P(c 2,c 1),¬P(c 2,c 2)}\neg P(c_1,c_0), \neg P(c_1,c_2),\neg P(c_2,c_0),\neg P(c_2,c_1),\neg P(c_2,c_2)\}

So, in a sense, we have “translated” the structure 𝒜\mathcal{A} into “syntax”.

The diagram lemma says, for any structure \mathcal{B} that interprets L CL_C,

diag(𝒜)\mathcal{B} \models diag(\mathcal{A}) if and only if there is an embedding f:𝒜f : \mathcal{A} \to \mathcal{B}

In the example above, we can convert diag(𝒜)diag(\mathcal{A}) to a single formula by taking the conjunction, since |A||A| is finite. If we add the formula

w(w=c 0w=c 1w=c 2)\forall w(w = c_0 \vee w = c_1 \vee w = c_2)

we get a single formula ϕ 𝒜\phi_{\mathcal{A}} which uniquely defines \mathcal{B} up to isomorphism. I.e.,

ϕ 𝒜\mathcal{B} \models \phi_{\mathcal{A}} if and only if 𝒜\mathcal{B} \cong \mathcal{A}.

This means we can, in a sense, convert models to syntax: to diagram formulas. To get rid of the constants, one just quantifies them away with existential quantifiers. So, the diagram formula, Φ 𝒜\Phi_{\mathcal{A}}, for 𝒜\mathcal{A} above is:

xyz((xy)(xz)(yz)P(x,y)P(y,y)¬P(x,x)¬P(x,z)\exists x \exists y \exists z((x \neq y) \wedge (x \neq z) \wedge (y \neq z) \wedge P(x,y) \wedge P(y,y) \wedge \neg P(x,x) \wedge \neg P(x,z) \wedge

¬P(y,x)¬P(y,z)¬P(z,x)¬P(z,y)¬P(z,z)w(w=xw=yw=z))\neg P(y,x) \wedge \neg P(y,z) \wedge \neg P(z,x) \wedge \neg P(z,y) \wedge \neg P(z,z) \wedge \forall w(w = x \vee w = y \vee w = z))

This does generalize to infinite structures 𝒜\mathcal{A} by taking a sufficiently large infinitary language L κ,λL_{\kappa,\lambda}. If |A|=κ|A| = \kappa, then the diagram formula Φ 𝒜\Phi_{\mathcal{A}} is in L κ +,κ +L_{\kappa^{+},\kappa^{+}}.

If one is careful about how one labels the relations in the syntax, then we get:

𝒜Φ 𝒜Φ \mathcal{A} \cong \mathcal{B} \Leftrightarrow \Phi_{\mathcal{A}} \equiv \Phi_{\mathcal{B}}.

So, isomorphic structures are “converted” into logically equivalent formulas.

Scott’s Isomorphism Theorem is explained in John Bell’s article on Infinitary Logic (again on SEP). Scott showed that, for countable structures 𝒜\mathcal{A}, one can define a rather complicated formula ϕ 𝒜 Scott\phi^{Scott}_{\mathcal{A}} in the language L ω 1,ωL_{\omega_1,\omega} such that any countable model of ϕ 𝒜 Scott\phi^{Scott}_{\mathcal{A}} is isomorphic to 𝒜\mathcal{A}.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 25, 2013 1:55 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Oops - apologies, I replied too quick: I hadn’t realised the links you gave were the same as the links I gave!

Jeff

Posted by: Jeffrey Ketland on November 25, 2013 3:17 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Why, John, do you want what you ask for? What’s missing in what we already have?

No doubt at some point a clever person will extend Awodey and Forssell’s logical duality between first-order theories and their models to homotopy type theories and their models, as we discussed here.

What kind of result do you want?

Posted by: David Corfield on November 25, 2013 8:55 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David wrote:

Why, John, do you want what you ask for?

Because I think Jeffrey has an interesting idea that can only be clarified using more category theory.

He’s got this map sending each model of a first-order theory TT to something he calls the ‘abstract theory’ of that model: roughly, it says what’s valid in that model.

I think there should be a map like this that’s a functor from some category Mod(T)Mod(T) of models of TT to some other category which is ‘more syntactic’ in nature. And, in the nicest context, it should be an equivalence.

But unfortunately, Jeffrey seems to have only defined his map on objects, and it sends isomorphic objects of Mod(T)Mod(T) to equal element of some set. For a while I was hoping he had defined his map on morphisms too, but something Mike said made me doubt this.

What’s missing in what we already have?

You’re making it sound like ‘we’ is a unified entity, the collective consciousness of mathematicians… but I’m not an expert on logic, so I’m not part of that ‘we’. The result I’m looking for could easily be already known.

And it looks like you’re getting me a lot closer! I had to dig around to find Makkai’s paper, but I missed your blog article on this thesis:

• Henrik Forssell, First-order logical duality.

This comes a lot closer to what I want: a nice categorified version of Stone duality good for the predicate calculus. It may be exactly what I want — I’ll need to read it more carefully.

It’s easier to explain what I want in a simpler situation, namely propositional logic. Here there is just a set of models, not a category, so everything simplifies. You know everything I’m about to say, but I’ll say it anyway, just to ponder how Forssell or someone could categorify it, and how close that comes to what Jeffrey is doing, or should be doing. Indeed, what I’m about to say can be found in Forssell’s thesis!

A good way to describe a theory in classical propositional logic is via a Boolean algebra. A model of a Boolean algebra AA is homomorphism A2A \to 2. The set of models of AA is

Mod(A)=hom Boole(A,2)Mod(A) = hom_{Boole}(A,2)

and this is a topological space, actually a Stone space. A point in this space says which propositions are true. Conversely, given a topological space XX, we get back a Boolean algebra

Prop(X)=hom Top(X,2)Prop(X) = hom_{Top}(X,2)

namely the Boolean algebra of closed and open sets in XX. Think of this as the Boolean algebra of propositions about where you are in the space XX.

These two constructions give an adjunction

Mod:BooleTop:Prop Mod: Boole \stackrel{\to}{\leftarrow} Top : Prop

but as usual, you can tweak it to become an equivalence, for example:

Mod:BooleStone:Prop Mod: Boole \stackrel{\to}{\leftarrow} Stone : Prop

where we restrict to Stone spaces. So, if we start with a Boolean algebra, form its space of models Mod(T)Mod(T), and then the Boolean algebra Prop(Mod(T))Prop(Mod(T)), you get back where started!

It looks like Forsell is generalizing exactly this idea to first-order predicate logic! That would be good. Ideally, we’ll wind up with an equivalence of 2-categories. In one direction, taking some sort of first-order theory TT, we get its groupoid of models, Mod(T)Mod(T). According to Forsell this is some sort of topological groupoid. In the reverse direction, we take a topological groupoid XX and get some sort of first-order theory Prop(X)Prop(X). And we have an equivalence

ι:TProp(Mod(T)) \iota : T \stackrel{\sim}{\to} Prop(Mod(T))

so we can recover our theory, up to equivalence, from its groupoid of models.

All this is looking good, and it’s even better that Forsell mentions Beth definability, which should be a key part of this idea.

As you may recall, all this is closely related to stuff I used to talk about with you and Jim Dolan. If we go one more step up the categorical ladder we should get 2-groupoids of models for theories some very nice sort of ‘modal logic’ (better than the kind most people study), and we should be able to recover such a theory from its 2-groupoids of models.

However, I’m not sure how all this stuff relates to my personal interpretation of what Jeffrey should be doing. I’m imagining. Remember, I was hoping to get some ‘more syntactic’ description of the groupoid X=Mod(T)X = Mod(T). The equivalence

ϵ:Mod(Prop(X))X \epsilon : Mod(Prop(X)) \stackrel{\sim}{\to} X

might be what I’m seeking, but I can’t tell yet.

Posted by: John Baez on November 26, 2013 1:45 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John,

Mike is right that I didn’t define how to go from an (iso-)morphism f:ABf : A \to B of models to a morphism Φ(f)\Phi(f) between the corresponding diagram formulas Φ A\Phi_{A} and Φ B\Phi_{B}. But I think there is some way to define it.

For each model AA, to define Φ A\Phi_A, one selects bijections

v:dom(A)v[A]v: dom(A) \to v[A],

where v[A]v[A] is a set of first-order variables, and

r:Rel(A)r[Rel(A)]r: Rel(A) \to r[Rel(A)]

where r[Rel(A)]r[Rel(A)] is a set of second-order variables (where Rel(A)Rel(A) is the set of distinguished relations of AA). One then defines the corresponding diagram (see of literals) and defines the resulting formula, which, properly speaking, is Φ A v,r\Phi^{v,r}_A, depending on v,rv,r.

In fact, the choice of vv doesn’t matter, because all first-order variables in Φ A v,r\Phi^{v,r}_A have been quantified. Given any pair of models, A,BA,B, so long as the labellings r,r r, r^{\prime} are compatible, then we do have:

Equivalence theorem

ABΦ A v,rΦ B v ,r A \cong B \Leftrightarrow \Phi^{v,r}_A \equiv \Phi^{v^{\prime},r^{\prime}}_B.

To try and answer Mike’s point, suppose we have a witness

f:ABf : A \to B

of isomorphism, then we can define a corresponding “infinitary proof”, taking us from the diagram formula Φ A v,r\Phi^{v,r}_A to the diagram formula Φ B v ,r \Phi^{v^{\prime},r^{\prime}}_B. This proof, conceptually, is quite simple.

Step 1 - skolemize Φ A v,r\Phi^{v,r}_A, using α:v[A]C\alpha : v[A] \to C, to get sk α(Φ A v,r)sk_{\alpha}(\Phi^{v,r}_A).

Step 2 - existentially generalize, using β 1:Cv [B]\beta^{-1} : C \to v^{\prime}[B], to get Φ B v ,r \Phi^{v^{\prime},r^{\prime}}_B.

The proofs p α,βp_{\alpha,\beta} are then indexed by pairs of skolemizations α:v[A]C\alpha : v[A] \to C and β:v [B]C\beta : v^{\prime}[B] \to C which yield the (literally) same result.

So, given some isomorphism f:ABf : A \to B, how does one find p α,βp_{\alpha, \beta}? First, one picks a set of constants CC of cardinality equal to |dom(A)||dom(A)|.

Next, one selects any bijection,

α:v[dom(A)]C\alpha : v[dom(A)] \to C,

which skolemizes Φ A v,r\Phi^{v,r}_A. So,

αv:dom(A)C\alpha \circ v : dom(A) \to C.

in effect, assigns to each elementt adom(A)a \in dom(A) a unique constant α(v(a))C\alpha(v(a)) \in C.

Next, let the required skolemization,

β:v [dom(B)]C\beta : v^{\prime}[dom(B)] \to C

be defined by (what amounts to a commutative diagram):

β=αvf 1(v ) 1\beta = \alpha \circ v \circ f^{-1} \circ (v^{\prime})^{-1}

The proof p α,βp_{\alpha,\beta} is then the corresponding “morphism”, taking one from the formula Φ A v,r\Phi^{v,r}_A to the formula Φ B v ,r \Phi^{v^{\prime},r^{\prime}}_B.

I think, but am not sure, that this answers Mike’s question. (There is an “arbitrary choice” to be made in the proof: that is, selecting some bijection α:v[dom(A)]C\alpha : v[dom(A)] \to C, where CC is a set of constants.)

This is all quite different from Lindenbaum-Tarski algebra stuff.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 26, 2013 4:03 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I don’t follow what you’re doing, and all the arbitrary choices make me nervous, because typically something tends to be a functor when there are very few arbitrary choices involved in its definition. But there’s an easy way to settle the matter if you understand what’s going on. Just see if your recipe for sending morphisms f:ABf : A \to B to morphisms Φ^ f:Φ^ AΦ^ B\hat{\Phi}_f : \hat{\Phi}_A \to \hat{\Phi}_B obeys the key condition any functor must obey:

Φ^ gf=Φ^ gΦ^ f \hat{\Phi}_{g \circ f} = \hat{\Phi}_g \circ \hat{\Phi}_f

If this is true, all the arbitrary choices you made were ‘innocuous’.

Posted by: John Baez on November 26, 2013 6:31 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John, yes, the arbitrary choices might cause a problem.

Let me give really simple example, of two isomorphic graphs, so I can think about it. (This is all pretty basic predicate logic …)

G 1=(V 1,E 1)G_1 = (V_1,E_1) with V 1={0,1,2}V_1 = \{0,1,2\} and E 1={(0,1),(0,2)}E_1 = \{(0,1),(0,2)\}.

G 2=(V 2,E 2)G_2 = (V_2,E_2) with V 2={3,4,5}V_2 = \{3,4,5\} and E 2={(3,4),(3,5)}E_2 = \{(3,4),(3,5)\}.

So each graph has three vertices; G 1G_1 has a vertex 00, with directed edges to both 11 and 22; and G 2G_2 has a vertex 33 with, directed edges to both 33 and 44. Clearly, G 1G 2G_1 \cong G_2. And there are two isomorphisms f,f :G 1G 2f,f^{\prime} : G_1 \to G_2.

f(0)=3f(0) = 3; f(1)=4f(1) = 4; f(2)=5f(2) = 5.

f (0)=3f^{\prime}(0) = 3; f (1)=5f^{\prime}(1) = 5; f (2)=4f^{\prime}(2) = 4.

The diagram formulas are a bit ugly, I’m afraid. I also need to map vertices to variables, using a domain labelling vv, and map the edge relation both to a second-order variable (in both cases, I map the edge relation to the variable XX). Let me have the domain labellings:

v 1:V 1{x 0,x 1,x 2}v_1 : V_1 \to \{x_0,x_1,x_2\}.

v 2:V 2{x 3,x 4,x 5}v_2 : V_2 \to \{x_3,x_4,x_5\}.

In the first case, I get Φ G 1 v 1,r\Phi^{v_1,r}_{G_1} as the formula:

x 0x 1x 2(x 0x 1x 0x 2x 1x 2¬X(x 0,x 0)z(z=x 0z=x 1z=x 2))\exists x_0 \exists x_1 \exists x_2(x_0 \neq x_1 \wedge x_0 \neq x_2 \wedge x_1 \neq x_2 \wedge \neg X(x_0,x_0) \wedge \dots \wedge \forall z(z = x_0 \vee z = x_1 \vee z = x_2)).

In the second case, I get Φ G 2 v 2,r\Phi^{v_2,r}_{G_2} as the formula:

x 3x 4x 5(x 3x 4x 3x 5x 4x 5¬X(x 3,x 3)z(z=x 3z=x 4z=x 5))\exists x_3 \exists x_4 \exists x_5(x_3 \neq x_4 \wedge x_3 \neq x_5 \wedge x_4 \neq x_5 \wedge \neg X(x_3,x_3) \wedge \dots \wedge \forall z(z = x_3 \vee z = x_4 \vee z = x_5)).

It should be blindingly obvious that they’re equivalent! I.e.,

Φ G 1 v 1,rΦ G 2 v 2,r\Phi^{v_1,r}_{G_1} \cong \Phi^{v_2,r}_{G_2}

So, my isomorphic graphs have been “translated” into equivalent formulas. But to do this, I had to choose how to label the domain elements in V 1,V 2V_1, V_2, using variables. This is what the superscripts v 1,v 2v_1,v_2 refer to; and I had to choose how to label the edge relations (I labelled both with XX; this is what the “rr” superscript refers to). But in order to label a model (A,R 1,R 2,)(A, R_1, R_2, \dots) something into a language, I have to specify mappings somehow that map domain elements aAa \in A to variables, and to map distinguished relations R iR_i to second-order variables.

Let me now write down a proof of the second formula Φ G 2 v 2,r\Phi^{v_2,r}_{G_2}from the first Φ G 1 v 1,r\Phi^{v_1,r}_{G_1}:

1 x 0x 1x 2(x 0x 1x 0x 2x 1x 2¬X(x 0,x 0)z(z=x 0z=x 1z=x 2))\exists x_0 \exists x_1 \exists x_2(x_0 \neq x_1 \wedge x_0 \neq x_2 \wedge x_1 \neq x_2 \wedge \neg X(x_0,x_0) \wedge \dots \wedge \forall z(z = x_0 \vee z = x_1 \vee z = x_2)).

2 x 1x 2(c 0x 1c 0x 2x 1x 2¬X(c 0,c 0)z(z=c 0z=x 1z=x 2))\exists x_1 \exists x_2(c_0 \neq x_1 \wedge c_0 \neq x_2 \wedge x_1 \neq x_2 \wedge \neg X(c_0,c_0) \wedge \dots \wedge \forall z(z = c_0 \vee z = x_1 \vee z = x_2)).

3 x 2(c 0c 1c 0x 2c 1x 2¬X(c 0,c 0)z(z=c 0z=c 1z=x 2))\exists x_2(c_0 \neq c_1 \wedge c_0 \neq x_2 \wedge c_1 \neq x_2 \wedge \neg X(c_0,c_0) \wedge \dots \wedge \forall z(z = c_0 \vee z = c_1 \vee z = x_2)).

4 (c 0c 1c 0c 2c 1c 2¬X(c 0,c 0)z(z=c 0z=c 1z=c 2))(c_0 \neq c_1 \wedge c_0 \neq c_2 \wedge c_1 \neq c_2 \wedge \neg X(c_0,c_0) \wedge \dots \wedge \forall z(z = c_0 \vee z = c_1 \vee z = c_2)).

5 x 5(c 0c 1c 0x 5c 1x 2¬X(c 0,c 0)z(z=c 0z=c 1z=x 5))\exists x_5(c_0 \neq c_1 \wedge c_0 \neq x_5 \wedge c_1 \neq x_2 \wedge \neg X(c_0,c_0) \wedge \dots \wedge \forall z(z = c_0 \vee z = c_1 \vee z = x_5)).

6 x 4x 5(c 0x 4c 0x 5x 4x 2¬X(c 0,c 0)z(z=c 0z=x 4z=x 5))\exists x_4 \exists x_5(c_0 \neq x_4 \wedge c_0 \neq x_5 \wedge x_4 \neq x_2 \wedge \neg X(c_0,c_0) \wedge \dots \wedge \forall z(z = c_0 \vee z = x_4 \vee z = x_5)).

7 x 3x 4x 5(x 3x 4x 3x 5x 4x 5¬X(x 3,x 3)z(z=x 3z=x 4z=x 5))\exists x_3 \exists x_4 \exists x_5(x_3 \neq x_4 \wedge x_3 \neq x_5 \wedge x_4 \neq x_5 \wedge \neg X(x_3,x_3) \wedge \dots \wedge \forall z(z = x_3 \vee z = x_4 \vee z = x_5)).

Apologies for this being messy, but it is quite simple in principle. I skolemize three times (introducing a constant for an initial existentially bound first-order variable), to get the formula (4), and I then existentially generalize three times to get the formula (7), which is the required formula!

This proof in fact corresponds (once we chose the skolemization that took us from x 0x_0 to c 0c_0, x 1x_1 to c 1c_1, x 2x_2 to c 2c_2) to the isomorphism f:G 1G 2f : G_1 \to G_2. So, this proof is Φ(f)\Phi(f).

There two isomorphisms g,g :G 2G 1g, g^{\prime} : G_2 \to G_1, i.e.,

g(3)=0g(3) = 0; g(4)=1g(4) = 1; g(5)=2g(5) = 2.

g (3)=0g^{\prime}(3) = 0; g (5)=1g^{\prime}(5) = 1; g (4)=2g^{\prime}(4) = 2.

Now gf:G 1G 1g \circ f : G_1 \to G_1 is just the identity. But g f:G 1G 1g^{\prime} \circ f : G_1 \to G_1 is a non-trivial automorphism of G 1G_1: it transposes 1,21,2. Φ(g )\Phi(g^{\prime}) delivers a proof taking us from Φ G 2\Phi_{G_2} to Φ G 1\Phi_{G_1}, as required. And we define

Φ(g)Φ(f)\Phi(g) \circ \Phi(f) to mean: “concatenation of proofs”.

We can then show, I think, that,

Φ(g f)=Φ(g )Φ(f)\Phi(g^{\prime} \circ f) = \Phi(g^{\prime}) \circ \Phi(f)

Unfortunately, the labelling parameters all become quite complicated…

Possibly I should perhaps consider not a category of models, but a category of labeled models, triples of the form (𝒜,v,r)(\mathcal{A}, v, r), and let the functor Φ\Phi be understood as a functor operating on the category of these labeled models to formulas in LL, by giving proofs. I am unsure.

I think, but I’m not sure, that the answer to Mike’s question is that when

f:(𝒜 1,v 1,r 1)(𝒜 2,v 2,r 2)f : (\mathcal{A}_1, v_1,r_1) \to (\mathcal{A}_2, v_2, r_2)

is an isomorphism, then is a morphism Φ(f)\Phi(f) (“proof”) taking us from the formula Φ(𝒜 1,v 1,r 1)\Phi(\mathcal{A}_1,v_1,r_1) to the formula Φ(𝒜 2,v 2,r 2)\Phi(\mathcal{A}_2,v_2,r_2).

Or possibly I should include a labelling that maps elements to constants as well, and define “isomorphism” accordingly. In that case, then I think Φ(f)\Phi(f) will be uniquely determined and satisfy Φ(fg)=Φ(f)Φ(g)\Phi(f \circ g) = \Phi(f) \circ \Phi(g). So, then, the mapping Φ\Phi is a functor from labelled models (with morphisms being isomorphisms) to formulas (with morphisms being proofs). I think the second category is a groupoid, but again not so sure.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 26, 2013 10:09 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Before you can ask whether Φ(gf)=Φ(g)Φ(f)\Phi(g\circ f) = \Phi(g) \circ \Phi(f), you need to say what you mean by two proofs being “equal”. Obviously they are not going to be syntactically identical, so you need some looser notion of equality.

Posted by: Mike Shulman on November 26, 2013 4:01 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mike,

Yes, you’re right. The definition of Φ fΦ g\Phi_f \circ \Phi_g that I suggested was syntactic concatenation of the proof sequences. The (possibly infinitary) proofs Π(A,B)\Pi(A,B) I describe are linear Hilbert-style proofs and all have the same form

We are given a diagram formula Φ A\Phi_A, and a bijection f:dom(A)dom(B)f : dom(A) \to dom(B) and a skolemization α:v[A]Const\alpha : v[A] \to Const, where ConstConst is some set of constants in LL. We skolemize Φ A\Phi_A using α\alpha, and then generalize, using ff, to get a result. The result is Φ B\Phi_B just if f:ABf : A \to B is an isomorphism.

Call such a proof Π f,α(A,B)\Pi_{f,\alpha}(A,B); this is the SG-proof of Φ B\Phi_B from Φ A\Phi_A, relative to f,αf, \alpha.

(They are “constructive” in the sense that they only use the standard rules for quantifiers; they don’t do anything odd for connectives. The diagram formulas are made up from atomic formulas, negated atomic formulas, conjunction, disjunction and quantifiers. So, e.g., (LEM) is never involved in any SG-proof. On the other hand, an SG-proof is non-constructive in involving “infinitary operations”, such as “replace infinite many variables by infinite many constants”.)

It seems right that if f:ABf : A \to B is an isomorphism, then Π f,α(A,B)\Pi_{f,\alpha}(A,B) is an SG-proof of Φ B\Phi_B from Φ A\Phi_A. It also true that the particular skolemizaiton α:v[A]Var(L)\alpha : v[A] \to Var(L) chosen is “innocuous”. So, my definition of Φ f\Phi_f is:

Φ f\Phi_f is defined to be Π f,α(A,B)\Pi_{f,\alpha}(A,B), for some (hopefully, innocuous) choice of skolemization α:v[A]Const\alpha : v[A] \to Const.

I suggested that Φ fΦ g\Phi_f \circ \Phi_g is simply concatenation, Φ f Φ g\Phi_f^{\frown} \Phi_g.

But you’re right: the concatenation of two SG-proofs is not an SG-proof. So, I don’t get composition of morphisms.

Let me try again.

given Φ A\Phi_A, and an isomorphism f:ABf: A \to B and a skolemization α\alpha: skolemize, and then generalize to get Φ B\Phi_B. The result is a sequence of the form

(Φ A,,sk α(Φ A),,Φ B)(\Phi_A, \dots, sk_{\alpha}(\Phi_A), \dots, \Phi_B)

Let me call sk α(Φ A)sk_{\alpha}(\Phi_A) the mid-point of the proof.

Now suppose we have SG-proofs, corresponding to isomorphisms f:ABf : A \to B and g:BCg : B \to C:

(Φ A,,sk α(Φ A),,Φ B)(\Phi_A, \dots, sk_{\alpha}(\Phi_A), \dots, \Phi_B)

(Φ B,,sk β(Φ B),,Φ C)(\Phi_B, \dots, sk_{\beta}(\Phi_B), \dots, \Phi_C)

Their concatenation is,

(Φ A,,sk α(Φ A),,Φ B,Φ B,,sk β(Φ B),,Φ C)(\Phi_A, \dots, sk_{\alpha}(\Phi_A), \dots, \Phi_B, \Phi_B, \dots, sk_{\beta}(\Phi_B), \dots, \Phi_C)

This is not an SG-proof relative to the isomorphism gfg \circ f. But we can “cut out the middle part”, and get,

(Φ A,,sk α(Φ A),,Φ C)(\Phi_A, \dots, sk_{\alpha}(\Phi_A), \dots, \Phi_C)

where the second half of the proof, as it were, uses the composed bijection gfg \circ f,

(Φ A,,sk α(Φ A),,Φ C)(\Phi_A, \dots, sk_{\alpha}(\Phi_A), \dots, \Phi_C)

and this is an SG-proof Π gf,α(A,C)\Pi_{g \circ f, \alpha}(A,C).

So, we redefine composition of morphisms Φ f,Φ g\Phi_f, \Phi_g as, roughly, “concatenation + cutting out the middle part”. Then, I think we get something very close to,

Φ gf=Φ fΦ g\Phi_{g \circ f} = \Phi_{f} \circ \Phi_g

up to a choice of some skolemization of the starting formula.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 27, 2013 7:17 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

It sounds possible, but very sketchy. In order for this to be interesting, I would want to see a complete definition of a category of some kind of formulas whose morphisms are some kind of proofs, including composition and identities, prior to beginning the definition of Φ\Phi. Why? Well, consider the following:

Suppose we have a category CC, a set XX, and for each x,yXx,y\in X a set Y(x,y)Y(x,y). Suppose furthermore we have an injection i:ob(C)Xi : ob(C) \to X and for each c,dob(C)c,d\in ob(C) an injection j c,d:C(c,d)Y(x,y)j_{c,d}:C(c,d) \to Y(x,y). Then we can transport the structure of category from CC to define a category CC' whose objects are im(i)Xim(i) \subseteq X and whose morphisms C(i(c),i(d))C'(i(c),i(d)) are im(j c,d)Y(i(c),i(d))im(j_{c,d}) \subseteq Y(i(c),i(d)). But this doesn’t tell us anything interesting about the relationship of CC to the sets XX and Y(x,y)Y(x,y) except that there exist the injections ii and j c,dj_{c,d}.

This construction is starting to me to feel like an instance of this, with C=ModelsC = Models and X=FormulasX=Formulas and Y(x,y)=ProofsY(x,y) = Proofs.

Posted by: Mike Shulman on November 27, 2013 6:18 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

FWIW, there’s a standard argument that in classical logic, there is no interesting notion of equality on proofs. For suppose Π 1\Pi_1 and Π 2\Pi_2 are two proofs of a statement ϕ\phi. Then for any statement ψ\psi, consider the proof

Π 1\Pi_1, therefore ϕ\phi, and thus, ϕ¬ψ\phi\vee\neg\psi. Also, Π 2\Pi_2, therefore ϕ\phi, and thus ψϕ\psi \vee \phi. Now by LEM, either ψ\psi or ¬ψ\neg\psi, and in either case we obtain ϕ\phi.

As long as our notion of proof equivalence includes “cut elimination”, then this proof ends up having to be equal to both Π 1\Pi_1 and Π 2\Pi_2. Hence, all proofs are equal.

Posted by: Mike Shulman on November 26, 2013 4:27 PM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

I missed your blog article

Well you didn’t, since you were one of the few to contribute to the discussion of it. But I find my memory isn’t what it used to be :(

So do they leave anything undone? What more would you want from the theory that’s reconstructed from a topological groupoid of models? Presumably that groupoid could be connected, so all models are isomorphic. Retaining all the isomorphisms will be necessary to the reconstruction of the theory.

It’s very like a Tannaka-Krein reconstruction.

Posted by: David Corfield on November 26, 2013 10:00 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

David Corfield wrote:

But I find my memory isn’t what it used to be :(

Lucky devil. I’m not even sure of that.

So do they leave anything undone?

Not sure. For a while I thought Jeffrey had the germ of some other idea which unfortunately he was presenting in somewhat decategorified form. But thanks to Mike’s questions I’m beginning to doubt that. My dream of boosting Jeffrey’s idea into an interesting equivalence of categories may have been a will-o’-the-wisp.

What more would you want from the theory that’s reconstructed from a topological groupoid of models?

Certainly Forsell’s thesis does a good job of what it seeks to do. However, from a Boolean algebra we get something better than a mere topological space. We get a Stone space, meaning a topological space that’s compact, Hausdorff and totally disconnected: the only connected subsets are the trivial ones. There’s a contravariant equivalence between the category of Boolean algebras and the category of Stone spaces.

So, going up the ladder one notch, I’d want the groupoid of models of a (suitable) first-order theory to be not merely a topological groupoid, but some sort of ‘Stone groupoid’. And I’d want a contravariant equivalence between the 2-category of these first-order theories and the 2-category of these Stone groupoids.

I don’t know if Forsell does this or not!

Also, everything I just described is for classical logic but there should also be an intuitionistic version.

Presumably that groupoid could be connected, so all models are isomorphic. Retaining all the isomorphisms will be necessary to the reconstruction of the theory.

We don’t expect all models of a typical first-order theory to be isomorphic: it’s certainly not true for the first-order theory of groups! It’s only true for so-called categorical theories, like the theory of 5-element groups.

(This use of the word ‘categorical’ has little to do with the way category theorists use this word!)

Posted by: John Baez on November 28, 2013 5:40 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

John,

I’m still unsure about how to make this category-theoretically ok; I think the groupoid 𝒢 A\mathcal{G}_A of models (= structured sets) isomorphic to AA (morphisms as isomorphisms) might still be equivalent (in the Cat-sense) to another groupoid 𝒟 A\mathcal{D}_A, of diagram formulas (with morphisms f:ABf : A \to B in 𝒢\mathcal{G} mapped to “skolemization-existential generalization” proofs, Π f:AB\Pi_{f: A \to B} of Φ B\Phi_B from Φ A\Phi_A). Mike raised the concern about composition of morphisms, since the concatenation of two such proofs Π f:AB,Π g:BC\Pi_{f: A \to B}, \Pi_{g : B \to C} is not syntactically identical to Π (gf):AC\Pi_{(g \circ f) : A \to C}. I agree. But it might be possible to define “composition” \circ of these proofs by “cutting out the middle part” and concatenation, so that Π f:ABΠ g:BC=Π (gf):AC\Pi_{f : A \to B} \circ \Pi_{g : B \to C} = \Pi_{(g \circ f) : A \to C}.

Maybe if this works, then

Φ:𝒢 A𝒟 A\Phi : \mathcal{G}_A \to \mathcal{D}_A

is a functor with the right properties, and the category 𝒟 A\mathcal{D}_A might be called the “diagram category” for AA. Mike’s objection, however, might be entirely right; or, maybe something works, but it’s somehow very trivial and not mathematically interesting. Strictly speaking, there isn’t a single functor, but rather an indexed set, {Φ v,r}\{\Phi^{v,r}\}, where v,rv,r are functions that “label” the “parts” (elements of carrier set and distinguished relations) of any given model in 𝒢 A\mathcal{G}_A.

Yes, it’s not about Mod(T)Mod(T) for ordinary first-order theories TT in L ω,ωL_{\omega,\omega}, and Lindenbaum-Tarski-Stone-etc., stuff, because these are never interestingly categorical (in the logician’s sense: one-model-up-to-isomorphism; or one-model-in cardinality-κ\kappa-up-to-isomorphism) theories TT, when TT has an infinite model. So, Makkai’s article, and Forsell’s work seems to have a different focus. I want all my models to be isomorphic, and all the formulas to be logically equivalent. So, I use L κ,λL_{\kappa,\lambda}.

Cheers,

Jeff

Posted by: Jeffrey Ketland on November 28, 2013 7:17 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Well, we don’t quite have a contravariant equivalence, but the theory of classifying toposes comes close to giving one: by Morleyisation, it suffices to consider only theories in the coherent fragment of first order logic, and the classifying toposes for coherent theories are known to have enough points; but Butz and Moerdijk have shown that every Grothendieck topos with enough points is equivalent to the category of equivariant sheaves on a (non-canonical) topological groupoid. This groupoid is basically constructed by considering a sufficiently large (= enough to decide any formula of the theory) family of models and the isomorphisms between them, and the topology is essentially the Krull topology.

So I think there is hope yet to find a more precise duality between topological groupoids and coherent theories.

Posted by: Zhen Lin on November 28, 2013 8:43 AM | Permalink | Reply to this

Re: The Covariance of Coloured Balls

Mightn’t the truly topos-theoretic point of view be that it’s the classifying topos itself that should be regarded as the categorified “space of models”?

Posted by: Mike Shulman on November 28, 2013 5:49 PM | Permalink | Reply to this

Post a New Comment