From the formalist perspective, Principia Mathematica is best understood not as a successful reduction of mathematics to logic, but as a landmark exercise in the rigorous formalization of mathematical reasoning - one whose deepest significance lies in its demonstration that mathematical thought can be systematically encoded in explicit symbolic rules, independent of any appeal to intuitive meaning or Platonic objects. Formalists hold that Russell and Whitehead's project, whatever its logicist ambitions, achieved something of lasting importance precisely in its formal machinery: its notation, its inference rules, its type-theoretic scaffolding. This viewpoint is associated with mathematicians and philosophers working in the tradition of David Hilbert, and finds contemporary expression among those who treat proof theory, formal systems, and metamathematics as the proper frame for evaluating PM's legacy.
Mathematics is the manipulation of symbols according to explicit rules. Formalists argue that mathematical truth is not discovered by grasping abstract objects but is constituted by derivability within a formal system. On this view, the propositions of PM are meaningful insofar as they are well-formed strings derivable from stated axioms via stated rules - nothing more is required, and nothing more should be sought.1)
The logicist interpretation of PM imports unnecessary metaphysics. Formalists contend that Russell's claim that mathematics is logic - that mathematical propositions are logical truths known a priori - commits PM to a philosophically laden account of logical objects and logical truth that is neither required nor supported by the formal system itself. The system's value, they argue, survives the collapse of its logicist justification.2)
The axioms of PM are posits, not self-evident truths. The Axiom of Reducibility and the Axiom of Infinity, which PM requires but which Russell himself acknowledged were not purely logical, are on the formalist reading simply formal stipulations adopted to make the system work. Formalists regard this not as a fatal concession but as transparency: all powerful formal systems rest on posited axioms, and honesty about this is a virtue rather than a flaw.3)
Gödel's incompleteness results vindicate the formalist research program. Formalists generally hold that Gödel's 1931 theorems, while placing limits on what any consistent formal system can prove about itself, are intelligible only because PM and related systems were specified with enough precision to be treated as mathematical objects. The incompleteness theorems presuppose formalization; they are a product of the tradition PM helped establish, not a refutation of it.4)
Type theory is a formal achievement, not a logical discovery. The ramified theory of types that structures PM is, in the formalist reading, a powerful device for blocking paradox within a formal system - not a revelation about the nature of propositional functions or the metaphysics of classes. Its interest is technical: it demonstrates that paradox-free formalization of a large portion of mathematics is achievable.5)
The formalist tradition from which this reading of PM draws emerged most sharply in the early twentieth century through the work of David Hilbert, whose program sought to secure the foundations of mathematics by axiomatizing mathematical theories and proving their consistency by finitary metamathematical means. Hilbert's program and Russell's logicism were rival responses to the same foundational crisis - the paradoxes of naive set theory - and their relationship was combative as well as mutually illuminating.
Russell and Whitehead published Principia Mathematica in three volumes between 1910 and 1913. Hilbert and his collaborators followed its formal development closely, and the notation and methods of PM fed directly into the development of proof theory. By the 1920s, figures such as Wilhelm Ackermann and John von Neumann were working within a framework that owed as much to PM's formal machinery as to Hilbert's metamathematical ambitions.
When Gödel published his incompleteness theorems in 1931, he framed them explicitly as results about the formal system of PM and related systems. Formalists have since argued that this framing confirms their interpretation: PM mattered because it was a sufficiently precise formal system, and it is in that capacity that it became an object of rigorous mathematical investigation.
Through the latter twentieth century, the formalist reading of PM was reinforced by the development of type theory as a foundation for computer-assisted proof verification. Systems such as ML, Coq, and later Lean drew on the type-theoretic architecture of PM as a practical engineering resource, largely indifferent to the logicist philosophy that motivated it.6)
David Hilbert (1862-1943) did not comment extensively on PM as such, but his formalist philosophy of mathematics - that mathematical existence is consistency, and that meaning in mathematics is given by formal rules - supplies the dominant framework through which the formalist reading of PM is developed.
Haskell B. Curry (1900-1982) articulated a thoroughgoing formalist philosophy of mathematics that explicitly distanced the value of formal systems from any logicist or Platonist interpretation of their content. His account of PM's significance emphasizes its role as a precise syntactic object.
W. V. O. Quine (1908-2000), though not a formalist in the strict Hilbertian sense, engaged closely with PM and argued that its apparent logical self-evidence was an artifact of notational choices, not a reflection of logical truth.7)
Per Martin-Löf (b. 1942) developed constructive type theory in explicit dialogue with the type-theoretic tradition descending from PM, interpreting that tradition through a formal and computational lens.
Strict vs. liberal formalism. Some formalists in the Hilbertian tradition insist that a meaningful formalism must admit finitist metamathematical justification - a standard PM does not meet, given its reliance on infinitary axioms. Others take a more liberal view, treating any sufficiently explicit formal system as a legitimate object of study regardless of its metamathematical status.
Whether PM is a good formalism. Formalists disagree about whether PM's type-theoretic architecture, with its ramification and its axiom of reducibility, represents a well-designed formal system or a cumbersome one superseded by Zermelo-Fraenkel set theory and simpler type theories. Some regard PM as historically important but technically obsolete; others see its type-theoretic structure as genuinely preferable for certain foundational purposes.
The relevance of intent. A minority of formalist interpreters argue that Russell and Whitehead's logicist intentions are not irrelevant to evaluating the system - that the gap between those intentions and what the system actually achieves is philosophically instructive, not merely a historical curiosity. The majority view holds that the system should be assessed on its formal merits alone.
<footnotes />