The Principia Mathematica数学原理

数学原理 - 维基百科，自由的百科全书 (wikipedia.org)
《数学原理》（英語：Principia Mathematica）是由伯特兰·罗素与他的老师阿尔弗雷德·诺思·怀特黑德合著的一本数学书籍，书籍共分三卷，分别出版于1910年，1912年，1913年。

它通常缩写為PM (Principia Mathematica)，為表述所有数学真理在一组数理逻辑內的公理和推理规则下，原则上都是可以证明的。因此这一雄心勃勃的项目對於数学史和哲学史都是非常重要的，[1]然而在1931年，哥德尔不完备性定理证明對於数学原理或其他任何類似的尝试，这个崇高的目标皆永远无法达到；也就是说，任何尝试以一组公理和推理规则來建立的数学系統，不是不自洽，就是不完備 (即存在一些数学真理不能由此系統推理演绎出來)。

数学原理的一个主要的灵感和动机来自于逻辑学家戈特洛布·弗雷格的工作，但伯特兰·罗素发现其允许建设有矛盾的集合（罗素悖论）。数学原理排除无限制创建任意的集合來试图避免这个问题，它以不同“类型”的集合來取代一般的集合，一组特定类型的集合只能包含套較低的类型。然而在当代数学，會使用如Zermelo-Fraenkel的集合理论体系，來避免如罗素的笨拙方式。

现代图书馆將此書排在二十世纪英文非虚构书籍中的第23名。[2]

基本范围
该原理仅覆盖集理论，基数，序数和实数。从现实分析，更深层次的定理并没有包括在内。 几何的基础第四卷已在筹划，但作者在第三卷完成后智力枯竭。

理论基础
由于在理论上由库尔特·哥德尔（下同）的批评指出，不同于形式主义理论，PM的“logicistic”理论有没有“形式主义的语法明确说明”。另一种看法是，在理论上，（在模型论的意义上）解释的真值的符号的行为来表述“⊢”（真理断言），“〜”（逻辑非）和“V”（逻辑或）。

真值：PM嵌入“真”和“假”的概念，“原始命题”的概念。原料（纯）形式主义理论所不能提供形成了“原始命题”诚，符号本身可能是绝对武断和陌生的符号的含义。该理论将符号行为也只是如何基于理论的语法指定。再后来，通过“价值”的分配，模式将指定什么公式说的解释。因此，在正式的克莱尼符号下方设置，“解释”什么样的符号通常是指，并暗示他们如何最终被采用，在括号内，例如，“¬（不）”。但是，这不是一个纯粹的形式主义理论。

正式的理论的当代建构
下面的形式主义理论是作为对比PM的logicistic理论。一个现代的形式系统将构造如下：

使用的符号：该组是开始集合，其它符号可以出现，而是仅由从这些开始码的定义。起始组可能是Kleene从中导出的以下一组：逻辑符号“→”（意味着，IF-THEN“⊃”），“＆”（和）中，“V”（或），“¬”（不） “∀”（所有），“∃”（存在）;谓词符号“=”（等于）;函数符号“+”（算术加法），“∙”（算术乘法），“'”（继任者）;个别符号“0”（零）;变量“一”，“B”，“C”等;和括号“（”和“）”。 符号串：该理论将通过串联（并列）建立这些符号的“弦”.[3] 形成规则：理论指定的语法规则（语法规则），通常为以“0”开头，并指定如何建立可接受的字符串或“合式公式”（Wff）递归定义[4]这包括对于所谓的“变量”（相对于其他符号类型）中的符号串的规则对“替代”。[5] 变换规则（S）：指定符号和符号序列的行为的公理。 推理，支队规则，肯定前件：允许理论从“前提”，导致到了“分离”一个“结论”的规则，并随后放弃“处所”（符号到行的左边│或符号线之上，如果水平）。如果不是这种情况，那么取代会导致在必须进行前向越来越长的字符串。事实上，假言推理的应用程序后，没有什么是离开，但结论，剩下的永远消失。 当代理论往往指定为第一公理古典或假言推理或“脱离规则”： A，A⊃乙│乙 符号“│”通常写为水平线，这里“⊃”是指“意味着”。符号A和B是“替身”的字符串;这种形式的符号被称为“公理模式”（即，有一种特殊形式的符号可以采取可数）。这可以读取类似的方式IF-THEN但有区别：给定的符号串IF A和A蕴涵B，那么B（并保留进一步使用仅B）。但符号都没有“解释”（例如，没有“真值表”或“真值”或“真理功能”）和假言推理机制上进行，由单独的语法。

构成
PM理论既有相似之处显著，以及类似的差异，当代形式理论。克林指出，“这种演绎的数学与逻辑提供了直观希尔伯特的公理被设计成相信，或者至少被接受为关于世界的假设合理的。”[6]事实上，PM理论不像形式主义理论，即操纵符号根据语法规则，PM引入了“真值”的概念，即在现实世界意义的真理和谬误，以及“断言真相”几乎立即作为理论结构的第五和第六元素（PM 1962：4-36）：

版本差异
卷I有五个新增：

附录A,编号为8.15新增谢费尔竖线
附录B,编号为* 89,讨论感应没有还原性的公理
附录C、8页讨论命题函数
8页的列表定义最后,给急需的索引使用的大约500个符号。
1962年杯发表缩短平装版包含部分的第二版的卷I:新介绍,正文* 56,和附录a和C。
參見
各種數學敘述









 

Principia Mathematica - Wikipedia

The Principia Mathematica (often abbreviated PM) is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell 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 was conceived as a sequel to Russell's 1903 The Principles of Mathematics, 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 notions, axioms, and inference rules; (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 at the turn of the 20th century, like Russell's paradox.[3]

This third aim motivated the adoption of the theory of types 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.[4] Indeed, PM was in part brought about by an interest in logicism, 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 anymore: 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. 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.[5] 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 Principia's logical system.

Scope of foundations laid
The Principia covered only set theory, cardinal numbers, ordinal numbers, and real numbers. Deeper theorems from real analysis 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 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 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

List of propositions referred to by names
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 ")".[6]
Symbol strings: The theory will build "strings" of these symbols by concatenation (juxtaposition).[7]
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).[8] This includes a rule for "substitution"[9] of strings for the symbols called "variables".
Transformation rule(s): The axioms 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":
A, A ⊃ B | B
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.[clarification needed] 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".[10] 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 "[space] ... [space]":[11]
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) (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. "[If] '⊦. 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 ' [in 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 ("|") 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").[12] PM then "advance[s] 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.

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 modern 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, PM allows two propositional functions to be different even if they take the same values on all arguments; this differs from modern mathematical practice where one normally identifies two such functions.)

In Zermelo 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 {true,false}. 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.)