1 Introduction

A mathematical proof is typically characterized as a sequence of mathematical assertions—declarative mathematical statements about mathematical objects and their properties. In this characterization, a proof of a theorem begins with assumptions and other accepted assertions, new assertions are deduced from previous assertions, and ultimately the theorem statement is reached. Because truth flowed from the assumptions and accepted assertions to the theorem statement via deductive reasoning, a reader of the proof can be assured that the theorem must be true, at least if the assumptions were true.

In several recent papers, Fenner Tanswell (in press; Tanswell & Inglis, in press) has demonstrated that in mathematical practice, many accepted proofs deviate from the description above in an interesting way. Many sentences in proofs are imperatives. Readers are told to suppose certain assumptions are true, pick objects that satisfy certain properties, draw auxiliary lines, extend orders, color graphs, and divide intervals. Tanswell was not the first to observe the frequent use of imperatives in proofs (see, e.g., Ernest, 1998, 2018; Pimm, 1987; Morgan, 1996; Rotman, 1988, 1993), but Tanswell (in press) argued that the epistemic consequences of the use of imperatives in proofs had yet to be explored. In this paper, I consider the use of instructions in mathematical proofs where the reader is directed to take a mathematical action. Instructions include imperatives, but also some sentences in which the impersonal “we” is used as the subject.

The aim of this paper is to deepen our understanding of how instructions are used in proofs as they appear in mathematical practice. The first goal of this paper is first to present a typology of the different types of instructions that appear in proofs. The second goal of the paper is to describe how different types of instructions are coordinated in construction proofs to metaphorically build objects with desirable properties. I accomplish this by analyzing the proofs that appear in Kunen’s (1980) canonical graduate textbook on set theory. Finally, I will speculate on the cognitive actions that a reader is expected to take as she reads the instructions that appear in a proof.

2 Instructions in proofs

2.1 The use of instructions in mathematical proof

In this paper, I consider instructions in mathematical proofs. Instructions typically come in two forms. The first is in the form of an imperative. For instance, a proof in Rudin’s (1970) widely used textbook in real analysis contains the following text: “Let I be an ideal of A. Partially order the collection P of all ideals which contain I (by set inclusion)” (p. 357, italics are my emphasis). Here, the reader is directed to let I be an ideal and then told to partially order a set. Rotman (1988) noted the use of imperatives is common in mathematical writing, including in proofs:

“But proof in turn involves the idea of an argument, a narrative structure of sentences, and sentences can be in the imperative rather than the indicative. […] Mathematics is so permeated by instructions for actions to be carried out, orders, commands, injunctions to be obeyed — 'prove theorem T', 'subtract from y', 'drop a perpendicular from point P onto line L', 'count the elements of set S', 'reverse the arrows in diagram D', 'consider an arbitrary polygon with k sides', and similarly for the activities specified by the verbs 'add', 'multiply', 'exhibit', 'find', 'enumerate', 'show', 'compute', 'demonstrate', 'define', 'eliminate', 'list', 'draw’, 'complete', 'connect', 'assign', 'evaluate', 'integrate', 'specify', 'differentiate', 'adjoin', 'delete', 'iterate', `order', 'complete', 'calculate', 'construct’, etc. that mathematical texts seem at times to be little more than sequences of instructions written in an entirely operational, exhortatory language.” (p. 8).

Others, such as Ernest (2018), Morgan (1996), and Wagner (2009, 2010), have echoed Rotman’s sentiments. Morgan (1996) and Wagner (2009, 2010) have conducted in-depth semiotic analyses on the role of imperatives in reflecting agency in mathematical text; my work here will focus on how text is read, understood, and validated.

A second type of instruction in mathematical proofs are sentences with the impersonal “we” as a subject. For instance, instead of using an imperative directing the reader to partially order a set P, the text may say, “we partially order P”. Halmos (1970) claimed the “we” in such sentences refers to “the author and the reader” (p. 141). Krantz (1997) noted that “the custom in modern mathematics is to use the first person plural, or “we”. It stresses the participatory nature of the enterprise, and encourages the reader to push on.” (p. 33).Footnote 1

