tag:blogger.com,1999:blog-4987609114415205593.post8715843111148192686..comments2024-03-28T13:40:26.497+00:00Comments on M-Phi: Leibniz Abstraction, Structure Identity and UnivalenceJeffrey Ketlandhttp://www.blogger.com/profile/01753975411670884721noreply@blogger.comBlogger7125tag:blogger.com,1999:blog-4987609114415205593.post-37819740567519421312013-06-24T17:11:57.951+01:002013-06-24T17:11:57.951+01:00Ulrik,
If $\mathcal{C}$ is a cateory, does $\hat{...Ulrik,<br /><br /><i>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?</i><br /><br />Yes, $\hat{\Phi}_{\mathcal{C}}$ only captures $\mathcal{C}$ up to isomorphism, not equivalence of categories. <br /><br />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 ...<br /><br />Cheers,<br /><br />JeffJeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-91826514206415393322013-06-23T16:45:35.435+01:002013-06-23T16:45:35.435+01:00Ulrik,
Yes, we no longer talk about the models, b...Ulrik,<br /><br />Yes, 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).<br /><br /><i>Is there a transparent translation of structural talk about $\mathcal{A}$ into talk about $\hat{\Phi}_{\mathcal{A}}$?</i><br /><br />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.,<br /><br />$\mathcal{A} \models \phi$ iff $\hat{\Phi}_{\mathcal{A}}(\vec{X}) \vDash \phi$.<br /><br />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})$. <br /><br />(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.)<br /><br />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.<br /><br />Cheers,<br /><br />JeffJeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-30067567696084392922013-06-23T03:19:11.168+01:002013-06-23T03:19:11.168+01:00Jeff,
thanks, that sounds all right. But I'm ...Jeff,<br /><br />thanks, 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}$?<br /><br />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?<br /><br />Cheers,<br />UlrikUlrik Buchholtzhttps://www.blogger.com/profile/10982601109033031728noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-41123637192497230762013-06-22T18:04:39.983+01:002013-06-22T18:04:39.983+01:00Ulrik,
Yes, the construction of the diagram langu...Ulrik,<br /><br />Yes, 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$.)<br /><br />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}$.<br /><br />(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). <br /><br />Then, we can prove a categoricity result, which lets us transfer between isomorphic models. But the only properties which are transferred are purely "structural".<br /><br />Does that sound ok? What I'm doing is coming from model theory, rather than category theory though.<br /><br />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.<br /><br />(Hope the latex works, as our preview here doesn't run the latex - if not, I may have to edit and redo the comment.)<br /><br />Cheers,<br /><br />JeffJeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-69731182112932645132013-06-22T17:17:39.704+01:002013-06-22T17:17:39.704+01:00Jeff,
well, the point of HTT is that in fact $A$ ...Jeff,<br /><br />well, 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!<br /><br />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?<br /><br />Cheers,<br />UlrikUlrik Buchholtzhttps://www.blogger.com/profile/10982601109033031728noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-23874985807868709452013-06-22T05:08:18.833+01:002013-06-22T05:08:18.833+01:00Ulrik,
Oh thanks - I guessed you must be the same...Ulrik,<br /><br />Oh thanks - I guessed you must be the same Ulrik! <br /><br />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. <br /><br />On the diagram construction, we get a map $A \mapsto \hat{Phi}_{A}$ such that the Leibniz abstraction principle,<br /><br />$\hat{\Phi}_{A} = \hat{\Phi}_B$ iff $A \cong B$.<br /><br />holds. <br /><br />(And I think that's very close to what you mean by Structure Identity Principle ...)<br /><br />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.<br /><br />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.<br /><br />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. <br /><br />Cheers,<br /><br />JeffJeffrey Ketlandhttps://www.blogger.com/profile/01753975411670884721noreply@blogger.comtag:blogger.com,1999:blog-4987609114415205593.post-12281730752124870532013-06-22T04:00:39.891+01:002013-06-22T04:00:39.891+01:00Hi Jeff,
thanks for the mention of my talk! I don...Hi Jeff,<br /><br />thanks 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?<br /><br />Cheers,<br />UlrikUlrik Buchholtzhttps://www.blogger.com/profile/10982601109033031728noreply@blogger.com