Does Reason Evolve? (Does the Reasoning in Mathematics Evolve?)

Abstract

Hersh (1997) in a book aptly named What Is Mathematics Really? stresses the great distance he detects between the reality of professional mathematical practice—contemporary and historical—and the reasoning in formal languages that philosophers (since Frege) have largely characterized mathematical proof in terms of. Hersh criticizes the reasoning-in-formal-languages view of mathematical practice and mathematical proof as “isolated,” “timeless,” “ahistorical,” and indeed, even “inhuman.” Hersh (1997, xi) contrasts this derivation-centered view of mathematics (and mathematical proof) with an alternative view that takes mathematics to be a human activity and a social phenomenon, one which historically evolves and is intelligible only in a social context. His alternative view pointedly roots mathematical practice in the actual proofs that mathematicians create—actual proofs that Hersh claims philosophers of mathematics often ignore.

What Is Mathematics, Really? Two (Families of) Positions

Hersh (1997) in a book aptly named What Is Mathematics Really? stresses the great distance he detects between the reality of professional mathematical practice—contemporary and historical—and the reasoning in formal languages that philosophers (since Frege) have largely characterized mathematical proof in terms of. Hersh criticizes the reasoning-in-formal-languages view of mathematical practice and mathematical proof as “isolated,” “timeless,” “ahistorical,” and indeed, even “inhuman.” Hersh (1997, xi) contrasts this derivation-centered view of mathematics (and mathematical proof) with an alternative view that takes mathematics to be a human activity and a social phenomenon, one which historically evolves and is intelligible only in a social context. His alternative view pointedly roots mathematical practice in the actual proofs that mathematicians create—actual proofs that Hersh claims philosophers of mathematics often ignore.

I’ve just indicated two extreme positions (among a family of more moderate ones that are possible). Extreme positions offer clarity—so I’ll start by exploring the first one. Call it “the derivationist account.” The derivationist account characterizes strict derivations (in one or another artificial language, such as a first-order predicate one) as the only genuine proofs. Genuine proofs, that is, are sequences of formulas of an artificial language, each of which is either an axiom (drawn from a set of axioms characterizing a particular mathematical subject matter) or a formula that recognizably follows from ones earlier in the sequence by the application of one or more logical rules. If the nonlogical axioms and the rules of the background logic are recursive, then derivations are mechanically recognizable. The derivationist account takes the mechanical recognizability of derivations to explain one widely noticed peculiar quality of mathematical proof: professionals convince one another of the validity of their proofs (subject, of course, to the time limits of successful surveyability that the lengths of such items pose).¹

This means, notice, that the derivationist account takes formal derivations to play an epistemic role in mathematical practice. The existence of formal derivations explains an otherwise puzzling aspect of that practice: why mathematicians are so agreeable to one another—comparatively speaking. In order to explain this agreeableness of mathematicians, notice further that derivations can’t merely exist isolated somewhere or other in Platonic heaven. Mathematicians must actually have access to the pertinent properties of derivations in ways that are reflected in mathematical practice. In particular, that access must be evidentially relevant to their recognition of (for example) the validity of theorems in order for this explanation of mathematical agreement to fly.

Three important observations about the flexibility of the derivationist account. First, having “access to the pertinent properties of such derivations” doesn’t require those derivations to be Platonic objects or, indeed, to be realities of any sort. Derivations can be virtual objects—nonexistent projections of the (shared) cognitive faculties of mathematicians. According to this view of the ontology of derivations, we explain the mathematician’s grasp of validity in terms of psychological changes or sequences of thoughts (conscious or unconscious) that we code in terms of “manipulations” of those projections. So the phrase, “the existence of formal derivations explains …,” used above shouldn’t be understood to be ontologically committing. The derivationist account is compatible—pretty much—with any ontological position about mathematical objects: nominalistic denials of the existence of abstracta altogether, views (like Hersh’s) that take such objects to be historically evolving social entities of some sort or claims of the traditional Platonic sort. Ontology is largely irrelevant to the issues of this paper, so I’m going to sideline the topic here.²

Second, no assumption is needed that the mathematician has psychological access to the needed derivations in the sense that she can actually carry out transformations of informal rigorous proofs into their formal analogues or that she has an awareness of these transformations. The derivationist account can accommodate the fact that professional mathematicians are often unaware or ignorant of formal derivations, provided the practice of informal rigorous mathematical proof that mathematicians do engage in contains the tools for transforming such informal proofs into corresponding formal derivations. The idea is to treat the distance between formal derivations and real-world professional proofs as similar to the distance between the actual utterances of a natural language and the grammatical sentences posited in linguistics. Although in practice, and almost without exception, we speak in broken ungrammatical phrases (that are understood only because speakers and listeners share contexts of utterances), transformations of “what we’ve said” into impeccable grammatically correct sentences are possible, although they aren’t within reach of all speakers, and perhaps they’re only within reach of appropriately trained speakers.

On this version of the derivationist account, local context-specific criteria for validity all turn out to be various rules of thumb and other abbreviatory shortcuts (included is the common knowledge among specialists that specific kinds of proof procedures are widely used) that together indicate how informal rigorous proofs can be transformed into derivations. The derivationist account—so construed—allows that the same thing is true of grammatically impeccable sentences and formal derivations. The various local context-specific criteria that license ungrammatical (but acceptable) utterance fragments and the various local context-specific criteria that license informal rigorous mathematical proofs are both linked (respectively) to grammatical-impeccable sentences and to formal derivations in ways practitioners are barely conscious of.³

Third, the derivationist account can also handle the open-endedness of standard mathematical topics due to Gödel’s theorem—that, for example, the set of truths of the standard model of the natural numbers outstrips any (recursive) axiomatization of number theory. The derivationist account treats “number theory”—when studied by professional mathematicians over time—as individuated by an (open-ended) family of axiom systems which are conservative extensions of one another.⁴

Assuming that the appropriate access of mathematicians to derivations can be established (but acknowledging that this is an important promissory note—I discuss it further in sections 8 and 9), the widely recognized “objectivity” of mathematics can be explained by the nature of formal derivations. Given a set of axioms and a presumed background logic, the consequences of these axioms are matters purely of that logic. Apart from mistakes, there is no space for disagreement. Finally, formal derivations (and the mathematician’s access to them) are used to explain the long pedigree of many mathematical results: that they have eternal shelf lives. This isn’t merely a matter of robustness; rather, apart from mistakes, a mathematical result, once established, is a keeper.

I’ll describe how the derivationist account explains aspects of mathematical practice in terms that I’ll borrow from Tanswell (2015, 297-298): the derivationist account is taken to explain—at least in principle—what he calls, Rigor, Correctness, Agreement, Content, and Techniques. That is, the following properties are to be explained (at least in part) by the access of mathematicians to formal derivations: first, the standards of rigor of informal rigorous mathematical proofs; second, the correctness (and incorrectness) of such proofs; and third, that mathematicians largely agree upon perusing candidate informal rigorous informal proofs about whether they’re suitably rigorous and whether they’re correct. Next, the account must explain how the content of an informal proof determines which formal proof(s) it indicates, and (finally) that account must explain the role of informal techniques of proof that aren’t obvious transcriptions of formally licensed inference steps.

I wrote, “at least in part,” because the derivationist account can help itself to many of the properties that have been noticed about informal rigorous proofs by opponents of that account. For example, the tacit shared knowledge in a particular mathematical context (a particular branch of topology, say) might be crucial to seeing that an informal proof procedure is correct and to supplying a standard about what can be explicitly stated and what can be left tacit in proofs. And, what’s taken to be tacit shared knowledge (and therefore not worth bothering to articulate) can change over time for purely sociological reasons. But when the proof is appropriately filled out to explicitly include this context-dependent tacit material, it can be seen how the content of the (filled-out) proof determines which formal derivation(s) it indicates. The role of the informal techniques of proof in this specific area can also be explained as being abbreviations of certain sorts, or content-specific inference patterns which, again, when spelled out explicitly, make clear which formal derivation(s) are indicated.

Inference as Action; Objects of Inferential Actions

It’s been suggested more than once (e.g., in conversation with me—but in print as well) that the data of mathematical practice isn’t as I’ve described it in the last section. And so, Agreement (for example) isn’t an aspect of mathematical practice that needs explaining by any account, let alone the derivationist account. Not only have the standards of mathematical proof mutated over the ages (so it’s claimed), not only are proofs refined and developed over time as standards change, but there have even been heated disputes (by academic standards anyway) over appropriate proof methods. Take as an illustration the loud row between British and Continental mathematicians in the eighteenth century over the notation for the calculus, or for another example, the more recent debate between proponents of classical mathematics and their intuitionistic opponents.⁵ Furthermore, once it’s recognized how large a role diagrammatic reasoning plays in informal mathematical proof, it can look like over time methods of reasoning evolve in mathematics.