Using mathematics papers posted in the mathematical ArXiv, Tanswell and Inglis (in press) conducted a corpus analysis that investigated the use of instructions in mathematical proofs. They found that instructions were more common in proofs than in ordinary mathematical prose. Further, while some verbs such as “let” and “suppose” were especially common as mathematical instructions, there was also a wide variety of instructions that were used in the corpus.

2.2 The epistemic importance of instructions

Tanswell (in press) argued that imperatives pose a challenge to traditional accounts about proof. As I previously mentioned, a proof is traditionally viewed as a sequence of mathematical assertions, where the proof begins with assumptions or assertions that are taken to be true (e.g., axioms, definitions, previously proven results) and new assertions are deductive consequences of previous assertions. However, instructions have different truth semantics than assertions. Imperatives cannot be true or false, and they cannot be deductive consequences of prior assertions or instructions. For statements of the form “we X”, the truth of the statement is not in question. It is presumed that both the author and the reader will carry out the instruction. The concern is not whether “we X” is a true or false statement, but whether the instruction is possible to obey. The main point is that the traditional view that truth flows from the assumptions of the proof to the conclusion by logical deduction does not obviously relate to proofs that contain instructions. Instructions cannot be carriers for truth.

Tanswell (in press) argued that proofs are analogous to recipes. Recipes instruct the reader to engage in specific cooking activities to obtain a culinary goal. Proofs instruct the reader to perform proving activities to obtain the epistemic goal of establishing and believing a theorem. In this paper, I will argue that constructions in proofs are frequently used to establish sub-goals in proofs: the reader can believe that a particular type of object exists because the proof supplies a recipe for building such an object.

3 Instructions in Kunen’s set theory: an introduction to independence proofs

3.1 The rationale for using Kunen’s text

Philosophers of mathematical practice have long been interested in how the proofs that mathematicians actually produce deviate from formalist accounts of proving, and the epistemic consequences that this has for why mathematicians believe theorems (De Toffoli, 2021; De Toffoli & Giardino, 2014, 2016; Larvor, 2012; Rav, 1999, 2007; Tanswell, 2015). Traditionally, these philosophers have used two approaches to analyzing mathematical text. The first is a close reading, in which the philosopher performs a modern or historical case study, using a particular proof in a mathematical domain in which she is conversant to illustrate a particular idea. This approach affords a rich and contextualized account of a given proof. However, since mathematical practice is heterogeneous (Hanna & Larvor, 2020), there is the risk that what the author is analyzing is atypical and that she is exploring a phenomenon that rarely occurs in mathematical practice. An alternative approach is an automated linguistic corpus analysis in which statistical patterns on language usage are systematically analyzed over thousands or millions of mathematical papers (Mejía-Ramos et al., 2019).Footnote 2 Such analyses can indirectly document the frequency of a phenomenon occurring in mathematical texts.Footnote 3 However, as these analyses ignore mathematical context,Footnote 4 they can provide at best suggestive trends as to the nature of the phenomenon in question. In general, close readings and linguistic corpus analyses complement each other in providing a more robust picture of what is transpiring. Tanswell (in press) used close readings to develop his recipe model of instructions; Tanswell and Inglis (in press) performed a corpus analysis to document that instructions were indeed common in proofs in mathematical practice.

In this paper, I take an approach that lies between close reading and corpus analysis. I catalog every instruction that appears in Kunen’s (1980) Set theory: An introduction to independence proofs. There are three benefits to focusing on Kunen’s volume. First, as Kunen’s textbook is widely used and has been praised for the quality of its writing (e.g., Baumgartner, 1986), it is reasonable to assume that the proofs in Kunen’s volume meet accepted standards for rigor and exposition. Second, while one cannot presume that Kunen’s use of instructions generalizes to other mathematicians (even in the context of graduate textbooks in set theory),Footnote 5 Kunen’s textbook has been used to teach the subject to a generation of set theorists, meaning Kunen’s work is of historical importance that has likely influenced the subject.Footnote 6 Third, by exploring an introductory graduate textbook, real mathematics is being investigated, but this mathematics is still accessible to the author and hopefully many readers of this article. This allows for nuanced analysis based upon the mathematical content being discussed.

