On Formally Undecidable Propositions of Principia Mathematica and Related Systems

Gödel established metamathematical results about the strings of his formal system by considering numbers co-ordinated with the strings. (View Highlight)

Gödel’s rule of arithmetization ensures that to every class of strings there corresponds a unique class of Gödel numbers, and vice versa. And that to any relation R between strings there corresponds a unique relation R′ between Gödel numbers, and vice versa: i.e. the n-adic relation R′ holds between n Gödel numbers if and only if the n-adic relation R holds between the n strings. For example, the metamathematical statement that the series s of formulae is a ‘proof’ of the formula f is true if and only if a certain arithmetical relation holds between the Gödel numbers of s and of f which corresponds to the relation: being a ‘proof’ of (View Highlight)

The most comprehensive formal systems yet set up are, on the one hand, the system of Principia Mathematica (PM)2 and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann).3 These two systems are so extensive that all methods of proof used in mathematics today have been formalized in them, i.e. reduced to a few axioms and rules of inference (View Highlight)