III—What can we Mean? on Practices, Norms and Pluralisms

Abstract

I

In his presentation to this Society sixty-five years ago, Michael Dummett (1959) took his initial steps on what became a fifty-year exploration of the connections between truth, logic, the foundations of semantics, and fundamental issues in metaphysics. Dummett’s work on realism and anti-realism was at the centre of active debate from the 1970s to the 1990s. Dummett’s revisionary view of fundamental logical principles is at the heart of this discussion (Dummett 1977, 1991).

According to Dummett, many logical principles are self-justifying on neutral semantic grounds, without prejudging the debate between the realist and the anti-realist.¹ However, not all principles pass muster. In particular, double negation elimination (the step from $¬¬p$ to $p$⁠) is not so harmless. To adopt it involves a metaphysical commitment that skews debate in favour of the realist—or so the story goes. The neutral logical perspective, acceptable to all sides, would be to accept only intuitionistic logic, whose constructive reasoning principles can be justified independently of the debate over realism concerning any subject matter.

The debate over realism and anti-realism and the status of intuitionistic logic reached its peak in the 1980s and early 1990s (Taylor 1987; Wright 1992; see also Green 2002). Fashions change in logic as much as elsewhere, and this disagreement has receded from view. Since the heyday of this debate, philosophical logic has turned to different issues, including vagueness, contextualism and assessment sensitivity, paradox, logical pluralism, whether logic is in any way exceptional among the sciences, and more. Even in Oxford—ground zero for the debate over Dummettian anti-realism—the scene is now dominated by higher-order modal logic, and the whole host of metaphysical concerns that arise (Williamson 2013; Bacon 2023; Fritz and Jones 2024). Almost everywhere, Dummettian concerns are sidestepped, rather than addressed head-on.²

This is reversed in the world of mathematics. In Dummett’s day, the call to adopt intuitionistic logic fell mostly on deaf ears. The tradition of constructive mathematics, in which mathematics is refounded on intuitionistic principles, was, in the second half of the twentieth century, in the minority (Bishop and Bridges 1985; Bridges et al. 2023).

Things are different today, as intuitionistic logic has gained a new foothold in mathematical practice, not directly through the arguments or the example of philosophical logicians, but with the rise of proof assistants (Avigad 2024). A proof assistant acts as a proof checker. It provides both a formal language in which natural language proofs are encoded and a system of checking that the supplied proof is correct (Avigad, de Moura and Kong 2023).

As mathematicians rush to formalize mathematical results in the proof assistants like Agda (Bove, Dybjer and Norell 2009) and Lean (Avigad, de Moura and Kong 2023), the most fundamental and basic logical principles in formalized mathematics are the principles Dummett advocated as metaphysically neutral. Popular proof assistants like Agda and Lean are, at their core, constructivists, reasoning intuitionisticially, while being prepared to countenance additional classical principles as an additional commitment you might make only when needed (see, for example, Avigad, de Moura and Kong 2023, §3.5). So the widespread use of constructive reasoning methods in formalized mathematics is a prompt to revisit decades-old discussions in philosophical logic, with the insight we can gain from this unexpected development.

The questions raised here have wider philosophical interest. The use of proof assistants in mathematics is one example among many of the use of machines as a part of our cognitive activities. Semantics is not just a matter of ascribing meanings to our thoughts and words—it matters at the human–machine interface. How should we understand computational systems’ role in our own practices of explanation, inference and justification? There is scope to revisit Dummett’s concerns about meaning, truth and realism, broadening our perspective to take in the role that computational devices play.

The upshot of all this will not be an argument for anti-realism over realism (or vice versa), or for one logic over another. As a logical pluralist (Beall and Restall 2006), I am inclined to try to understand the kinds of practices we might engage in, and what we can do by taking part in those practices, without necessarily taking practice as somehow correct while the others are incorrect. How do the different things that we do when we reason and argue—and that our devices do when we co-opt them in that process—manage to mean things, and make claims on the world and on each other?

II