This approach has benefits over close readings of text. By exploring a larger volume, I can notice trends in instruction use across many proofs.Footnote 7 Automated corpus analyses have virtues that my approach does not. Automated corpus analyses are generalizable and replicable. My analysis is specific to Kunen’s text and involves subjectivity in classifying whether sentences are instructions or not. However, my approach has the benefits of increased validity and allows for the content-based and contextual considerations that lend themselves to deeper philosophical inquiry. Consequently, I contend that close readings, corpus analysis, and textbook analyses are complementary, with each having strengths that allow them to contribute to a robust understanding of mathematical practice.

3.2 Method

When analyzing Kunen’s text, I did not consider section headings, homework problems, appendices, or numbered assertions (usually axioms, definitions, theorems, lemmas, and corollaries). I broke the remaining text into two parts. Proof text was the text that appeared between the word “PROOF” and the square denoting the completion of the proof. Prose text was everything else, which included a mixture of surveys of the existing literature on a topic, philosophical commentary, informal descriptions of set theoretic ideas, and organizational prose about the numbered assertions.

I read through the textbook, noting every time an instruction was given. All imperatives were coded as instructions. Sentences of the form “We [VERB]” were coded as instructions if I believed the text was asking the reader to take a mathematical action. Not all “We [VERB]” sentences were coded as instructions. For instance, sentences beginning with “We show” and “We prove” were commonplace in proofs, but were almost always used as advanced organizers alerting the reader about what will occur in an argument that follows. Such interpretive judgments potentially reduce the reliability of the coding; another coder might wind up with a different list of instructions than I did. However, coding by hand in this way produced a more accurate list of instructions than could be done by, say, the type of automated corpus analysis that is popularly done (Mejía-Ramos et al., 2019; Tanswell & Inglis, in press).Footnote 8

3.3 Instruction use in Kunen’s volume

3.3.1 Overall use of instructions

There were 262 proofsFootnote 9 in Kunen’s volume. There were 876 instructions that appeared in these proofs. Overall, 196 proofs (75% of the proofs in the volume) contained at least one instruction. However, many of the proofs in Kunen’s volume were quite short. By restricting the analysis to the 151 proofs that were more than four lines long, 143 (95%) of these proofs contained at least one instruction.

The 13 most common instructions that occurred in proofs appear in Table 1. These 13 instructions account for 88% of the instructions that were present in proofs in Kunen’s volume. (The word “let” accounted for slightly more than one third of the instructions by itself). Nonetheless, there was considerable diversity in the instructions being used, with 54 different instructions appearing in proofs. In some cases, the instructions were specific to the content being discussed. For instance, one proof contains the instruction, “In all cases, start with M satisfying ZFC + GCH” and then proceeds to direct the reader to “For (c), force three times and construct M ⊂ N1 ⊂ N2 ⊂ N3” (Kunen, 1980, p. 216, throughout the next two sections, the italicized text is my emphasis on which verbs were instructions). Starting with models that satisfy the ZFC axioms (and sometimes satisfy other desirable properties as well) and then forcing over them to construct new models is obviously specific to set theory contexts. Other infrequent instructions were common colloquialisms on how one should go about performing verifications. In one proof, Kunen directs the reader “We now simply go down the list and, using only the axioms ZF−—P—Inf, check that the defining formulas are equivalent to D0 formulas” (p. 120).Footnote 10 While the types of checks are specific to logical contexts, the notion of going down a list and checking that something holds for each item on the list could be described in other contexts as well.

Table 1 The thirteen most common instructional verbs in Kunen’s volume
Full size table

3.3.2 Types of instructions used

To form a typology of instructions, I used an open coding schemeFootnote 11 to create five categories of instructions where the instructions in each category served a similar purpose within Kunen’s proofs. The five categories were inclusive instructions, exclusive instructions, inference instructions, observational instructions, and reference instructions. I elaborate on each below.

