数理逻辑 Mathematcial Logic

简介

数理逻辑是数学的一个分支,其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑的主要分支包括:模型论、证明论、递归论和公理化集合论。

数理逻辑和计算机科学有许多重合之处,这是因为许多计算机科学的先驱者既是数学家、又是逻辑学家,如艾伦·图灵、邱奇等。 程序语言学、语义学的研究从模型论衍生而来,而程序验证中的模型检测则从模型论衍生而来。柯里-霍华德同构给出了“证明”和“程序”的等价性,这一结果与证明论有关,直觉主义逻辑和线性逻辑在此起了很大作用。λ演算和组合子逻辑这样的演算现在属于理想程序语言。计算机科学在自动验证和自动寻找证明等技巧方面的成果对逻辑研究做出了贡献,比如说自动定理证明和逻辑编程。

基本定理

  • 一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说,证明集合是原始递归的。实质上,这就是哥德尔完全性定理,虽然那个定理的通常陈述使它与算法之间的关系不明显。
  • 有效的一阶公式的集合是无限不可数(Uncountable Infinite)的。这一集合是“递归枚举的”,即不存在一图灵机(从而不存在任何现有计算机和算法)可以对某个非一阶公式的输入告诉你“这个输入一定不是一阶公式”——它可能一直运算下去。
  • 普遍有效的二阶公式的集合甚至不是递归可枚举的。这是哥德尔不完全性定理的一个结果。
  • 勒文海姆-斯科伦定理。
  • 相继式演算中的切消定理。
  • 保罗·约瑟夫·科恩(Paul Cohen)在1963年证明的连续统假设的独立性。

相关书籍

For Beginners

Smullyan, R. M. (2014). A Beginner’s Guide to Mathematical Logic. Courier Corporation.

恩德滕. (2007). 数理逻辑(第2版). 人民邮电出版社.

For Experts

Bell, J. L. (1977). A course in mathematical logic.

Ebbinghaus, H. D., Flum, J., & Thomas, W. (2013). Mathematical logic. Springer Science & Business Media.

计算机科学中的数理逻辑

数理逻辑是研究计算机科学的基础工具。

计算机科学与数理逻辑的关系

类型系统 Type Theory, Proof Theory
结构操作语义 Term Writing, Proof Theory, Recursion Theory
抽象机器 Recursion Theory
Operational Semantics Proof Systems
Denotational Semantics Model Theory*, Set Theory, Domain Theory
逻辑编程语言 Proof Theory
综合 Categorical Logic
程序分析 Category Theory
程序验证 Model Theory
Curry–Howard Isomorphism Proof Theory (Intuitionistic Logic)

相关书籍

For Beginners

Nerode, A., & Shore, R. A. (2012). Logic for applications. Springer Science & Business Media.

Huth, M., & Ryan, M. (2004). Logic in Computer Science: Modelling and reasoning about systems. Cambridge university press.

哈斯, 瑞安, 何伟, & 樊磊. (2007). 面向计算机科学的数理逻辑:系统建模与推理. 机械工业出版社.

For Experts

Recursive Theory:

Soare, R. I. (1999). Recursively enumerable sets and degrees: A study of computable functions and computably generated sets. Springer Science & Business Media.

Type Theory:

Harper, R. (2016). Practical foundations for programming languages. Cambridge University Press.

Pierce, B. C. (2002). Types and programming languages. MIT press.

Pierce, B. C. (2005). Advanced topics in types and programming languages. MIT press.

Category Theory:

Pierce, B. C. (1991). Basic category theory for computer scientists. MIT press.

递归论 Recursion Theory

递归论或可计算性理论,是一个数理逻辑分支。它起源于可计算函数和图灵度的研究。它的领域增长为包括一般性的可计算性和可定义性的研究。在这些领域中,这门理论同证明论和能行描述集合论(effective descriptive set theory)有所重叠。

数理逻辑中的可计算性理论家经常研究相对可计算性、可归约性概念和程度结构的理论。相对于计算机科学家,他们研究次递归层次,可行的计算和公用于可计算性理论研究的形式语言。在这两个社区之间有着相当大的知识和方法上的重叠,而没有明显的界限。

