ramified theory of types
   HOME

TheInfoList



OR:

The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the
foundations of mathematics Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathe ...
written by mathematician–philosophers Alfred North Whitehead and
Bertrand Russell Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, ...
and published in 1910, 1912, and 1913. In 1925–1927, it appeared in a second edition with an important ''Introduction to the Second Edition'', an ''Appendix A'' that replaced ✸9 and all-new ''Appendix B'' and ''Appendix C''. ''PM'' is not to be confused with Russell's 1903 ''
The Principles of Mathematics ''The Principles of Mathematics'' (''PoM'') is a 1903 book by Bertrand Russell, in which the author presented his famous Russell's paradox, paradox and argued his thesis that mathematics and logic are identical. The book presents a view of ...
''. ''PM'' was originally conceived as a sequel volume to Russell's 1903 ''Principles'', but as ''PM'' states, this became an unworkable suggestion for practical and philosophical reasons: "The present work was originally intended by us to be comprised in a second volume of ''Principles of Mathematics''... But as we advanced, it became increasingly evident that the subject is a very much larger one than we had supposed; moreover on many fundamental questions which had been left obscure and doubtful in the former work, we have now arrived at what we believe to be satisfactory solutions." ''PM'', according to its introduction, had three aims: (1) to analyze to the greatest possible extent the ideas and methods of mathematical logic and to minimize the number of
primitive notion In mathematics, logic, philosophy, and formal systems, a primitive notion is a concept that is not defined in terms of previously-defined concepts. It is often motivated informally, usually by an appeal to intuition and everyday experience. In an ...
s, axioms, and
inference rule In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
s; (2) to precisely express mathematical propositions in symbolic logic using the most convenient notation that precise expression allows; (3) to solve the paradoxes that plagued logic and
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
at the turn of the 20th century, like
Russell's paradox In mathematical logic, Russell's paradox (also known as Russell's antinomy) is a set-theoretic paradox discovered by the British philosopher and mathematician Bertrand Russell in 1901. Russell's paradox shows that every set theory that contains ...
. This third aim motivated the adoption of the theory of
types Type may refer to: Science and technology Computing * Typing, producing text via a keyboard, typewriter, etc. * Data type In computer science and computer programming, a data type (or simply type) is a set of possible values and a set of allo ...
in ''PM''. The theory of types adopts grammatical restrictions on formulas that rules out the unrestricted comprehension of classes, properties, and functions. The effect of this is that formulas such as would allow the comprehension of objects like the Russell set turn out to be ill-formed: they violate the grammatical restrictions of the system of ''PM''. There is no doubt that ''PM'' is of great importance in the history of mathematics and philosophy: as Irvine has noted, it sparked interest in symbolic logic and advanced the subject by popularizing it; it showcased the powers and capacities of symbolic logic; and it showed how advances in philosophy of mathematics and symbolic logic could go hand-in-hand with tremendous fruitfulness. Indeed, ''PM'' was in part brought about by an interest in
logicism In the philosophy of mathematics, logicism is a programme comprising one or more of the theses that — for some coherent meaning of 'logic' — mathematics is an extension of logic, some or all of mathematics is reducible to logic, or some or all ...
, the view on which all mathematical truths are logical truths. It was in part thanks to the advances made in ''PM'' that, despite its defects, numerous advances in meta-logic were made, including Gödel's incompleteness theorems. For all that, ''PM'' notations are not widely used today: probably the foremost reason for this is that practicing mathematicians tend to assume that the background Foundation is a form of the system of
Zermelo–Fraenkel set theory In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such ...
. Nonetheless, the scholarly, historical, and philosophical interest in ''PM'' is great and ongoing: for example, the Modern Library placed it 23rd in a list of the top 100 English-language nonfiction books of the twentieth century. There are also multiple articles on the work in the peer-reviewed ''Stanford Encyclopedia of Philosophy'' and academic researchers continue working with ''Principia'', whether for the historical reason of understanding the text or its authors, or for mathematical reasons of understanding or developing ''Principias logical system.


Scope of foundations laid

The ''Principia'' covered only
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
,
cardinal numbers In mathematics, cardinal numbers, or cardinals for short, are a generalization of the natural numbers used to measure the cardinality (size) of sets. The cardinality of a finite set is a natural number: the number of elements in the set. The ...
,
ordinal numbers In set theory, an ordinal number, or ordinal, is a generalization of ordinal numerals (first, second, th, etc.) aimed to extend enumeration to infinite sets. A finite set can be enumerated by successively labeling each element with the least ...
, and real numbers. Deeper theorems from
real analysis In mathematics, the branch of real analysis studies the behavior of real numbers, sequences and series of real numbers, and real functions. Some particular properties of real-valued sequences and functions that real analysis studies include conv ...
were not included, but by the end of the third volume it was clear to experts that a large amount of known mathematics could ''in principle'' be developed in the adopted formalism. It was also clear how lengthy such a development would be. A fourth volume on the foundations of
geometry Geometry (; ) is, with arithmetic, one of the oldest branches of mathematics. It is concerned with properties of space such as the distance, shape, size, and relative position of figures. A mathematician who works in the field of geometry is ...
had been planned, but the authors admitted to intellectual exhaustion upon completion of the third.


Theoretical basis

As noted in the criticism of the theory by Kurt Gödel (below), unlike a formalist theory, the "logicistic" theory of ''PM'' has no "precise statement of the syntax of the formalism". Furthermore in the theory, it is almost immediately observable that ''interpretations'' (in the sense of model theory) are presented in terms of ''truth-values'' for the behaviour of the symbols "⊢" (assertion of truth), "~" (logical not), and "V" (logical inclusive OR). Truth-values: ''PM'' embeds the notions of "truth" and "falsity" in the notion "primitive proposition". A raw (pure) formalist theory would not provide the meaning of the symbols that form a "primitive proposition"—the symbols themselves could be absolutely arbitrary and unfamiliar. The theory would specify only ''how the symbols behave based on the grammar of the theory''. Then later, by ''assignment'' of "values", a model would specify an ''interpretation'' of what the formulas are saying. Thus in the formal
Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
symbol set below, the "interpretation" of what the symbols commonly mean, and by implication how they end up being used, is given in parentheses, e.g., "¬ (not)". But this is not a pure Formalist theory.


Contemporary construction of a formal theory

The following formalist theory is offered as contrast to the logicistic theory of ''PM''. A contemporary formal system would be constructed as follows: # ''Symbols used'': This set is the starting set, and other symbols can appear but only by ''definition'' from these beginning symbols. A starting set might be the following set derived from Kleene 1952: ''logical symbols'': "→" (implies, IF-THEN, and "⊃"), "&" (and), "V" (or), "¬" (not), "∀" (for all), "∃" (there exists); ''predicate symbol'' "=" (equals); ''function symbols'' "+" (arithmetic addition), "∙" (arithmetic multiplication), "'" (successor); ''individual symbol'' "0" (zero); ''variables'' "''a''", "''b''", "''c''", etc.; and ''parentheses'' "(" and ")". # ''Symbol strings'': The theory will build "strings" of these symbols by
concatenation In formal language theory and computer programming, string concatenation is the operation of joining character strings end-to-end. For example, the concatenation of "snow" and "ball" is "snowball". In certain formalisations of concatenat ...
(juxtaposition). # ''Formation rules'': The theory specifies the rules of syntax (rules of grammar) usually as a recursive definition that starts with "0" and specifies how to build acceptable strings or "well-formed formulas" (wffs). This includes a rule for "substitution" of strings for the symbols called "variables". # ''Transformation rule(s)'': The
axioms An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or f ...
that specify the behaviours of the symbols and symbol sequences. # ''Rule of inference, detachment, ''modus ponens'' '': The rule that allows the theory to "detach" a "conclusion" from the "premises" that led up to it, and thereafter to discard the "premises" (symbols to the left of the line │, or symbols above the line if horizontal). If this were not the case, then substitution would result in longer and longer strings that have to be carried forward. Indeed, after the application of modus ponens, nothing is left but the conclusion, the rest disappears forever. Contemporary theories often specify as their first axiom the classical or modus ponens or "the rule of detachment": The symbol "│" is usually written as a horizontal line, here "⊃" means "implies". The symbols ''A'' and ''B'' are "stand-ins" for strings; this form of notation is called an "axiom schema" (i.e., there is a countable number of specific forms the notation could take). This can be read in a manner similar to IF-THEN but with a difference: given symbol string IF ''A'' and ''A'' implies ''B'' THEN ''B'' (and retain only ''B'' for further use). But the symbols have no "interpretation" (e.g., no "truth table" or "truth values" or "truth functions") and modus ponens proceeds mechanistically, by grammar alone.


Construction

The theory of ''PM'' has both significant similarities, and similar differences, to a contemporary formal theory. Kleene states that "this deduction of mathematics from logic was offered as intuitive axiomatics. The axioms were intended to be believed, or at least to be accepted as plausible hypotheses concerning the world". Indeed, unlike a Formalist theory that manipulates symbols according to rules of grammar, ''PM'' introduces the notion of "truth-values", i.e., truth and falsity in the ''real-world'' sense, and the "assertion of truth" almost immediately as the fifth and sixth elements in the structure of the theory (''PM'' 1962:4–36): # ''Variables'' # ''Uses of various letters'' # ''The fundamental functions of propositions'': "the Contradictory Function" symbolised by "~" and the "Logical Sum or Disjunctive Function" symbolised by "∨" being taken as primitive and logical implication ''defined'' (the following example also used to illustrate 9. ''Definition'' below) as
''p'' ⊃ ''q'' .=. ~ ''p'' ∨ ''q'' Df. (''PM'' 1962:11)
and logical product defined as
''p'' . ''q'' .=. ~(~''p'' ∨ ~''q'') Df. (''PM'' 1962:12) # ''Equivalence'': ''Logical'' equivalence, not arithmetic equivalence: "≡" given as a demonstration of how the symbols are used, i.e., "Thus ' ''p'' ≡ ''q'' ' stands for '( ''p'' ⊃ ''q'' ) . ( ''q'' ⊃ ''p'' )'." (''PM'' 1962:7). Notice that to ''discuss'' a notation ''PM'' identifies a "meta"-notation with " pace... pace:
Logical equivalence appears again as a ''definition'':
''p'' ≡ ''q'' .=. ( ''p'' ⊃ ''q'' ) . ( ''q'' ⊃ ''p'' ) (''PM'' 1962:12),
Notice the appearance of parentheses. This ''grammatical'' usage is not specified and appears sporadically; parentheses do play an important role in symbol strings, however, e.g., the notation "(''x'')" for the contemporary "∀''x''". # ''Truth-values'': "The 'Truth-value' of a proposition is ''truth'' if it is true, and ''falsehood'' if it is false" (this phrase is due to
Gottlob Frege Friedrich Ludwig Gottlob Frege (; ; 8 November 1848 – 26 July 1925) was a German philosopher, logician, and mathematician. He was a mathematics professor at the University of Jena, and is understood by many to be the father of analytic ph ...
) (''PM'' 1962:7). # ''Assertion-sign'': "'⊦. ''p'' may be read 'it is true that' ... thus '⊦: ''p'' .⊃. ''q'' ' means 'it is true that ''p'' implies ''q'' ', whereas '⊦. ''p'' .⊃⊦. ''q'' ' means ' ''p'' is true; therefore ''q'' is true'. The first of these does not necessarily involve the truth either of ''p'' or of ''q'', while the second involves the truth of both" (''PM'' 1962:92). # ''Inference'': ''PM''s version of ''modus ponens''. " f'⊦. ''p'' ' and '⊦ (''p'' ⊃ ''q'')' have occurred, then '⊦ . ''q'' ' will occur if it is desired to put it on record. The process of the inference cannot be reduced to symbols. Its sole record is the occurrence of '⊦. ''q'' ' n other words, the symbols on the left disappear or can be erased (''PM'' 1962:9). # ''The use of dots'' # ''Definitions'': These use the "=" sign with "Df" at the right end. # ''Summary of preceding statements'': brief discussion of the primitive ideas "~ ''p''" and "''p'' ∨ ''q''" and "⊦" prefixed to a proposition. # ''Primitive propositions'': the axioms or postulates. This was significantly modified in the second edition. # ''Propositional functions'': The notion of "proposition" was significantly modified in the second edition, including the introduction of "atomic" propositions linked by logical signs to form "molecular" propositions, and the use of substitution of molecular propositions into atomic or molecular propositions to create new expressions. # ''The range of values and total variation'' # ''Ambiguous assertion and the real variable'': This and the next two sections were modified or abandoned in the second edition. In particular, the distinction between the concepts defined in sections 15. ''Definition and the real variable'' and 16 ''Propositions connecting real and apparent variables'' was abandoned in the second edition. # ''Formal implication and formal equivalence'' # ''Identity'' # ''Classes and relations'' # ''Various descriptive functions of relations'' # ''Plural descriptive functions'' # ''Unit classes''