There is nothing in the abstract notion of a proof assistant that favours one way of understanding valid proof over another. A formalist about proof could specify some arbitrary system of ‘proof rules’, and a proof assistant programmed to check those rules could check that any given string of symbols supplied to it satisfies whatever the constraints the ‘proof’ checker was designed to check. Contemporary proof assistants are not formalists in this sense. Proof assistants such as Agda (Bove, Dybjer and Norell 2009) and Lean (Avigad, de Moura and Kong 2023) are more opinionated about what kind of thing a proof is, and this is why it turns out that the logic of proof assistants is, at heart, constructive.

Agda and Lean treat proofs as functions, where a valid argument from some premisses to a conclusion is represented as a function using grounds for the premisses to supply grounds for the conclusion. The ground for a conjunction of two propositions consists of a pair, the first element of which is a ground for the first conjunct, the second a ground for the second conjunct. The ground for a conditional statement $(A→B)$ is a function that transforms grounds from the antecedent $A$ to grounds for the consequent $B$⁠. The ground for a universally quantified judgement of the form ‘all $F$s are $G$s’ is also a function, which, given an object (of the relevant type) and a ground for the claim that this object has type $F$⁠, is able to provide a ground for the claim that the object has type $G$⁠. The negation of $A$ is understood as $A→⊥$ where $⊥$ is a given contradictory proposition that never has a ground. So, a ground for the negation of $A$ is a function which can provide, for any ground given for $A$⁠, per impossibile, a ground for $⊥$⁠. So, we can ground the negation of $A$ only when $A$ can have no ground.

This sounds straightforward, at least for anyone familiar with logical vocabulary. Straightforward enough, that is, except for the unspecified notion of ground. What is a ground? A philosopher is interested in this question (Prawitz 2012), but the designer of proof assistants need not take a stand on metaphysics or the epistemology of grounds. As far as logic goes, proofs are functions that combine grounds and supply new grounds from old in regular ways. When it comes to mathematics, the definitions of the basic concepts will tell us what we need to know, structurally, about the grounds of atomic judgements. In fact, in type theory, propositions are just a special instance of the more general class of types, and proofs are a special instance of terms inhabiting those types. Constructive type theory is a general account of types and terms, some of which are propositions and proofs. A proof $π$ from $A$ to $B$ and a function $f$ from $R$ to $N$ are the same kind of thing (Martin-Löf 1985).

The principles arising naturally in type theory are familiar from intuitionistic logic (Heyting 1956; Dummett 1977; Rathjen 2023), and Agda and Lean implement Martin-Löf’s dependent type theory (1985). Since this framework takes the construction of proofs to be a specific case of constructing functions, functional programming languages provide a useful framework for developing proof assistants. So, as mathematicians labour to encode their definitions and proofs in the vocabulary of proof assistants like Agda and Lean, they are learning to express their results in the language of dependent type theory (Escardó and collaborators 2024; Lean community 2024).

Mathematics encoded in this way is constructive. A proof of $A∨B$(from an appropriately determinate background context) may be transformed into a proof of one of the disjuncts, $A$ or $B$⁠. A proof of $∃xϕ(x)$ may be transformed into an algorithm supplying a witness term $t$⁠, where we can prove $ϕ(t)$⁠. Such results are impossible in classical logic, since $p∨¬p$ is a classical tautology, but we cannot prove an arbitrary $p$or $¬p$⁠.³ Classical mathematical theories can tell us that $f$ is a continuous function where $f(0)<0$ and $f(1)>0$⁠, and so that there is some number $r$ between $0$ and $1$ where $f(r)=0$ (this is the intermediate value theorem), but we may be in no position to find $r$⁠.

Mathematicians nonetheless regularly make use of classically valid principles, and proof assistants allow for this by permitting proofs where classicality is an added assumption (Avigad, de Moura and Kong 2023, §3.5). The situation parallels Dummettian semantic anti-realism, where constructive reasoning principles are the neutral agreed-upon core and distinctively classical principles are an optional extra, to be adopted when the metaphysics asks for it.

However, adding classical principles is optional, and distinctively constructive mathematics is possible, where classical assumptions are avoided.⁴ The resulting theorems not only have the distinctive computational properties mentioned above, they also apply to a wide range of mathematical structures, which are of independent interest whether you start out as committed to intuitionistic logic or not.⁵

