Principia Mathematica is modern and insightful
Principia Mathematica is modern and insightful
《数学原理》：现代且富有洞见
Introduction
引言
Principia Mathematica by Whitehead and Russell was published back in 1910 — and yet it reads like a modern text on programming languages. I have found Principia quite engaging and hard to put away. Principia discusses, with great insight, such modern topics as extensionality/intensionality, referential transparency, type. It contains perhaps the first mentioning of domain', alpha renaming’ and type' in the modern sense. Its incomplete symbols’ — the ones that only make sense in a context — anticipate continuations and control operators. It insightfully observes that the notions of free and bound variables, substitution, abstraction, and application all come from linguistics. I could not help but feel that Principia already contained lambda-calculus. It also seems that Russell and Whitehead anticipated intuitionism, for example, when insisting on separate notations for ‘any’ vs. `all’ (although admitting the equivalence of these notions in their theory).
怀特海（Whitehead）和罗素（Russell）合著的《数学原理》（Principia Mathematica）出版于1910年，但读起来却像是一本现代编程语言教材。我发现《数学原理》非常引人入胜，令人爱不释手。书中以深刻的见解探讨了外延性/内涵性、引用透明性、类型等现代课题。它可能首次提到了现代意义上的“定义域”（domain）、“α-重命名”（alpha renaming）和“类型”（type）。其“不完全符号”（incomplete symbols）——即那些只有在特定上下文中才有意义的符号——预示了延续（continuations）和控制算子（control operators）的概念。书中敏锐地指出，自由变量与约束变量、代换、抽象和应用等概念均源于语言学。我不禁感到，《数学原理》中其实已经蕴含了λ-演算。此外，罗素和怀特海似乎还预见了直觉主义，例如他们坚持为“任意”（any）与“所有”（all）使用不同的符号（尽管他们承认在他们的理论中这些概念是等价的）。
Referential transparency, extensionality
引用透明性与外延性
Page 8 of Principia has perhaps the first mention in mathematical literature of intensions and extensions, and what is now called `referential transparency’: if p≡q we shall have f(p)≡f(q)''. Here f(p) is a proposition that includes another proposition p. In modern terms, we would call f a context and denote by C[], and say that if p≡q then C[p]≡C[q], which is the familiar statement of a referential transparent context. The page then shows an example of a non-referentially transparent context A believes p”: a proposition whose meaning varies when p is substituted with equivalent propositions. The example betrays the origin of this concept, from linguistics, specifically, from the work of Frege (who is mentioned in a footnote). The book states that “mathematics is always concerned with extensions rather than intensions.” (again borrowing Frege terms, but in English translation.)
《数学原理》第8页可能首次在数学文献中提到了内涵与外延，以及现在所谓的“引用透明性”：“若 p≡q，则有 f(p)≡f(q)”。此处 f(p) 是一个包含另一个命题 p 的命题。用现代术语来说，我们会称 f 为上下文并记作 C[]，并称若 p≡q 则 C[p]≡C[q]，这就是引用透明上下文的常见定义。该页随后展示了一个非引用透明上下文的例子——“A 相信 p”：当 p 被等价命题替换时，该命题的含义会发生变化。这个例子揭示了该概念源于语言学，具体来说源于弗雷格（Frege）的工作（他在脚注中被提及）。书中指出，“数学总是关注外延而非内涵。”（同样借用了弗雷格的术语，但采用了英文翻译。）
Definitions: a mere typographic convenience of most importance
定义：至关重要的排版便利
On p12, the book states that definitions are merely typographic conveniences. On the other hand, definitions are of most importance, because they show the intent. …the definitions are not part of our subject, but are, strictly speaking, mere typographical conveniences.… In spite of the fact that definitions are theoretically superfluous, it is nevertheless true that they often convey more important information than is contained in the propositions in which they are used. … The collection of definitions embodies our choice of subjects and our judgement as to what is most important. Secondly, … the definition contains an analysis of a common idea, and may therefore express a notable advance.
在第12页，书中指出定义仅仅是排版上的便利。另一方面，定义又至关重要，因为它们展示了意图。“……定义并非我们研究对象的一部分，严格来说，它们仅仅是排版上的便利……尽管定义在理论上是多余的，但它们往往传达了比使用它们的命题本身更重要的信息……定义集合体现了我们对研究对象的选择，以及我们对何者最为重要的判断。其次，……定义包含了对一个通用概念的分析，因此可能代表了显著的进步。”
Propositional functions: anticipation of lambda-calculus
命题函数：对λ-演算的预见
Page 15 introduces propositional functions'', what is now known as lambda-terms. See for yourself, from the running example on the page. "x is hurt" [called ambiguous] really makes no assertion at all, till we have settled who x is. Yet owing to the individuality retained by the ambiguous variable x, it is an ambiguous example from the collection of propositions arrived at by giving all possible determinations to x in "x is hurt" which yield a proposition, true or false. The authors then introduce the notation for that propositional function”: “\hat{x} is hurt”. Although “x is hurt” and “y is hurt” occurring in the same context can be distinguished, "\hat{x} is hurt" and "\hat{y} is hurt" convey no distinction of meaning at all.'' The paragraph concludes: More generally, φx is an ambiguous value of the propositional function φ\hat{x}, and when a definite signification a is substituted for x, φa is an unambiguous value of φ\hat{x}.” Here we have it: free variables, bound variables, substitution and alpha-equivalence.
第15页引入了“命题函数”，即现在所知的λ-项。请看书中给出的例子：“x 受伤了”[被称为模糊的] 在我们确定 x 是谁之前，实际上并没有做出任何断言。然而，由于模糊变量 x 保留了个体性，它是通过对“x 受伤了”中的 x 进行所有可能的确定（从而产生真或假的命题）所得到的命题集合中的一个模糊实例。作者随后引入了该“命题函数”的符号：“\hat{x} 受伤了”。尽管在同一上下文中，“x 受伤了”和“y 受伤了”可以区分，但“\hat{x} 受伤了”和“\hat{y} 受伤了”在含义上没有任何区别。该段落总结道：“更一般地，φx 是命题函数 φ\hat{x} 的一个模糊值，当用一个确定的指代 a 代替 x 时，φa 就是 φ\hat{x} 的一个明确值。”这就是我们所说的：自由变量、约束变量、代换和α-等价。