Primitive ideas

Cf. ''PM'' 1962:90–94, for the first edition: * (1) ''Elementary propositions''. * (2) ''Elementary propositions of functions''. * (3) ''Assertion'': introduces the notions of "truth" and "falsity". * (4) ''Assertion of a propositional function''. * (5) ''Negation'': "If ''p'' is any proposition, the proposition "not-''p''", or "''p'' is false," will be represented by "~''p''" ". * (6) ''Disjunction'': "If ''p'' and ''q'' are any propositions, the proposition "''p'' or ''q'', i.e., "either ''p'' is true or ''q'' is true," where the alternatives are to be not mutually exclusive, will be represented by "''p'' ∨ ''q''" ". * (cf. section B)


Primitive propositions

The ''first'' edition (see discussion relative to the second edition, below) begins with a definition of the sign "⊃" ✸1.01. ''p'' ⊃ ''q'' .=. ~ ''p'' ∨ ''q''. Df. ✸1.1. Anything implied by a true elementary proposition is true. Pp modus ponens (✸1.11 was abandoned in the second edition.) ✸1.2. ⊦: ''p'' ∨ ''p'' .⊃. ''p''. Pp principle of tautology ✸1.3. ⊦: ''q'' .⊃. ''p'' ∨ ''q''. Pp principle of addition ✸1.4. ⊦: ''p'' ∨ ''q'' .⊃. ''q'' ∨ ''p''. Pp principle of permutation ✸1.5. ⊦: ''p'' ∨ ( ''q'' ∨ ''r'' ) .⊃. ''q'' ∨ ( ''p'' ∨ ''r'' ). Pp associative principle ✸1.6. ⊦:. ''q'' ⊃ ''r'' .⊃: ''p'' ∨ ''q'' .⊃. ''p'' ∨ ''r''. Pp principle of summation ✸1.7. If ''p'' is an elementary proposition, ~''p'' is an elementary proposition. Pp ✸1.71. If ''p'' and ''q'' are elementary propositions, ''p'' ∨ ''q'' is an elementary proposition. Pp ✸1.72. If φ''p'' and ψ''p'' are elementary propositional functions which take elementary propositions as arguments, φ''p'' ∨ ψ''p'' is an elementary proposition. Pp Together with the "Introduction to the Second Edition", the second edition's Appendix A abandons the entire section ✸9. This includes six primitive propositions ✸9 through ✸9.15 together with the Axioms of reducibility. The revised theory is made difficult by the introduction of the
Sheffer stroke In Boolean functions and propositional calculus, the Sheffer stroke denotes a logical operation that is equivalent to the negation of the conjunction operation, expressed in ordinary language as "not both". It is also called nand ("not and") ...
(", ") to symbolise "incompatibility" (i.e., if both elementary propositions ''p'' and ''q'' are true, their "stroke" ''p'' , ''q'' is false), the contemporary logical NAND (not-AND). In the revised theory, the Introduction presents the notion of "atomic proposition", a "datum" that "belongs to the philosophical part of logic". These have no parts that are propositions and do not contain the notions "all" or "some". For example: "this is red", or "this is earlier than that". Such things can exist ''ad finitum'', i.e., even an "infinite enumeration" of them to replace "generality" (i.e., the notion of "for all"). ''PM'' then "advance to molecular propositions" that are all linked by "the stroke". Definitions give equivalences for "~", "∨", "⊃", and ".". The new introduction defines "elementary propositions" as atomic and molecular positions together. It then replaces all the primitive propositions ✸1.2 to ✸1.72 with a single primitive proposition framed in terms of the stroke: : "If ''p'', ''q'', ''r'' are elementary propositions, given ''p'' and ''p'', (''q'', ''r''), we can infer ''r''. This is a primitive proposition." The new introduction keeps the notation for "there exists" (now recast as "sometimes true") and "for all" (recast as "always true"). Appendix A strengthens the notion of "matrix" or "predicative function" (a "primitive idea", ''PM'' 1962:164) and presents four new Primitive propositions as ✸8.1–✸8.13. ✸88. Multiplicative axiom ✸120. Axiom of infinity