This well-established, if still minority, practice of constructive mathematical theorizing raises a question. How are we to understand the relation between constructive and classical mathematics? A relatively standard account of the difference is illustrated in Bishop and Bridges’s 1987 monograph on constructive analysis:

[T]ake the assertion that every bounded non-void set $A$ of real numbers has a least upper bound. (The real number $b$ is the least upper bound of $A$ if $a≤b$ for all $a$ in $A$⁠, and if there exist elements of $A$ that are arbitrarily close to $b$⁠.) … If this assertion were constructively valid, we could compute $b$⁠, in the sense of computing a rational number approximating $b$ to within any desired accuracy … (Bishop and Bridges 1987, p. 7)

Here, the thought is that we can prove less when we reason constructively than when we reason classically. Constructive mathematics is a restriction on classical mathematics.

However, we need not think of constructive mathematics as a restriction. Consider, for contrast:

[C]onstructive logic is stronger (more expressive) than classical logic, because it can express more distinctions (namely, between affirmation and irrefutability), and because it is consistent with classical logic. Proofs in constructive logic have computational content: they can be executed as programs, and their behaviour is described by their type. Proofs in classical logic also have computational content, but in a weaker sense than in constructive logic. Rather than positively affirm a proposition, a proof in classical logic is a computation that cannot be refuted. (Harper 2016, p. 104)

Here, constructive mathematics is seen as an expansion of classical mathematics, because more distinctions can be drawn, and the constructive mathematician has more expressive power. For the classical reasoner, $¬¬(p∨¬p)$ and $p∨¬p$ say the same thing, while the constructivist takes them to have different content.

What should we say? Is constructive practice a restriction or an expansion of classical reasoning? In the remainder of this paper, I will attempt to clarify what is at stake in each of these perspectives, by paying attention to proof assistants and what we do with them.

III

Let me start with an analogy. Consider the calculator—a device that plays an essential role in giving us knowledge that we might not otherwise have: when a calculator says that $345×678=233,910$⁠, I thereby learn that $345$ times $678$ is $233,910$⁠. How does the calculator do this? A calculator is more than an abacus or a pencil and paper, which each serve as a memory aid when we do our sums. We use calculators to do sums for us.

We acquire our knowledge of basic facts of arithmetic by way of an education involving counting things, adding collections together, and so learning about addition of numbers, generalizing to multiplication, while also learning some kind of notational system for numbers and methods for doing elementary arithmetic exploiting those representational systems. The details of people’s training will differ, but at root it is difficult to see how someone could learn arithmetic without knowing how to count.

Calculators do not count things. They manipulate patterns—states of the computational system—in ways that we recognize as representing numbers in regular ways. It is enough for our purposes for it to serve as a reliable intermediary and a tool in our counting and calculating practice. It does not need to be able to count five things, any more than an abacus does. But it is necessary that the regularities observed in the action of the calculator can be read by a user as a part of a mathematical explanation, if we want the calculator’s action to play a role in a demonstration that $345×678=233,910$⁠.

Exactly what regularities are required for the actions of a calculator to count as reliably doing arithmetic? The simple answer is that it needs to get arithmetic right. That is true, but since there are infinitely many different arithmetic statements, it is an infinite set of requirements, and one that is, if we leave it in this form, not feasible either to impose in the first place as we build a machine or to check for compliance once a machine is built.⁶ We can check this infinitely large (or even just a stupendously large finite) collection of constraints by verifying that the calculator’s output matches the content of some theory, which can be finitely specified.⁷

What theory might we use? There is more than one candidate, because arithmetic (and our counting practices) can be made rigorous in more than one way. Peano Arithmetic is one familiar scheme. Here, there are three axioms governing the notion of zero and the successor function, which supplies for each number $x$ its successor $sx$⁠.⁸

Then, arithmetic functions on the natural numbers, like addition and multiplication, can be defined recursively:

Since the natural numbers are only those numbers found by starting with zero and taking successive applications of the successor function, we add the principle of induction, according to which if zero has a feature $ϕ$ and whenever a number has $ϕ$ so does its successor, then all numbers have that feature.