I am adapting inclusive instructions from Rotman’s inclusive imperatives, which are used for creating shared discourse by introducing shared referents, standards, notation, and nomenclature. Inclusive instructions were instructions that either established a convention or introduced a new mathematical object that was not defined in terms of previous objects that were mentioned in the proof. For instance, “For brevity, write pred(x) and cl(x) for pred (A, x, R) and cl (A, x, R), respectively” (p. 104) is an instance of the former and “Suppose B were an uncountable chain” (p. 84) is an instance of the latter. There were 232 inclusive instructions in Kunen’s proofs. The most common inclusive instruction verbs were assume (72 instances), let (62), fix (51), and suppose (24).

I am adapting exclusive instructions from Rotman’s exclusive imperatives, which take shared mathematical discourse for granted and operate within it. By exclusive instructions, I mean instructions that direct the reader to act on mathematical objects that have previously been introduced in the proof. Often, this involves defining a new object in terms of existing objects. As a basic example, to show that there is no upper bound on the cardinals (Theorem I.10.16), Kunen presents the following short proof: “Assume α > ω. Let W = {R ∈ ℘(α x α): R well-orders α}. Let S = {type(< α, R >): R ∈ W}. (S exists by replacement). Then sup(S) is a cardinal > α” (p. 30). The assume instruction was an inclusive instruction as it introduced an ordinal α. The two subsequent let instructions were exclusive instructions. R was defined in terms of α and S was defined in terms of R. It was also common for exclusive instructions to direct the reader to choose an object that had properties defined in terms of previous elements (e.g,. “Now, inductively pick x in B for each α < ω1 so that ht(xα, T) > sup{ht(f(xβ, T)): β < α}” (p. 81)). Less common were exclusive instructions that involved the transformation of a given object. An example is “We may assume the list ϕ1, ϕ2, …, ϕn, is subformula-closed; if the original list is not, we simply expand it to one that is” (p. 137). Here, Kunen is telling the reader to transform a list of formulas by lengthening it so that the list is subformula closed. There were 454 exclusive instructions in Kunen’s proofs. The most common exclusive instruction verbs were let (265 instances), fix (71), define (30), pick (18), and choose (10). However, there were a wide variety of exclusive imperatives that were used sporadically in the text. Readers were asked to add elements to a list, build iterated forcing constructions, force over models of ZFC, map one set to another, modify previous constructions, and well-order sets. Finally, it is worth noting that in Kunen’s proofs, defining was usually an exclusive instruction for creating an object that was used specifically for the purposes of that proof.

Inference instructions directed the reader to make a particular type of inference. In contrast to exclusive instructions, which acted on mathematical objects, inference instructions acted upon previous assertions in the proof to form new assertions. In some cases, the reader is asked to apply a previous fact to reach a desired conclusion. For instance, the entire proof of Lemma II.2.17 is “Apply Theorem 2.15 with B = C \ A” (p. 57). In other cases, the reader is asked to write a subproof. (e.g., “For (c), show by induction that ∪ n A ⊂ T” (p. 99–100)). There were 47 inference instructions in Kunen’s proofs. The most common inference instruction verbs were apply (16 instances) and show (10 instances).

Observational instructions directed the reader to notice a particular fact, often one that seems to be relatively straightforward. (e.g., “observe that by GCH, all weak inaccessibles are strong inaccessibles” (p. 177)). There were 53 observational instructions in Kunen’s proofs. The most common instructional verbs were note (26 instances) and observe (16). In general, Kunen seems to write as if the observational instructions were a matter of perception. In the cases where Kunen elaborated on an observational inference, he generally did so by starting with the phrase “to see this”. Reference instructions occurred when Kunen directed the reader to another part of the text, usually as a justification for why a particular step in a proof was permissible (e.g., “see Lemma 3.4” (p. 198)). There were 51 reference instructions in Kunen’s proofs, all of which used the verb see.