递归论所考虑的基本问题是,给定一个从自然数到自然数的函数f,f是否是可以被计算的。“可以被计算”,我们先将其当作一个直观的概念。根据直觉,人们一般会认为,一个函数可以被计算是存在一个给定的过程,接受一个自然数n后,该过程进行一定的操作并给出f(n)作为输出。将计算这一直观的概念上升到数学层面的形式化定义这一工作是递归论的根本,并由哥德尔、邱奇、图灵、克莱尼和Emil Post等人在1930年代奠定。他们将图灵可计算性作为有效计算的形式化。

相关书籍

For Beginners

Cutland, N. (1980). Computability: An introduction to recursive function theory. Cambridge university press.

Cooper, S. B. (2003). Computability theory. CRC Press.

莫绍揆. (1987). 递归论. 科学出版社.

For Experts

Soare, R. I. (1999). Recursively enumerable sets and degrees: A study of computable functions and computably generated sets. Springer Science & Business Media.

Smullyan, R. M. (1993). Recursion theory for metamathematics. Oxford University Press on Demand.

证明论 Proof Theory

简介

证明论是数理逻辑的一个分支,它将数学证明表达为形式化的数学客体,从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达,例如链表,盒链表,或者树,它们根据逻辑系统的公理和推理规则构造。因此,证明论本质上是语法逻辑,和本质上是语义学的模型论形相反。和模型论,公理化集合论,以及递归论一起,证明论被称为数学基础的四大支柱之一。

Formal proofs are constructed with the help of computers in interactive theorem proving. Significantly, these proofs can be checked automatically, also by computer. Checking formal proofs is usually simple, whereas finding proofs (automated theorem proving) is generally hard. An informal proof in the mathematics literature, by contrast, requires weeks of peer review to be checked, and may still contain errors.

相关书籍

For Beginners

Takeuti, G. (2013). Proof theory (Vol. 81). Courier Corporation.

公理化集合论 Axiomatic Set Theory

公理化集合论是集合论透过建立一阶逻辑的严谨重整,以解决朴素集合论中出现的悖论。

集合论中其中一套由Skolem最后整理的公理系统,称为Zermelo-Fraenkel集合论(ZF)。实际上,这个名称通常不包括历史上远比今天具争议性的选择公理,当包括了选择公理,这套系统被称为ZFC。

  • 外延公理:(Axiom of extensionality)两个集合相同,当且仅当它们拥有相同的元素。
  • 分类公理:(Axiom schema of specification / axiom schema of separation / axiom schema of restricted comprehension)或称子集公理,给出任何集合及命题P(x),存在着一个原来集合的子集包含而且只包含使P(x)成立的元素。
  • 配对公理:(Axiom of pairing)假如x, y为集合,那就有另一个集合{x,y}包含x与y作为它的仅有元素。
  • 并集公理:(Axiom of union)每一个集合也有一个并集。也就是说,对于每一个集合x,也总存在着另一个集合y,而y的元素也就是而且只会是x的元素的元素。
  • 空集公理:存在着一个不包含任何元素的集合,我们记这个空集合为{ }。可由分类公理得出。
  • 无穷公理:(Axiom of infinity)存在着一个集合x,空集{ }为其元素之一,且对于任何x中的元素y,y ∪ {y}也是x的元素。
  • 替代公理:(Axiom schema of replacement)
  • 幂集公理:(Axiom of power set)每一个集合也有其幂集。那就是,对于任何的x,存在着一个集合y,使y的元素是而且只会是x的子集。
  • 正规公理:(Axiom of regularity / Axiom of foundation)每一个非空集合x,总包含着一元素y,使x与y为不交集。
  • 选择公理:(Axiom of choice,Zermelo’s version)给出一个集合x,其元素皆为互不相交的非空集,那总存在着一个集合y(x的一个选择集合),包含x每一个元素的仅仅一个元素。

    相关书籍

    For Beginners

Takeuti, G., & Zaring, W. M. (2013). Axiomatic set theory (Vol. 8). Springer Science & Business Media.

