On Formally Undecidable Propositions of Principia Mathematica and Related Systems

Kurt Gödel

• Publisher: Dover Publications
• Year: 2012
• Print ISBN: 9780486669809
• eBook ISBN: 9780486158402
• Topic: Mathematics
• Subtopic: Logic in Mathematics
• Index: Mathematics

In 1931, a young Austrian mathematician published an epoch-making paper containing one of the most revolutionary ideas in logic since Aristotle. Kurt Giidel maintained, and offered detailed proof, that in any arithmetic system, even in elementary parts of arithmetic, there are propositions which cannot be proved or disproved within the system. It is thus uncertain that the basic axioms of arithmetic will not give rise to contradictions. The repercussions of this discovery are still being felt and debated in 20th-century mathematics.
The present volume reprints the first English translation of Giidel's far-reaching work. Not only does it make the argument more intelligible, but the introduction contributed by Professor R. B. Braithwaite (Cambridge University}, an excellent work of scholarship in its own right, illuminates it by paraphrasing the major part of the argument.
This Dover edition thus makes widely available a superb edition of a classic work of original thought, one that will be of profound interest to mathematicians, logicians and anyone interested in the history of attempts to establish axioms that would provide a rigorous basis for all mathematics. Translated by B. Meltzer, University of Edinburgh. Preface. Introduction by R. B. Braithwaite.

ON FORMALLY UNDECIDABLE PROPOSITIONS OF PRINCIPIA MATHEMATICA AND RELATED SYSTEMS I¹

by Kurt Gödel, Vienna

1

The development of mathematics in the direction of greater exactness has—as is well known—led to large tracts of it becoming formalized, so that proofs can be carried out according to a few mechanical rules. The most comprehensive formal systems yet set up are, on the one hand, the system of Principia Mathematica (PM)² and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann).³ 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. It may therefore be surmised that these axioms and rules of inference are also sufficient to decide all mathematical questions which can in any way at all be expressed formally in the systems concerned. It is shown below that this is not the case, and that in both the systems mentioned there are in fact relatively simple problems in the theory of ordinary whole numbers⁴ which cannot be decided from the axioms. This situation is not due in some way to the special nature of the systems set up, but holds for a very extensive class of formal systems, including, in particular, all those arising from the addition of a finite number of axioms to the two systems mentioned,⁵ provided that thereby no false propositions of the kind described in footnote 4 become provable.

Before going into details, we shall first indicate the main lines of the proof, naturally without laying claim to exactness. The formulae of a formal system—we restrict ourselves here to the system PM—are, looked at from outside, finite series of basic signs (variables, logical constants and brackets or separation points), and it is easy to state precisely just which series of basic signs are meaningful formulae and which are not.⁶ Proofs, from the formal standpoint, are likewise nothing but finite series of formulae (with certain specifiable characteristics). For metamathematical purposes it is naturally immaterial what objects are taken as basic signs, and we propose to use natural numbers ⁷ for them. Accordingly, then, a formula is a finite series of natural numbers,⁸ and a particular proof-schema is a finite series of finite series of natural numbers. Metamathematical concepts and propositions thereby become concepts and propositions concerning natural numbers, or series of them,⁹ and therefore at least partially expressible in the symbols of the system PM itself. In particular, it can be shown that the concepts, “formula”, “proof-schema”, “provable formula” are definable in the system PM, i.e. one can give¹⁰ a formul...

Table of contents

• Dover Books on Mathematics
• Title Page
• Copyright Page
• Table of Contents
• Dedication
• PREFACE
• INTRODUCTION
• NOTE
• ON FORMALLY UNDECIDABLE PROPOSITIONS OF PRINCIPIA MATHEMATICA AND RELATED SYSTEMS I