I conclude this section by noting that the same instructional verb can have different uses. The verb “let” is frequently used as inclusive instruction to assume a particular object exists and as an exclusive instruction to build a new object from ones that were previously introduced. Kunen employed the word “use” as an inclusive instruction to introduce notation (“we use the notation q||ta to abbreviate…” (p. 260)), an exclusive instruction (“Use the order < L on L(ω2) to define Skolem functions…” (p. 178)), and as an inferential instruction to explain how to write a sub-proof (“To see that in fact (2ω2 = ω7)N[H], use the method of Theorem 6.17” (p. 216). This highlights the utility of checking individual instructions, as context determines how individual instructional verbs are used.

3.3.3 Comparing proof text to non-proof prose

Instructions were about three times more frequent in Kunen’s proof text than his prose text. There were 874 instructions in 2,425 lines of proof text, for a ratio of 36.0 instructions per every 100 lines of proof text. In contrast, there were 517 instructions in 3875 lines of prose text, for a ratio of 13.3 instructions per every 100 lines of prose text. Table 2 presents the distribution of types of instructions in proof text and prose text.

Table 2 The number of instructions by type for proof text and prose text
Full size table

As Table 2 indicates, nearly half the instructions in the prose test were reference instructions, which often occurred when Kunen presented a survey of what was known about a particular topic. In these surveys, Kunen would reference both results from his textbook and the research literature. Another striking feature of Table 2 is the large difference in exclusive instructions in the proof text and the prose text. There were 454 exclusive instructions in Kunen’s proofs (for a ratio of 18.7 exclusive instructions for every 100 lines of proof text) and 46 exclusive instructions in the prose text (for a ratio of just 1.1 exclusive instructions for every 100 lines of prose text).

3.4 Summary

I highlight three findings from the analysis above. The first two echo points established in Tanswell and Inglis’ (in press) corpus analysis. First, instructions are common in Kunen’s proofs. Most of his proofs contain them. This implies that any account of how these proofs were written or should be understood would need to explain the role that instructions play. Second, there is a wide diversity of instructional verbs, especially for the exclusive instructions. This suggests that there probably is not a mechanistic account for how readers handle instructions when they arise in proofs, as it seems unlikely that readers share precise rules for dealing with so many different verbs. In particular, I argue against the possibility that reading instruction-based proofs simply involves the reader first translating the instructions into assertions. Finally, a particularly sharp difference between Kunen’s proof text and prose text is the frequency of exclusive instructions, which were a regular occurrence in proof text and a rare occurrence in prose text. The use of exclusive instructions is explored more in the next section.

4 How instructions are used to construct objects in proofs

4.1 Exclusive instructions in proof constructions

In the previous section, I have shown that a key difference between proof text and prose text in Kunen’s textbook was the prevalence of exclusive instructions. In contrast to the prose text, Kunen’s proofs frequently directed the reader to form new objects based on objects that were previously introduced in the proofs. In this section, I explore why exclusive instructions appear so often in Kunen’s proofs. I also illustrate how they are used in tandem with other types of instructions.

Many proofs in Kunen’s volume take the form of constructions, where Kunen establishes that a certain type of object exists by showing how the object can be built or constructed from other objects that are assumed to exist. This frequently occurred even when the lemmas or theorems being proven were not “for all, there exists” statements. For instance, a key theorem in Kunen’s volume is to show that the Continuum Hypothesis is consistent with the ZFC axioms.Footnote 12 To accomplish this, Kunen assumes that a model M of the ZFC axioms exists and then uses M to build a new model L in which the Continuum Hypothesis holds. Showing that a Suslin tree exists in the constructible universe L involved two constructions. Assuming a model L exists, the first construction shows how to build a diamond sequence in L. The second construction assumes there is a diamond sequence and shows how to use this diamond sequence to build a Suslin tree. The main point here is that many of Kunen’s proofs involve transforming the theorem statement into a “for all x, there exists y” statement, and then using a sequence of instructions that specify how to use x to build the object y.

I illustrate how constructions work by considering Kunen’s proof that for any partially ordered set P and any countable collection of dense subsets of P, there is a filter that intersects each of the dense subsets.Footnote 13 Kunen’s proof is numbered below to facilitate reference, but it is otherwise given verbatim. Again, the italicized instructions are my emphasis.

  1. [1]

    Let D = {Dn| n ∈ ω} and

  2. [2]

    define, by induction on n, pn in P so that p0 is an arbitrary element of P

  3. [3]

    (since P ≠ 0) and

  4. [4]

    pn+1 is any extension of pn such that pn+1 ∈ Dn;

  5. [5]

    this is possible since Dn is dense.

  6. [6]

    So p0 ≥ p1 ≥ p2 …

  7. [7]

    Let G be the filter generated by {pn| n ∈ ω} —i.e., G = {q ∈ P| ∃n (q ≥ pn)};

  8. [8]

    then G is a filter and for all n, (G ∩ Dn ≠  Ø).

    (p. 55)

This simple example illustrates a format that many of Kunen’s construction proofs followed. What Kunen shows is that for any countable collection of dense subsets of P, he can construct a filter that intersects all of these dense subsets. He begins with an inclusive instruction in [1], labeling the (arbitrarily chosen) countable collection of dense subsets D. In [2], [4], and [7], Kunen uses a sequence of exclusive instructions to describe how to build the desired filter G. Of course, not every exclusive instruction is permissible in a proof. Kunen justifies why [2] is possible to carry out in [3] and why [4] is possible to carry out in [5]. Finally, Kunen asserts properties that G has in [8], where [8] is (implicitly) justified by the process of constructing the filter and the observation in [6].

In this simple case, Kunen justifies that each instruction is possible to carry out in a single sentence. Further, the properties of the constructed filter G are simply asserted. As the proofs become more complicated in the volume, Kunen elaborates on why instructions can be implemented and why the resultant objects have the properties that he claims. In some cases, he uses a reference instruction to a prior lemma or theorem to justify why a step in the construction is possible. In others, he provides a sub-proof that a particular instruction is possible to carry out or that the constructed object has the desirable property that Kunen asserts of it. To illustrate a slightly more complicated proof, I present the start of Kunen’s proof that if any Suslin lines exist at all, then a nice well-behaved Suslin lineFootnote 14 exists:

  1. [1]

    Let Y be a Suslin line.

  2. [2]

    Define an equivalence relation ~ on Y by setting x ~ y iff the interval between them ((x, y) if x < y, or (y, x) if x > y) is separable.

  3. [3]

    Let X be the set of ~ -equivalence classes.

  4. [4]

    If I ∈ X, then I is convex; i.e., x, y ∈ I ∧ x < y → (x, y) ⊂ I).

  5. [5]

    We totally order X by setting I < J iff some (any) element of I is less than some (any) element of J.

  6. [6]

    Note that each I ∈ X is separable.

  7. [7]

    To see this, let M be a maximally disjoint collection of non-0 open intervals of the form (x, y) in I.(p. 67).