If the output of our calculator agrees with the judgements of Peano Arithmetic, it is reliably doing finite arithmetic, no matter how it does this. Such a calculator could be understood as calculating. The theory of Peano Arithmetic is a well-understood regularization and formalization of our arithmetical practice, even though it does not involve any notion of counting or enumerating.

Other formalizations of arithmetic do make some kind of use of a notion of counting. Neo-Fregean formalizations of arithmetic introduce arithmetical concepts by way of a notion of predicate abstraction. For any unary predicate $F$⁠, we have a singular term $♯F$⁠, to be read as ‘the number of $F$’s’, and the key principle governing $♯$ is Hume’s Principle (Wright 1983),

which, using the resources of second-order logic, states that the number of $F$s is the number of $G$s if and only if there is a bijection between the $F$s and the $G$s. Neo-Fregean arithmetic more explicitly corresponds with the conception of numbers as involving counting. With the help of abstraction,⁹ we can introduce the finite numbers using the notion of identity:

We can define addition by first settling $♯F+♯G$ to be $♯λx(Fx∨Gx)$when nothing is both $F$ and $G$ (corresponding to the naive idea of addition as counting two disjoint collections), and continuing from there.

If our calculator’s output agrees with a neo-Fregean theory, it would also count as recognizably doing arithmetic.

There are more formal theories for arithmetic than just these: any theory is an account of possible patterns in which our practices can run. A calculator might implement a neo-Fregean arithmetic, or a Peano Arithmetic, or something else besides. For it to be intelligible as doing arithmetic, there must be some translation between what it is doing and some recognizable arithmetic practice. The same holds for you and me and anyone else who uses arithmetic vocabulary.

These counting practices agree on a great deal, but disagree at the margins. Ask yourself: is there a number $n$ where $n=n+1$? The answer is no for someone whose concept of arithmetic complies with the conditions of Peano Arithmetic,¹⁰ and yes in a neo-Fregean arithmetic, since the number $♯N$ of finite natural numbers satisfies $♯N=♯N+1$—since we can put the natural numbers in bijection with the natural numbers plus one extra thing (recall Hilbert’s Hotel).

It would not be a surprise for a competent user of arithmetic vocabulary to find that their own concept of number simply does not settle the issue of whether a number can be its own successor. On some precisifications of the number-concept (finite ordinal numbers, modelled in Peano Arithmetic), no number is its own successor. On others (cardinal numbers, modelled in a neo-Fregean arithmetic), there are numbers, like $♯N$⁠, the number of naturals, that equal their own successor. Everyday mathematical practice need not settle on one way of understanding the concept ‘number’, and we get away with not distinguishing these concepts in our everyday arithmetical life. We tend not to concern ourselves with abstract generalizations about numbers. Our practices are settled enough, and the general rules are nailed down only when our aims require it—such as when we build an exact arithmetic calculator, start doing abstract mathematics, or get into an argument in the playground about whether there is a biggest number. When we stray into those areas, we need to become more rigorous and define our terms well enough for the task at hand.

So, is it correct to say that there is some number $n$ where $n=n+1$? To get a useful answer to that question, we must be more specific about how we will interpret the word ‘number’ in the question, and our practice is unsettled enough to allow for different ways to settle this issue.

So, suppose I come across a neo-Fregean calculator, which can solve elementary equations. I ask it to solve the equation $x=x+1$⁠, and it returns an answer, $x=♯N$⁠, rather than saying there is no solution. Should I conclude, then, that there is some amount of money I could have in my bank account such that adding one pound makes literally no difference to my balance? Not unless there is some bank that allows for a literally infinite balance. To interpret the results of such a neo-Fregean calculator, we must attend to what such results mean. In neo-Fregean arithmetic, two predicates have the same number if and only if they are equinumerous, and the only numbers so defined that are equal to their own successors are infinite. To interpret the findings of such a calculator, we appeal to the patterns that it instantiates, and use those patterns to understand the significance of the results the calculator produces.

IV