Jech, T. (2013). Set theory. Springer Science & Business Media.

张锦文. (1997). 公理集合论导引. 科学出版社.

For Experts

Kunen, K. (2014). Set theory an introduction to independence proofs (Vol. 102). Elsevier.

模型论 Model Theory

简介

数学上,模型论(英语:Model theory)是从集合论的论述角度对数学概念表现(representation)的研究,或者说是对于作为数学系统基础的“模型”的研究。粗略地说,该学科假定有一些既存的数学“对象”,然后研究:当这些对象之间的一些运算或者一些关系乃至一组公理被给定时,可以相应证明出什么,以及如何证明。

比如实数理论中一个模型论概念的例子是:我们从一个任意集合开始,作为集合元素的每个个体都是一个实数,其间有一些关系和(或)函数,例如{ ×, +, −, ., 0, 1 }。若我们在该语言中问”∃ y (y × y = 1 + 1)”这样一个问题,显然该陈述对实数而言成立 - 确实存在这样的一个实数y,即所谓2的平方根;对于有理数,该陈述却并不成立。一个类似的命题,”∃ y (y × y = 0 − 1)”,在实数中不成立,却在复数中成立,因为i × i = 0 − 1。

模型论研究什么是在给定的数学系统中可证的,以及这些系统相互间的关系。它特别注重研究当我们试图通过加入新公理和新语言构造时会发生什么。

现在模型论(及其方法)已经广泛地应用于其它数学分支甚至理论计算机与工程计算中。例如Hrushovski用模型论方法证明了代数几何中的Mordell-Lang猜想。

定义

结构被形式的定义于某个语言L的上下文中,它由常量符号的集合,关系符号的集合,和函数符号的集合组成。在语言L上的结构,或L-结构,由如下东西组成:

  1. 一个全集或底层集合A,它包含所有感兴趣的对象(”论域”),
  2. 给L的每个常量符号一个在A中元素,
  3. 给L的每个n价函数符号一个从An到A的函数,和
  4. 给L的每个n价关系符号一个在A上的n-元关系(换句话说,An的一个子集)。

函数或关系的价有时也叫做元数(术语”一元”、”二元”和”n-元”中的那个元)。

在语言L中的理论,或L-理论,被定义为L中的句子的集合。如果句子的集合闭合于通常的推理规则之下,则被称为闭合理论。例如,在某个特定L-结构下为真的所有句子的集合是一个闭合L-理论。

L-理论T的模型由在其中T的所有句子都为真的一个L-结构组出,它通常用T-模式的方式定义。

理论被称为可满足的,如果它有模型。

例如,偏序的语言有一个二元关系≥。因而偏序的语言的结构就是带有≥所指示的二元关系的一个集合,它是偏序的理论的模型,如果此外它还满足偏序的公理。

定理

  • 哥德尔完备性定理表明理论有一个模型当且仅当它是一致的,也就是说没有矛盾可以被该理论所证明。这是模型论的中心,因为它使得我们能够通过检视模型回答关于理论的问题,反之亦然。不要把完全性定理和完备理论的概念混淆。一个完备的理论是包含每个句子或其否命题的理论。重要的是,一个完备的协调理论可以通过扩展一个协调的理论得到。

  • 紧致性定理说一组语句S是可满足的(即有一个模型)当且仅当S的每一个有限子集可满足。在证明理论的范围内类似的定义是下显而易见的,因为每个证明都只能有有限量的证明前提。在模型论的范畴内这个证明就更困难了。目前已知的有两个证明方法,一个是库尔特·哥德尔提出的(通过证明论),另一个是阿纳托利·伊万诺维奇·马尔采夫提出的(这个更直接,并允许我们限制最后模型的基数)。

  • 模型论一般与一阶逻辑有关。许多模型论的重要结果(例如哥德尔完备性定理和紧致性定理)在二阶逻辑或其它可选的理论中不成立。在一阶逻辑中对于一个可数的语言,任何理论都有可数的模型。这在勒文海姆-斯科伦定理中有表达,它说对于任何可数的语言中的任何有一个无限模型都有一个可数的初等子模型。

  • 莫雷(Morley)证明了著名的范畴定理。即对于可数语言的任何可数完备理论,如果它在某个不可数基数上是范畴的,则它在所有不可基数上都是范畴的。这个定理极大的刺激了模型论的发展,产生了后来的所谓稳定性理论(stable theory)。

  • 近来模型论更加着重于对于其它数学分支,尤其是代数和代数几何的应用。

