Why don't formalized proofs make formalism true?

All mathematicians are familiar with the (extremely plausible) fact that any ordinary mathematical proof can be formalized inside some foundational theory, e.g., ZFC.

Why doesn't this imply that formalism is true?

By formalism I mean this (taken from Wikipedia):

In the philosophy of mathematics, formalism is the view that holds that statements of mathematics and logic can be considered to be statements about the consequences of the manipulation of strings (alphanumeric sequences of symbols, usually as equations) using established manipulation rules.

When I look at formalized proofs (e.g., this one for the area of a circle), I can't see how this is not evidence in favor of formalism. I'm obviously not understanding something.

• Formalism in the philosophy of mathematics is a semantic claim, whereas formalism in the design of actual, case-by-case proofs is a more syntactic process. The semantic version is that formalistic proofs are themselves the proper objects of mathematics, and that there is no notation-transcendent information for these proofs to derive from. It can be seen as akin to intuitionism, or then as a strongly empirical intuitionism, where (empirical) semiotic intuitions play the congruent role played by pure space/time intuition in e.g. Brouwer. Jan 8, 2023 at 20:43
• Maybe "true" is not really the point - I think we should be careful about the word "true". It is very over-used, in my opinion. Jan 8, 2023 at 23:20
• As a (mostly-)formalist, my personal take is that formalized proofs make formalism tenable: they show that the formalist doesn't need to ultimately appeal to a community of subjective mathematicians in order to justify their mathematical claims. In a sense, the formalist can participate "with a clear philosophical conscience" in mathematics because they can take natural-language proofs as outlines of purely-formal proofs. However, this doesn't make formalism true. Jan 8, 2023 at 23:34
• @NoahSchweber What would: "formalism is true/false" even mean? Jan 9, 2023 at 2:27
• Because Wikipedia screwed up what "formalism" means, see SEP for a more competent account. Most non-formalists agree that most mathematical theorems "can be considered" derivable in ZFC. The substantive claim of formalism is that there is nothing more to it. No platonic realm, no Kantian intuition, no empirical verification, nothing over and above to judge what is true, as opposed to just derivable, or why ZFC and not, say, ZF+AD. It is just a game of symbols, and ZFC are the rules, period. And that is not so extremely plausible. Jan 9, 2023 at 7:02

The simplest reason for a gap between formal proofs and formalism as a foundation for mathematics is that the former are given with existential quantifications over specific proof objects, whereas the latter is a universal quantification over all possible objects of proofs. You might say:

1. xy(xy) (where "⟝" is read as "proves").
2. xy(Mxxy) (where "Mx" reads "x is a mathematical object").

... but so then (1) does not imply (2).

Moreover, the set of intuitively-known sets, modulo intuitions of notation, is not subject to closure because knowledge in general doesn't clearly require closure anyway and intuitive knowledge specifically is, for Kantian reasons, empirically open even if discursive knowledge is closer to closed (indeed, however, closure might be the sine qua non of discursion, here). So regardless of whether we could prove that all known mathematical objects can be assimilated to proof objects in re, the outside possibility of ante rem proof objects would remain. And indeed, then, if there are ante rem proof objects, why not other such mathematical objects?

"Worse," it seems easy to go from semiotic formalism to intuitionism, but then from intuitionism to a more transcendent notion (Brouwer seriously failed to grasp the implications of the "freely creating mathematical subject," since in Kantian terms, such an entity would be equipped with intellectual intuition and so would comprehend absolute infinity, not just the relative infinity of the alephs and the omegas, yet Brouwer did not attribute even relatively infinite intuition to the FCMS). Or one can go from formalism to multiversal realism without skipping too many beats.

Semiotic formalism less so, but game-theoretic formalism moreso, can also mutate well enough into mathematical fictionalism, yet a fictionalist might later be exposed to a compelling (for some, not all, individual fictionalists) argument about fictional objects being possible objects, where we are speaking of "mere possibilia"; so now we have evolved either modal logicism or modal realism out of our base philosophical animal, and either of those could mutate into the other later.

Alternatively, logicism could be turned into formalism, and formalism into logicism, and generic logicism into temporal epistemic logicism, which could easily be reimagined as intuitionism; or multiversal realism could be converted into modal logicism, and vice versa; and so on and on, until we find it hard to differentiate any of these positions in an absolutely conclusive way (their premises vary, as do the intentions behind the acceptance of said premises, but whatever the followers of whichever camps would like to believe in the end, the blurring-together of the camps' boundaries is difficult if not impossible to avoid; c.f. the practice of showing that a theory can be represented by a Boolean algebra as well as in some other, e.g. sequent-calculus, style, or of showing that a logic based on one notion of quantification can be translated into a logic with a subtly different quantification subtheory).