What goes for understanding the counting and calculating functions of devices can also serve for interpreting the function of proof assistants. Just as a calculator does not literally count anything, neither does a proof assistant assert anything. As we have seen, in a proof assistant implementing a dependent type theory, a proof represents a function that takes grounds for the premisses and delivers a ground for the conclusion. I will argue that such a type theory—instantiated by a proof assistant system—stands to our everyday assertoric and inferential practice as a particular formal theory of arithmetic—instantiated by some particular calculating system—stands to our everyday practice of counting and calculating.

To start with, we should consider what we do when we assert. It is no surprise that there are many proposals for how to understand assertion (Brown and Cappelen 2011), but for our purposes it is enough to briefly consider two different kinds of approaches: those describing the function of assertion at the point of production (speaker norms), and those describing it at the point of reception (hearer norms).¹¹  Speaker norms govern the one who asserts: for example, assert only what you know (the knowledge norm), or assert only what is true (the truth norm), or assert only what you believe with justification, and so on; while hearer norms govern what the hearer can do: for example, to assert $p$ entitles the hearer to (a) ask for a justification of the assertion, and (b) to reassert $p$⁠, handing back the request for justification to the original speaker.

Here it is not hard to see¹² how the inferential structure instantiated in proofs as represented in a proof assistant can play a role in allowing the deliverances of proof assistants to satisfy these assertion norms. The proof function shows how grounds of the premisses of an argument may be used to produce grounds for the conclusion (Prawitz 2012). For the human who wants to assert the conclusion, given a context in which the premisses have been granted (and thereby are supposed to have grounds), the proof is available to show how the conclusion follows from the premisses (Restall 2024). So, something proved by a proof assistant becomes apt for assertion, provided that having such a ground is sufficient for knowledge, and therefore truth and justified belief.

So, using the proof to produce grounds, production norms for assertion may be satisfied. Further, the proof of a proposition can be used to fulfil a justification request for the assertion, and there is thereby something with which to answer the hearer who asks for a justification request, or who refers to the proof assistant to justify their reassertion of the claim, should it be questioned. To represent a theorem in a proof assistant is taken as an epistemic achievement, reassuring us that the proof is complete, and so it can play the justificatory role when called upon.¹³

In the context of our attempt to understand the difference between constructive and classical logic, we cannot stop here. Our point of contention is not primarily about what can be proved with the aid of a proof assistant, but what cannot be so proved. When we learn that some result—such as the intermediate value theorem, mentioned above—cannot be given a proof in a proof assistant without making explicit classicality assumptions, does this have any significance? To answer this question, we should return to what, precisely, the proof assistant is doing, in the same way that if a calculator tells us that there is some number $x$ where $x=x+1$⁠, we should attend to what theory the calculator is encoding. What is the corresponding account of the constructive invalidity of the intermediate value theorem?¹⁴ It is that there is no function that supplies, for each continuous $f:[0,1]→R$ where $f(0)<0$ and $f(1)>0$⁠, a ground for the claim that there is some $x∈(0,1)$ where $f(x)=0$⁠. Further, there are different constructive mathematical ‘universes’ inside which this formulation of the intermediate value theorem can be refuted, while there are other models (including classical spaces) inside which the theorem holds.

This result has epistemic significance, if the standards of evidence appropriate in the discussion are appropriately high. When we do constructive mathematics, the standard of evidence asks for constructive grounds, and proof assistants using dependent type theory model such grounds.¹⁵ So, if a claim fails to have those grounds, it may be rejected as out of bounds for not having met the appropriate standard of assertion. A bald assertion of an instance of the law of the excluded middle, $p∨¬p$⁠, in the context of a constructive proof may ruled out, since no grounds can in general be provided, as any such ground brings with it means to ground $p$⁠, or to ground $¬p$⁠, and there is no way to do this in general.

So, constructive mathematics is recognizably a kind of assertoric and inferential practice in which claims are made, and constructive proof is the coin by which assertions are justified. With proof assistants based on dependent type theory, many mathematicians are becoming fluent in constructive proof, and the practice is emerging into the mainstream of mathematics.