相关书籍

For Beginners

Chang, C. C., & Keisler, H. J. (1990). Model theory (Vol. 73). Elsevier.

王世强. (2001). 模型论基础. 科学出版社.

形式系统 Formal System

简介

在逻辑与数学中,一个形式系统(英语:Formal system)是由两个部分组成的,一个形式语言加上一个推理规则或转换规则的集合。一个形式系统也许是纯粹抽象地制定出来,只是为了研究其自身。另一方面,也可能是为了描述真实现象或客观现实的领域而设计的。

在数学领域里,形式证明是形式系统的产物,由一些公理与演绎规则组成。定理便是形式证明可能的最后一行结论。这几个步骤总和起来便是数学界通称的形式主义。大卫·希尔伯特创立元数学以作为讨论形式系统的学科。任何用于讨论形式系统的语言称为元语言。元语言也许像普通语言一样自然,或它可能部分形式化,但它通常比起受检验系统的形式语言来得较不正规化。此形式语言称为对象语言,意指问题议论的对象。

某些理论学家将形式主义粗略视为形式系统的同义词,但此词也同时指称特定风格的符号,例如保罗·狄拉克的狄拉克符号。

定义

在数学中的形式系统由以下要素组成:

  1. 一群有限数量,且可用于建构公式的符号集合。
  2. 一套文法,说明了如何以上述符号建构形式良好的公式(通称合式公式,或Well-formed formula,wff)。通常会要求有一个判定某公式是否为形式良好的算法。
  3. 一群公设或公理模式的陈述,每个公理都必须是合式公式。
  4. 一群推理规则。

相关书籍

For Beginners

Smullyan, R. M. (1961). Theory of formal systems. Princeton University Press.

Peter Linz. (2005). 形式语言与自动机导论. 机械工业出版社.

一阶逻辑 First-order Logic

简介

一阶逻辑和命题逻辑的不同之处在于,一阶逻辑有使用量化变数和断言。一个一阶逻辑,若具有由一系列量化变数、一个以上有意义的断言字母及包含了有意义的断言字母的纯公理所组成的特定论域,即是一个一阶理论。

一阶逻辑和其他高阶逻辑不同之处在于,高阶逻辑的断言可以有断言或函数当做引数,且允许断言量词或函数量词的(同时或不同时)存在。在一阶逻辑中,断言通常和集合相关连。在有意义的高阶逻辑中,断言则会被解释为集合的集合。

存在许多对一阶逻辑是可靠(所有可证的叙述皆为真)且完备(所有为真的叙述皆可证)的演绎系统。虽然一阶逻辑的逻辑归结只是半可判定性的,但还是有许多用于一阶逻辑上的自动定理证明。一阶逻辑也符合一些使其能通过证明论分析的元逻辑定理,如勒文海姆–斯科伦定理及紧致性定理。

一阶逻辑是数学基础中很重要的一部分,因为它是公理系统的标准形式逻辑。许多常见的公理系统,如一阶皮亚诺公理和包含策梅洛-弗兰克尔集合论的公理化集合论等,都可以形式化成一阶理论。然而,一阶定理并没有能力去完整描述及范畴性地建构如自然数或实数之类无限的概念。这些结构的公理系统可以由如二阶逻辑之类更强的逻辑来取得。

相关书籍

For Beginners

Smullyan, R. M. (1995). First-order logic. Courier Corporation.

类型论 Type Theory

简介

类型论是关注把实体分类到叫做类型的搜集中的数学和逻辑分支。

In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every “term” has a “type” and operations are restricted to terms of a certain type.