The italicized phrase of the last paragraph doesn’t explicitly occur in Larvor (2012), but the evolving-methods-of-reasoning-position itself does (and it’s something that’s believed by a number of philosophers of mathematics). Larvor argues that mathematical reasoning is best treated as “inference as action”; he argues further that such a position has significant consequences for our understanding of (informal) mathematical proof. He writes (723),

The benefit of viewing inference as action is that we can see how the subject-matter of informal arguments shapes and contributes to inferences. Indeed, instead of two highly abstract categories, the form of an argument and its content, we now have an indicative list of many and various concrete objects of inferential action (diagrams, models, expressions in special notations, experimental set-ups and so forth). This goes some way towards answering (or at least, making more precise) our question about which activities to count as mathematical practice. The cost is that we have to abandon the hope of establishing a general test for validity.

De Toffoli and Giardino (2014, 333), commenting on this passage in light of their previous discussion of Rolfsen’s picture proof (with words) of the equivalence of surgery codes and Heegaard diagrams of the Poincaré homology sphere, write:

In Rolfsen’s proof, we saw that among the permissible actions on the pictures are continuous transformations. These are part of the background material in the sense that any topologist knows immediately that these transformations can be interpreted in terms of homeomorphisms. The validity is thus based on the “practice”: it is the practice itself that integrates a way of controlling the actions on the representations used, which results in the establishment of local criteria for validity. The responsibility is shared among experts: since in low-dimensional topology different forms of reasoning are employed, some of which are specific to it, purely external criteria of validity cannot exhaust all the criteria actually adopted. As Brown suggests, we should acknowledge the existence of non-formal reasoning in mathematics: “first-order logic may be well understood, but what passes for acceptable proof in mathematics includes much more than that” (Brown 1999, p. 164). If this is true, then, as Larvor has exhaustively discussed, “the cost is that we have to abandon the hope of establishing a general test for validity.” (Larvor 2012, p. 723)

So (modulo certain differences among the thinkers here), a second position has emerged, one that starts from the assumption that inferences are actions; on this view, mathematics—mathematical proof, specifically—evolves. In contrast to the—once and for all—establishing of (a particular) logic as the backbone of all reasoning, or at least, of all reasoning in mathematics, the counterposition is that reason itself evolves. (At least it does in mathematics; but if it does in mathematics, then surely it does so everywhere else.) Reasoning itself, borrowing language from Hersh, is a social phenomenon which historically changes with the passage of time; and some of these changes can only be explained by sociological factors. This is part of what motivates Larvor’s twice quoted sentence, “the cost is that we have to abandon the hope of establishing a general test for validity.”

As it turns out, not only can the derivationist account handle a mathematical practice that involves localized context-dependent inference patterns, but it also isn’t incompatible with a position that takes mathematical practice to be one of “inferential actions” on “concrete objects of some sort,” as we’ve just seen Larvor put it.⁶ At least, it isn’t incompatible if we set aside ontological concerns about formal derivations. For called for, any proponent of the derivationist account will claim (one who’s inclined, anyway, to take seriously the actual facts of mathematical practice) is a distinction between the mathematician acting on “concrete objects of some sort” and the concrete objects themselves. According to proponents of the derivationist account, the mathematician acts by imaginatively moving from one step in a formal derivation to the next; similarly, in reasoning, on the views of opponents of the derivationist account, the mathematician also acts by imaginatively moving (say) from one stage of a diagram to a later one. (For example, a topologist may stretch the visual representation of one knot smoothly into the visual representation of another—see De Toffoli and Giardino (2014) for discussion of this.) Furthermore, even the phrase “concrete objects of some sort” can be understood to make no distinction between how proponents of the derivationist account view mathematical practice and how their opponents view it (at least in this respect). Even the most concrete of diagrams must be grouped into classes of semantically related items (e.g., token diagrams that belong to groups of token diagrams, all of which establish the same mathematical result in exactly the same way). Humans always engage with specific items, even if their thinking is characterized in terms of the grasping of formal derivations. That is, the specific psychological actions of mathematicians, when engaged in mathematical reasoning, although always directed toward particular concrete objects, are grouped together into relevant collections according to both views.⁷

Let’s turn, therefore, to the other aspect of informal proof that Larvor points to. He writes, recall, that, “instead of two highly abstract categories, the form of an argument and its content, we now have an indicative list of many and various concrete objects of inferential action (diagrams, models, expressions in special notations, experimental set-ups and so forth).”

This contrast between informal rigorous mathematics and formal derivations is stressed often, although philosophers and logicians who draw attention to it often disagree on its consequences.⁸ Rav (2007, 315), in particular, summarizing his discussion of several examples of informal rigorous mathematical proofs, writes, “I hold that mathematicians’ manner of reasoning and inferences are based on meanings and an informal notion of truth that a formal deduction calculus cannot capture” (italics his).

This too fails to track a genuine difference between informal rigorous mathematical proofs and formal derivations (and, specifically, the last clause quoted from Rav can be challenged). It’s true that informal rigorous proofs—diagrammatic proofs in particular—are composed of parts or involve actions (in Larvor’s sense) that are understood to represent mathematical objects or operations; it’s true that they are understood to have semantic contents. Dots on a page, the lines that are drawn, pencilled triangles (in Euclidean diagrams)—these represent points (without dimension), lines (without breadth), and the perfectly bounded triangles of Euclidean geometry. Similarly, continuous smooth deformations of diagrammatic shapes (drawings of doughnuts into drawings of cups, say) represent homeomorphisms among different geometrical shapes that are depicted in stages in topological diagrams (or continuously in computer graphics). In other diagrammatic proofs, contiguous squares represent sums of areas, boxed arrays of numbers represent operators on vector spaces, andsoon.

But formal derivations are the same in this respect, at least as far as their “meanings” are concerned.⁹ The formulas of a formal language are often given an intended semantics—an “intended model,” as it’s put. There is, for example, the well-known intended model of Dedekind-Peano arithmetic (the familiar counting numbers), and more generally, there are the various axiomatizations of any mathematical field that come with intended models—in particular, the mathematical subject areas that are axiomatized. Just as with informal rigorous mathematics (diagrams in particular), the well-formed formulas—“wffs” as they’re sometimes called—of artificial formal languages have syntactic “parts” that are understood to have semantic contents because of their relationships to the intended model (or, for that matter, because of their relationships to models). The quantifiers, standardly, are interpreted as “ranging over” the domain of a model, the constants in the language are taken refer to items in that domain, and the n-place predicates are taken to hold of subsets of the n-product of that domain. Equally importantly, rule-governed inferential movements from one formula to another—syntactically characterized (and therefore mechanically recognizable)—correspond to semantic relations of implication (defined in terms of the models of such formal languages, and not syntactically at all, although provably equivalent to syntactic characterizations in the case of some formal languages).

Although philosophers of mathematics are aware of these elementary points about formal languages, and the semantics such languages are standardly given, some of those philosophers still seem to think that there are important differences between formal and informal mathematical proofs, with respect to the phenomenon of meaning. Meaning is irrelevant to formal proofs, it’s often suggested. The fact that such proofs are “machine-checkable” means that validity can be recognized even if the device (or person) checking the proofs has no idea what the propositions of these proofs mean. Furthermore, at least in the first-order case, there are (the well-known) nonstandard models. Even with logics (say, higher-order logics) that have models that are isomorphic to one another (unlike the first-order case), the objects in the differing models of formal languages can be swapped for one another easily. (More generally, anything, e.g., apples, can be swapped for objects—say, some of the numbers—in any model of a higher-order logic.) It’s thought, therefore, that there is no intrinsic relationship in the case of formal languages between what the formal propositions are taken to mean and how they are shown to follow from one another; the meanings of these propositions (if any) are completely irrelevant to the process of derivation.

Informal rigorous mathematical proofs are seen as differing in just this respect. Rav (1999, 11) stresses this supposed distinction, even building it definitionally into his nomenclature:

Let us fix our terminology to understand by proof a conceptual proof of customary mathematical discourse, having an irreducible semantic content, and distinguish it from derivation, which is a syntactic object of some formal system. … [F]urthermore, given a finite sequence of formulas in a formal system, there is a purely mechanical way for ascertaining whether the given sequence satisfies the conditions of being a derivation in the system [italics his].

Rav adds (1999, p. 12), speaking of transformations of informal proofs into formal derivations:

