mathematics probably began as platonism, but eudoxos put it on a purely hypothetico-deductive basis before platon's corpse was cold, so this debate has been going on for a while already. however, from the end of the hellenistic age until the 19th century, mathematics was utterly dominated by platonism
the social situation is quite different today. as you and i both know, there are plenty of formalists in mathematics, and quite a few constructivists as well, and none of them are platonists; we might even argue that at this point formalism is more popular than platonism among people working on foundations of mathematics. wildberger, a constructivist, is probably the most notorious living anti-platonist extremist who's still within the mainstream (i.e., he's a real mathematician, not just some bozo like me): https://njwildberger.com/2021/10/07/finite-versus-infinite-r... is a sample of his anti-platonist rhetoric. and, as you are certainly aware, voevodsky's extremely influential hott is fundamentally constructivist. https://en.wikipedia.org/wiki/Ultrafinitism is (or was) full of mathematicians who do (or did) not believe in the natural numbers. and it's easy to find working mathematicians saying things like https://old.reddit.com/r/math/comments/fx6bqv/why_did_brouwe...:
> I don't even know if 7 "exists," let alone pi. Such questions may be interesting, but they're philosophy, not math. Meanwhile, it's useful and mathematically interesting to count to 7, so we do it.
from a sociological perspective, a reasonable definition of 'mathematical reasoning' might be 'whatever arguments platonists can use to convince formalists and constructivists, or vice versa, without resorting to empirical evidence'. (this obviously isn't a logical definition, but i would argue that definitions of commonly used words and phrases are always sociological rather than logical in nature, though we can certainly stipulate a logical definition within the context of a given discussion.) this excludes, for example, which territory rightfully belongs to belgium, whether the earth orbits in an ellipse, or whether the natural numbers exist or not; but it includes the area inside a particular proposed national border for belgium, the properties of ellipses, and the consequences of the peano axioms
i think it is correct that formalists do not believe that formal logic is justified in any fundamental sense, but i haven't actually asked them
Here's the thing: any definition of mathematical reasoning that excludes the natural numbers, isn't a definition of mathematical reasoning.
For example, I cannot convince some constructivists that A or not A is always true when it comes to mathematical reasoning. But it is always true, anything else just doesn't make sense. So a constructivist who doesn't acknowledge that, I cannot take anything serious they say. Note that this is different from coming up with interpretations of ∨ and ¬ such that A ∨ ¬A is not always ⊤, such as Heyting Algebras, for example. And it is different from doing constructive mathematics, which is a very interesting subject.
Voevodsky was not a constructivist. He was looking for a way to do the kind of mathematics he likes on a computer to ensure correctness. He first visited the Isabelle development group to find about that, but simple type theory was not flexible enough for his purposes. So afterwards he fell into the hands of the dependent type theorists, who are all constructivists. He tried to do classical mathematics in their framework, that's where his univalence axiom comes from, but that didn't really work out well so far, and I doubt it ever will (but I don't really understand it, so that's just my opinion).
certainly you have to be able to do mathematical reasoning about natural numbers, but that doesn't necessarily imply determining their ontological status
another useful definition of mathematical reasoning is 'arguments strong enough to convince someone who cannot take seriously anything you are saying and does not trust you at all'
i appreciate the correction about voevodsky; i don't have a phd in the field myself, so that may not be all i got wrong
> certainly you have to be able to do mathematical reasoning about natural numbers, but that doesn't necessarily imply determining their ontological status
That's true, of course you can use something without understanding it, but can you use something, and then deny its existence?
I want to correct what I said earlier about the natural numbers and infinity. Of course you could add infinity to the natural numbers, if you wanted to. This can be done in different ways. It's just that natural numbers without infinity are a simpler starting point.
if i use monopoly dollars to buy the b&o railroad, does that entail that i believe that monopoly dollars exist? surely not in the same platonic sense that you and i believe that 53 exists. monopoly dollars are, i think uncontroversially, merely a socially constructed consensus hallucination, like national borders, google, or adultery; as far as i can tell, formalists claim that 53 is too. for that matter, subjective idealists like berkeley claim that so are physical objects like electrons
i haven't seen a satisfying formalist explanation of why mathematicians of different cultures come to identical conclusions about 53 but vastly different conclusions about national borders and adultery. (borges' tlön, uqbar, and orbis tertius famously makes a similar point satirically about subjective idealism.) but i am forced to admit that the formalists themselves do exist and do make this assertion about 53, and while many working mathematicians are unwilling to wholeheartedly embrace formalism (and even fewer constructivism, though, as you point out, for example in type theory constructivists are ubiquitous), fairly few of them are willing to wholeheartedly reject it and declare certainty about platonic realism, as you are
what i was saying about the natural numbers and infinity is that the "common sense" of many children (though perhaps not your own childhood self) insists to them not that a maximum natural number is logically consistent, which i agree with you that it is, but that it is logically necessary, which of course the peano axioms reject. this, to me, is good evidence that common sense is not a solid enough foundation for reaching mathematical truth
by the way, i want to express gratitude for your willingness to discuss epistemology and ontology without descending into the kinds of vicious personal attacks i generally expect on this website, or more generally when discussing epistemology
A most interesting book in this context is [1]. It has introductory discussions of logicism, intuitionism, and formalism by Carnap, Heyting, and von Neumann, and interestingly, they were not aware yet of Gödel's results at that point which were published in the same year. After that, Heyting's "Dispute" is a nice exposition of the different view points, and I find myself agreeing with much of the intuitionist point of view, namely that mathematical reasoning cannot be reduced to formalism (but I don't agree that intuitionistic reasoning is the only allowed form of mathematical reasoning). I mean, Gödel's incompleteness result is as hard a proof of this as you will ever get! And again, in a later piece by Paul Bernays, "On platonism in mathematics", Bernays states: 'Is it possible to draw an exact boundary between what is evident, and what is only plausible? I believe that one must answer [this question] negatively'. In other words: Common sense is a necessary part of mathematical reasoning. Fundamentally, there is no way around this.
the social situation is quite different today. as you and i both know, there are plenty of formalists in mathematics, and quite a few constructivists as well, and none of them are platonists; we might even argue that at this point formalism is more popular than platonism among people working on foundations of mathematics. wildberger, a constructivist, is probably the most notorious living anti-platonist extremist who's still within the mainstream (i.e., he's a real mathematician, not just some bozo like me): https://njwildberger.com/2021/10/07/finite-versus-infinite-r... is a sample of his anti-platonist rhetoric. and, as you are certainly aware, voevodsky's extremely influential hott is fundamentally constructivist. https://en.wikipedia.org/wiki/Ultrafinitism is (or was) full of mathematicians who do (or did) not believe in the natural numbers. and it's easy to find working mathematicians saying things like https://old.reddit.com/r/math/comments/fx6bqv/why_did_brouwe...:
> I don't even know if 7 "exists," let alone pi. Such questions may be interesting, but they're philosophy, not math. Meanwhile, it's useful and mathematically interesting to count to 7, so we do it.
from a sociological perspective, a reasonable definition of 'mathematical reasoning' might be 'whatever arguments platonists can use to convince formalists and constructivists, or vice versa, without resorting to empirical evidence'. (this obviously isn't a logical definition, but i would argue that definitions of commonly used words and phrases are always sociological rather than logical in nature, though we can certainly stipulate a logical definition within the context of a given discussion.) this excludes, for example, which territory rightfully belongs to belgium, whether the earth orbits in an ellipse, or whether the natural numbers exist or not; but it includes the area inside a particular proposed national border for belgium, the properties of ellipses, and the consequences of the peano axioms
i think it is correct that formalists do not believe that formal logic is justified in any fundamental sense, but i haven't actually asked them
for those who don't have a phd in logic but might still be reading this thread, a good short introduction to the late modern schism in mathematics (from an ardently platonist perspective!) is https://plus.maths.org/content/philosophy-applied-mathematic... another introduction is https://web.archive.org/web/20170611144646/http://math.stanf... and a much deeper introduction is https://plato.stanford.edu/entries/mathematics-constructive/