Leibniz Abstraction, Structure Identity and Univalence
In mathematics, one gets used to thinking of a particular mathematical object - say a group, or a graph, or a partial order, or a field, or a topological space in abstract terms. That is, given the model $(X, R_1, \dots)$ one "forgets" the specific nature of the carrier set $X$, and one focuses only on properties of the mathematical model/structure, which are invariant under isomorphism. This means that one is, in a sense, thinking of some "entity" which all isomorphic copies "have in common".
So, for example, if our models $G_1 = (V_1, E_1)$ and $G_2 = (V_2, E_2)$ are isomorphic graphs, then one imagines that there is some other thingy -- call it $\hat{G_1}$ -- such that $\hat{G}_1 = \hat{G}_2$. Obviously, the carrier sets $V_1$ and $V_2$ can be distinct. But this is "abstracted away". If our models are isomorphic partial orders $\mathbb{P}_1 = (X_1, \preceq_1)$ and $\mathbb{P}_2 = (X_2, \preceq_2)$, then we imagine that there are corresponding "abstract structures" $\hat{\mathbb{P}}_1$ and $\hat{\mathbb{P}}_2$ such that $\hat{\mathbb{P}}_1 = \hat{\mathbb{P}}_2$.
More generally, we imagine we have some map,
Vladimir Voevodsky's Univalence Axiom, as I understand, is an attempt to make this very intuitive idea mathematically precise. There are many formulations, including in the book on Homotopy Type Theory, of course. Here is a formulation from Ulrik Buchholtz, from a 2013 talk on "Univalent Foundations and the Structure Identity Principle":
Now I'm fairly sure that this overlaps very closely with the following: one can define "thingies" $\hat{\Phi}_{\mathcal{A}}$ such that Leibniz Abstraction holds, for set-sized mathematical models $\mathcal{A},\mathcal{B}$ as follows:
The rough idea is this: let $\mathcal{A} = (A, R_1, \dots)$ be some mathematical object, with a set-sized carrier set/domain $A$ (and special or distinguished relations $R_i$). $\mathcal{A}$ can be a graph, a group, etc.
One can define a purely logical formula $\Phi_{\mathcal{A}}(\vec{X})$, in a language $\mathcal{L}(\mathcal{A})$, possibly infinitary, with free (second-order) variables amongst $\vec{X}$, such that categoricity holds:
Then we let $\hat{\Phi}_{\mathcal{A}}$ be the propositional function expressed by the diagram formua $\Phi_{\mathcal{A}}(\vec{X})$. Then Leibniz Abstraction follows. So far as I can tell, this also implements the intuitive idea that Univalence is intended to implement too: namely, the Structure Identity Principle.
So, for example, if our models $G_1 = (V_1, E_1)$ and $G_2 = (V_2, E_2)$ are isomorphic graphs, then one imagines that there is some other thingy -- call it $\hat{G_1}$ -- such that $\hat{G}_1 = \hat{G}_2$. Obviously, the carrier sets $V_1$ and $V_2$ can be distinct. But this is "abstracted away". If our models are isomorphic partial orders $\mathbb{P}_1 = (X_1, \preceq_1)$ and $\mathbb{P}_2 = (X_2, \preceq_2)$, then we imagine that there are corresponding "abstract structures" $\hat{\mathbb{P}}_1$ and $\hat{\mathbb{P}}_2$ such that $\hat{\mathbb{P}}_1 = \hat{\mathbb{P}}_2$.
More generally, we imagine we have some map,
$\mathcal{A} \mapsto \hat{\mathcal{A}}$taking us from graphs, orderings, groups, linear spaces, topological spaces, etc., etc., to abstract graphs, orderings, groups, linear spaces, etc., etc. such that
$\hat{\mathcal{A}}_1 = \hat{\mathcal{A}}_2$ iff $\mathcal{A}_1 \cong \mathcal{A}_2$.holds. I call this principle Leibniz Abstraction. But, unfortunately, no one knows that these abstract "thingies" $\hat{\mathcal{A}}$ are ... But whatever they are, they are not models, with a carrier set. Their carrier set has been abstracted away, somehow.
Vladimir Voevodsky's Univalence Axiom, as I understand, is an attempt to make this very intuitive idea mathematically precise. There are many formulations, including in the book on Homotopy Type Theory, of course. Here is a formulation from Ulrik Buchholtz, from a 2013 talk on "Univalent Foundations and the Structure Identity Principle":
Univalence Axiom (Voevodsky)(I think that the "Structure Identity Principle" amounts to what I call "Leibniz Abstraction" above; certainly, this is what has been discussed a lot by philosophers of mathematics for decades. Particularly structuralist philosophers of mathematics, like Shapiro, Hellman and Resnik.)
For types $A$ and $B$, the identity type $Id_U(A, B)$ is equivalent to the type $Eq(A,B)$ of (homotopy) equivalences between $A$ and $B$.
Now I'm fairly sure that this overlaps very closely with the following: one can define "thingies" $\hat{\Phi}_{\mathcal{A}}$ such that Leibniz Abstraction holds, for set-sized mathematical models $\mathcal{A},\mathcal{B}$ as follows:
Leibniz AbstractionThese entities are propositional diagrams.
$\hat{\Phi}_{\mathcal{A}} = \hat{\Phi}_{\mathcal{B}}$ iff $\mathcal{A} \cong \mathcal{B}$.
The rough idea is this: let $\mathcal{A} = (A, R_1, \dots)$ be some mathematical object, with a set-sized carrier set/domain $A$ (and special or distinguished relations $R_i$). $\mathcal{A}$ can be a graph, a group, etc.
One can define a purely logical formula $\Phi_{\mathcal{A}}(\vec{X})$, in a language $\mathcal{L}(\mathcal{A})$, possibly infinitary, with free (second-order) variables amongst $\vec{X}$, such that categoricity holds:
$\mathcal{B} \models \Phi_{\mathcal{A}}(\vec{X})$ iff $\mathcal{B} \cong \mathcal{A}$.Thus the formula $\Phi_{\mathcal{A}}(\vec{X})$ defines the isomorphism type (groupoid) of $\mathcal{A}$. The formula $\Phi_{\mathcal{A}}(\vec{X})$ is called the diagram formula for $\mathcal{A}$. It is called this by analogy with the notion of a diagram in model theory. The diagram of a model $\mathcal{A}$ is a kind of "picture" of all the basic relationships between elements of the model $\mathcal{A}$, obtained by introducing a constant $c_a$ to name each $a \in A$. But the diagram formula $\Phi_{\mathcal{A}}(\vec{X})$ itself does not contain any constants labelling domain elements, Rather, these have been existentially quantified.
Then we let $\hat{\Phi}_{\mathcal{A}}$ be the propositional function expressed by the diagram formua $\Phi_{\mathcal{A}}(\vec{X})$. Then Leibniz Abstraction follows. So far as I can tell, this also implements the intuitive idea that Univalence is intended to implement too: namely, the Structure Identity Principle.
Hi Jeff,
ReplyDeletethanks for the mention of my talk! I don't quite see how your construction implements the SIP, though: If A and B are isomorphic structures, then we'd like any statement made about A to hold for B, and we'd like any construction mentioning A to work for B as well. Obviously, we can only allow suitably “structural” statements and constructions. This works when A and B are equal (as per univalence), but how does it help that A and B are mapped to equal objects by your construction?
Cheers,
Ulrik
Ulrik,
ReplyDeleteOh thanks - I guessed you must be the same Ulrik!
The thing is, if $A$ and $B$ are mathematical objects, they have their carrier sets with them, so can't be literally equal. E.g., let $(X, <_1)$ and $(Y, <_2)$ be isomorphic linear orders, with $X \neq Y$. They can't be identical, because $X \neq Y$. On the other hand, if A and B are isomorphic models, then (structural) statements true of A are true of B, and vice versa.
On the diagram construction, we get a map $A \mapsto \hat{Phi}_{A}$ such that the Leibniz abstraction principle,
$\hat{\Phi}_{A} = \hat{\Phi}_B$ iff $A \cong B$.
holds.
(And I think that's very close to what you mean by Structure Identity Principle ...)
The entity $\hat{\Phi}_{A} $ is a quasi-syntactic entity: a purely "structural picture" of A. And the carrier set/domain of A has been eliminated entirely. Only the abstract structure remains.
So, to use the example in your talk, suppose $Z = (X, <_1)$ is the Zermelo model of the numbers, and $VN = (Y, <_2)$ is the von Neumann model. The carrier sets X and Y are distinct; and the relations $<_1$ and $<_2$ are extensionally distinct.
But, since they're isomorphic, we get: $\hat{\Phi}_{Z} = \hat{\Phi}_{VN}$. That is, the Zermelo model and the von Neumann model have the same "abstract structure": their structural picture is identical.
Cheers,
Jeff
Jeff,
ReplyDeletewell, the point of HTT is that in fact $A$ and $B$ can be equal; not literally, but via an inhabited identity type. Since identity types let you do almost everything you want with “equal” objects, it works out. Of course, you have to give up proof irrelevance: as you note, the carrier sets will be equal, and in general that can happen in several ways, so you need to remember “how” they're equal. But you can't make an omelette without breaking some eggs, I guess!
I looked at your post on abstract structure (here: http://m-phi.blogspot.com/2013/03/what-is-abstract-structure.html), but I'm still unclear how you perform the transport: If $\Psi$ is a propositional function of structures (over a fixed signature), and $\Phi$ holds of $A$, and $\hat\Phi_A$ equals $\hat\Phi_{A'}$ (so $A$ and $A'$ are isomorphic), how do conclude that $\Psi$ holds of $A'$? Do you need some extra conditions on $\Psi$? Presumably it works when $\Psi$ is a formula over the signature?
Cheers,
Ulrik
Ulrik,
ReplyDeleteYes, the construction of the diagram language $\mathcal{L}(\mathcal{A})$ depends on the starting model $\mathcal{A} = (A, R_1, \dots)$ and its signature. (Here $A$ is the carrier set/domain, $R_i$ are the special relations on $A$.)
The diagram formula $\Phi_{\mathcal{A}}(\vec{X})$ has a sequence $\vec{X}$ of second-order variables, which are "labels" of the carrier set $A$ and distinguished relations in $\mathcal{A}$.
(In the notes on this I have, I call this a "relation-labelling", $\rho$, which takes us from the distinguished relations to second-order variables, preserving arity: - so, $\rho$ maps the carrier set $A$ to a unary second-order variable, say $X_0$, and maps each special relation $R_i$ to a second-order variable $X_i = \rho(R_i)$ of the same arity. To define $\Phi_{\mathcal{A}}(\vec{X})$, there is also a "domain labelling", $\nu$, which maps each domain element $a \in A$ to a first-order variable $\nu(a)$ in $\mathcal{L}(\mathcal{A})$. These free first-order variables are then existentially quantified).
Then, we can prove a categoricity result, which lets us transfer between isomorphic models. But the only properties which are transferred are purely "structural".
Does that sound ok? What I'm doing is coming from model theory, rather than category theory though.
The propositional function bit is to remove the dependence on syntactic issues, because strictly speaking one can get syntactically distinct formulas defining the isomorphism type of $\mathcal{A}$. So, logically equivalent formulas express the same propositional function. And, eventually the "abstract structure" of $\mathcal{A}$ is the propositional function expressed by the diagram formula $\Phi_{\mathcal{A}}(\vec{X})$. And I write $\hat{\Phi}_{\mathcal{A}}$ for this propositional function.
(Hope the latex works, as our preview here doesn't run the latex - if not, I may have to edit and redo the comment.)
Cheers,
Jeff
Jeff,
ReplyDeletethanks, that sounds all right. But I'm still a little skeptical as to whether it really provides an implementation of the SIP: Is the proposal to talk not about $\mathcal{A}$ anymore, but about $\hat\Phi_{\mathcal{A}}$ instead? Is there a transparent translation of structural talk about $\mathcal{A}$ into talk about $\hat\Phi_{\mathcal{A}}$ that preserves all the meaningful statements about $\mathcal{A}$?
I also worry about getting the correct notion of equivalence for higher-categorical notions, for instance “category” itself: If $\mathcal{C}$ is a cateory, does $\hat\Phi_{\mathcal{C}}$ capture $\mathcal{C}$ up to equivalence of categories (that's what we want), or merely up to isomorphism?
Cheers,
Ulrik
Ulrik,
DeleteYes, we no longer talk about the models, but rather about their abstract structures instead. E.g., instead of talking about the von Neumann implementation, or the Zermelo implementation, we have the abstract structure itself (that both "have in common") instead. This abstract structure is the propositional function (in Frege's sense) expressed by the diagram formula. But because propositional functions are hard to deal with, it's easier to talk about the diagram formula, which expresses the propositional function (and defines the isomorphism type).
Is there a transparent translation of structural talk about $\mathcal{A}$ into talk about $\hat{\Phi}_{\mathcal{A}}$?
It's easier to deal with the diagram formula $\hat{\Phi}_{\mathcal{A}}(\vec{X})$. So, roughly, the translation is one that shows that, for a formula $\phi \in \mathcal{L}(\mathcal{A})$, then "$\phi$ is true in $\mathcal{A}$" is equivalent to "$\phi$'s is implied by the diagram formula $\hat{\Phi}_{\mathcal{A}}(\vec{X})$". I.e.,
$\mathcal{A} \models \phi$ iff $\hat{\Phi}_{\mathcal{A}}(\vec{X}) \vDash \phi$.
It's a bit easier to see how it works if one skolemizes the diagram formula to get $\hat{\Phi}^{sk}_{\mathcal{A}}(\vec{X})$.
(It then turns out that pairs of skolemizations of the formula induce permutations of the original carrier set $A$ of $\mathcal{A}$. These permutations are then automorphisms of $\mathcal{A}$ just when the skolemizations are logically equivalent. Intuitively, it's like labelling an unlabelled graph using two distinct labellings; the resulting labelled graphs are (literally) identical because of an automorphism of the graph.)
That said - perhaps the Leibniz Abstraction Principle is different, in some important conceptual sense, from the intent behind the Structure Identity Principle. What I'm doing is more like "quotienting" with respect to isomorphism of relational models. The abstract representative of an equivalence type of models isn't a model though, because the carrier set has been thrown away: on my view, they're propositional diagrams.
Cheers,
Jeff
Ulrik,
DeleteIf $\mathcal{C}$ is a cateory, does $\hat{\Phi}_{\mathcal{C}}$ capture $\mathcal{C}$ up to equivalence of categories (that's what we want), or merely up to isomorphism?
Yes, $\hat{\Phi}_{\mathcal{C}}$ only captures $\mathcal{C}$ up to isomorphism, not equivalence of categories.
I suspect that, given $\mathcal{C}$, there may be a way of defining this tighter notion "quasi-syntactically" too and then the result would be some kind of "equivalence structure" of $\mathcal{C}$. But to be honest, I'm not sure ...
Cheers,
Jeff