Once we have crossed the Hibert Bridge into the land of meaningless symbols, we find ourselves on the shuffleboard of symbol manipulations, and as these symbols do not encode meanings, we cannot return via the Hilbert Bridge and restore meanings on the basis of a sequence of symbols representing formal derivations. After all, it is the very purpose of formalisation to squeeze out the sap of meanings in order not to blur focusing only on the logico-structural properties of proofs. Meanings are now shifted to the metalanguage, as is well known [italics his].

The same view of the relationship of informal proofs and meanings is indicated by the earlier quotations I gave from Larvor and from De Toffoli and Giardino: the meanings—the interpretations—of the terms and sentences of informal rigorous mathematical proofs are essential to their functioning. It’s this, on such views, that makes context so important to mathematical proof. (De Toffoli and Giardino (2014, 333) write, recall from above, “[continuous transformations on pictures] are part of the background material in the sense that any topologist knows immediately that these transformations can be interpreted in terms of homeomorphisms.”) Professionals, that is, know what’s being talked about in an informal mathematical proof because of their antecedent training in such mathematical contexts. This is seen as true, in particular, of diagrammatic proofs.

In the next few sections, I’ll endeavor to undercut this supposed difference between informal professional mathematical proofs and formal derivations.

Rule-Governed Games

I’ll start by engaging in what might initially appear to be a section-long digression about the characteristics of a specific kind of rule-governed game that connect those games to notions of computability. But in the sections that follow, I’ll return to the topic at hand by sketching a characterization of diagrammatic proof systems—specifically, the venerable system of the Book I of The Elements—directly in terms of the notions of computability that are applied to these games. Finally, I’ll return to the debate between proponents of the derivationist account and their opponents and show that this material illuminates that debate by providing a successor view to the derivationist account that shows in what sense Agreement is a datum of mathematical practice and shows how the satisfaction of Agreement by mathematical practice can be explained in terms of the rule-governed games that are described in sections 3 and 4.

To start, a game has a finite set of kinds of game pieces. Game pieces are various physical items stipulated as useable in that specific game. Any of the following can be game pieces in a game: chips; balls; chess pieces; playing cards; humans; mental entities (of one sort or another); written items of various kinds on paper or sand or whatever; diagrammatic entities, such as drawings of specified sorts; computer graphics; and so on. Game pieces are understood to have properties. In particular (and very importantly), they are easily distinguished from one another by participants (and by observers of the game)—this is both in the sense that the tokens of a kind of game piece are distinguishable from one another and also in the sense that different kinds of game pieces are distinguishable from one another. The properties game pieces are presumed to have (and that enable these distinctions), however, aren’t their pure physical properties; they aren’t even their perceivable physical properties—the physical properties of these items that are perceivable, say, by participants. Rather, and crucially, their properties are stipulated, either explicitly or tacitly. Their “properties,” that is, are conventional ones that they can be specified to have because of their perceivable physical properties. I’ll discuss this in more detail in section 6.

Important also is the assumption of a field that the game takes place on. This is simply the space—either one, two, or three dimensions, that game pieces are placed in (or on). Any field is exhaustively divided into cells—again, cells of either one, two, or three dimensions. These cells have adjacency relations: Each cell is stipulated to be immediately adjacent to a fixed set (and finite number) of other cells; adjacency relations are reflexive, symmetric, and not transitive. Each cell can contain one and only one game piece at any time. A Turing-machine tape, for example, extends linearly along one dimension and is divided into squares, each of which is adjacent to its two adjoining squares. A piece of paper on which diagrams are drawn uses a field of two dimensions, and a game played in space (such as baseball) can require three dimensions. (Correspondingly, the game pieces themselves can be items of one, two, or three dimensions.) The field can be (potentially) infinite in any or all of its dimensions, although its resolution is always finite. That is, any finite subregion of a field contains only a finite number of cells.¹⁰ (I’ll call this the finite-subregion-finite-cell property in what follows.) Call a cell occupied iff it contains a game piece. A configuration of the field is any placement of a finite number of game pieces in its cells. A set of cells is connected (in a field) if, for any two cells c_a and c_b, there is a sequence of cells, c_a, c₁, …, c _n , c_b, where each cell is adjacent to the cells immediately before and after it in the series. A subconfiguration of a configuration is any subset of the cells of that configuration.

Game states are recursively specified configurations of none, some, or all of the game pieces according to the rules of the game. The rules, usually, don’t specify all the acceptable configurations directly, but only in terms of transitions from earlier configurations and the null configuration (the empty field). These rules, that is, specify the admissible game episodes, which are sequences of game states over time, each one admissible according to the rules on the basis of earlier game states. An admissible game episode, that is, is any physical (or mental) movement of the game pieces into cells or from cells to other cells that’s licensed by the rules of the game. I’ll sometimes call these “admissible transitions” or “admissible game-state transitions.” An umpire is someone (human or machine) who watches the game and knows the rules. I include among umpires, in addition, those who execute derivations according to the rules of a logic. More generally, if a game has only one player, that player is also an umpire—and, of course, anyone who watches a game (or a record of that game) is an umpire. A game is mechanically recognizable if an umpire can immediately recognize at a time (by a mechanical or unintelligent application of the rules the umpire has memorized) the admissible transitions occurring at that time of any episode in that game. In particular, this is only possible if the admissible transitions allowed by the rules are all locally constrained: they operate only on finite subregions of the field that are within the immediate purview of the umpire(s) at that stage in the game.¹¹

Playable games, as I’ve characterized them, are a very broad class of human activities. I intend to be among them the sports games so popular in our culture, but also role-playing games, board games, various card games, as well as the calculational devices of various sorts that we engage in: arithmetical calculations using pen and paper, more physical ways of manipulating things to execute calculations, beads on strings (for adding, say), and so on. They are also meant to include formal proofs and algorithms, as well as the informal rigorous mathematical proofs that use diagrams. Included among these games are “nondeterministic” ones— say, ones using dice or other devices that introduce an “element of chance” into the game. The construction of a formal derivation, of course, is also “nondeterministic” in the sense that there is (usually) more than one subsequent (interim conclusion) that follows from a sequence of formal propositions at any one time.

The focus here, however, isn’t on the production of game episodes; it’s on the ability of the umpire(s) to mechanically recognize that every game state in a game is due to an admissible transition from earlier game states. I’m not assuming that an entire admissible episode is effectively or mechanically recognizable “at a glance” or “immediately.” The recognition that a game episode is admissible is usually the result of memory and/or the inspection of a record of the game: one sees in this way that all the game-state transitions in that game episode are admissible.

Finite Resources for Judging Games

Turing (1936) originally characterized the intuitive notion of an “effective” or “mechanical” procedure for calculating sequences of numerals in terms of “computers” (human calculators) with unlimited time, paper, and pencils on their hands—as well as a pretty inhuman capacity to concentrate endlessly on mechanical tasks. Hefurther assumed such beings have (in principle) only a finite set of mental states and a finite set of symbols available.¹² Despite these apparent limitations, he was able to indicate good reasons for thinking that the intuitive notion of an “effective” or “mechanical” numerical function is equivalent to what has subsequently come to be called Turing computability. (This is a version of the Turing-Church thesis.)

Sieg (2000, 2008, and elsewhere) has stressed the importance of Turing’s discussion of the memory and the sensory limitations of humans engaged in mechanical tasks, both in motivating Turing’s characterization of Turing “machines” (human calculators), and as the distinctive element in Turing’s approach to computability—as opposed to Gödel, Church, Kleene, and others.¹³ Sieg uses this characterization of human limits to axiomatize the intuitive notion of mechanical or effective procedure and to show its equivalence to an axiomatized notion of Turing computability. Thus, instead of linking Turing computability (and the other notions equivalent to it) to the intuitive notion of effective or mechanical procedure by the Turing-Church thesis, he captures the relationship by characterizing both notions axiomatically and showing their equivalence.¹⁴

In any case, these limitations motivate two “boundedness conditions” and two “locality conditions” that I borrow from Sieg (2008, 575) and modify to apply to the games I’ve just characterized:

• (B.1) There is a fixed finite bound on the number of cells (with or without game pieces in them) that any umpire can immediately recognize (at a time).

• (B.2) There is a fixed finite bound on the set of rules of any game.¹⁵

• (L.1) An admissible transition of a configuration to another configuration can only be based upon the movement of game pieces with respect to immediately recognized cells.

• (L.2) The class of immediately recognized cells can be changed, but each of the new observed cells must be within a bounded distance L of (any of) the previously immediately observed cells.

There are two points about these constraints. They can be motivated, first, directly as requirements on games, as I indicated earlier, by the ordinary (and indisputable) limitations of human memory and human sensory systems—this is pretty much how Turing (and Sieg) motivates them. I should add that these limitations of memory and sensory capacity are shared by current machines and—particularly—current “machine vision.”¹⁶ But, second, and more particularly, B.1–L.2 together motivate the specific constraints I’ve placed on games—particularly, the constraints that any finite subregion of the field of a game has only a finite number of cells and that admissible transitions affect only finite subregions of fields that are being immediately surveyed by umpire(s).