The proof continues by using M to build a countable dense subset of I.

Much like the previous proof, this one begins with an inclusive instruction, naming a Suslin line Y. Steps [2], [3], and [5] are exclusive instructions, using Y to construct a “nicer” Suslin line X. Line [6] contains an observational inference about the result of this process—that each I is separable. For the remainder of this paragraph, Kunen supposes the existence of an I in X (although in this case, no inclusive instruction explicitly posits this I) and, starting in [7], gives a series of instructions for building a countable dense subset of I.

In summary, in Kunen’s text, many proofs involve showing that sets or models with desirable properties exist (often modulo the assumption that other sets or models exist). Kunen establishes the existence of these sets or models by giving the reader a sequence of exclusive instructions that will construct or build these sets and models.

4.2 How should the reader understand exclusive instructions that appear in a proof?

According to the standard view of proof (Hamami, 2022), proofs are characterized as sequences of assertions. When reading a proof, if the reader encounters an assertion that is not part of her knowledge base, the reader must determine why that new assertion can be reached from previous assertions in the proof by applying her known rules of inference. Hence, as the reader encounters deductive steps that appear in a proof, she will engage in the cognitive activity of inferring (Hamami & Morris, 2021). Of course, when a mathematician develops or presents a proof, the deductive steps are not arbitrary, but are goal-directed. The deductive steps within a proof are chosen exactly because they help the author and the reader get closer to the goal state of proving the theorem. Part of understanding a proof involves understanding the rationality of the deductive steps, which Hamami and Morris (2023) argue consists of seeing how each step fits into part of a coherent plan to prove the theorem.

Proofs that contain exclusive instructions require an elaboration to Hamami and Morris’ characterization. As Tanswell (in press) noted, instructions have a different truth semantics that mathematical assertions. In contrast to assertions, instructions cannot be true or false, and an instruction cannot be a deductive consequence of previous assertions or instructions. This raises a question of what a reader is doing when she reads a construction-based proof and is asked to infer that the object that is built in the proof exists and has the properties that the proof claims it does.

