User talk:Dominic Mayers (old)/sandbox

About transportability

I finally read the proof by Marshall et al. My comment on it and on transportability in general is that what is a transportable sentence depends heavily on the choice of individual constants used in the first order language that defines the possible sentences. This might be obvious, but worth keeping in mind nevertheless. In Marshall et al., every individual constant is to be interpreted either as an element $Y_{i}$ of a scale set, as a base set $X_{i}$ or as the universe of sets over the base sets $X_{i}$ of rank less than or equal to $n$. The universe of sets is only added in Marshall et al. as a flexible way to restrict the range of the variables. For example, when $n=0$, we have the usual cases where the variables range over the base sets. The other constants are the expected constants of a structure: the base sets and the operations (or relations). This is a reasonable choice of constants given the definition of structures in Bourbaki and the fact that the purpose of the sentences is to define species of structures.

However, the definition of transportability does not have to be tightly linked to the notion of structures, even less, to the specific notion of structures defined by Bourbaki. It can be defined for any first order language with equality that has membership as binary predicate, some constants for the base sets, other constants for other sets defined over the base sets and a constant for a universe of set over the base sets, which we also use to restrict the range of the variables. This is a simple generalization of the language ${\cal {L}}$ defined in Marshall et al. In Marshall et al., the other sets (beside the universe of sets and the base sets) are elements of some scale set, but the language can be generalized to any other way to identify sets over the base sets

In Bourbaki, for any pair of base sets, the canonical extensions to scale sets of any bijections between the two base sets are expected to be themselves bijections. Similarly, a language is transportable if, for any pair of base sets, the canonical extensions to the universe of sets and to the sets in the universe of sets of any bijections between the two base sets are themselves bijections. Note that Bourbaki does not define such canonical extensions, but it is not hard to do that. However, these canonical extensions are not necessarily bijections in general.

The interesting point is that, given a transportable language ${\cal {L}}$, every sentence in ${\cal {L}}$ is transportable. The key idea of the proof is simply that every occurrence of $x\in y$ is equivalent to $F(x)\in F(y)$, where $F$ is the canonical extension. The converse is ill defined or trivially true if it means that every transportable sentence of ${\cal {L}}$ is a sentence in ${\cal {L}}$.

For example, if we restrict ourselves to a single principal base set, then the language is transportable. This is interesting, given that, when we allow auxiliary base sets, the language becomes very flexible. One can even simulate many principal base sets using a mapping from the single principal base sets to a set of identifiers for the simulated principal base sets.

What's going on? How comes it is so complicated in Marshall et al. and only a sub-language of ${\cal {L}}$, namely the sentences (equivalent to a sentence) of type theory, are transportable? Note that, in Marshall the proof is also relative to sentences in ${\cal {L}}$. So, if all the sentences of ${\cal {L}}$ were transportable, the converse will be trivial, just as we discussed above. Therefore, the key question is why, in their case, only the sentences of a sub-language are transportable. Look at the basic idea of the proof. Why would it fail in their case? Because the canonical extension on a set in the universe of sets is not necessarily a bijection. If it is not a bijection, then the argument of the simple proof fails. Note that, if we consider sentences of type theory, then the simple proof does not fail, because then each variable runs over one type, all the "evil" sets are eliminated, and the canonical extension is a bijection on all sets of the new universe. We might have to generalize the arguments to the case of many universe of sets, one for each type: the disjoint union of these universes becomes the single universe.

It's not that type theory makes the issue go away. If you think that type theory is the explanation, then explain why, in which way, it makes the issue go away? The reason is that a canonical extension of bijections on the set of the universe is always a bijection. This is what makes the issue go away and it can be done without type theory. Of course, if you believe that type theory is the way to describe structures and isomorphisms, then there is no good definitions without type theory - they will always look "evil" to you. But, even if we have this attitude, we can accept that to better understand the "non evil" case of type theory, it is useful to take a step back and accept to consider the evil cases as well.

My conclusion is that, if you feel that the union of sets of different types and similar operations are "evil", then work in type theory and every thing is simple: all sentences of type theory are transportable. If, on the other hand, you feel more like working with the flexibility of ZFC, and allow arbitrary union, etc. then define isomorphism and structure in an intelligent manner so that the canonical extension of bijections is always a bijection. If we do that, every thing is always simple: all sentences of the transportable language are transportable. Marshall et al. work at the level of a problem that was created by a bad choice of definitions in Bourbaki. Bourbaki should either have fully adopted type theory or else used definitions such that the language ${\cal {L}}$ is transportable, for example, by further requiring a bijection between the two unions of the base sets. In both cases, Marshall et al. would not have existed. The question would not have been even raised and I doubt mathematics would have suffered from that. On the contrary, it would have been better that way.