Are Certain Diagrammatic Proofs Analogue or Infinite?

It may well be thought that my description of the field of any game explicitly excludes an application of this game model to most physical games that take place in space and time.¹⁷ In the case of baseball, for example, it may be thought that certain events, such as catching a ball in the outfield, involve continuum-many (or at least, countably many) similar possible events, because any such particular event can vary ever so slightly in its trajectory in space and time (without a lower limit in closeness).

Furthermore, attempting to apply this approach to diagrammatic proofs may seem to result in something even more inadequate. Consider the initial instructions we’ve given in Book I of Euclid’s Geometry. We may place a point anywhere; we may draw a circle anywhere.¹⁸ Assuming the background space of the diagram is a real manifold—something that seems required by other assumptions of Euclidean geometry (in particular, that intersections of lines always yield points)—any hope that Euclidean diagrams aren’t analogue seems dashed. Thus, treating a piece of paper as a field with the finite-subregion-finite-cell property seems ruled out by Euclidean diagrammatic practices. Similarly, recall that De Toffoli and Giardino (2014, 33) write about continuous transformations being permissible actions on pictures; the phrase “continuous transformations” is clearly meant to apply to diagrams, and the semantic interpretations of the diagrams so continuously transformed are homeomorphisms. Even more dramatically, Feferman (2012) is titled: “And so on …: reasoning with infinite diagrams.” If Feferman is to be taken literally (and he makes it clear in the paper that he is to be taken literally),¹⁹ this rules out pretty explicitly a characterization of the configurations such diagrams are embodied in being finite.

It’s important, however, to keep the properties of the diagrams mathematicians peruse (on paper, on computer screens, or in their minds) strictly distinct from what those diagrams are semantically associated with. Let me start with Feferman’s claims about diagrams and oppose those claims with a truism: No infinite diagrams appear anywhere in Feferman’s paper. Everything that does appear in those papers is finite. Below are two examples from his paper (Feferman 2012, 376, 379; I’ve retained his numbering: Fig. 3 and Fig. 7):

Notice that various conventionalized symbols do appear in the above. In particular, in the second diagrammatic proof, there are conventionalized pairings of arrows with ellipses that indicate that there is more of the same in the various directions the arrows are pointing to (or from, when ellipses precede the arrows). In Feferman’s Fig. 3, the conventionalized indications of “more of the same” are more intricate, involving a conventionalized description of how a pair of functions are supposed to operate.

What does not appear at all (anywhere) are the more of the diagrams that are indicated by arrows and ellipses. What does appear, to repeat, are just arrows and dots. It might be responded that I’m being unfair to Feferman by demanding that if an infinite diagram is involved, as he claims, then that infinite diagram must appear in his paper. Instead (recall from the quotation in footnote 19), what’s required is only that the diagram in question be “visualized in full.” This response isn’t going to do. Feferman, in his paper, is making a distinction between two kinds of cases where a finite depiction conventionally indicates how we are to go on should we desire to sketch more of the diagram on paper (or think of further parts of that diagram in our minds). In the cases above, what’s involved is a further sketching of the diagram that looks the same as what’s already present to the mathematician’s eye on paper. But Feferman understands other cases differently. Consider the diagrammatic proof of the existence of a bounded continuous closed curve with no finite length and no tangent at any point (the “Koch snowflake”). I provide the diagrammatic proof, immediately below, that Feferman (2012, 374) gives (but which I have borrowed from somewhere or other on the web and have modified to include the needed ellipses):

This, as Feferman (2012, 374) puts it:

is the limiting curve of a sequence of polygons beginning with an equilateral triangle of side 1. The sequence is described inductively: at each stage, one simultaneously divides each side of the polygon before us into three equal segments, then builds an equilateral triangle on the middle segment, and finally deletes the base of the new triangle except for its endpoints. Since the length of the circumference of this figure at each stage is multiplied by 4/3, and since (4/3)ⁿ approaches infinity, the limiting curve has no finite length.

The limiting curve cannot be visualized because it has infinite length (and no tangent at any point). This is true, however, of none of the diagrams in the infinite sequence that converges (as it were) to the limiting curve: all of them have finite lengths (which can be explicitly calculated as Feferman indicates) and each lacks tangents at only finite many points. But what’s important to realize is that beyond a certain finite number of these diagrams (say 140, to be very conservative), none of the remaining (infinitely many) members of the sequence of diagrams can be visualized either—this is in the sense that the viewer’s eye becomes incapable of distinguishing differences between any of them. Notice this important point: limitations in what viewers can see are also (pretty much) limitations in what the viewers can see in their “mind’s eye.”

For the same reasons, one cannot visualize in full—in one’s mind—the infinite diagrams indicated by Feferman’s figures 3 and 7. Visualization can only be something that involves a mental replication—at least, in the relevant respects—of what we do when we use our eyes to see anything. But we have no examples of seeing (using our eyes) a fully infinite pattern of any sort. So, unless, mental visualizing can sprint beyond the capacities of our senses with respect to the infinite, we cannot be said to visualize completed infinities. There is a difference, of course, between the Koch snowflake and the other diagrams Feferman mentions. This is that the subsequent diagrams in the series (e.g., extending Feferman’s Figure 3 or Figure 7) are just “more of the same.” But that we understand that there is more of the same to a diagram doesn’t mean we can (visually) complete that diagram in our mind’s eye by presenting to ourselves (mentally) all of that “more of the same.”²⁰

Because Feferman describes these diagrams as infinite, therefore, I have to accuse him of confounding two very different phenomena. (I really don’t want to accuse him of this, but I think I have no choice.) On the one hand, there are the actual physically real (although conventionalized) diagrams that we instantiate physically in space and time on computer screens or with paper and pencil, or on blackboard with chalk, etc. (or that we imagine in time), and there are other sorts of completions of such items that we can conceive of but that don’t actually occur instantiated anywhere in our diagrammatic practices—either on or in visual media of various sorts or in our minds.

Consider the simple diagrammatic proof below that the series ½ + ¼ + … sums to 1:

This diagram can be viewed in any of three ways. The first is as I urge, the diagram itself, on my approach, contains nothing infinite. Instead, there are three dashes which conventionally stand for something like “a diagram-like object that continues (forever) the pattern you actually see on the paper.” The second interpretation is one that Feferman attributes to the diagrammatic proofs of the Koch snowflake. We’re given a couple of diagrams which visually indicate how a manipulation of the diagrams to produce further ones in the series can be continued infinitely and where (up to a finite point!) each of the resulting diagrams can be visualized, but where the limit of the series isn’t visualizable because it doesn’t “go on in the same way” as any of the diagrams in the series do. The third interpretation is the one that Feferman attributes to his figures 3 and 7: actual infinite diagrams—items that he takes us as able to “fully visualize.”

What tempts Feferman to his latter two interpretations of diagrams (I claim) is that the diagrams that actually appear in his paper (and in mine) involve both intended (and explicit) semantic relations to mathematical objects that they are to show results about (series of numbers, curves of various sorts, set-theoretic objects) as well as semantic relations to what should be called “diagrammatic objects”—items, however, that don’t appear in these papers but are conventionally indicated by the use of dots, arrows, or lines). Results about these latter items are used, in turn, to show results about the mathematical objects these items also have semantic relations to.

However, to treat the semantically indicated (infinite) diagrammatic objects as diagrams that are part of the informal rigorous diagrammatic proofs that mathematicians provide to one another is a mistake. Instead, “diagrammatic objects” in this second sense of “diagrammatic” are (as I’ve noted) themselves mathematical objects that are the referential targets of the diagrams that actually appear on paper (or on computer screens, or whatever) just as numbers, curves, and set-theoretic objects are. Anything can be treated as an object of mathematical study—that includes “diagrams” understood as certain sorts of idealized objects only certain parts of which can appear concretely. We should not, therefore, confuse the actual diagrams that Feferman reproduces in his paper (or the ones that we can constitute in our thinking) with the ones only referred to by this diagrammatic practice—referred to along with other mathematical objects that are also referred to. These (finite!) diagrammatic proofs, in practice, refer to certain sorts of infinite processes (completed or continuously engaged in) applied to what are ultimately mathematical diagrammatic objects. These infinite processes (which are also mathematical—not part of the proof but part of what the proofs are about) in turn yield infinite (or limits of continuous series of) diagrammatic objects (which are also called “diagrams”). Results about these, finally, are understood to imply the desired number theoretic or set-theoretic theorems.²¹

