Type Theory for the Working Mathematical Music Theorist
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912747985305600 |
|---|---|
| author | Flieder, Drew |
| author_facet | Flieder, Drew |
| contents | Many formal languages of contemporary mathematical music theory -- particularly those employing category theory -- are powerful but cumbersome: ideas that are conceptually simple frequently require expression through elaborate categorical constructions such as functor categories. This paper proposes a remedy in the form of a type-theoretic symbolic language that enables mathematical music theorists to build and reason about musical structures more intuitively, without relinquishing the rigor of their categorical foundations. Type theory provides a syntax in which elements, functions, and relations can be expressed in simple terms, while categorical semantics supplies their mathemusical interpretation. Within this system, reasoning itself becomes constructive: propositions and proofs are treated as objects, yielding a framework in which the formation of structures and the reasoning about them take place within the same mathematical language. The result is a concise and flexible formalism that restores conceptual transparency to mathemusical thought and supports new applications, illustrated here through the theory of voice-leading spaces. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_04090 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Type Theory for the Working Mathematical Music Theorist Flieder, Drew Category Theory 03B38 (Primary), 18C40, 18C50, 18C10 (Secondary) Many formal languages of contemporary mathematical music theory -- particularly those employing category theory -- are powerful but cumbersome: ideas that are conceptually simple frequently require expression through elaborate categorical constructions such as functor categories. This paper proposes a remedy in the form of a type-theoretic symbolic language that enables mathematical music theorists to build and reason about musical structures more intuitively, without relinquishing the rigor of their categorical foundations. Type theory provides a syntax in which elements, functions, and relations can be expressed in simple terms, while categorical semantics supplies their mathemusical interpretation. Within this system, reasoning itself becomes constructive: propositions and proofs are treated as objects, yielding a framework in which the formation of structures and the reasoning about them take place within the same mathematical language. The result is a concise and flexible formalism that restores conceptual transparency to mathemusical thought and supports new applications, illustrated here through the theory of voice-leading spaces. |
| title | Type Theory for the Working Mathematical Music Theorist |
| topic | Category Theory 03B38 (Primary), 18C40, 18C50, 18C10 (Secondary) |
| url | https://arxiv.org/abs/2512.04090 |