As a specific example, consider line [6] in the first proof that is presented in this section—namely that the process described earlier in the proof will yield an infinite decreasing chain of elements in the partial order P. One possibility is that the reader would simply be expected to translate all instructions into mathematical assertions, and then use the accounts of Hamami and Morris (Hamami, 2022; Hamami & Morris, 2021, 2023) to understand the proof. I hypothesize that this is not usually done by a student or a mathematician who is reading this proof. Note that the proof makes implicit use of the Axiom of Choice,Footnote 15 which suggests that the reader of the proof translating the explicit instructions to assertions would need to specify the properties of a choice function at the outset of the proof. While Kunen’s volume does provide the reader with the resources to carry out such a translation,Footnote 16 I hypothesize that readers would not ordinarily do so. What I speculate instead is that the reader would reason that if one continually chooses elements of a partially ordered set that are less than the previously chosen one with respect to the order, one will obviously obtain an infinite decreasing chain of elements. It is the Axiom of Choice that allows one to continually “choose” infinitely (or in some other proofs, transfinitely) many elements. There is evidence that Kunen himself did not expect all of his readers to formalize his arguments,Footnote 17 and Kunen would occasionally argue that unproveable statements were “Platonically true” by describing procedures for building objects, even when the procedure could not be formalized within ZFC.Footnote 18 However, a discussion of these metamathematical issues is beyond the scope of this paper. How students and mathematicians would actually read the proofs in Kunen’s volume is an empirical matter that would need to be investigated in a psychological study.

If my speculation in the previous paragraph is correct, then I suggest that De Toffoli and Giardino’s (2014) enhanced manipulative imagination may provide a good account of how exclusive instructions and Kunen’s construction proofs can be understood and validated by the reader. De Toffoli and Giardino illustrated how in proofs in low dimensional topology, some claims are warranted by asking the reader to imagine the outcome of manipulating a manifold in a prescribed way. Mathematicians’ ability to do this is based on their kinesthetic experience in the real world and enhanced by one’s experience working in topology. I suggest that in Kunen’s texts (and in other mathematical domains as well, see Weber, 2022), some claims are justified by asking the reader to imagine the outcomes of engaging in set theoretic constructions. The reader is asked to believe the set theoretic construction is possible because the reader can see how she could execute every exclusive instruction in the process. The reader will accept some claims about the objects that are produced because the reader can anticipate the outcome of executing explicit instructions.

Finally, just as the deductive steps in a proof are not arbitrary or planned, the same is true of exclusive instructions. Kunen’s proofs do not ask the reader to take arbitrary mathematical actions. Rather each exclusive instruction is part of a coherent plan to build a mathematical object with certain mathematical properties. Part of seeing the rationality of Kunen’s proofs and understanding them at a deep level involves understanding how each of Kunen’s exclusive instructions fit within that plan: How does each exclusive instruction in a construction guarantee that the final resultant object will have a desirable property, or how does that exclusive instruction ensure that it is possible for future exclusive instructions to be carried out?

5 Discussion

5.1 Summary of contributions

The aim of this paper was to build on Tanswell’s work on imperatives (Tanswell, in press; Tanswell & Inglis, in press) by providing a more detailed account of how instructions were used in proofs. I did so by conducting a systematic analysis of the instructions used in Kunen’s (1980) canonical graduate set theory textbook. I presented a typology of five different ways that instructions were used in proofs. I corroborated Tanswell and Inglis’ (in press) results that instructions were common in proofs and a wide variety of instructions were used. I further observed that a key feature distinguishes proof text from ordinary mathematical prose in Kunen’s volume is the use of exclusive instructions—i.e., commands to transform objects or build new objects from other objects that appeared earlier in the proof. Finally, I illustrated how Kunen frequently used sequences of exclusive instructions to construct new objects with desirable properties.

5.2 Implications for the analysis of mathematicians’ written proofs