The attribution of properties to diagrams that, strictly speaking, apply not to them but (at best) only to the objects to which these diagrams have semantic relations is hardly restricted to Feferman. It occurs widely. When, for example, De Toffoli and Giardino (2014, 33) write about “continuous transformations” of diagrams, this is actually a matter of discrete diagrams that represent continuous transformations, not anything that’s actually being continuously applied to diagrams on paper (or electronically—I include diagrams that move on the computer screen).

Part of the problem is how mathematicians themselves talk. In writing proofs that involve writing about diagrams, or notation more generally (which almost always happens), mathematicians studiously avoid the niceties of “use and mention”—in Quine’s sense. Mathematicians, for example, effortlessly shift between talk of “functions” (understood as mathematical items) and “functions” understood as the notation standing for functions—in the latter case, they will talk about the indices on certain functions and shift in the same sentence to describing the properties of those functions as mathematical objects.²² More elementary examples of the same practice are the use of the words “triangle” and “line,” in the Euclidean diagram tradition, to describe both the diagrammatic items themselves and what those diagrammatic items represent. (I do this sort of thing in this very paper, of course.)

But there is another important factor that arises more specifically with respect to diagrams and not with notation, generally. Mathematicians certainly speak (as De Toffoli and Giardino do) of “continuous transformations” of diagrams (in thought, but also on the computer screen). This way of speaking (and of thinking about diagrams) is derived, of course, from how we experience movements in space. We experience movements of objects through space (and of actions in space, such as drawing curves on paper) as continuous—more accurately, as space filling. But simultaneously, our experience of anything in space always involves finite resolution. This gives rise to subtleties in diagrammatic conventions that I’ll discuss in the next section.

The Role of Conventions in Diagrams

One thing that makes our experience of space intuitively puzzling (and this is also something that can easily mislead us when we theorize about diagrammatic proofs) is that although anything we do in space (by way of playing games, drawing diagrams, etc.) obeys the finite-subregion-finite-cell property, we don’t directly see this—in particular, we don’t see the cells the fields of these games are required to be composed of. The curves that we draw on paper, or the movements we make in space, as I mentioned earlier, look space filling: it’s this that makes the postulation of space as composed of continuum-many points seems intuitively plausible; conversely, it’s why any suggestion that the space we interact with is finite-region-finite-cell-structured seems, well, crazy.

But that any game we play in space (any diagram we draw on a page) must be on a field that obeys the finite-subregion-finite-cell property is easily established by the fact (which is also pretty obvious) that we cannot distinguish two spots, if they are within a certain closeness, or see a spot at all, if it’s too small.²³ We similarly recognize that we can only distinguish finitely many curves in any finite region of space (that we can immediately survey). These two facts motivate, pretty directly, a metaphysical picture of space and what’s in it as things that go infinitely beyond our visual senses: we can always (in principle) focus in more closely—either by eye or with magnifying instrumentation—and doing so will reveal further distinctions we can’t see otherwise. This is, intuitively, an infinitely iterable process of divisibility that’s limited only by practical considerations.²⁴

It should be clear, however, that any diagrammatic proof procedure must honor the finite-subregion-finite-cell property because of the simple requirement that whatever visual items that appear in that diagram must be, first, distinguishable and, second, recognizable as what they are supposed to be, by eye. This is why the mere visual qualities of diagrams are (and must be) supplemented by explicit and tacit conventions that able practitioners of diagrammatic proofs utilize automatically.²⁵ In saying this, I’m only pointing out the truism—in the particular case of Euclidean diagrams—that, for example, visual dots (that are perceived by us to have two dimensions) nevertheless stand for dimensionless points, diagrammatic lines (widthful things that are usually perceived by us to be both crooked and irregular in their widths) are to represent straight, one-dimensional items and so on.

The conventions I’ve invoked play two roles. I’ll discuss the first in this and the next paragraph and then turn to the second. There is, first, the classification of various physical items as game pieces. It’s not merely, for example, that a class of physical items that “look alike” are induced by that alone to be the same kind of game pieces. In practice, a game piece that in fact looks like a different game piece may, because of its role in a series of configurations, be recognized as the game piece it’s stipulated to be—despite its appearance. (So, e.g., during a game of chess, something that physically looks like a pawn may in fact be recognized by everyone watching the game to be a king.) Similarly, conventions require us to be able to distinguish distinct game pieces—in different spatial locations—as, indeed, located “in different places.” Notice that the actual metaphysics of the field—whatever it really is (e.g., quantum foam)—is completely irrelevant to the stipulated properties of the field; we perceive the drawing of a line (of whatever length) as completely space filled. But, instead, if such a line is finitely extended, this is by the placing of conventionally stipulated parallel line symbols (ones stipulated to be parallel to the line symbols already present) in a finite number of cells immediately adjacent to one another. This is a given of the Euclidean diagrammatic practice because we can’t distinguish more than finitely many distinctions among the possible lengths and angles of the lines we draw or could have drawn.

In the case of Euclidean diagrams, the game pieces are (one-cell) portions of lines, circles, and so on. In the case of formal derivations, the game pieces are the primitive alphabetic items, individual variable symbols, the quantifier symbols, and so on. Notice further that individual game pieces are manipulated in admissible transitions of formal derivations—although, in practice, more than one piece is manipulated at a time. In the case of Euclidean diagrams, as I’ve been describing them, finite sets of game pieces (in connected cells) are always manipulated all at once. One never extends a line, for example, by occupying only a single adjacent cell with a line symbol. Many such must be occupied simultaneously (although only finitely many many such, of course). This is simply because the cells are below visual threshold in Euclidean diagrams—although they must exist because of B1–L2.²⁶

The second role that the conventions I’ve invoked above play is to stipulate semantic relationships between the game pieces (and configurations of game pieces) and mathematical objects. It’s by the (usually tacit) stipulation of these semantic relationships that game pieces become symbols. These semantic conventions often shift historically because of the background evolution of mathematical concepts. For example, the notion of a function underwent a progressive evolution,²⁷ from an early notion of function to a spread of later notions (arbitrary function, everywhere differentiable function, continuous function). What class of mathematical objects (what set of functions) a drawn curve on a piece of paper represents is not given “by eye”; it’s given by conventional stipulation of the semantic relations of the game pieces (even if the conventions in question are tacit ones).

Although I won’t dwell on this in this paper, conventional choices of semantic relations can be better or worse for the value of the resulting diagrammatic proof procedure. The soundness and validity of the standard diagrammatic proof of the intermediate value theorem (see fig. 3.2 immediately below this paragraph, from Brown (1999, 27)), for example, turns completely on what class of functions are stipulated as indicated by curves on pieces of paper. If smoothly drawn curves are to represent only continuous functions, then the proof shows what it’s supposed to show. Otherwise it may not.²⁸ The mechanical recognizability of a proof—of any sort—all by itself proves nothing. That proof must have an interpretation: this is equally true of formal derivations and informal rigorous mathematical proofs. And, there is nothing intrinsic to diagrams that forces one interpretation on them and not another. To assume this is to simply overlook that a visual appearance of a diagram may make a certain interpretation natural; but naturalness isn’t a requirement on interpretation.

An important point should be brought to attention (although the details about it are developed further in other work cited in a footnote at the end of this paragraph). The effective procedures that can be applied to game pieces and the semantic conventions that determine the mathematical subject matter these game pieces (and their configurations) are about must coordinate appropriately if a diagrammatic proof procedure is to operate successfully. So, for example, allowing the visually measured lengths of lines in Euclidean diagrams to be semantically significant (to correspond to actual lengths of the depicted lines) will yield an unsuccessful diagrammatic practice because effective recognition of the conventionalized properties of the resulting diagrams is absent. (We can’t tell exactly how long these things are by eye: an appropriate semantic convention using visually perceived lengths to stand for the lengths of the corresponding mathematical objects isn’t easily established.)²⁹

That is, the properties that game pieces are stipulated to have, in cases where configurations are interpreted, must be ones that yield effective recognition of the properties of configurations while at the same time being sound with respect to the mathematical interpretation of these configurations. These are not exactly straightforward requirements to satisfy. In particular, this explains why diagrammatic proof techniques are hard to invent—why serious mathematical talent is needed to do this.

