The following is an essay I wrote in 2023 for a course in philosophy of mathematics as an undergraduate in Computer Science Philosophy at Oxford. Like my essay [[On the Origin of Theories]], its one of my pieces of philosophical writing from that time of which I'm most proud, and whose philosophical conclusions I by-and-large continue to believe and follow in my own work. The essay deals with arguments for and against the philosophy of *intuitionism* and related *constructivist* philosophies of mathematics. As a practicing computer scientist who works primarily with constructive systems of logic/mathematics (proof assistants, etc.) I obviously care a great deal about constructivity. However, I am, at heart a pragmatist regarding choice of logic (c.f. my [[Tractatus]] for my opinions on whether there is any such thing as "one true logic,") and so I sought to give a fair appraisal to both constructive and classical mathematics, and to show how, contrary to appearances, they are not as opposed to one another as they may initially seem. --- ## A Constructive Critique of Constructivism by Corinthia Beatrix Aberlé May 12, 2023 The mathematical philosophy of *intuitionism* advocates a radical reconception of the validity of certain mathematical inferences, and accordingly, the very logic by which such inferences are made. To infer the truth of a proposition from the falsity of its negation, i.e. to infer the proposition from its double-negation, may seem the most natural thing in the world, but the intuitionist urges that by a principled reflection on (what they claim as) the nature of mathematics and logic, we shall ultimately find such *non-constructive* modes of inference to be illegitimate. Yet, curiously, intuitionistic logic – in its most common forms, at any rate – admits many inferences that seemingly have much in common with the *verboten* non-constructive patterns of inference: e.g. although one cannot intuitionistically infer a proposition from its double-negation, one *can* intuitionistically infer a negated proposition from its triple-negation. One wonders, then, to what extent intuitionist critique of classical mathematics and logic can be justified, and not end up undermining itself, in the presence of such commonality. Toward answering such questions, let us begin with an examination of some of the principal motivations for intuitionism. Within the canons of classical mathematics, one finds all manner of strange and fantastical theorems. From Banach and Tarski, one learns how to divide a sphere into finitely many pieces that may be recombined in such a way as to produce two identical copies of the original sphere. Von Neumann, meanwhile, teaches how to break a square into parts which may be deformed by area-preserving transformations into shapes both having the same size as the original square. Such results may strain credulity, but the classical mathematician will assure us that this is only due to our limited ability, as finite creatures, to comprehend the kinds of infinitistic constructions that underlie their proofs. Yet there remains something unsettling about these examples – their proofs all depend critically upon methods of reasoning whereby one establishes that something is the case without showing *how* it is the case. In fact such reasoning abounds in ordinary mathematics, and is based precisely in such modes of inference as the above-mentioned double negation elimination. To establish the existence of some mathematical object within classical mathematics, it suffices merely to show that its non-existence would be contradictory, rather than providing a definite construction of the object – it is in this sense that such inferences are *non-constructive*. The more disquieting one finds such reliance on non-constructive modes of inference, the more one may be inclined to reject the ordinary logic of mathematics and seek a *constructive* alternative; for (one might argue) mathematics is the result of *human* activity, that yields definite knowledge only insofar as it furnishes definite constructions that can, at least in principle, be witnessed by a human mind. This is the principal objection leveled against classical mathematics by the intuitionists, who claim that the reliance of such counter-intuitive results as the Banach-Tarski Theorem upon non-constructive methods of reasoning ought to cast doubt on the legitimacy of employing such methods in mathematics. Though prefigured in the views of mathematicians such as Kronecker and Poincaré, intuitionism as a full-bodied philosophy of mathematics emerged under the pen of L.E.J. Brouwer, who advocated a Kantian conception of mathematics in which mathematical truths are *a priori synthetic* – *synthetic* in that they are the result of *construction* (not merely true by definition, nor due to some mind-independent platonic reality), and *a priori* in that such construction, at least in principle, takes place entirely ‘in the human intellect’, grounded in our intuitions of *space* and *time* (c.f. Brouwer, 1912). Though not widely accepted by working mathematicians, intuitionism has hung on in pockets of research over the years, occasionally attracting the interest of a stray few mathematicians (to name some: Kolmogorov, Bishop, Martin-Löf, Voevodsky) and increasingly, computer scientists. Philosophical interest in intuitionism was revived in the 1970s by Michael Dummett, who advanced a more linguistically-oriented justification of intuitionism than Brouwer, based instead in the doctrine of *meaning as use* (where the *use* of mathematical/logical terms is here to be thought of as their *role* in communication, c.f. Dummett 1975, p. 216). What these accounts of intuitionism have in common is their exclusive endorsement of constructive patterns of inference over non-constructive inference, such as double-negation elimination, on the grounds that the former are somehow more directly intelligible to us than the latter. As previously indicated, the problems posed by intuitionism cut deep into the body of mathematics, for the very logic in which ordinary mathematics is couched (classical logic) is rife with non-constructive modes of inference that must, on the intuitionist's view, be eliminated from mathematics if it is to count as a legitimate source of knowledge. Is such intuitionist critique of classical mathematics and logic justified? Do the alternatives posed by intuitionists fare any better, by their own standards? My answer to these questions is mixed: there are good reasons for adopting intuitionistic logic over classical logic, at least in certain situations, but these are by and large *not* the reasons that have been advanced in favour of intuitionism in the philosophical literature. Rather, the best arguments in favour of intuitionistic logic are of a more pragmatic character, having to do with applications of intuitionistic logic to the study of central mathematical notions such as computability, geometry/topology, etc. More generally, I claim that any justification for choosing either one of intuitionistic logic or classical logic over the other as the basis for mathematics must be pragmatic in nature, for there is a sense in which these two logics are but two sides of the same coin. To argue as much, I shall first consider in some detail the intuitionist conceptions of logic and mathematics and how they depart from their classical counterparts, before critically assessing some of the main arguments that have been made for and against intuitionism. ## Constructive logic and mathematics A fruitful point of departure for distinguishing classical logic from intuitionistic logic lies in how the meanings of the logical constants are explained under each conception. For the classical logician, the meanings of connectives, quantifiers, etc., are established by specifying conditions under which propositions involving such constructs are to count as true. The intuitionist, on the other hand, explains the meaning of complex logical sentences by specifying how such a proposition may be *proved*. In both classical and intuitionistic logic, the semantics of the logical vocabulary is compositional – the meaning of a compound formula (in terms of truth-conditions or proof, respectively) is a function of the meanings of its subformulae. Along these lines, the truth-conditions of classical logic are usually given by way of Tarskian semantics, e.g. * $\phi \wedge \psi$ is true if and only if $\phi$ is true and $\psi$ is true. * $\neg \phi$ is true if and only if $\phi$ is false. * $\exists x \phi(x)$ is true if and only if $\phi(a)$ is true for some object $a$ in the domain of discourse. On the other hand, attempts by the Brouwerian school at specifying the intuitionistic notion of *proof* ultimately led to the development of the so-called Brouwer-Heyting-Kolmogorov (BHK) interpretation of intuitionistic logic: * $\bot$ (falsity) has no proofs * a proof of $\phi \wedge \psi$ is a pair consisting of a proof of $\phi$ and a proof of $\psi$ * a proof of $\phi \vee \psi$ is either a proof of $\phi$ or a proof of $\psi$, along with some indication of *which* of $\phi$ or $\psi$ is thereby proved * a proof of $\phi \to \psi$ is a process or procedure for obtaining a proof of $\psi$ from any proof of $\phi$ * a proof of $\exists x \phi(x)$ is a pair consisting of an object $a$ in the domain of discourse and a proof of $\phi(a)$ * a proof of $\forall x \phi(x)$ is a process or procedure which, given any object $a$ in the domain of discourse, produces a proof of $\phi(a)$ * $\neg \phi$ is treated as synonymous with $\phi \to \bot$ (c.f. Troelstra & van Dalen 1988, Vol. 1, ch. 1 $\S$ 3). The BHK interpretation is not wholly precise, since some of its central notions (namely that of *process/procedure*) are left unspecified. Such indeterminacy is not necessarily of concern to the intuitionist – Brouwer himself resisted all attempts at the full formalisation of intuitionist logic, on the belief that human intuition transcends any formal system. Brouwer would likely have thought of the terms 'process' and ‘procedure’ as covering everything that could reasonably be grasped by the human mind as a process/procedure. From an altogether different perspective, it is the very underdetermination of these fundamental concepts of intuitionism that gives intuitionistic logic its edge – by varying the interpretation of the concept of *process/procedure* at play in the above (e.g. by interpreting 'process' to mean *computable function*), one is able to give diverse semantic interpretations to intuitionistic logic. For traditional intuitionism, then, so long as there is such an interpretation that makes the attendant notion of proof suitably *apprehensible* to us (e.g. by way of mental construction), this justifies intuitionistic logic as such. As Dummett (1977, $\S$ 1.2) notes, such apprehensibility of proof is critical to the intuitionist project, both in that it explains how such proof is grounded in the faculties of the human intellect, and in that it constitutes an explanatory *advantage* of the intuitionistic account of mathematics and logic over the classical – having explained what it is for a proposition to be true, the classical logician has yet to indicate whether and how such truth may become knowable to us, or indeed be of any practical significance. Whether or not intuitionism really enjoys such advantages remains to be seen. Nonetheless, despite its informality, the BHK interpretation is capable of illuminating key differences between classical and intuitionistic logic and mathematics. Implicit in the classical notion of *truth* is the idea that every proposition is either true or false. From this, one immediately obtains the classical validity of double-negation elimination: if a proposition is not false, then it is true. By the same token, one obtains the classical Law of Excluded Middle (LEM): for every proposition, either it or its negation is true. It can be shown, in fact, that adding either one of double-negation elimination or LEM to intuitionistic logic as an axiom renders the other provable (and in fact makes the resultant logic equivalent to classical logic, c.f. Burgess 2009 $\S$ 6.4). Hence an argument against the intuitionistic validity of LEM suffices also as an argument against the intuitionistic validity of double-negation elimination. In order to intuitionistically affirm the LEM, it would have to be the case that for every proposition, either it or its negation is not merely true, but *provable*. Moreover, in order to be able to prove LEM *in general* (i.e. for every proposition $\phi$) we must, per the BHK interpretation, have some general method or procedure for determining which of $\phi$ or $\neg \phi$ (i.e. $\phi \to \bot$) is to be proved, but per Church and Turing’s negative solutions to the *entscheidungsproblem*, provability of formulae in first-order logic (FOL) is *undecidable* – there is no effective procedure for determining whether an arbitrary proposition of FOL is provable. The intuitionist therefore rejects the validity of LEM, as well as any classical validities that would imply LEM, such as double-negation elimination. Intuitionistic mathematics proceeds atop intuitionistic logic analogously – appealing to the BHK interpretation (or a similar semantic interpretation) as a criterion for determining which mathematical axioms are constructively acceptable and which are not. For instance, one may determine that a mathematical axiom is not constructively valid by showing that the candidate axiom would imply a non-constructive axiom such as LEM, if added to an otherwise constructive mathematical theory. The Axiom of Choice (e.g.) can be shown to imply the LEM when added to constructive forms of set theory (Diaconescu 1975), and is therefore rejected from intuitionistic set theory. Further deviations from classical mathematics have at times been prompted by some intuitionists’ (particularly those of the Brouwerian school) scruples over the treatment of completed infinities in mathematics – the thought being that human intuition cannot apprehend an infinite totality. Such intuitionists have thereby been led to adopt alternative formalisations of e.g. real analysis, which depart radically from their classical counterparts. Brouwer was able to argue, on intuitionistic grounds, that all functions $\mathbb{R \to R}$ are continuous, in (seemingly) outright contradiction of classical real analysis, where discontinuous functions abound. In these cases, intuitionistic mathematics is no longer simply a weaker subset of classical reasoning. However, such departures from classical mathematics are not *as* universally accepted amongst practitioners of constructive mathematics (e.g., Bishop, who took great pains to ensure his constructive treatment of analysis was consistent with classical mathematics, c.f. Bishop 1967). Having considered the ways in which intuitionistic logic and mathematics depart from their classical counterparts, we are now in a position to assess some of the central arguments that have been made, both by intuitionism's proponents, and its detractors. Let us therefore return now to both Brouwer and Dummett's arguments for rejecting classical validities on intuitionistic grounds. ## Against intuitionism The classical mathematician may cede that intuitionistic modes of reasoning – at least those that form a subset of classical reasoning – are of some special interest due to their constructive nature, while maintaining that classical logic on the whole remains sound. In advocating the abandonment of e.g. double-negation elimination, the intuitionist must produce reasons for regarding such principles as illegitimate. Brouwer had his Kantian reasons, and Dummett his linguistically-motivated reasons in favour of such a rejection. Let us consider each of these in turn. Brouwer’s renunciation of classical logic rested in his conviction that (at least in mathematics) ‘there are no non-experienced truths’ (Brouwer, 1949). One who did not share Brouwer’s convictions – a believer in a mind-independent mathematical reality, or one who considers mathematics a pragmatic fiction, say – would not be swayed by such arguments. Viewed even on its own terms, however, Brouwer's Kantianism about mathematics is questionable in its foundational coherence. Kant (1781, A716-717/B744-745) claimed that our intuition of space provided the basis for the assumptions of geometry, which in Kant's time was specifically *Euclidean* geometry. With the advent of non-Euclidean geometry in the 19th century, and its prosperous application to the description of spacetime in the theory of General Relativity in the following century, however, a dilemma emerges for the Kantian/Brouwerian intuitionist. One must either suppose that our intuition of space is not exclusively Euclidean, as it may have once seemed, in which case the purported *apprehensibility* of such intuition becomes dubious, or one must admit that our intuitions of e.g. space may lead us astray from scientific insight, in which case it is questionable whether such intuition can serve as a reliable basis for mathematics. Brouwer, to his credit, was sensitive to this objection, but drew from it only the lesson that spatial intuition should be discarded in favour of *temporal* intuition as the basis of mathematical reasoning (Brouwer 1912, p. 80). But who is to say that Brouwer's own proffered intuitions of *process*, etc., are any less suspect? Dummett, meanwhile, staked his argument for intuitionism in the idea that the intuitionist account of the meaning of logical terms (i.e. BHK) is the correct such account under the conception of *meaning as use* (Dummett, 1975). By Dummett’s own admission, a broad, holistic reading of *meaning as use* would lend itself just as much to a justification of the classical explanations of the meanings of logical terms. Under such a conception the (classical) meanings of the logical constants are simply their use in the language-games of classical logic and mathematics as determined by the ordinary truth-conditional semantics. Dummett therefore argues for a narrower conception of *meaning as use* whereby each element of the logical vocabulary has associated with it definite and publicly observable criteria for its *correct* use in language, that exhaustively determine its meaning. Some, such as John Burgess (1984), have charged that such a conception of meaning lapses into a kind of behaviourism which puts Dummett at odds with our current understanding of linguistics and psychology. However, even without getting into the weeds of the philosophy of language, there is a fatal objection that may be raised to Dummett's (and, by the same token, Brouwer's) rejection of classical reasoning, which is that classical logic is – in a certain, precise sense – *contained within* intuitionistic logic, and so any claim of greater coherence for the latter over the former is self-defeating. A key theorem to understanding the precise relationship between intuitionistic and classical logic is the following, due originally to Glivenko: a formula $\phi$ of propositional logic is classically true if and only if its double negation $\neg \neg \phi$ is intuitionistically provable (notably, this theorem is provable even in an intuitionistic metatheory). This theorem serves as the basis of so-called *double-negation* translations, whereby any theorem of classical logic may be converted into one of intuitionistic logic (analogous translations exist for first-order logic, due to Gentzen & Gödel, and Kuroda, respectively, which are somewhat more complicated in details than Glivenko's but essentially similar, c.f. Troelstra & van Dalen 1988, Vol. 1, ch. 2 $\S$ 3). The upshot of all this is that an argument such as Dummett's that intuitionistic logic is somehow more meaningful or apprehensible to us than classical logic is no argument at all – for classical propositions enjoy just as much meaning/apprehensibility as do their intuitionistic double-negations. It is instructive to think of double-negation in intuitionistic logic as a kind of modality (in the sense of modal logic) – specifically a modality of *logical possibility*. This is consistent with the BHK interpretation, whereby a proof of the double negation of a proposition $\phi$ is a procedure for obtaining a proof of falsity from a proof of the negation of (i.e. a counterexample to) $\phi$. Since we expect there to be no proofs of falsity, we should therefore expect there to be no counterexamples to $\phi$, so we are free to assume $\phi$ without fear of contradiction. Thus, the classical logician could well accept either of Brouwer's or Dummett's positions concerning the nature of human understanding, yet still count their use of classical logic as legitimate, by simply claiming that they are principally interested in mapping out the space of such *logical possibility*, and hence (implicitly) working within the modality thereof in their logic. More broadly, I want to suggest that it is simply incorrect for proponents of intuitionistic logic/constructive mathematics to view their classical counterparts as something to be opposed – as we have just seen, the use of classical logic is entirely commensurate with intuitionistic methods, and indeed forms a part thereof. Classical mathematicians do their constructive brethren a great service by forging ahead into the uncharted mathematical territory of logical possibility, laying out paths for constructive mathematicians to follow in seeking constructive proof. ## In defense of intuitionism Intuitionists thus have ample reason to consider classical reasoning a legitimate and worthwhile part of logic and mathematics, even if they do not consider it the *whole* thereof. Yet if the intuitionist cannot claim that their logic enjoys any greater meaningfulness or apprehensibility than classical logic, is there any reason to constrain oneself to intuitionistic logic and constructive mathematics, or does this have all the effect, as Hilbert put it, of denying a boxer the use of his fists (Hilbert 1927, p. 476)? Having argued that classical reasoning is after all an integral part of intuitionistic logic and mathematics, I now seek to argue that the reverse is also true. That is, beyond the trivial sense in which e.g. intuitionistic logic is contained within classical logic, there is a much deeper sense in which classical mathematics itself gives rise to intuitionistic reasoning: many topics of central concern in (classical) mathematics, such as computability, geometry/topology, etc., are naturally described in terms of intuitionistic logic, in a manner that allows one to reason about such mathematical phenomena at a greater level of clarity and generality. Thus, I claim, it is better not to view intuitionistic logic and classical logic as separate, but rather as entwined parts of the greater whole of logic, so that questions of which logic to use are ultimately pragmatic questions of where to focus one's attention within this logical constellation. To argue as much, I shall present two main examples of mathematical domains where intuitionistic logic proves useful: 1) the study of computability in terms of typed $\lambda$-calculi, and 2) the study of differential geometry via non-standard analysis. The basis of the connection between computation and intuitionistic logic is the so-called Curry-Howard Correspondence, which broadly shows that the *types* of programs in certain computational formalisms correspond exactly to logical propositions in certain (constructive) logics, with the programs inhabiting those types corresponding to proofs of their respective propositions. The correspondence was laid out formally by William Howard (and prefigured in remarks of Haskell Curry) who established that the structure of proofs in intuitionistic natural deduction is isomorphic to that of Alonzo Church’s Simply Typed $\lambda$-Calculus (Howard, 1980). The original correspondence was established for propositional logic, but has since been extended to predicate logic and higher-order logic. Moreover, the correspondence is essentially what would be suggested by the BHK interpretation: a proof of $\exists x \phi(x)$ (where $x$ ranges over natural numbers, say) in intuitionistic natural deduction corresponds to a term in typed $\lambda$-calculus that calculates some number $n$, along with a further program inhabiting the proposition/type $\phi(n)$. The upshot of such a connection between logical formalisms and computational formalisms is that this allows for theorems about such logics to be translated into theorems about computation, and vice versa. For instance, methods of showing that such logics are consistent (e.g. cut elimination), can be adapted to show that the corresponding $\lambda$-calculi are strongly normalising, i.e. every computation terminates and yields a result in *normal form*. In conjunction with the theorem that normal forms in $\lambda$-calculus are unique, this constitutes a powerful vindication of the intuitionist’s aspirations for constructivity – from an intuitionistic proof of any proposition one can extract a definite, terminating procedure for producing a uniquely-specified computational artifact witnessing the truth of the proposition. Moreover, one may bring all the power of computer science to bear on putting such computational artifacts to good use in the applications we make of logic and mathematics. Notably, it is precisely the fact that non-constructive principles such as LEM are not generally valid in intuitionistic logic that enables such a translation of intuitionistic proofs into computable procedures – as we have seen already, an intuitionistic 'proof' of LEM would necessarily correspond to something uncomputable. Thus, the seemingly stricter rules of intuitionistic logic prove in this sense to be more flexible than those of classical logic, in that they admit semantic interpretations – in terms of e.g. computability – that are incompatible with classical logic. This is all well and good, but a mathematician whose concerns have nothing to do with computability may yet argue that while intuitionistic logic may be of interest to *computer scientists*, classical mathematicians yet have no compelling reason to venture outside of classical logic. Against such a view, I now seek to present an example of intuitionistic logic's utility that ought to hit closer to home for (classical) mathematicians, which is the striking appearance of intuitionistic logic within certain domains of geometry & topology. A central aspect of the connection between intuitionistic logic and geometry is the category-theoretic concept of a *topos*. This concept, originally introduced by Grothendieck in the study of algebraic geometry, and subsequently developed (in the slightly more general form of what is known as an *elementary topos*) by Lawvere in the realm of categorical logic, encompasses a broad class of ‘universes’ of mathematical objects, including various notions of *space* arising in geometry and topology. Notably, in any topos, the *subobjects* of a given object (e.g. the subspaces of a given space) obey a logic similar to that which governs the lattice of subsets of a given set. Thus each topos possesses an *internal logic* of its own. Indeed, sets form a topos, whose internal logic (in classical mathematics) is classical (i.e. power sets are Boolean algebras), but this is rather exceptional, and the internal logic of toposes in general is in fact precisely higher-order intuitionistic logic (in particular, the lattice of subobjects of an object in a topos is generally a [Heyting algebra](https://en.wikipedia.org/wiki/Heyting_algebra), but not necessarily a Boolean algebra). Roughly speaking, the internal logic of each topos is the interpretation of intuitionistic logic one obtains from the BHK interpretation by specifying the notion of procedure/process employed therein as *structure-preserving transformation* for the appropriate notion of *structure* of the objects of the ambient topos (c.f. Lambek & Scott 1986, Pt. II). This fact has many profound consequences – too many to cover in the remainder of this essay. I shall present but one such consequence, which is that intuitionistic logic thus enables an elegant treatment of nonstandard analysis with application to the study of smooth manifolds, which goes varyingly by the names of *smooth infinitesimal analysis* and *synthetic differential geometry*. Synthetic differential geometry (SDG) arose out of efforts by Kock and Lawvere to axiomatise the internal logic of certain toposes of *smooth spaces* (smooth manifolds in particular). This led to the definition of a *smooth topos* as a topos possessing appropriate structure to express statements of analysis and differential geometry in its internal logic, such that many natural categories of spaces equipped with an appropriate notion of 'differentiation' come out as smooth toposes, in this sense. Curiously, the form of analysis one is able to express within a smooth topos is a kind of *non-standard analysis*, where e.g. the derivative is defined in terms of *infinitesimal* quantities, rather than limits, as in ordinary analysis. More strikingly still, the infinitesimals in a smooth topos have the following key property: they are quantities that are (in the internal logic of the topos) *not not equal to zero*[^1] (c.f. Bell 2003, p. 5). [^1]: In this sense, Berkeley's pejorative description of infinitesimals as 'ghosts of departed quantities' was not far off the mark, for what is undeath but the double-negation of life? In order for the characterisation of infinitesimals in SDG to be non-trivial, it must therefore not generally be the case that a proposition is logically equivalent to its double-negation in the internal logic of the ambient topos, i.e. the logic must be intuitionistic, rather than classical. More generally, one finds echoes of intuitionistic ideas throughout SDG, for instance: in (the logic of) SDG, not only is every function from the real line to itself continuous, as Brouwer argued, in fact every such function is *smooth* (i.e. infinitely differentiable). Adopting this approach to the treatment of infinitesimals, smoothness, etc., thereby allows one to use such properties in proving various statements of analysis (which often enables cleaner/more direct proofs than the corresponding proofs in terms of limits) and then cash these out into theorems about the objects of *any* smooth topos, including, in particular, smooth manifolds. Here again we see that the strictness of intuitionistic logic buys it a greater semantic flexibility than classical logic, and in this case, the rewards of such flexibility are significant, even for the mathematician who takes no interest in constructivity or computability. A final point to be made in reference to the above example is how it demonstrates a degree of contingency in our current preference for classical logic in mathematics. Time was when infinitesimals and classical principles such as LEM and double-negation elimination uneasily coexisted within mathematics. In response to the foundational crises experienced by mathematics over the course of the 19th and 20th centuries, the mathematical community generally chose to uphold classical logic and dispense with infinitesimals. But it could have been otherwise. E.g., writing in the late 1800s & early 1900s, Peirce speculated that a proper treatment of the continuum (with infinitesimals) might require abandoning the Excluded Middle (Peirce, *Collected Papers* 6.168). Had such a conception of the continuum proved more influential, our current mathematical foundations could very well have come to resemble something like SDG, in which case our underlying logic would after all have been intuitionistic, rather than classical. Moreover, the existence of models for SDG within classical mathematics shows that such an alternative choice of foundations would have been every bit as consistent as our current mathematical theories. This is not to say that the choice of classical over constructive foundations was incorrect, but only that it was – to an extent – arbitrary. What I have sought to argue is that intuitionistic and classical logic/mathematics are not related to each other as opposing forces, but rather are to one another like Escher's Drawing Hands: each begets the other. For this reason, there is no place for arguments that one logic enjoys primacy over the other. The dogmatic intuitionist and the dogmatic classical mathematician who each cast aspersions on the other's methods are thus of a kind in that they both fail to recognise how each other's logic is reflected in their own, and both are the worse off for it. Returning, then, to Hilbert's comments about intuitionism, we may identify two counts on which Hilbert was mistaken. Mathematics is not like a boxing match or even a series of such matches – it is rather like the enterprise of martial art itself, a practice made up of diverse techniques built up and passed down over generations. And intuitionistic logic & constructive mathematics are not so much like boxing without fists as they are like prioritising agility and footwork, whereas (by way of analogy) classical mathematics concentrates on brute physical strength – one is appropriate for situations where flexibility and nimbleness are key, the other for those in which raw power is the deciding factor. Just as it takes some strength and some agility to win any fight, so the prizes offered up by mathematics are not to be won by either of intuitionistic logic or classical logic alone, but rather by the judicious application of each in concert with the other. ## References * J.L. Bell (2003), "An Invitation to Smooth Infinitesimal Analysis", unpublished note, retrieved at: https://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf * E. Bishop (1967), *Foundations of Constructive Analysis*, New York: McGraw-Hill * L.E.J. Brouwer (1912), "Intuitionism and formalism", trans. A. Dresden in P. Benacerraf \& H. Putnam (eds.), *Philosophy of mathematics*, Cambridge: Cambridge University Press, pp. 77-90 * L.E.J. Brouwer (1949), "Consciousness, philosophy, and mathematics", reprinted in P. Benacerraf \& H. Putnam (eds.), *Philosophy of mathematics*, Cambridge: Cambridge University Press, pp. 90-97 * J. Burgess (1984), "Dummett’s case for intuitionism", *History and Philosophy of Logic*, 5:2, pp. 177-194 * J. Burgess (2009), "Intuitionistic Logic", Ch. 6 of his *Philosophical Logic*, Princeton: Princeton University Press * R. Diaconescu (1975), "Axiom of Choice and Complementation", *Proceedings of the American Mathematical Society*, Vol. 51, No. 1, pp. 176-178 * M. Dummett (1977), *Elements of Intuitionism*, Oxford: Clarendon Press * M. Dummett (1975), "The Philosophical Basis of Intuitionistic Logic", in H.E. Rose and J.C. Shepherdson (eds.), *Proceedings of the Logic Colloquium ’73*, special issue of *Studies in Logic and the Foundations of Mathematics* 80, pp. 5–40 * D. Hilbert (1927), "The Foundations of Mathematics", trans. S. Bauer-Mengelberg (1967) in van Heijenoort (ed.) *From Frege to Gödel*, Cambridge, MA: Harvard University Press, pp. 464-479 * W.A. Howard (1980), "The formulae as types notion of construction", in J.P. Seldin \& J.R. Hindley (eds.), *To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism*, Cambridge, MA: Academic Press, pp. 479-490 * I. Kant (1781), *Kritik der Reinen Vernunft*, trans. P. Guyer \& A.W. Wood (1998) as *Critique of Pure Reason*, Cambridge: Cambridge University Press * C.S. Peirce, *Collected Papers*, Cambridge, MA: The Belknap Press of Harvard University Press * A.S. Troelstra & D. van Dalen (1988), *Constructivism in Mathematics*, Amsterdam: Elsevier Science Publishers