As noted earlier in the paper, in the philosophy of mathematical practice, mathematical text is usually analyzed by close reading (e.g., Tanswell, in press) or via an automated corpus analysis (e.g., Mejía-Ramos et al., 2019). The approach in this paper differed, in that I individually cataloged each of the instructions that appeared in Kunen’s volume. In this paper, I highlighted several virtues of this approach. For instance, the typology that was produced was developed by identifying trends across a large corpus of text and hence would be difficult to develop from the close reading of a single proof. Further, the typology was developed by considering mathematical context. For instance, the word “use” played the role of an inclusive instruction, an exclusive instruction, and an inference instruction at different points in Kunen’s volume. For this reason, an automated corpus analysis would not yield this type of topology.

The weakness of this methodology of this paper is that the analysis was completely grounded in Kunen’s textbook, so the extent that these findings are specific to Kunen’s writing style or generalize to mathematical disciplines beyond set theory is unclear (although this is also a weakness of close readings as well). Given that Kunen’s textbook is respected and a widely used resource in graduate courses in axiomatic set theory, it is reasonable to say that Kunen’s style of writing analyzed in this paper is an acceptable way of writing proofs in mathematical practice, but more work is needed to see if the phenomena that I identified are common in mathematical practice.

The analysis in this paper can be generative in the following respect. The typology proposed in this paper is a theoretical tool for other philosophers of mathematical practice who analyze mathematicians’ written proofs. The trends I identified in this paper can be viewed as hypotheses that can be empirically tested. Are exclusive instructions much more common in proof than in expository text in general? Does this trend hold in disciplines other than set theory (or even with other set theorists’ writings other than Kunen’s)? Does this trend hold in research papers or is it specific to textbooks? Similar questions can be asked about the other phenomena described in this paper, such as whether construction proofs often contain sequences of exclusive instructions.

5.3 Implications and future research in the philosophy of mathematical practice

The analysis in this paper can inform future research in two research programs in the philosophy of mathematical practice. First, many philosophers of mathematical practice have analyzed the ways in which the proofs that mathematicians actually write differ from formal accounts of proving, and the epistemic consequences that this has for how mathematicians understand proofs and why mathematicians believe theorems (e.g., De Toffoli, 2021; Larvor, 2012; Rav, 1999, 2007; Tanswell, 2015). For instance, De Toffoli and Giardino (2014, 2016) suggested that proofs in knot theory and low dimensional topology frequently ask the reader to mentally manipulate knots and manifolds which are represented as diagrams. From this observation and their own experience as mathematicians, De Toffoli and Giardino suggested that in topological practice, mathematicians use enhanced manipulative imagination to understand and verify these proofs. I suggest that when reading Kunen’s textbook, students may also use enhanced manipulative imagination to understand and verify proofs containing exclusive instructions. I further speculated that enhanced manipulative imagination may generalize beyond performing physical manipulations of three dimensional objects to building sets and models in set theory. Here I suggest that enhanced manipulative imagination may help us to understand construction proofs in other areas of mathematics as well. In my own prior work, I have argued that enhanced manipulative imagination can be used to understand proofs in real analysis textbooks (Weber & Tanswell, 2022) and research papers in computability (Weber, 2022). Psychological studies can verify the extent to which mathematicians actually use enhanced manipulative imagination to understand proofs; philosophers of mathematical practice can explore the extent that enhanced manipulative imagination can (or cannot) account for how proofs are understood in other areas of mathematics.

A second related research program in mathematical practice is exploring how proof in contemporary mathematics is not a homogenous practice, but varies by community and discipline (e.g., Larvor, 2012; Rav, 2007). Larvor (2012), for instance, is interested in inferential actions that are valid or common in some mathematical areas, but not others. Looking at the instructions that are used in these proofs provides one lens for seeing how proofs vary by practice. For instance, De Toffoli and Giardino (2016) have shown how some proofs in knot theory and low dimensional topology ask participants to manipulate manifold and knots by actions such as drilling holes in the manifolds or throwing a portion of a knot over one’s shoulder. Some real analysis proofs ask participants to continually break intervals in half and carefully choose elements of a sequence (e.g., Weber & Tanswell, 2022). It is likely the case that the types of instructions that appear in a proof are dependent upon the types of mathematical objects being studied.