My use of the word, “stipulation,” to describe these two roles of conventions can be misleading (so let me try to fix that). In practice, especially with diagrammatic proofs, the experience of the semantic relationships between configurations of game pieces, such as triangles drawn on a piece of paper, and what those triangles are supposed to depict, is so automatic and seamless that it may strike some as an intrinsic semantic property of diagrammatic items—in the sense that these diagrammatic items must depict certain mathematical objects and not others. This, however, is surely not true. Nevertheless, our automatic and pretty involuntary experience of certain semantic relationships between diagrammatic items (e.g., drawn lines and mathematical lines) explains the impression some have that the role of meaning and truth is intrinsic to informal rigorous proofs and that this aspect of such proofs can’t be captured by formalized imitation. A similar experience with words on a page can give the same impression about the meanings we associate with those words: The impression that certain words intrinsically refer to what they refer to. Visual experience, in general, always contains conventionalized elements that are an involuntary part of that experience. In neither case should we think either that the conventionalized elements are required to be there or that they are intrinsic in some way to what’s given to us visually by our senses nor should we think that such conventionalized elements are simply a matter of what “we see,” whether those are words or diagrams that appear on a page.

Conventions being an involuntary part of visual experience misleads in a second way, especially with respect to diagrammatic proofs. Many philosophers find it tempting to see us (and mathematicians, generally) as “abstracting” or “intuiting” pure mathematical objects from what we see in the world. Although I shouldn’t say anything further about this now (solely for reasons of space), it should be clear that I regard this as a completely mistaken characterization of how perception (and the mind) works with respect to our “grasp” of abstracta.³⁰

With respect to the rest of this paper, the upshot of the foregoing analysis is this. Because of human (and machine) limitations, the (implicit) conventions of diagrammatic proofs force the field that such diagrams appear on to obey the finite-subregion-finite-cell property. In particular, each cell will have a finite number of immediately accessible cells (this is empirically established by our practice of requiring diagrams to be comfortably perusable by professionals). The same point holds of playable games in space and time, as well as mental playable games. This is because the games we play in our minds are limited in the same ways by our capacities for memory (and imagination) that the games that we play physically are.

The Turing Computability of Diagrammatic Proof Methods and, More Generally, of Playable Games

Everything is pretty much in place to establish that diagrammatic proof methods, ones that we recognize (intuitively) to be effective or mechanically recognizable, have Turing computable recognition procedures. There are (offhand) four strategies for establishing this that I’ll sketch. The first is to bypass the work of sections 3, 4, and 6, by instead invoking a strong form of the Turing-Church thesis (where the intuitive notion to be identified with Turing computability is one of effective or mechanical calculation of any sort—not merely that of effectively calculable numeral functions). The second and third strategies go this way. The first (shared) step is to establish, applying finitary-capacity considerations for resolution (both physical and sensory) of humans and machines, that any game humans and machines play is a playable game in the sense of section 3. Then (this is the second strategy) one uses something like Gödel coding to transform any particular admissible game episode into a sequence of single-step transformations that can be directly seen to be Turing computable. Or (this is the third way), one follows the first shared step with a second step of instead establishing that Gandy machines can recognize the admissible moves of any playable game and then relying on the fact that anything computable by Gandy machines is computable by Turing machines. (See Gandy (1980).) The fourth way, finally, is to utilize the generalization of Turing computability to k-graphs, following Sieg and Byrnes (1996), by first establishing that Euclidean diagrammatic proofs can be characterized as the manipulation of k-graphs.

Algorithmic Reasoning Is on the Surface of Mathematical Practice

Let’s return now to the issue this paper opened with. Proponents of the derivationist account, recall, hope to capture certain aspects of mathematical practice by attributing to mathematicians a grasp of the formal derivations that informal rigorous mathematical proofs correspond to. I’m continuing to leave aside the objection I mentioned that mathematical practice doesn’t exhibit the kind of agreement among mathematicians that it purports to detect (Agreement). I’ll take this up in section 9. For now, assume mathematical practice is as Agreement describes it to be (call the phenomenon, “public mathematical surety”) and let’s worry instead about the possibility that formal derivations are psychologically unavailable to mathematicians—even in the generalized sense described in the third observation of section 1—and so they cannot provide the needed public mathematical surety.

Broadly speaking, there are two strategies for establishing the psychological unavailability of formal derivations. I’ll be brief about the first strategy because I’ve discussed it in other work (and others have too). It essentially turns on the fact that the formal derivations that must correspond to informal rigorous mathematical proofs are (1) too long to plausibly be what mathematicians are using (consciously or otherwise) to convince themselves that their informal rigorous proofs are valid. Furthermore, (2) these derivations don’t have the appropriate epistemic qualities to provide surety to mathematicians. (Call (1) and (2) the “too-long objection.”)

On (1): Once a formal system is specified—in particular, once the proprietary language of the nonlogical axioms is specified—the resulting mechanical step-by-step derivation is (in general) extremely long.³¹ This all by itself makes it implausible that such derivations are grasped by mathematicians in any real sense because recognizing the validity of these derivations turns solely on their fine structure (the effective step-by-step recognition that each line follows by the rules from ones earlier in the derivation). This means that the line-by-line fine structure of extremely lengthy derivations (and not some global property that they syntactically possess) is what’s supposed to be used by the mathematician to recognize the validity of their informal rigorous proofs and to explain Agreement. If so, the mere lengthiness of the derivations all by itself is a strike against them because there is no distilling—even syntactically—some more abstract global property that the mathematician can be seen to be grasping when he or she recognizes the validity of an informal rigorous mathematical proof on the basis of its corresponding derivation.

On (2): But this fine-structure fact about how the validity of derivations has to be recognized makes the derivations corresponding to informal rigorous mathematical proofs epistemically opaque in a significant way. Anyone who reads such a formal derivation can tell (after finishing it—if that’s possible, I mean) that every step follows from the one before it. That is, anyone will grasp the validity of the derivation in (and only in) the fine-structure sense of the following: this step follows from that step, this next step follows from these steps, and so on. But, no global (aha!) experience of understanding how the proof “comes together” that explains why the initial assumptions result in the theorem they result in arises (or can arise) in this way. So this can’t explain the common experience of understanding that ordinary informal rigorous mathematical proofs often provide.³²

It’s important to realize that early formalization programs (e.g., Russell and Whitehead’s Principia), and many contemporary ones as well, require a foundational proprietary ideology (a set-theoretic one, category theory, one or another modal logic, etc.) that all derivations are required to be in terms of. This is also true of (current) projects of formalizing mathematical results in computer-checkable form. The proprietary language of the MIZAR system, for example, is formal logic plus set theory. But adhering to a requirement of a particular vocabulary (rather than allowing the relevant derivations to belong to any “nearby” algorithmic system) lengthens the needed derivations all by itself. The derivationist approach doesn’t obviously require—without specific argument—a proprietary ideology. This means that the derivations it needs to explain mathematical practice can be much much shorter. I press this point after presenting the second strategy against the availability of formal derivations to explain mathematical practice.

The second strategy is to argue for an overgeneration problem that there are often multiple candidate derivations (in rather different mathematical ideologies) that correspond to an informal rigorous mathematical proof; but there is no principled way to decide which of these (if any) is being utilized by mathematicians to induce public surety. Furthermore, these candidate derivations are too different to provide the needed public mathematical surety as a group.³³

The mutilated chessboard³⁴ is an illuminating example that Tanswell gives. Here is a description of it that’s due to Black (1946, 157)—but I’m borrowing the quote from Tanswell (2015, 305):

An ordinary chess board has had two squares—one at each end of a diagonal—removed. There is on hand a supply of 31 dominos, each of which is large enough to cover exactly two adjacent squares of the board. Is it possible to lay the dominos on the mutilated chess board in such a manner as to cover it completely?

And this is the solution, quoted from Gardner (1988)—but I’m again taking the quote from Tanswell (2015, 305):

It is impossible … and the proof is easy. The two diagonally opposite corners are the same color. Therefore their removal leaves a board with two more squares of one color than of the other. Each domino covers two squares of opposite color, since only opposite colors are adjacent. After you have covered 60 squares with 30 dominos, you are left with two uncovered squares of the same color. These two cannot be adjacent, therefore they cannot be covered by the last domino.

Tanswell (2015, 306) points out that this proof “has been formalised a number of times in different systems as a good example of informal reasoning that is tricky to capture formally.” In particular, one approach is by reconstructing it set-theoretically, by representing the board as sets of coordinates, defining an adjacency relation on the sets of coordinate, and a tiling that uses the relation. A different approach uses inductive definitions for the set of dominoes and the tiling (and this way proves crucial properties by rule induction). A third approach, finally, uses an ideology of states of the chessboard and actions of placing dominoes on the board, and it approaches the problem using finite-state machines.³⁵

The point of the objection, as I mentioned, is that if the derivationist account is supposed to explain the public surety of informal rigorous mathematical proofs in terms of the mathematician (in some sense) grasping derivations corresponding to those proofs, it faces an objection if there are too many sorts of derivations that are quite different in their ideological resources. The point is to explain Agreement, after all—but if the underlying derivations are quite different, we face a problem of explaining why mathematicians would think they’re looking at the same informal rigorous mathematical proof, since it isn’t the surface appearances of proofs that’s supposed to be explaining Agreement.³⁶