Note that nothing in this explanation of the rise of constructive mathematics leads inexorably to favouring mathematical anti-realism over realism. The importance and usefulness of the constructive practice is motivated on internal mathematical grounds, and not by any view of the metaphysics of mathematics (Bauer 2017).

V

However, constructive mathematics is not the only way that the norms of mathematical proof are made precise. The majority tradition in mathematical reasoning remains classical. A lot of everyday mathematical reasoning appeals to the law of excluded middle and other non-constructive reasoning principles. These principles are found everywhere, both in mathematics and in philosophy. Consider this recent philosophical monograph:

It is unclear whether there is here a genuine disagreement between Gadamer and Davidson. It is undeniable that someone may lack a concept that others have, and that we now have many concepts that no one had three hundred years ago. New concepts are continually introduced. They cannot always be defined in the existing language, but they can be explained by means of it; a study of how we acquire concepts, such as the concept of infinity, that could not even be expressed before their introduction would be highly illuminating. It is also undeniable that we can now recognize, of certain concepts that were used in some previous age, that they were incoherent or confused. (Emphasis mine)

Here, the author is treating it is undeniable that as an intensifier, twice in quick succession. It would be a strange thing, in the context of this discussion, were one to agree with the author and continue: ‘Yes, I cannot deny that someone may lack a concept that others have … but I do not see why it follows that I should grant it.’ Yet the claim that it is undeniable that  $p$ is a form of double negation, since the denial, $¬p$⁠, is ruled out. The natural reading is to take the author to be committed to the inference, here, from $¬¬p$ to $p$⁠.¹⁶

We need not treat this as a mistake: it is appropriate, in the given context. Here is one way to understand that context. It is very natural to think that there is a certain kind of discourse in which we seek to settle issues. We want to know whether $p$ holds or not, and to rule out one of these options out is to leave the other. In this course of reasoning, the author asks us whether someone may lack a concept that others have … or not. The no case is ruled out, and so only yes remains. It wins by being the last option standing, not necessarily because it has been given any positive (constructive) ground. This move—according to which showing that something is undeniable is enough to show that it is true—is at the heart of a certain kind of deductive reasoning,¹⁷ and we make this move time and again in our thought and our talk, even if we also practice constructive mathematics, in which we refrain from applying double negation elimination.¹⁸

Rather than asking whether the classical practice of inference is correct or not, let’s consider what this practice is good for and what it isn’t—by analogy with the fact we are doing different things when we use cardinal numbers and when we use ordinals.

‘Issue-settling’ discourse is fundamentally bilateral (taking yes and no, or assertion and denial, on a par).¹⁹ Since $p∨¬p$ is undeniable (as we saw above), it follows that we have grounds for $p∨¬p$⁠. We have not suddenly been able to ground one disjunct of $p∨¬p$ or the other—we have settled it only because it is undeniable, and not necessarily because we have any positive ground for $p$ or for $¬p$⁠. Restricting ourselves to classical inference (and imposing the bilateral inference norms) means that we might be in a position to assert a disjunction without possessing a ground for either disjunct. Similarly, we may categorically classically prove $∃xϕ(x)$ without thereby finding some term $t$ where we can prove $ϕ(t)$⁠, but rather by showing that $∃xϕ(x)$ is undeniable.

What we lose in terms of the constructive power of assertion, when adopting classical reasoning principles, we gain in the ability to express denial. Consider some domain of constructive mathematics and some proposition $A$⁠, where we have no ground for $A∨¬A$⁠, and furthermore, we know that we have no ground. Then someone asks us the question: is it the case that $A$? What can we say? We cannot answer yes (since $A$ has no ground) and we cannot answer no (since $¬A$ has no ground). Our constructive theory will have some models where $A$ holds (since $¬A$ fails, $A$ is at least consistent with our theory), and some models where $¬A$ holds (since $A$ fails, $¬A$ is consistent with our theory), but the fact that our theory has two extensions, one where $A$ holds and another where $¬A$ holds, does not mean that our indecision about $A∨¬A$ is a matter of ignorance, to be settled with more information. Such ignorance is consistent with a classical theory, in which $A∨¬A$  is true, but our theory does not decide on which disjunct holds. The constructive reasoner wants to be able to rule  $A$  out, without going so far as to say that $¬A$ is true. But to do this, constructively speaking, requires semantic ascent—we can say $A$ is not proved, or $A$ is not known, or some such thing.²⁰ But this, it seems, changes the subject from whatever it was we were talking about when asking whether $A$ holds. We have not answered the question about whether $A$ or not, we have only said something about our state of knowledge, or of our theory. If I restrict myself to constructive reasoning about some domain, I can only go so far in describing what is going on with the phenomena at hand.