Ramified types and the axiom of reducibility

In simple type theory objects are elements of various disjoint "types". Types are implicitly built up as follows. If τ1,...,τ''m'' are types then there is a type (τ1,...,τ''m'') that can be thought of as the class of propositional functions of τ1,...,τ''m'' (which in set theory is essentially the set of subsets of τ1×...×τ''m''). In particular there is a type () of propositions, and there may be a type ι (iota) of "individuals" from which other types are built. Russell and Whitehead's notation for building up types from other types is rather cumbersome, and the notation here is due to
Church Church may refer to: Religion * Church (building), a building for Christian religious activities * Church (congregation), a local congregation of a Christian denomination * Church service, a formalized period of Christian communal worship * C ...
. In the ramified type theory of PM all objects are elements of various disjoint ramified types. Ramified types are implicitly built up as follows. If τ1,...,τ''m''1,...,σ''n'' are ramified types then as in simple type theory there is a type (τ1,...,τ''m''1,...,σ''n'') of "predicative" propositional functions of τ1,...,τ''m''1,...,σ''n''. However, there are also ramified types (τ1,...,τ''m'', σ1,...,σ''n'') that can be thought of as the classes of propositional functions of τ1,...τ''m'' obtained from propositional functions of type (τ1,...,τ''m''1,...,σ''n'') by quantifying over σ1,...,σ''n''. When ''n''=0 (so there are no σs) these propositional functions are called predicative functions or matrices. This can be confusing because current mathematical practice does not distinguish between predicative and non-predicative functions, and in any case PM never defines exactly what a "predicative function" actually is: this is taken as a primitive notion. Russell and Whitehead found it impossible to develop mathematics while maintaining the difference between predicative and non-predicative functions, so they introduced the axiom of reducibility, saying that for every non-predicative function there is a predicative function taking the same values. In practice this axiom essentially means that the elements of type (τ1,...,τ''m'', σ1,...,σ''n'') can be identified with the elements of type (τ1,...,τ''m''), which causes the hierarchy of ramified types to collapse down to simple type theory. (Strictly speaking this is not quite correct, because PM allows two propositional functions to be different even if they take the same values on all arguments; this differs from current mathematical practice where one normally identifies two such functions.) In
Zermelo Ernst Friedrich Ferdinand Zermelo (, ; 27 July 187121 May 1953) was a German logician and mathematician, whose work has major implications for the foundations of mathematics. He is known for his role in developing Zermelo–Fraenkel axiomatic se ...
set theory one can model the ramified type theory of PM as follows. One picks a set ι to be the type of individuals. For example, ι might be the set of natural numbers, or the set of atoms (in a set theory with atoms) or any other set one is interested in. Then if τ1,...,τ''m'' are types, the type (τ1,...,τ''m'') is the power set of the product τ1×...×τ''m'', which can also be thought of informally as the set of (propositional predicative) functions from this product to a 2-element set . The ramified type (τ1,...,τ''m'', σ1,...,σ''n'') can be modeled as the product of the type (τ1,...,τ''m''1,...,σ''n'') with the set of sequences of ''n'' quantifiers (∀ or ∃) indicating which quantifier should be applied to each variable σ''i''. (One can vary this slightly by allowing the σs to be quantified in any order, or allowing them to occur before some of the τs, but this makes little difference except to the bookkeeping.)


Notation

One author observes that "The notation in that work has been superseded by the subsequent development of logic during the 20th century, to the extent that the beginner has trouble reading PM at all"; while much of the symbolic content can be converted to modern notation, the original notation itself is "a subject of scholarly dispute", and some notation "embodies substantive logical doctrines so that it cannot simply be replaced by contemporary symbolism". Kurt Gödel was harshly critical of the notation: :"It is to be regretted that this first comprehensive and thorough-going presentation of a mathematical logic and the derivation of mathematics from it sso greatly lacking in formal precision in the foundations (contained in ✸1–✸21 of ''Principia'' [i.e., sections ✸1–✸5 (propositional logic), ✸8–14 (predicate logic with identity/equality), ✸20 (introduction to set theory), and ✸21 (introduction to relations theory)]) that it represents in this respect a considerable step backwards as compared with Frege. What is missing, above all, is a precise statement of the syntax of the formalism. Syntactical considerations are omitted even in cases where they are necessary for the cogency of the proofs". This is reflected in the example below of the symbols "''p''", "''q''", "''r''" and "⊃" that can be formed into the string "''p'' ⊃ ''q'' ⊃ ''r''". ''PM'' requires a ''definition'' of what this symbol-string means in terms of other symbols; in contemporary treatments the "formation rules" (syntactical rules leading to "well formed formulas") would have prevented the formation of this string. Source of the notation: Chapter I "Preliminary Explanations of Ideas and Notations" begins with the source of the elementary parts of the notation (the symbols =⊃≡−ΛVε and the system of dots): :"The notation adopted in the present work is based upon that of
Peano Giuseppe Peano (; ; 27 August 1858 – 20 April 1932) was an Italian mathematician and glottologist. The author of over 200 books and papers, he was a founder of mathematical logic and set theory, to which he contributed much notation. The sta ...
, and the following explanations are to some extent modeled on those which he prefixes to his ''Formulario Mathematico'' .e., Peano 1889 His use of dots as brackets is adopted, and so are many of his symbols" (''PM'' 1927:4). PM changed Peano's Ɔ to ⊃, and also adopted a few of Peano's later symbols, such as ℩ and ι, and Peano's practice of turning letters upside down. ''PM'' adopts the assertion sign "⊦" from Frege's 1879 ''
Begriffsschrift ''Begriffsschrift'' (German for, roughly, "concept-script") is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book. ''Begriffsschrift'' is usually translated as ''concept writing'' or ''concept notatio ...
'': :"(I)t may be read 'it is true that'" Thus to assert a proposition ''p'' ''PM'' writes: :"⊦. ''p''." (''PM'' 1927:92) (Observe that, as in the original, the left dot is square and of greater size than the period on the right.) Most of the rest of the notation in PM was invented by Whitehead.