Both challenges to the derivationist account (and, correspondingly, the force of the mutilated chessboard example), however, turn on implicitly saddling that approach with a language-based requirement on derivations: the relevant derivations must occur in formal systems which are purely language based.³⁷ But this restriction seems badly motivated because the crucial value of mechanical recognizability isn’t restricted to language-based algorithmic systems. In point of fact, one basic way of directly characterizing effective computability is in terms of Turing machines, which aren’t language based.

Any translation of an algorithmic proof procedure that isn’t purely language-based to one that is will always require a serious lengthening of the proof, as well as a multiplication of alternative choices in ideology (nonlogical vocabulary). This is because of the need to axiomatize the fields of diagrammatic algorithmic procedures, and their properties, as well as the conventionalized properties of the game pieces and the admissible operations on configurations of the fields. Notice that this is the case whether, in original informal diagrammatic proofs, the spatial relations play semantic roles (as they do in the Euclidean diagrammatic tradition) or whether they function in a purely calculational way (as they do, say, with two-dimensional matrix diagrams in linear algebra).

In diagrammatic proofs (as with Turing machines), on the other hand, the spatial relations are instantiated only in the proof procedures themselves: they aren’t part of what’s demonstrated but instead are among the items by which the demonstration occurs. That is, they play the same role that distinctions among vocabulary items play in the characterization of the syntax in the metalanguage of an axiomatic system.³⁸ In transcribing any such diagrammatic proof to a language-based form, therefore, proof-theoretic content that’s strictly speaking extraneous to the informal rigorous proof must be introduced into the derivation itself. That is, content must be moved from the proof-theoretic mechanisms of the diagrammatic proof procedure and be made part of what is proved in the course of the proof. To repeat, that there are, in general, many ways to do this is hardly surprising.

As a result, debates over the force of the too-long objection and the underdetermination objection have been revealed to be largely nomenclatural. Suppose the “derivations” relevant to the derivationist account are mechanically recognizable sequences of inference steps in a particular formal alphabetic language. Then the derivationist account faces Tanswell’s challenge because diagrammatic proofs (in particular) require axiomatic elimination of their proof-theoretical properties that rely on spatial relations. More accurately (since formal proofs rely on the spatial relationship of concatenation and, relatedly, the visual capacity of umpires to distinguish kinds and tokens of the alphabet of any formal language), they require the transformation of proof-theoretical properties that rely on space in ways other than sheer concatenation (and a conventionalized distinction between vocabulary items) into proof-theoretical properties that rely on space only with respect to concatenation (and conventionalized “resemblance”). Similarly, the derivationist account faces the too-long objection because diagrammatic proofs can’t be taken largely as is (merely refining the algorithmic procedures mathematicians are aware of and employing) but requires a translation to one or another language-based derivational system. If diagrammatic proofs are characterized directly as effectively recognizable, then what’s required to make them “fully rigorous” is, at best, filling in—the relevant derivations can truly be seen as ones “indicated” by the informal rigorous proof mathematicians actually give. In particular, the ideology of the rigorous informal mathematical proof will need little or no supplementation.

So if what’s crucial to mathematical proof is only that such proofs be mechanically recognizable, regardless of whether this is managed in a pure language-based way or diagrammatically, then the “derivations” needed to explain public mathematical surety can be understood as including diagrammatic proofs. In this case both the too-long objection and Tanswell’s challenge vanish because, as I indicated in the last paragraph, “informal” rigorous mathematical proofs can themselves (at least to a very large extent), and on the basis of proof algorithms used in informal mathematical proofs, explain properties like Rigor, Correctness, and Agreement.

What about the other conditions described in section 1 that the derivationist account is supposed to handle? Content, to a very large extent, lapses as a requirement on the derivationist account (because the need to translate informal rigorous mathematical proofs to derivations with substantially different ideology is gone). Techniques remain a substantial matter for the derivationist account to discuss, and the explanation of it is, indeed, intricate (although I’ve already raised the relevant points earlier in the paper—in section 6). One shows that particular “informal” proof procedures are effective, and one shows, given the mathematical interpretation they have, that they are sound. There is more to say about this—I’ll do this in section 9.

The Heterogeneity of Informal Rigorous Mathematical Proof

To some extent, the preceding discussion has focused on recognizing nuances in the phrase “informal rigorous” that occur in the label, “informal rigorous mathematical proof.” One claim I’ve tried to establish is that “informal” contrasts with “formal,” apart from abbreviatory shortcuts, only in that the adjective “informal” allows algorithmic systems that aren’t purely language based, whereas the latter doesn’t. This provides content to the phrase “rigorous” in “informal rigorous mathematical proof.” An informal rigorous mathematical proof is “rigorous” in the sense that mathematicians are convinced that an effectively recognizable derivation (that’s in the ideological neighborhood of the proof they’ve inspected) has been shown to exist by that proof. The effectively recognizable derivation, that is, isn’t very far from what’s already present on paper (or computer screen, or whatever). This view becomes much more plausible, once the surface algorithms of ordinary mathematical proofs are seen to possess the epistemically valuable property of being mechanically recognizable and once the local context-dependent background material alluded to by De Toffoli and Giardino and by Larvor is seen to only amount to “filling in” aspects of the already visible algorithms used in ordinary proofs.

If the foregoing were the only relevant considerations, we’d be done. Mathematical practice would be fully explained in terms of algorithmic systems, where such systems go far beyond the language-based ones traditionally taught in logic classes everywhere. The derivationist account would have successful responses to the too-long objection and the overgeneration objection. In particular, that computer-checking proofs involve such a long process of putting a standard textbook proof into the appropriate form (that a computer can check) would also be explained by the fact that current systems (like MIZAR) are also language based and use a proprietary vocabulary which greatly lengthens proofs. Some day in the far (or, possibly, near) future, one imagines that Gandy robots with appropriate machine vision will be checking our diagrammatic proofs directly—and in pretty much the ways professional mathematicians do already.

As I said, we’d be done—except for one large wrinkle. This is the point I mentioned in footnote 32. A large diet of mathematical proof, especially in functional analysis and the like, gives the impression of enormous heterogeneity rather than that of all the proofs (in a subject area of mathematics) belonging straightforwardly to one algorithmic system, or even a set of such systems that are tightly constrained to one another in their nonlogical vocabulary.³⁹ Rather, especially if one realizes how much topology (for example) shows up in analysis, proofs of all sorts are being used in all subject areas (although, sometimes, only theorems—without their proofs—explicitly appear). Sheer algebraic computations, diagrammatic proofs (of various sorts, using various conventions and resources), conceptual connections, facts about notation, and any and all of this can occur in an informal rigorous mathematical proof. Rav (1999, 12) largely puts the point correctly. He writes:

Proofs employ deductive reasoning; so do judicial rulings. In both cases logical inferences cement sequences of topic-specific claims and considerations.

This isn’t quite right as it stands because what’s doing the “cementing” (most of the time) aren’t logical inferences but instead the notions of truth and meaning⁴⁰—in the various kinds of proofs that are taken to be about a certain subject area (and other subject areas). That is, the cementing is managed by the inter-algorithmic use of common terms that are understood to mean the same things and, more importantly, to refer to the same things (to be true of the same things). For example, the definite integrals that appear in matrices refer to the same old functions and, via those functions, to numbers that are studied, say, in any Advanced Calculus course, and those numbers, of course, are the same old items we’ve (for millennia) been counting with.⁴¹

What’s required to justify this aspect of mathematical practice is a collection of soundness proofs. Suppose a kind of proof procedure is imported into a mathematical subject area (one that applies to semantically significant items of one sort of another—notation, to use a general term that’s to indifferently cover diagrammatic configurations and alphabetic terms). And suppose items of that notation are identified with items of notation already in the subject area (algebraic formulas identified with certain diagrammatic items, say, numbers characterized in one way with numbers characterized in a quite different way). Then what has to be shown is that the one way of mathematically characterizing items (proving results about them in one algorithmic system) is compatible with the other ways of doing so. That is, the indiscriminate borrowing of mathematical results (and informal rigorous mathematical techniques) that occurs in standard mathematical practice has to be shown to be coherent.

We thus have found our way back to the suggestion made by Larvor (2012, 723) that was quoted several times at the beginning of this paper: “the cost is that we have to abandon the hope of establishing a general test for validity,” although we’ve gotten here by means of very different considerations.

