Theorem in C

1. Introduction

A Hilbert-style proof is a finite sequence of formulas, each of which is either an axiom or follows from two earlier entries by modus ponens; a piece of music is a finite sequence of pitches. Both are, in the end, strings over a small alphabet, and it is natural to ask whether the dictionary between the two can be chosen so carefully that a proof checker runs directly on the pitches, with the composition standing or falling as a derivation. The purpose of this note is to record such a construction, together with a short two-voice piece, Theorem in C, which as far as I am aware is the first composition whose correctness is decided by a proof checker. The piece and its checker are embedded as Figure 1 below; the reader is invited to play it, and then to attempt to falsify it, by selecting any note and hearing what becomes of the derivation.

The main observations are as follows. First, if one works in prefix (Polish) notation, formulas require no parentheses, which is convenient, as parentheses are inaudible.¹ Secondly, the temporal structure of counterpoint supplies exactly the well-foundedness that a proof requires: if an application of modus ponens may only cite phrases that have finished sounding before it begins, then the citations are forced to respect the order of time, and soundness follows by induction along the score (Proposition 2.5). Thirdly — and this was the pleasant surprise — the theorem proved by the piece, α→α, is spelled by the melody G, C, C: a fall from the dominant degree to the tonic. The proof ends on a cadence because the theorem does.

2. The calculus

Definition 2.1 (Alphabet). Pitch classes are read as symbols by the table G ↦ →, C ↦ α, E ↦ β, A ↦ γ, D ↦ δ. Octave, duration and dynamics are ignored by the lexer. Any other pitch class is a lexical error.

Remark 2.2. The five legal pitch classes are precisely the C major pentatonic scale: the logic is pentatonic. The two white keys excluded, F and B, are precisely the pair of white keys a tritone apart.²

Definition 2.3 (Phrases). A phrase is a maximal run of notes between rests. A phrase is well-formed if the string it spells, read in prefix notation with → of arity two, is a formula of the implicational fragment over the atoms α, β, γ, δ. We write → right-associatively, so that α→α→α abbreviates α→(α→α).

Definition 2.4 (Admissibility). A roll is a finite set of phrases, distributed among voices, each occupying an interval of time. A roll is admissible if every phrase either is an instance of K: A→B→A, or of S: (A→B→C)→(A→B)→A→C, or has formula Y while some two phrases with formulas X and X→Y have both ended before it begins. Citations may cross voices freely.

Proposition 2.5 (Soundness). If a roll is admissible, the formula of every phrase — in particular of the last phrase to sound — is a theorem of the implicational fragment of minimal logic.

Proof. Induct on start time. A phrase justified by modus ponens cites only phrases that ended strictly earlier, so the citation graph is compatible with the order of time and has no cycles; the axiom cases are immediate.

Remark 2.6 (Completeness). Conversely, every theorem in at most four atoms can be scored: linearize any derivation and sing it in one voice, each phrase after its premises. The singable theorems are thus exactly the theorems of the fragment in at most four variables. A reader requiring more atoms will have to go chromatic, at some cost to the key signature.

3. The composition

The piece performs the standard derivation of the identity from K and S:

Voice I sings lines (1) through (5) in order. Voice II doubles lines (3) and (5) an octave lower; it states no axioms, and every phrase it sings is justified by modus ponens from phrases it has already heard. Imitation between voices, the basic device of contrapuntal writing, is here the reuse of a lemma; and Voice II cannot enter any earlier than it does, since at any earlier moment its premises have not yet sounded. The constraint that makes the counterpoint is the constraint that makes the proof.

Table 1. The checker’s ledger: seven phrases in order of entry, each with its formula and justification.

Remark 3.1. In the key of C, the pitch G is the dominant degree and C the tonic, so the final phrase α→α is sung G, C, C and closes the piece with a dominant-to-tonic fall — a perfect cadence, in the only sense available to a single voice. I record the coincidence without attempting to explain it: the shortest theorem of the system and the strongest close in tonal music happen to be transcriptions of one another.

4. Exercises and a question

Exercise 4.1. Show that no admissible phrase of fewer than three notes exists, and that every admissible three-note phrase proving a theorem is, up to choice of atom, the cadence of Figure 1.

Exercise 4.2. Score the composition of implications, (β→γ)→(α→β)→α→γ, and estimate the number of notes required by its shortest roll.

Question 4.3. In a fugue the answer restates the subject transposed to the dominant. Under the dictionary of Definition 2.1 transposition is meaningless: moving the subject up a fifth carries C to G, an atom onto the arrow, and out of the alphabet altogether. One would like an alphabet closed under transposition by a fifth, so that the answer becomes literally a substitution instance of the subject and parametricity becomes a contrapuntal device. I do not currently know a satisfactory way to arrange this.

Music has been written in the shape of proofs before; Emily Howard’s miniatures with Marcus du Sautoy [HowE] compose with proof-shaped procedures, and the general correspondence between proofs and constructions is of course classical [How80]. What appears to be new here is only the direction of the arrow: the music is not describing the proof; the proof is being run on the music.