Type theory is closely related to (and in some cases overlaps with) type systems, which are a programming language feature used to reduce bugs. Type theory was created to avoid paradoxes in a variety of formal logics and rewrite systems.

Two well-known type theories that can serve as mathematical foundations are Alonzo Church’s typed λ-calculus and Per Martin-Löf’s intuitionistic type theory.mbda

相关书籍

Nederpelt, R., & Geuvers, H. (2014). Type theory and formal proof.

范畴论 Category Theory

简介

范畴论是数学的一门学科,以抽象的方法来处理数学概念,将这些概念形式化成一组组的“物件”及“态射”。数学中许多重要的领域可以形式化成范畴,并且使用范畴论,令在这些领域中许多难理解、难捉摸的数学结论可以比没有使用范畴还会更容易叙述及证明。 范畴最容易理解的一个例子为集合范畴,其物件为集合,态射为集合间的函数。但需注意,范畴的物件不一定要是集合,态射也不一定要是函数;一个数学概念若可以找到一种方法,以符合物件及态射的定义,则可形成一个有效的范畴,且所有在范畴论中导出的结论都可应用在这个数学概念之上。 范畴最简单的例子之一为广群,其态射皆为可逆的。群胚的概念在拓扑学中很重要。范畴现在在大部分的数学分支中都有出现,在理论计算机科学的某些领域中用于对应资料型别,而在数学物理中被用来描述向量空间。

函子

再抽象化一次,范畴自身亦为数学结构的一种,因此可以寻找在某一意义下会保持其结构的“过程”;此一过程即称之为函子。函子将一个范畴的每个物件和另一个范畴的物件相关连起来,并将第一个范畴的每个态射和第二个范畴的态射相关连起来。

实际上,即是定义了一个“范畴和函子”的范畴,其元件为范畴,(范畴间的)态射为函子。

经由研究范畴和函子,不只是学习了一类数学结构,及在其之间的态射;还学习了“在不同类型的数学结构之间的关系”。此一基本概念首次出现于代数拓扑之中。不同的“拓扑”问题可以转换至通常较易解答的“代数”问题之上。在拓扑空间上如基本群或基本群胚等基本的架构,可以表示成由群胚所组成的范畴之间的基本函子,而这个概念在代数及其应用之中是很普遍的。

相关书籍

For Experts

Mac Lane, S. (2013). Categories for the working mathematician (Vol. 5). Springer Science & Business Media.

λ演算 Lambda Calculus

简介

λ演算(英语:lambda calculus,λ-calculus)是一套从数学逻辑中发展,以变量绑定和替换的规则,来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家阿隆佐·邱奇在20世纪30年代首次发表。Lambda演算作为一种广泛用途的计算模型,可以清晰地定义什么是一个可计算函数,而任何可计算函数都能以这种形式表达和求值,它能模拟单一磁带图灵机的计算过程;尽管如此,Lambda演算强调的是变换规则的运用,而非实现它们的具体机器。

Lambda演算可比拟是最根本的编程语言,它包括了一条变换规则(变量替换)和一条将函数抽象化定义的方式。因此普遍公认是一种更接近软件而非硬件的方式。对函数式编程语言造成很大影响,比如Lisp、ML语言和Haskell语言。在1936年邱奇利用λ演算给出了对于判定性问题(Entscheidungsproblem)的否定:关于两个lambda表达式是否等价的命题,无法由一个“通用的算法”判断,这是不可判定性能够证明的头一个问题,甚至还在停机问题之先。

Lambda演算包括了建构lambda项,和对lambda项运行归约的操作。在最简单的lambda演算中,只使用以下的规则来建构lambda项:

语法 名称 描述
a 变量 表示参数或数学/逻辑值的字符或字符串
(λx.M) 抽象化 函数定义(M是一个lambda项)。变量x在表达式中已被绑定。
(M N) 应用 将函数应用于参数。 M 和 N 是 lambda 项。