And just because the considerations that have given rise to this earlier concern are so different from the ones Larvor (and others) have raised, there is a response: There are two ways to establish the coherence of this holistic mathematical practice. The first is to transliterate the entire practice into one in—one or another—formal system. Doing so allows a straightforward interpretation of all the apparently disparate algorithmic systems in a single domain—and that straightforwardly shows (via a soundness proof relative to that interpretation) the coherence of the entire mathematical practice. Notice that the facts that there is more than one way to do this (Tanswell’s objection) or that the result involves the replacement of relatively short effectively recognizable proofs with extremely long (practically unsurveyable) proofs are irrelevant. The mechanical effectiveness of informal rigorous proofs and, relatedly, the public surety of ordinary mathematical practice are not being established by this transliteration.

There is a qualification, of course. A lot of mathematical practice involves seriously alternative mathematics: intuitionistic set theory, for example, or more generally, mathematics based on systems of logic other than classical ones. But mathematical practice acknowledges this: mathematical results aren’t indiscriminately applied across alternative logical frameworks or across disparate subject areas (e.g., alternative set theories). And so the phrase “the entire practice” used above doesn’t include these nonstandard aspects of mathematical practice. There are numerous alternative branches of mathematics that largely don’t intersect.

The second way to establish the coherence of the holistic practice of borrowing results and techniques from alternative proof traditions (that nevertheless are treated as about the same subject areas) is to provide piecemeal soundness results: this is a matter of leaving the algorithmic practices as is, but (in the metalanguage, as it were) providing soundness proofs relative to a shared interpretation.

Where does this leave Larvor’s remarks about “giving up on a general test of validity”? It tames its significance. There certainly is a general test of validity (i.e., a general recognition procedure—which is how I interpret Larvor’s use of the phrase “general test of validity”). This directly follows from the coherence results, provided we’re in a first-order classical setting, where completeness proofs for validity are available. Nevertheless, in practice one works with specific ways of establishing validity—the ones generated by the specific algorithmic systems being used.

One last bit to round out this section. Recall the concern (that I’ve set aside for so long) that the datum of mathematical practice that this paper has been dedicated to explaining isn’t a real one. Mathematical practice does exhibit significant “sociological drift,” the objection goes, new approaches to mathematical proof are invented all the time, and they are often controversial.

A comparison with rule-governed games is helpful. Here too, new games are invented all the time, and these games are bewilderingly variable. Nevertheless, their game episodes are all mechanically recognizable. In this sense, new games are “the same old thing” all over again.⁴² I can put it this way: In one sense, games are always evolving; lots of new games are always emerging with new kinds of objects (game pieces) and new rules to enable opponents to compete in new ways. In another sense, it’s just the same old thing all over again: here are the rules, and here is what you do to play a game.

It might seem that this analogy isn’t particularly helpful. Games, after all, are generally content-free—unlike mathematics. That they are all governed by rules that allow game episodes to be mechanically recognizable hardly introduces much of a constraint. In the case of mathematics, the corresponding point looks like it’s only a Pickwickian victory. Describing “reasoning” as algorithmic, and noting that all mathematics is “proof as usual”—intuitionistic, quantum-logical, various extensions of classical logic, and so on—is to leave out exactly what’s significantly different about all this mathematics: how different these branches of mathematics are in content.

I agree with the Pickwickian charge, but the reasons for agreement are subtle enough to deserve further discussion. To see the implications of any algorithmic system (and, in the case of a mathematical system, to understand seeing the implications as a matter of recognizing the theorems of a set of premises—relative to a logic) is to recognize what follows in an “if … then” (antecedent/consequent) sense. Given such-and-such (where such-and-such includes both the (sometimes implicit) logic of a proof procedure and the nonlogical characterizations of a subject area), then so-and-so follows. As a general characterization of mathematical reasoning, this is content-free because anything, nearly enough, can be incorporated into the antecedent.⁴³

This yields, however, an ecumenical characterization of mathematical practice, but at the cost of leaving out the significance of applied mathematics. Given that the application of mathematical discourse is to a subject area that’s characterized, nearly enough, by a grammatically indicative discourse, and given that the applied mathematics is to facilitate the inference of empirical consequences of that discourse, it follows that we don’t want those consequences to occur trapped in conditionals. We need to use the mathematics to draw results from empirical discourse of the form C, that we can apply, and not consequences of the form, A → C, where A is the antecedent mathematics presupposed in the deduction of C from the empirical discourse.

What this requires, in turn, is that applied mathematics (as a whole) needs to presuppose the same logical framework as the empirical sciences it’s applied to. That forces a certain amount of shared content across the branches of mathematics that are applied; in particular, it requires a sharing of the background inferential framework (e.g., first-order logic).⁴⁴

Conclusion and Summary (and Some Further Thoughts)

The original version of the derivation-indicator view (“the derivationist account”—as Tanswell labels it) was intended to explain Agreement and other aspects of mathematical practice in a largely non-sociological fashion. The mechanical recognizability of formal derivations was supposed to be graspable by mathematicians in a sense that would be sufficient to explain Agreement. Restricting the relevant “derivations” to those occurring in purely language-based formal systems (with proprietary vocabulary), however, faces two serious objections because both the logical and nonlogical vocabularies of informal rigorous mathematical proofs are so different from that in language-based formal systems: the too-long objection and the overgeneration problem. The solution I’ve argued for in this paper is to understand the relevant derivations to belong to algorithmic systems that needn’t be pure language-based ones. This allows the indicated derivations to be near or at the surface of mathematical practice, in the sense that the vocabulary (and proof procedures) actually used by mathematicians is already close to what the needed algorithmic systems look like. The key to responding to the too-long objection and the overgeneration problem is to recognize that what’s essential to explaining Agreement is recognizing the mathematician’s use of effectively recognizable proofs, and not by employing mappings of these ordinary proofs to derivations in a formal language with a proprietary vocabulary (e.g., that of set theory).

In the foregoing, I’ve been stressing diagrammatic aspects of informal rigorous proofs as those aspects of these proofs that especially give rise to the too-long and overgeneration objections—but it’s important to realize that what’s important to avoiding these objections is that the surface algorithms of informal rigorous mathematical proof (whether diagrammatic or not) not be replaced (as they are when such proofs are reduced to derivations in standard formal languages). So, for example, one does not replace the computational decision procedures we have with the counting numbers—addition, multiplication, etc.—with Peano arithmetic. Nor does one replace the rules of thumb (the recipes) for evaluating integrals with anything else. These (various) recipes are tied together either by background inferential facts (about how these recipes have been derived) or by the background interpretation of the notation. But in this way the surface algorithms that mathematicians are using (and that are convincing them collectively of the results on the basis of these algorithms) are preserved.

There has long been a picture of informal rigorous mathematical proof according to which any such proof is completed solely by “filling in” missing steps. (This model appears at least as early as Descartes.) Because this model is a semantic one—necessarily, because we had no real syntactic model for reasoning until the late nineteenth century—it pushes anyone in its grip to look for the appropriate derivations to occur in a mathematical framework that’s “conceptually complete.” This in turn motivates foundational programs in which all the appropriate concepts are given (e.g., set theory). Turning one’s attention, instead, to effectively recognizable derivations (of any form) allows the needed derivations indicated by informal rigorous proofs to be conceptually heterogeneous. This does raise the “unification issue” that I take up in the next paragraph and summarize the results of this paper on.

If informal rigorous mathematical proof is allowed to be proof-theoretically heterogeneous, then a coherence issue looms. One wants to know that the identification of mathematical “objects” across different proof-theoretical practices (various functions, operators, numbers, etc.) is the “same” in the sense that theorem results won’t conflict. Transcription of informal rigorous mathematical proofs into a (single) formal language with an intended interpretation can help with that issue. Doing so for this purpose doesn’t face the too-long objection or the overgeneration problem since this transcription isn’t meant to explain Agreement, Rigor, and so on. (Only Techniques is being partially explained in this way.)

I’ll close with some explicit remarks about the opening concerns of this paper. That alternative forms of reason—pace Frege—in principle exist is an indisputable result of the twentieth-century research in logic. One way to establish that first-order logic (or something in its neighborhood) is the appropriate logic for reasoning is to provide a neutral (a logic-independent) notion of “implicational content” and use it to argue that first-order implication is an inferential operation that genuinely adds no “content”: Given A → B, where “→” stands for first-order implication, B has no (logical) content beyond that contained in A. I won’t give further details here.⁴⁵ But with that assumption in place, an argument can be mounted that applying mathematics places a powerful constraint on the tool of inference for the whole package: applied mathematics and the empirical science it’s applied to must have the same background logic, a first-order one.

Regardless of the implications of the remarks of the last two paragraphs, the considerations raised in this paper undercut the claim that the evolution of new informal rigorous mathematical proof techniques all by itself reveals that different notions of “validity” are being developed in ordinary mathematical practice.⁴⁶