So, proof assistants based on dependent type theory—and their uptake by the mathematical community—show that there is a recognizable and intelligible assertoric and inferential practice that is essentially constructive. Yet this does not mean that classical mathematical practice is to be left behind, any more than the existence of ordinal numbers means that we should no longer use cardinal numbers, or vice versa.

VI

We return, then, to the divide between realism and anti-realism, which was Dummett’s original concern. Some classical mathematicians express their preference for classical mathematics in realist terms: their theory says that $A∨¬A$⁠, and they would like to discover which disjunct is true, because the mathematics is really one way or the other. They are studying the numbers (the sets, the topological spaces, or whatever else), and the success criterion is whether those descriptions are correct, not whether we are able to construct grounds for our claims.

There is something to this intuition: if we picture the phenomena in this way, we implicitly treat each issue as in fact settled, and so treating all our claims as issues that may be settled one way or the other is appropriate. Realism motivates classical reasoning. To restrict the grounds for our reasoning to what can be explicitly and positively constructed when the phenomena at hand might exceed our grasp is an artificial restriction if the aim is correct description. However, you can be as realist as you like about the mathematical universe and still see the value of constructively theorizing about that universe. Here we return to the first of the two perspectives on constructive mathematics mentioned above. On this view, we may not be able to constructively prove all the classical facts about mathematics: constructive mathematics is a restricted subset of classical mathematics, with its own distinctive virtues.

The reverse connection between realism and classical reasoning is harder to establish. There is no reason to think that classically reasoning about a phenomenon involves some implicit realist commitment to it, over and above what is incurred in constructive reasoning. It is well known that we can take a constructive theory (say, of arithmetic, thought of as a construction of the thinking subject, and not the description of some independently existing ‘realm’), and find inside it a perfectly classical theory, if we focus on the settleable issues (the sentences of the form $¬A$⁠).²¹ When we might say in our native constructive tongue $A∨B$⁠, we instead say the classical substitute, $¬(¬A∧¬B)$⁠. When we might say $∃xϕ(x)$⁠, we say $¬∀x¬ϕ(x)$⁠. And so on. As far as a classical semantics of disjunction and the existential quantifier goes, this makes no difference, but the result is a constructive vindication of classical reasoning about this domain, at the cost of making claims that are weaker than their constructive counterparts. If there was no controversial metaphysical commitment before, we have incurred no new commitments, because we make no new claims. The constructivist can translate the classical theoretical commitments into their own tongue at no theoretical or metaphysical cost. We have here a vindication of the second perspective on constructive mathematics mentioned above: we can constructively recover classical theorems when we isolate the classically behaving propositions inside our constructive theory.

VII

So, if all this is correct, when we say $p∨¬p$⁠, is what we have said true? Here this depends on how we are taken. To take something to be true is to evaluate it. Speech is communicative, requiring speaker and audience. If the audience treats our claim constructively, it may have no proof, and thus fail to meet its mark. Note, though, that to say that it is not the case that $p∨¬p$ would be to exceed those very same constructive bounds, since we have no grounds for $¬(p∨¬p)$ either. If we treat the claim $p∨¬p$ as expressing an issue to be settled, with all the classical norms of reasoning applying, then the answer is yes. It is true, since it is undeniable.

Notice, though, that to ask the question of whether $p∨¬p$ is true is just to ask about whether $(p∨¬p)$⁠. The question has been asked, and we are in the business of evaluating it. To evaluate it well, it seems best to pay close attention to the norms we apply, and to reflect on whether we want them to apply, instead of taking only one set of evaluative norms as given.²²

References

Footnotes