# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeAug 27th 2012
• (edited Aug 27th 2012)

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 “$L$-structure on a set”). The new version aims to reflect this properly.)

• CommentRowNumber2.
• CommentAuthorMike Shulman
• CommentTimeAug 28th 2012

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.

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeAug 28th 2012

I’ve tried to clarify this at structure.

• CommentRowNumber4.
• CommentAuthorUrs
• CommentTimeAug 28th 2012

Thanks. I see.

• CommentRowNumber5.
• CommentAuthorUrs
• CommentTimeAug 28th 2012

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 $L$-structures to their underlying sets not faithful?

• CommentRowNumber6.
• CommentAuthorMike Shulman
• CommentTimeAug 28th 2012

Yes, it is faithful. It’s just a question of how the language is used.

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeAug 28th 2012

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 “$X$-structure” or “set with $X$-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.

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeAug 28th 2012

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.

• CommentRowNumber9.
• CommentAuthorzskoda
• CommentTimeSep 10th 2012
• (edited Sep 10th 2012)

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 $L$-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 $L$ as different from other usages.

I also think that “structure in logic and model theory” should have “logic” dropped out.

• CommentRowNumber10.
• CommentAuthorzskoda
• CommentTimeSep 10th 2012
• (edited Sep 10th 2012)

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.

• CommentRowNumber11.
• CommentAuthorzskoda
• CommentTimeSep 10th 2012

• CommentRowNumber12.
• CommentAuthorTodd_Trimble
• CommentTimeSep 10th 2012

Thanks, Zoran. I made a few more changes, mostly some slight rearranging and fixing some minor linguistic errors.

• CommentRowNumber13.
• CommentAuthorzskoda
• CommentTimeSep 10th 2012
• (edited Sep 10th 2012)

Thanks, I like your improvements (as usual) at structure.

• CommentRowNumber14.
• CommentAuthorMike Shulman
• CommentTimeSep 10th 2012

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.

• CommentRowNumber15.
• CommentAuthorzskoda
• CommentTimeSep 10th 2012

Right, Mike, I understand, the deductive urge is here not congruent with the terminological conventions and subtleties. Thank you for your improvements.

• CommentRowNumber16.
• CommentAuthorTodd_Trimble
• CommentTimeSep 10th 2012

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.

• CommentRowNumber17.
• CommentAuthorMike Shulman
• CommentTimeSep 10th 2012

Looks good!

• CommentRowNumber18.
• CommentAuthorUrs
• CommentTimeJan 21st 2023
• (edited Jan 21st 2023)

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).

• CommentRowNumber19.
• CommentAuthorUrs
• CommentTimeJan 25th 2023
• (edited Jan 25th 2023)

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:

• The mathlib Community, §4 in: The Lean mathematical library, in CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (2020) 367–381 [arXiv:1910.09336, doi:10.1145/3372885.3373824]
• CommentRowNumber20.
• CommentAuthorUrs
• CommentTimeJan 26th 2023
• (edited Jan 26th 2023)

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”).

• CommentRowNumber21.
• CommentAuthorUrs
• CommentTimeJan 26th 2023

• 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]

• CommentRowNumber22.
• CommentAuthorUrs
• CommentTimeJan 26th 2023
• (edited Jan 26th 2023)

expanded out these references (previously only hinted at):

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:

• CommentRowNumber23.
• CommentAuthorUrs
• CommentTimeJan 26th 2023

• CommentRowNumber24.
• CommentAuthorUrs
• CommentTimeJan 27th 2023

have added also the data telescope of vector space structure: here

• CommentRowNumber25.
• CommentAuthorUrs
• CommentTimeJan 29th 2023

added the example of ring structure (here)

• CommentRowNumber26.
• CommentAuthorUrs
• CommentTimeJan 29th 2023
• (edited Jan 29th 2023)

replaced the example of vector space structure with module structure (here)

• CommentRowNumber27.
• CommentAuthorUrs
• CommentTimeJan 31st 2023

now starting a new section with examples of “higher strcutures”: here.

So far just one example (delooping of pointed types)

• CommentRowNumber28.
• CommentAuthorDavid_Corfield
• CommentTimeJan 31st 2023

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?

• CommentRowNumber29.
• CommentAuthorUrs
• CommentTimeJan 31st 2023

You are probably asking about the paragraph on the structure identity principle: here.

• CommentRowNumber30.
• CommentAuthorDavid_Corfield
• CommentTimeJan 31st 2023

Ok, let’s shift to the right thread.

• CommentRowNumber31.
• CommentAuthorUrs
• CommentTimeFeb 1st 2023

added also the example of “subgroup structure”: here

• CommentRowNumber32.
• CommentAuthorUrs
• CommentTimeFeb 4th 2023
• (edited Feb 4th 2023)

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.

• CommentRowNumber33.
• CommentAuthorUrs
• CommentTimeFeb 20th 2023

added also the example of group action structure and its specialization to torsors (here)