An introduction to the notation of "Section A Mathematical Logic" (formulas ✸1–✸5.71)

''PM''s dots are used in a manner similar to parentheses. Each dot (or multiple dot) represents either a left or right parenthesis or the logical symbol ∧. More than one dot indicates the "depth" of the parentheses, for example, ".", ":" or ":.", "::". However the position of the matching right or left parenthesis is not indicated explicitly in the notation but has to be deduced from some rules that are complex and at times ambiguous. Moreover, when the dots stand for a logical symbol ∧ its left and right operands have to be deduced using similar rules. First one has to decide based on context whether the dots stand for a left or right parenthesis or a logical symbol. Then one has to decide how far the other corresponding parenthesis is: here one carries on until one meets either a larger number of dots, or the same number of dots next that have equal or greater "force", or the end of the line. Dots next to the signs ⊃, ≡,∨, =Df have greater force than dots next to (''x''), (∃''x'') and so on, which have greater force than dots indicating a logical product ∧. Example 1. The line :✸3.4. ⊢ : p . q . ⊃ . p ⊃ q corresponds to :⊢ ((p ∧ q) ⊃ (p ⊃ q)). The two dots standing together immediately following the assertion-sign indicate that what is asserted is the entire line: since there are two of them, their scope is greater than that of any of the single dots to their right. They are replaced by a left parenthesis standing where the dots are and a right parenthesis at the end of the formula, thus: :⊢ (p . q . ⊃ . p ⊃ q). (In practice, these outermost parentheses, which enclose an entire formula, are usually suppressed.) The first of the single dots, standing between two propositional variables, represents conjunction. It belongs to the third group and has the narrowest scope. Here it is replaced by the modern symbol for conjunction "∧", thus :⊢ (p ∧ q . ⊃ . p ⊃ q). The two remaining single dots pick out the main connective of the whole formula. They illustrate the utility of the dot notation in picking out those connectives which are relatively more important than the ones which surround them. The one to the left of the "⊃" is replaced by a pair of parentheses, the right one goes where the dot is and the left one goes as far to the left as it can without crossing a group of dots of greater force, in this case the two dots which follow the assertion-sign, thus :⊢ ((p ∧ q) ⊃ . p ⊃ q) The dot to the right of the "⊃" is replaced by a left parenthesis which goes where the dot is and a right parenthesis which goes as far to the right as it can without going beyond the scope already established by a group of dots of greater force (in this case the two dots which followed the assertion-sign). So the right parenthesis which replaces the dot to the right of the "⊃" is placed in front of the right parenthesis which replaced the two dots following the assertion-sign, thus :⊢ ((p ∧ q) ⊃ (p ⊃ q)). Example 2, with double, triple, and quadruple dots: :✸9.521. ⊢ : : (∃x). φx . ⊃ . q : ⊃ : . (∃x). φx . v . r : ⊃ . q v r stands for :((((∃x)(φx)) ⊃ (q)) ⊃ ((((∃x) (φx)) v (r)) ⊃ (q v r))) Example 3, with a double dot indicating a logical symbol (from volume 1, page 10): :''p''⊃''q'':''q''⊃''r''.⊃.''p''⊃''r'' stands for :(''p''⊃''q'') ∧ ((''q''⊃''r'')⊃(''p''⊃''r'')) where the double dot represents the logical symbol ∧ and can be viewed as having the higher priority as a non-logical single dot. Later in section ✸14, brackets " appear, and in sections ✸20 and following, braces "" appear. Whether these symbols have specific meanings or are just for visual clarification is unclear. Unfortunately the single dot (but also ":", ":.", "::", etc.) is also used to symbolise "logical product" (contemporary logical AND often symbolised by "&" or "∧"). Logical implication is represented by Peano's "Ɔ" simplified to "⊃", logical negation is symbolised by an elongated tilde, i.e., "~" (contemporary "~" or "¬"), the logical OR by "v". The symbol "=" together with "Df" is used to indicate "is defined as", whereas in sections ✸13 and following, "=" is defined as (mathematically) "identical with", i.e., contemporary mathematical "equality" (cf. discussion in section ✸13). Logical equivalence is represented by "≡" (contemporary "if and only if"); "elementary" propositional functions are written in the customary way, e.g., "''f''(''p'')", but later the function sign appears directly before the variable without parenthesis e.g., "φ''x''", "χ''x''", etc. Example, ''PM'' introduces the definition of "logical product" as follows: :✸3.01. ''p'' . ''q'' .=. ~(~''p'' v ~''q'') Df. :: where "''p'' . ''q''" is the logical product of ''p'' and ''q''. :✸3.02. ''p'' ⊃ ''q'' ⊃ ''r'' .=. ''p'' ⊃ ''q'' . ''q'' ⊃ ''r'' Df. :: This definition serves merely to abbreviate proofs. Translation of the formulas into contemporary symbols: Various authors use alternate symbols, so no definitive translation can be given. However, because of criticisms such as that of Kurt Gödel below, the best contemporary treatments will be very precise with respect to the "formation rules" (the syntax) of the formulas. The first formula might be converted into modern symbolism as follows: : (''p'' & ''q'') =df (~(~''p'' v ~''q'')) alternately : (''p'' & ''q'') =df (¬(¬''p'' v ¬''q'')) alternately : (''p'' ∧ ''q'') =df (¬(¬''p'' v ¬''q'')) etc. The second formula might be converted as follows: : (''p'' → ''q'' → ''r'') =df (''p'' → ''q'') & (''q'' → ''r'') But note that this is not (logically) equivalent to (''p'' → (''q'' → ''r'')) nor to ((''p'' → ''q'') → ''r''), and these two are not logically equivalent either.


An introduction to the notation of "Section B Theory of Apparent Variables" (formulas ✸8–✸14.34)

