Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
After discussion here I have changed the organization of the entry structure and then expanded a bit by adding an Idea-section and a bit more here and there.
(The previous organization of the entry instead made it look like structure in model theory is a concept on par with that discussed at stuff, structure, property. But instead, the latter axiomatizes the general notion of “structure on something” as such, whereas the former is an example of a structure on something (namely an “-structure on a set”). The new version aims to reflect this properly.)
Ah, I see our confusion. It is true that “structure” in the sense of SSP is an “abstract general”, whereas a structure in the sense of model theory is a “concrete particular”. But, in model theory an L-structure is not the thing you put on a set; the L-structure is the set together with the structure (in the SSP sense) that got put on it.
I’ve tried to clarify this at structure.
Thanks. I see.
Hm, on the other hand, is this difference really one beyond the form of the English words which we use in the two cases?
Is the functor from the category of -structures to their underlying sets not faithful?
Yes, it is faithful. It’s just a question of how the language is used.
Okay, thanks for confirming.
But then I am back to thinking that structure in model theory should be regarded as a special case of the general notion of structure. The difference in just the choice of English words “-structure” or “set with -structure” I find not important enough to make us obfuscate the relation of the concepts here, which is independent of their English pronounciation.
I have allowed myself to slightly edit the page once more in order to reflect this. I hope you can see what I am trying to get at.
But if you’d ask me, I’d entirely restructure the page as I suggested earlier: I would move the discussion of structures in model theory to a subsection of the Examples-section. I think that would make the situation much clearer. Let me know if you’d object to that.
I am against restructuring the page, because someone coming to the page structure from nowhere might be starting by assuming either of the patterns of English usage. We should therefore make explicit up front that there are two different linguistic usages of the word “structure”, to avoid confusion, even if one of the usages denotes mathematically a special case of the other.
I do not understand this quote in structure:
In this case one defines a “language” or theory L that describes the operations and properties with which we want to equip sets
Language should be clearly distinct from a theory. Structure in model theory is equipped with operations, relations and constants, but one does not test properties. Properties are tested for a model of a theory, and they are expressed by sentences.
Urs said that one always says -structure. Well, you also say “a structure of a group” when you mean structure of a group. So I do not know how fundamental for that particular discussion is that they need to consider a particular as different from other usages.
I also think that “structure in logic and model theory” should have “logic” dropped out.
Yes, I definitely think it is misleading:
Thus the category theorist would refer to “the structure of a group” as consisting of a multiplication, a unit, etc., while the model theorist would say that each particular group (like ℤ) is a “structure (or model) for the language (or theory) of groups.”)
Structures for a language of groups may not be models, of course. For example, you can have a nonassociative magma with unit and two sided inverses. It is a structure for the language of groups but not a model for the theory of groups. This is just the standard terminology.
I made some changes.
Thanks, Zoran. I made a few more changes, mostly some slight rearranging and fixing some minor linguistic errors.
Thanks, I like your improvements (as usual) at structure.
I tried to clarify a bit further. The reason I wrote what I did was because I wanted to focus on the difference between the word “structure” in category theory referring to the abstract data (roughly, what the model theorist calls the language and theory), versus to the specific model of the theory in model theory. I feel like the current paragraph is confusing because it’s trying to draw two different distinctions at once: the one I intended, and also the one between properties being subsumed by structure but a structure not being necessarily a model. However, I don’t really know how to improve it.
Right, Mike, I understand, the deductive urge is here not congruent with the terminological conventions and subtleties. Thank you for your improvements.
I tried to take up the distinctions made by Mike in #14 and put them in separate remarks within a structured environment. Feel free to fiddle some more with the formulations.
Looks good!
I am starting a section “In dependent type theory” (here).
So far the section consists (only) of two examples: (1.) “lens structure” on a data base type and (2.) “group structure”.
(and a brief reference to the structure identity principle).
added references discussing mathematical structures via dependent type theory:
in Coq:
Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg, A Constructive Algebraic Hierarchy in Coq, Journal of Symbolic Computation 34 4 (2002) 271-286 [doi:10.1006/jsco.2002.0552, pdf]
Claudio Sacerdoti Coen, Enrico Tassi, Working with Mathematical Structures in Type Theory, in: Types for Proofs and Programs. TYPES 2007, Lecture Notes in Computer Science 4941 Springer (2008) [doi:10.1007/978-3-540-68103-8_11, pdf]
François Garillot, Georges Gonthier, Assia Mahboubi & Laurence Rideau, Packaging Mathematical Structures, in: Theorem Proving in Higher Order Logics. TPHOLs 2009, Lecture Notes in Computer Science 5674, Springer (2009) [doi:10.1007/978-3-642-03359-9_23]
Bas Spitters, Eelis van der Wegen Type classes for mathematics in type theory, Mathematical Structures in Computer Science 21 4 “Interactive Theorem Proving and the Formalisation of Mathematics” (2011) 795-825 [doi:10.1017/S0960129511000119]
Kazuhiko Sakaguchi, Validating Mathematical Structures, in Automated Reasoning. IJCAR 2020, Lecture Notes in Computer Science 12167, Springer (2020) [doi:10.1007/978-3-030-51054-1_8]
in Lean:
added pointer to:
Jeffery Zucker, Formalization of Classical Mathematics in Automath, Colloques Internationaux du Centre National de la Recherche Scientifique 249 (1975) 135-145 [web, pdf]
also in: Studies in Logic and the Foundations of Mathematics 133 (1994) 127-139 [doi:10.1016/S0049-237X(08)70202-7]
Nicolaas de Bruijn, Telescopic mappings in typed lambda calculus, Information and Computation 91 2 (1991) 189-204 [doi:10.1016/0890-5401(91)90066-B]
It seems that discussion between these two authors in the early 1970s is the origin of the understanding of expressing mathematical structures via iterated dependent pair types (“telescopes”).
added pointer to:
Leo Corry, Mathematical Structures from Hilbert to Bourbaki: The Evolution of an Image of Mathematics, in: Changing Images of Mathematics in History. From the French Revolution to the new Millenium Harwood Academic Publishers (2001) 167-186 [ISBN:9780415868273, pdf]
Leo Corry, Modern Algebra and the Rise of Mathematical Structures, Springer (2004) [doi:10.1007/978-3-0348-7917-0]
expanded out these references (previously only hinted at):
Charles Ehresmann, Gattungen in Lokalen Strukturen, Jahresbericht der Deutschen Mathematiker-Vereinigung 60 (1958) 49-77 [dml:146434]
Charles Ehresmann, Catégories et Structures, Séminaire Ehresmann. Topologie et géométrie différentielle 6 (1964) 1-31 [numdam:SE_1964__6__A8_0, dml:112200]
and added comment on what they are actually about (early proposal to grasp the notion of mathematical structures via category theory – specifically via forgetful functors between groupoids)
also deleted the similarly incomplete reference to a textbook on algebraic theories and instead added a general pointer:
For modern accounts on mathematical structures via categorical algebra see also at algebraic theory, monad, sketch.
added pointer to:
now starting a new section with examples of “higher strcutures”: here.
So far just one example (delooping of pointed types)
From the perspective of HOTT where laws are definitional, e.g., identity of pairs and pairs of identities (slide 3 and 13 of Mike’s slides) and this goes for dependent pair and function too (slide 40), what does one say about the structure identity principle? Won’t definitional univalence lead to structural definitional equality?
You are probably asking about the paragraph on the structure identity principle: here.
Ok, let’s shift to the right thread.
I am wondering which authors would admit that, thereby, “mathematical structure” and “data structure” becomes essentially synonymous (at least trilogous), along the same line by which “type” is ultimately nothing but a shorthand for “data type”. Evident as this may/should be, Google doesn’t known many such authors (do you?). So far it found a single one for me, just recently:
who writes in passing:
An example of a use case for non-binary sum types is the definition of mathematical “data structures” like a ring or a group. These data structures are usually defined as…
In fact, I would go further and suggest that the term “carrier type” often used in type-theoretic discussions of mathematical structure should be recognized for what it is: the base data type of a data structure, hence the underlying “data base”. This way, everything falls into place, terminologically.
1 to 33 of 33