The Price of Formality

The first five essays followed a change in mathematical trust. A description could no longer be treated as an automatic guarantee that an object existed. Type theory answered by disciplining expressions. Axiomatic set theory specified permitted constructions. Both responses made mathematical reasoning more explicit. Neither ended the philosophical questions.

When a description has no set

A concept can be given by a condition. Its extension consists of the things satisfying that condition, in whatever domain is under discussion. Within the natural numbers, “is an even prime greater than two” has the empty set as its extension. Empty extensions are harmless. The important question is whether a condition ranges over a domain that is itself a set.

Russell's condition $x\notin x$ is perfectly expressible in the language of ZF. Within a given set $A$, separation provides the extension $\{x\in A\mid x\notin x\}$. Across all sets, the same condition does not determine a set in ZF. The gap is between a meaningful formula and an existence claim supported by the axioms.

This is one way to understand the foundational crisis without turning it into a simple loss of confidence. Mathematics did not stop using definitions. It learned to ask what work a definition is permitted to do.

Two boundaries, two costs

Russell and Whitehead placed a boundary in the grammar of their system. A self-membership expression fails a type check before it can generate a contradiction. The full ramified theory then needed additional principles, especially reducibility, to recover much familiar mathematics.

ZF placed a different boundary around set formation. One may state $x\in x$, but only the axioms determine which sets exist. Separation permits subsets of known sets; infinity, pairing, power set, and the other axioms permit further constructions. This uniform language proved flexible, though it leaves substantive questions about the axioms themselves.

These are historical solutions to a particular problem, not a ranking of all possible foundations. Modern type theories, class theories, and categorical approaches pursue different aims and remain mathematically productive.

A proof as an object of study

A formal theory specifies a language, axioms, and rules of inference. If a sentence $\varphi$ can be derived from a theory $T$ by those rules, we write

$$T\vdash\varphi.$$

This is a statement about the existence of a proof: a finite sequence of symbols whose steps follow stated rules. A theory is consistent if it cannot derive a contradiction. Formalizing proof lets us study proofs themselves with mathematical methods.

Hilbert and his collaborators hoped to use especially secure, finitary reasoning to show that powerful mathematical theories could not lead to contradictions. That ambition is often called Hilbert's program. It is more precise than saying that mathematics is “just a game of symbols.” The point was to justify the use of powerful methods by understanding what their formal proofs can and cannot do.

A model gives the symbols a home

Syntax is one side of a formal theory. A model supplies a domain and interpretations of the symbols that make its axioms true. If a sentence $\varphi$ holds in a model $\mathcal M$, we write

$$\mathcal M\models\varphi.$$

For a familiar example, the group axioms speak of a set, an operation, an identity, and inverses. The integers with addition form one model: the operation is addition, the identity is zero, and the inverse of $n$ is $-n$. Nonzero real numbers with multiplication give another. The axioms describe a pattern shared by different mathematical structures.

For sound rules of first-order logic, a sentence proved from $T$ is true in every model of $T$. A model can therefore connect formal derivation with mathematical interpretation. Whether a mathematical model also describes an experiment or a physical system is a further question, answered with evidence from outside the formal theory.

The observer can be formalized too

When we discuss the rules of $T$ or ask whether $T$ is consistent, we initially speak in a metatheory about the theory under study. This is a difference of viewpoint, not an impermeable wall. In a sufficiently expressive theory, statements about finite strings and proofs can themselves be encoded by numbers. Some metamathematical questions can then be represented inside arithmetic.

This observation makes the end of the chapter a beginning. ZFC has become a common foundation because it can organize a great deal of mathematics in one language. Its usefulness does not select it as the unique philosophical account of mathematical reality, and formalizing a theory does not by itself establish its consistency.

The next part asks how far the methods of a system can reach when the system begins to speak about its own proofs. Hilbert's hope for a secure external vantage point meets a sharper question: can a mathematical theory certify its own reliability?

Sources

• Russell and Whitehead, Principia Mathematica, Introduction (1910), for the type-theoretic response.
• Hilbert, “On the Infinite” (1926), on formal methods and the foundational program.
• Tarski, “The Concept of Truth in Formalized Languages”, for the careful separation of language and semantic interpretation.