Type Theory for the Working Mathematical Music Theorist

TL;DR

This paper introduces a type-theoretic formalism for mathematical music theory that simplifies complex categorical expressions, making reasoning about musical structures more intuitive and constructive.

Contribution

It presents a novel type-theoretic language that integrates categorical semantics, enhancing conceptual clarity and reasoning capabilities in mathematical music theory.

Findings

Enables intuitive expression of musical structures

Supports constructive reasoning with propositions and proofs

Facilitates new applications like voice-leading spaces

Abstract

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.