These sections concern what is now known as
predicate logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
, and predicate logic with identity (equality). :* NB: As a result of criticism and advances, the second edition of ''PM'' (1927) replaces ✸9 with a new ✸8 (Appendix A). This new section eliminates the first edition's distinction between real and apparent variables, and it eliminates "the primitive idea 'assertion of a propositional function'. To add to the complexity of the treatment, ✸8 introduces the notion of substituting a "matrix", and the
Sheffer stroke In Boolean functions and propositional calculus, the Sheffer stroke denotes a logical operation that is equivalent to the negation of the conjunction operation, expressed in ordinary language as "not both". It is also called nand ("not and") ...
: :::* Matrix: In contemporary usage, ''PM''s ''matrix'' is (at least for
propositional function In propositional calculus, a propositional function or a predicate is a sentence expressed in a way that would assume the value of true or false, except that within the sentence there is a variable (''x'') that is not defined or specified (thus be ...
s), a
truth table A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—which sets out the functional values of logical expressions on each of their functional argumen ...
, i.e., ''all'' truth-values of a propositional or predicate function. :::* Sheffer stroke: Is the contemporary logical NAND (NOT-AND), i.e., "incompatibility", meaning: ::::"Given two propositions ''p'' and ''q'', then ' ''p'' , ''q'' ' means "proposition ''p'' is incompatible with proposition ''q''", i.e., if both propositions ''p'' and ''q'' evaluate as true, then and only then ''p'' , ''q'' evaluates as false." After section ✸8 the Sheffer stroke sees no usage. Section ✸10: The existential and universal "operators": ''PM'' adds "(''x'')" to represent the contemporary symbolism "for all ''x'' " i.e., " ∀''x''", and it uses a backwards serifed E to represent "there exists an ''x''", i.e., "(Ǝx)", i.e., the contemporary "∃x". The typical notation would be similar to the following: : "(''x'') . φ''x''" means "for all values of variable ''x'', function φ evaluates to true" : "(Ǝ''x'') . φ''x''" means "for some value of variable ''x'', function φ evaluates to true" Sections ✸10, ✸11, ✸12: Properties of a variable extended to all individuals: section ✸10 introduces the notion of "a property" of a "variable". ''PM'' gives the example: φ is a function that indicates "is a Greek", and ψ indicates "is a man", and χ indicates "is a mortal" these functions then apply to a variable ''x''. ''PM'' can now write, and evaluate: : (''x'') . ψ''x'' The notation above means "for all ''x'', ''x'' is a man". Given a collection of individuals, one can evaluate the above formula for truth or falsity. For example, given the restricted collection of individuals the above evaluates to "true" if we allow for Zeus to be a man. But it fails for: : (''x'') . φ''x'' because Russell is not Greek. And it fails for : (''x'') . χ''x'' because Zeus is not a mortal. Equipped with this notation ''PM'' can create formulas to express the following: "If all Greeks are men and if all men are mortals then all Greeks are mortals". (''PM'' 1962:138) :(''x'') . φ''x'' ⊃ ψ''x'' :(''x''). ψ''x'' ⊃ χ''x'' :⊃: (''x'') . φ''x'' ⊃ χ''x'' Another example: the formula: :✸10.01. (Ǝ''x''). φ''x'' . = . ~(''x'') . ~φ''x'' Df. means "The symbols representing the assertion 'There exists at least one ''x'' that satisfies function φ' is defined by the symbols representing the assertion 'It's not true that, given all values of ''x'', there are no values of ''x'' satisfying φ'". The symbolisms ⊃''x'' and "≡''x''" appear at ✸10.02 and ✸10.03. Both are abbreviations for universality (i.e., for all) that bind the variable ''x'' to the logical operator. Contemporary notation would have simply used parentheses outside of the equality ("=") sign: :✸10.02 φ''x'' ⊃''x'' ψ''x'' .=. (''x''). φ''x'' ⊃ ψ''x'' Df :: Contemporary notation: ∀''x''(φ(''x'') → ψ(''x'')) (or a variant) :✸10.03 φ''x'' ≡''x'' ψ''x'' .=. (''x''). φ''x'' ≡ ψ''x'' Df :: Contemporary notation: ∀''x''(φ(''x'') ↔ ψ(''x'')) (or a variant) ''PM'' attributes the first symbolism to Peano. Section ✸11 applies this symbolism to two variables. Thus the following notations: ⊃''x'', ⊃''y'', ⊃''x, y'' could all appear in a single formula. Section ✸12 reintroduces the notion of "matrix" (contemporary
truth table A truth table is a mathematical table used in logic—specifically in connection with Boolean algebra, boolean functions, and propositional calculus—which sets out the functional values of logical expressions on each of their functional argumen ...
), the notion of logical types, and in particular the notions of ''first-order'' and ''second-order'' functions and propositions. New symbolism "φ ! ''x''" represents any value of a first-order function. If a circumflex "^" is placed over a variable, then this is an "individual" value of ''y'', meaning that "''ŷ''" indicates "individuals" (e.g., a row in a truth table); this distinction is necessary because of the matrix/extensional nature of propositional functions. Now equipped with the matrix notion, ''PM'' can assert its controversial axiom of reducibility: a function of one or two variables (two being sufficient for ''PM''s use) ''where all its values are given'' (i.e., in its matrix) is (logically) equivalent ("≡") to some "predicative" function of the same variables. The one-variable definition is given below as an illustration of the notation (''PM'' 1962:166–167): ✸12.1 ⊢: (Ǝ ''f''): φ''x'' .≡''x''. ''f'' ! ''x'' Pp; :: Pp is a "Primitive proposition" ("Propositions assumed without proof") (''PM'' 1962:12, i.e., contemporary "axioms"), adding to the 7 defined in section ✸1 (starting with ✸1.1 modus ponens). These are to be distinguished from the "primitive ideas" that include the assertion sign "⊢", negation "~", logical OR "V", the notions of "elementary proposition" and "elementary propositional function"; these are as close as ''PM'' comes to rules of notational formation, i.e., syntax. This means: "We assert the truth of the following: There exists a function ''f'' with the property that: given all values of ''x'', their evaluations in function φ (i.e., resulting their matrix) is logically equivalent to some ''f'' evaluated at those same values of ''x''. (and vice versa, hence logical equivalence)". In other words: given a matrix determined by property φ applied to variable ''x'', there exists a function ''f'' that, when applied to the ''x'' is logically equivalent to the matrix. Or: every matrix φ''x'' can be represented by a function ''f'' applied to ''x'', and vice versa. ✸13: The identity operator "=" : This is a definition that uses the sign in two different ways, as noted by the quote from ''PM'': :✸13.01. ''x'' = ''y'' .=: (φ): φ ! ''x'' . ⊃ . φ ! ''y'' Df means: :"This definition states that ''x'' and ''y'' are to be called identical when every predicative function satisfied by ''x'' is also satisfied by ''y'' ... Note that the second sign of equality in the above definition is combined with "Df", and thus is not really the same symbol as the sign of equality which is defined." The not-equals sign "≠" makes its appearance as a definition at ✸13.02. ✸14: Descriptions: :"A ''description'' is a phrase of the form "the term ''y'' which satisfies φ''ŷ'', where φ''ŷ'' is some function satisfied by one and only one argument." From this ''PM'' employs two new symbols, a forward "E" and an inverted iota "℩". Here is an example: :✸14.02. E ! ( ℩''y'') (φ''y'') .=: ( Ǝ''b''):φ''y'' . ≡''y'' . ''y'' = ''b'' Df. This has the meaning: : "The ''y'' satisfying φ''ŷ'' exists," which holds when, and only when φ''ŷ'' is satisfied by one value of ''y'' and by no other value." (''PM'' 1967:173–174)


Introduction to the notation of the theory of classes and relations

The text leaps from section ✸14 directly to the foundational sections ✸20 GENERAL THEORY OF CLASSES and ✸21 GENERAL THEORY OF RELATIONS. "Relations" are what is known in contemporary
set theory Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly conce ...
as sets of ordered pairs. Sections ✸20 and ✸22 introduce many of the symbols still in contemporary usage. These include the symbols "ε", "⊂", "∩", "∪", "–", "Λ", and "V": "ε" signifies "is an element of" (''PM'' 1962:188); "⊂" (✸22.01) signifies "is contained in", "is a subset of"; "∩" (✸22.02) signifies the intersection (logical product) of classes (sets); "∪" (✸22.03) signifies the union (logical sum) of classes (sets); "–" (✸22.03) signifies negation of a class (set); "Λ" signifies the null class; and "V" signifies the universal class or universe of discourse. Small Greek letters (other than "ε", "ι", "π", "φ", "ψ", "χ", and "θ") represent classes (e.g., "α", "β", "γ", "δ", etc.) (''PM'' 1962:188): : ''x'' ε α :: "The use of single letter in place of symbols such as ''ẑ''(φ''z'') or ''ẑ''(φ ! ''z'') is practically almost indispensable, since otherwise the notation rapidly becomes intolerably cumbrous. Thus ' ''x'' ε α' will mean ' ''x'' is a member of the class α'". (''PM'' 1962:188) :α ∪ –α = V ::The union of a set and its inverse is the universal (completed) set. :α ∩ –α = Λ ::The intersection of a set and its inverse is the null (empty) set. When applied to relations in section ✸23 CALCULUS OF RELATIONS, the symbols "⊂", "∩", "∪", and "–" acquire a dot: for example: "⊍", "∸". The notion, and notation, of "a class" (set): In the first edition ''PM'' asserts that no new primitive ideas are necessary to define what is meant by "a class", and only two new "primitive propositions" called the axioms of reducibility for classes and relations respectively (''PM'' 1962:25). But before this notion can be defined, ''PM'' feels it necessary to create a peculiar notation "''ẑ''(φ''z'')" that it calls a "fictitious object". (''PM'' 1962:188) : ⊢: ''x'' ε ''ẑ''(φ''z'') .≡. (φ''x'') :: "i.e., ' ''x'' is a member of the class determined by (φ''ẑ'')' is ogicallyequivalent to ' ''x'' satisfies (φ''ẑ''),' or to '(φ''x'') is true.'". (''PM'' 1962:25) At least ''PM'' can tell the reader how these fictitious objects behave, because "A class is wholly determinate when its membership is known, that is, there cannot be two different classes having the same membership" (''PM'' 1962:26). This is symbolised by the following equality (similar to ✸13.01 above: : ''ẑ''(φ''z'') = ''ẑ''(ψ''z'') . ≡ : (''x''): φ''x'' .≡. ψ''x'' ::"This last is the distinguishing characteristic of classes, and justifies us in treating ''ẑ''(ψ''z'') as the class determined by he functionψ''ẑ''." (''PM'' 1962:188) Perhaps the above can be made clearer by the discussion of classes in ''Introduction to the Second Edition'', which disposes of the ''Axiom of Reducibility'' and replaces it with the notion: "All functions of functions are extensional" (''PM'' 1962:xxxix), i.e., : φ''x'' ≡''x'' ψ''x'' .⊃. (''x''): ƒ(φ''ẑ'') ≡ ƒ(ψ''ẑ'') (''PM'' 1962:xxxix) This has the reasonable meaning that "IF for all values of ''x'' the ''truth-values'' of the functions φ and ψ of ''x'' are ogicallyequivalent, THEN the function ƒ of a given φ''ẑ'' and ƒ of ψ''ẑ'' are ogicallyequivalent." ''PM'' asserts this is "obvious": : "This is obvious, since φ can only occur in ƒ(φ''ẑ'') by the substitution of values of φ for ''p, q, r, ...'' in a ogical-function, and, if φ''x'' ≡ ψ''x'', the substitution of φ''x'' for ''p'' in a ogical-function gives the same truth-value to the truth-function as the substitution of ψ''x''. Consequently there is no longer any reason to distinguish between functions classes, for we have, in virtue of the above, : φ''x'' ≡''x'' ψ''x'' .⊃. (''x''). φ''ẑ'' = . ψ''ẑ''". Observe the change to the equality "=" sign on the right. ''PM'' goes on to state that will continue to hang onto the notation "''ẑ''(φ''z'')", but this is merely equivalent to φ''ẑ'', and this is a class. (all quotes: ''PM'' 1962:xxxix).


Consistency and criticisms

According to Carnap's "Logicist Foundations of Mathematics", Russell wanted a theory that could plausibly be said to derive all of mathematics from purely logical axioms. However, Principia Mathematica required, in addition to the basic axioms of type theory, three further axioms that seemed to not be true as mere matters of logic, namely the
axiom of infinity In axiomatic set theory and the branches of mathematics and philosophy that use it, the axiom of infinity is one of the axioms of Zermelo–Fraenkel set theory. It guarantees the existence of at least one infinite set, namely a set containing th ...
, the
axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
, and the axiom of reducibility. Since the first two were existential axioms, Russell phrased mathematical statements depending on them as conditionals. But reducibility was required to be sure that the formal statements even properly express statements of real analysis, so that statements depending on it could not be reformulated as conditionals. Frank Ramsey tried to argue that Russell's ramification of the theory of types was unnecessary, so that reducibility could be removed, but these arguments seemed inconclusive. Beyond the status of the axioms as
logical truth Logical truth is one of the most fundamental concepts in logic. Broadly speaking, a logical truth is a statement which is true regardless of the truth or falsity of its constituent propositions. In other words, a logical truth is a statement whic ...
s, one can ask the following questions about any system such as PM: * whether a contradiction could be derived from the axioms (the question of inconsistency), and * whether there exists a
mathematical statement In logic, a predicate is a symbol which represents a property or a relation. For instance, in the first order formula P(a), the symbol P is a predicate which applies to the individual constant a. Similarly, in the formula R(a,b), R is a predicat ...
which could neither be proven nor disproven in the system (the question of completeness).
Propositional logic Propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. It deals with propositions (which can be true or false) and relations b ...
itself was known to be consistent, but the same had not been established for ''Principias axioms of set theory. (See
Hilbert's second problem In mathematics, Hilbert's second problem was posed by David Hilbert in 1900 as one of his Hilbert's problems, 23 problems. It asks for a proof that the arithmetic is consistency proof, consistent – free of any internal contradictions. Hilber ...
.) Russell and Whitehead suspected that the system in PM is incomplete: for example, they pointed out that it does not seem powerful enough to show that the cardinal ℵω exists. However, one can ask if some recursively axiomatizable extension of it is complete and consistent.


Gödel 1930, 1931

In 1930,
Gödel's completeness theorem Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic. The completeness theorem applies to any first-order theory: ...
showed that first-order predicate logic itself was complete in a much weaker sense—that is, any sentence that is unprovable from a given set of axioms must actually be false in some
model A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure. Models c ...
of the axioms. However, this is not the stronger sense of completeness desired for Principia Mathematica, since a given system of axioms (such as those of Principia Mathematica) may have many models, in some of which a given statement is true and in others of which that statement is false, so that the statement is left undecided by the axioms. Gödel's incompleteness theorems cast unexpected light on these two related questions. Gödel's first incompleteness theorem showed that no recursive extension of ''Principia'' could be both consistent and complete for arithmetic statements. (As mentioned above, Principia itself was already known to be incomplete for some non-arithmetic statements.) According to the theorem, within every sufficiently powerful recursive
logical system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...
(such as ''Principia''), there exists a statement ''G'' that essentially reads, "The statement ''G'' cannot be proved." Such a statement is a sort of
Catch-22 ''Catch-22'' is a satirical war novel by American author Joseph Heller. He began writing it in 1953; the novel was first published in 1961. Often cited as one of the most significant novels of the twentieth century, it uses a distinctive non-ch ...
: if ''G'' is provable, then it is false, and the system is therefore inconsistent; and if ''G'' is not provable, then it is true, and the system is therefore incomplete. Gödel's second incompleteness theorem (1931) shows that no
formal system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...
extending basic arithmetic can be used to prove its own consistency. Thus, the statement "there are no contradictions in the ''Principia'' system" cannot be proven in the ''Principia'' system unless there ''are'' contradictions in the system (in which case it can be proven both true and false).


Wittgenstein 1919, 1939

By the second edition of ''PM'', Russell had removed his ''axiom of reducibility'' to a new axiom (although he does not state it as such). Gödel 1944:126 describes it this way: :"This change is connected with the new axiom that functions can occur in propositions only "through their values", i.e., extensionally . . .
his is His or HIS may refer to: Computing * Hightech Information System, a Hong Kong graphics card company * Honeywell Information Systems * Hybrid intelligent system * Microsoft Host Integration Server Education * Hangzhou International School, in ...
quite unobjectionable even from the constructive standpoint . . . provided that quantifiers are always restricted to definite orders". This change from a quasi-''intensional'' stance to a fully ''extensional'' stance also restricts
predicate logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
to the second order, i.e. functions of functions: "We can decide that mathematics is to confine itself to functions of functions which obey the above assumption" (''PM'' 2nd edition p. 401, Appendix C). This new proposal resulted in a dire outcome. An "extensional stance" and restriction to a second-order predicate logic means that a propositional function extended to all individuals such as "All 'x' are blue" now has to list all of the 'x' that satisfy (are true in) the proposition, listing them in a possibly infinite conjunction: e.g. ''x1'' ∧ ''x2'' ∧ . . . ∧ ''xn'' ∧ . . .. Ironically, this change came about as the result of criticism from Wittgenstein in his 1919 ''
Tractatus Logico-Philosophicus The ''Tractatus Logico-Philosophicus'' (widely abbreviated and cited as TLP) is a book-length philosophical work by the Austrian philosopher Ludwig Wittgenstein which deals with the relationship between language and reality and aims to define th ...
''. As described by Russell in the Introduction to the Second Edition of ''PM'': :"There is another course, recommended by Wittgenstein† (†''Tractatus Logico-Philosophicus'', *5.54ff) for philosophical reasons. This is to assume that functions of propositions are always truth-functions, and that a function can only occur in a proposition through its values. .. orking through the consequencesit appears that everything in Vol. I remains true (though often new proofs are required); the theory of inductive cardinals and ordinals survives; but it seems that the theory of infinite Dedekindian and well-ordered series largely collapses, so that irrationals, and real numbers generally, can no longer be adequately dealt with. Also Cantor's proof that 2n > ''n'' breaks down unless ''n'' is finite." (''PM'' 2nd edition reprinted 1962:xiv, also cf. new Appendix C). In other words, the fact that an infinite list cannot realistically be specified means that the concept of "number" in the infinite sense (i.e. the continuum) cannot be described by the new theory proposed in ''PM Second Edition''.
Wittgenstein Ludwig Josef Johann Wittgenstein ( ; ; 26 April 1889 – 29 April 1951) was an Austrians, Austrian-British people, British philosopher who worked primarily in logic, the philosophy of mathematics, the philosophy of mind, and the philosophy o ...
in his ''Lectures on the Foundations of Mathematics, Cambridge 1939'' criticised ''Principia'' on various grounds, such as: * It purports to reveal the fundamental basis for arithmetic. However, it is our everyday arithmetical practices such as counting which are fundamental; for if a persistent discrepancy arose between counting and ''Principia'', this would be treated as evidence of an error in ''Principia'' (e.g., that Principia did not characterise numbers or addition correctly), not as evidence of an error in everyday counting. * The calculating methods in ''Principia'' can only be used in practice with very small numbers. To calculate using large numbers (e.g., billions), the formulae would become too long, and some short-cut method would have to be used, which would no doubt rely on everyday techniques such as counting (or else on non-fundamental and hence questionable methods such as induction). So again ''Principia'' depends on everyday techniques, not vice versa. Wittgenstein did, however, concede that ''Principia'' may nonetheless make some aspects of everyday arithmetic clearer.


Gödel 1944

In his 1944 ''Russell's mathematical logic'', Gödel offers a "critical but sympathetic discussion of the logicistic order of ideas": :"It is to be regretted that this first comprehensive and thorough-going presentation of a mathematical logic and the derivation of mathematics from it sso greatly lacking in formal precision in the foundations (contained in *1-*21 of ''Principia'') that it represents in this respect a considerable step backwards as compared with Frege. What is missing, above all, is a precise statement of the syntax of the formalism. Syntactical considerations are omitted even in cases where they are necessary for the cogency of the proofs . . . The matter is especially doubtful for the rule of substitution and of replacing defined symbols by their ''definiens'' . . . it is chiefly the rule of substitution which would have to be proved" (Gödel 1944:124)Gödel 1944 ''Russell's mathematical logic'' in ''Kurt Gödel: Collected Works Volume II'', Oxford University Press, New York, NY, .


Contents


Part I Mathematical logic. Volume I ✸1 to ✸43

This section describes the propositional and predicate calculus, and gives the basic properties of classes, relations, and types.


Part II Prolegomena to cardinal arithmetic. Volume I ✸50 to ✸97

This part covers various properties of relations, especially those needed for cardinal arithmetic.


Part III Cardinal arithmetic. Volume II ✸100 to ✸126

This covers the definition and basic properties of cardinals. A cardinal is defined to be an equivalence class of similar classes (as opposed to ZFC, where a cardinal is a special sort of von Neumann ordinal). Each type has its own collection of cardinals associated with it, and there is a considerable amount of bookkeeping necessary for comparing cardinals of different types. PM define addition, multiplication and exponentiation of cardinals, and compare different definitions of finite and infinite cardinals. ✸120.03 is the Axiom of infinity.


Part IV Relation-arithmetic. Volume II ✸150 to ✸186

A "relation-number" is an equivalence class of isomorphic relations. PM defines analogues of addition, multiplication, and exponentiation for arbitrary relations. The addition and multiplication is similar to the usual definition of addition and multiplication of ordinals in ZFC, though the definition of exponentiation of relations in PM is not equivalent to the usual one used in ZFC.


Part V Series. Volume II ✸200 to ✸234 and volume III ✸250 to ✸276

This covers series, which is PM's term for what is now called a totally ordered set. In particular it covers complete series, continuous functions between series with the order topology (though of course they do not use this terminology), well-ordered series, and series without "gaps" (those with a member strictly between any two given members).


Part VI Quantity. Volume III ✸300 to ✸375

This section constructs the ring of integers, the fields of rational and real numbers, and "vector-families", which are related to what are now called torsors over abelian groups.


Comparison with set theory

This section compares the system in PM with the usual mathematical foundations of ZFC. The system of PM is roughly comparable in strength with Zermelo set theory (or more precisely a version of it where the axiom of separation has all quantifiers bounded). * The system of propositional logic and predicate calculus in PM is essentially the same as that used now, except that the notation and terminology has changed. * The most obvious difference between PM and set theory is that in PM all objects belong to one of a number of disjoint types. This means that everything gets duplicated for each (infinite) type: for example, each type has its own ordinals, cardinals, real numbers, and so on. This results in a lot of bookkeeping to relate the various types with each other. * In ZFC functions are normally coded as sets of ordered pairs. In PM functions are treated rather differently. First of all, "function" means "propositional function", something taking values true or false. Second, functions are not determined by their values: it is possible to have several different functions all taking the same values (for example, one might regard 2''x''+2 and 2(''x''+1) as different functions on grounds that the computer programs for evaluating them are different). The functions in ZFC given by sets of ordered pairs correspond to what PM call "matrices", and the more general functions in PM are coded by quantifying over some variables. In particular PM distinguishes between functions defined using quantification and functions not defined using quantification, whereas ZFC does not make this distinction. * PM has no analogue of the
axiom of replacement In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite ...
, though this is of little practical importance as this axiom is used very little in mathematics outside set theory. * PM emphasizes relations as a fundamental concept, whereas in current mathematical practice it is functions rather than relations that are treated as more fundamental; for example, category theory emphasizes morphisms or functions rather than relations. (However, there is an analogue of categories called
allegories As a literary device or artistic form, an allegory is a narrative or visual representation in which a character, place, or event can be interpreted to represent a hidden meaning with moral or political significance. Authors have used allegory th ...
that models relations rather than functions, and is quite similar to the type system of PM.) * In PM, cardinals are defined as classes of similar classes, whereas in ZFC cardinals are special ordinals. In PM there is a different collection of cardinals for each type with some complicated machinery for moving cardinals between types, whereas in ZFC there is only 1 sort of cardinal. Since PM does not have any equivalent of the axiom of replacement, it is unable to prove the existence of cardinals greater than ℵω. * In PM ordinals are treated as equivalence classes of well-ordered sets, and as with cardinals there is a different collection of ordinals for each type. In ZFC there is only one collection of ordinals, usually defined as von Neumann ordinals. One strange quirk of PM is that they do not have an ordinal corresponding to 1, which causes numerous unnecessary complications in their theorems. The definition of ordinal exponentiation αβ in PM is not equivalent to the usual definition in ZFC and has some rather undesirable properties: for example, it is not continuous in β and is not well ordered (so is not even an ordinal). * The constructions of the integers, rationals and real numbers in ZFC have been streamlined considerably over time since the constructions in PM.


Differences between editions

Apart from corrections of misprints, the main text of PM is unchanged between the first and second editions. The main text in Volumes 1 and 2 was reset, so that it occupies fewer pages in each. In the second edition, Volume 3 was not reset, being photographically reprinted with the same page numbering; corrections were still made. The total number of pages (excluding the endpapers) in the first edition is 1,996; in the second, 2,000. Volume 1 has five new additions: * A 54-page introduction by Russell describing the changes they would have made had they had more time and energy. The main change he suggests is the removal of the controversial axiom of reducibility, though he admits that he knows no satisfactory substitute for it. He also seems more favorable to the idea that a function should be determined by its values (as is usual in current mathematical practice). * Appendix A, numbered as *8, 15 pages, about the Sheffer stroke. * Appendix B, numbered as *89, discussing induction without the axiom of reducibility. * Appendix C, 8 pages, discussing propositional functions. * An 8-page list of definitions at the end, giving a much-needed index to the 500 or so notations used. In 1962, Cambridge University Press published a shortened paperback edition containing parts of the second edition of Volume 1: the new introduction (and the old), the main text up to *56, and Appendices A and C.


Editions

* * * * * * * The first edition was reprinted in 2009 by Merchant Books, , , .


See also

* Axiomatic set theory *
Boolean algebra In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, whereas i ...
*
Information Processing Language Information Processing Language (IPL) is a programming language created by Allen Newell, Cliff Shaw, and Herbert A. Simon at RAND Corporation and the Carnegie Institute of Technology about 1956. Newell had the job of language specifier-applicat ...
– first computational demonstration of theorems in PM * '' Introduction to Mathematical Philosophy''


Footnotes


References

*
Stephen Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
(1952). ''Introduction to Metamathematics'', 6th Reprint, North-Holland Publishing Company, Amsterdam NY, . ** * Ivor Grattan-Guinness (2000). ''The Search for Mathematical Roots 1870–1940'', Princeton University Press, Princeton NJ, . *
Ludwig Wittgenstein Ludwig Josef Johann Wittgenstein ( ; ; 26 April 1889 – 29 April 1951) was an Austrian-British philosopher who worked primarily in logic, the philosophy of mathematics, the philosophy of mind, and the philosophy of language. He is con ...
(2009), ''Major Works: Selected Philosophical Writings'', HarperrCollins, New York, . In particular: :: ''Tractatus Logico-Philosophicus'' (Vienna 1918), original publication in German). *
Jean van Heijenoort Jean Louis Maxime van Heijenoort (; July 23, 1912 – March 29, 1986) was a historian of mathematical logic. He was also a personal secretary to Leon Trotsky from 1932 to 1939, and an American Trotskyist until 1947. Life Van Heijenoort was born ...
editor (1967). ''From Frege to Gödel: A Source book in Mathematical Logic, 1879–1931'', 3rd printing, Harvard University Press, Cambridge MA, . *
Michel Weber Michel Weber (born 1963) is a Belgian philosopher. He is best known as an interpreter and advocate of the philosophy of Alfred North Whitehead, and has come to prominence as the architect and organizer of an overlapping array of international ...
and Will Desmond (eds.) (2008)
Handbook of Whiteheadian Process Thought
', Frankfurt / Lancaster, Ontos Verlag, Process Thought X1 & X2.


External links

* * Stanford Encyclopedia of Philosophy: **
Principia Mathematica
' – by A. D. Irvine *
The Notation in ''Principia Mathematica''
– by Bernard Linsky.

in a more modern notation (
Metamath Metamath is a formal language and an associated computer program (a proof checker) for archiving, verifying, and studying mathematical proofs. Several databases of proved theorems have been developed using Metamath covering standard results in ...
) {{Authority control Large-scale mathematical formalization projects 1910 non-fiction books 1912 non-fiction books 1913 non-fiction books 1910 in science 1912 in science 1913 in science Books by Bertrand Russell Works by Alfred North Whitehead Books about philosophy of mathematics