产生了诸如:(λx.λy.(λz.(λx.zx)(λy.zy))(x y)的表达式。如果表达式是明确而没有歧义的,则括号可以省略。对于某些应用,其中可能包括了逻辑和数学的常量以及相关操作。 本文讨论的是邱奇的“无类型lambda演算”,此后,已经研究出来了一些有类型lambda演算。

相关书籍

Barendregt, H. P. (1984). The lambda calculus (Vol. 2). Amsterdam: North-Holland.

π演算 Pi Calculus

简介

In theoretical computer science, the π-calculus (or pi-calculus) is a process calculus. The π-calculus allows channel names to be communicated along the channels themselves, and in this way it is able to describe concurrent computations whose network configuration may change during the computation.

The π-calculus is elegantly simple, it has very few terms and so is a very small language, yet is very expressive. Functional programs can be encoded into the π-calculus, and the encoding emphasises the dialogue nature of computation, drawing connections with game semantics. Extensions of the π-calculus, such as the spi calculus and applied π, have been successful in reasoning about cryptographic protocols. Beside the original use in describing concurrent systems, the π-calculus has also been used to reason about business processes and molecular biology.

相关书籍

Fokkink, W. (2013). Introduction to process algebra. Springer Science & Business Media.

Sangiorgi, D., & Walker, D. (2003). The pi-calculus: a Theory of Mobile Processes. Cambridge university press.

Handbook

Bergstra, J. A., Ponse, A., & Smolka, S. A. (Eds.). (2001). Handbook of process algebra. Elsevier.

布尔函数 Boolean Functions

简介

布尔函数(Boolean function)描述如何基于对布尔输入的某种逻辑计算确定布尔值输出。它们在复杂性理论的问题和数字计算机的芯片设计中扮演基础角色。布尔函数的性质在密码学中扮演关键角色,特别是在对称密钥算法的设计中。

相关书籍

Crama, Y., & Hammer, P. L. (2011). Boolean functions: Theory, algorithms, and applications. Cambridge University Press.

二元决策图 Binary Decision Diagram

简介

在计算机科学中,二元决策图(binary decision diagram, BDD),或译为二元判定图,是被用来表达一个布尔函数的一种数据结构。二元决策图是布尔表达式的IF判断范式(If-then-else normal form, INF)的数据结构。每个布尔表达式都有唯一的INF,而且可以用多项式时间的算法确定其恒真性和可满足性。通常BDD指无冗降序二元决策图(reduced ordered binary decision diagram, ROBDD)。BDD是一族非常有用的数据结构,广泛地使用在程序分析和验证,基于知识库的系统等领域。

相关书籍

Andersen, H. R. (1997). An introduction to binary decision diagrams. Lecture notes, available online, IT University of Copenhagen.

Knuth, D. E. (2009). The Art of Computer Programming: Bitwise Tricks & Techniques; Binary Decision Diagrams, volume 4, fascicle 1.

Huth, M., & Ryan, M. (2004). Logic in Computer Science: Modelling and reasoning about systems. Cambridge university press.

模态μ逻辑 Modal μ-calculus

简介

In theoretical computer science, the modal μ-calculus (Lμ, Lμ, sometimes just μ-calculus, although this can have a more general meaning) is an extension of propositional modal logic (with many modalities) by adding a least fixpoint operator μ and a greatest fixpoint operator {\displaystyle \nu } \nu , thus a fixed-point logic.

The (propositional, modal) μ-calculus originates with Dana Scott and Jaco de Bakker, and was further developed by Dexter Kozen into the version most used nowadays. It is used to describe properties of labelled transition systems and for verifying these properties. Many temporal logics can be encoded in the μ-calculus, including CTL* and its widely used fragments—linear temporal logic and computational tree logic.

An algebraic view is to see it as an algebra of monotonic functions over a complete lattice, with operators consisting of functional composition plus the least and greatest fixed point operators; from this viewpoint, the modal μ-calculus is over the lattice of a power set algebra. The game semantics of μ-calculus is related to two-player games with perfect information, particularly infinite parity games.

相关书籍

Venema, Y. (2008). Lectures on the modal µ-calculus. Renmin University in Beijing (China).

Blackburn, P., van Benthem, J. F., & Wolter, F. (Eds.). (2006). Handbook of modal logic (Vol. 3). Elsevier.