Home About us Products Services Contact us Bookmark
:: wikimiki.org ::
谓词逻辑

谓词逻辑

一阶谓词演算或一阶逻辑(FOL)允许量化陈述的公式，比如"存在着 x，..." (\exists x) 或 "对于任何 x，..." (\forall x)，这里的 x 是论域(domain of discourse)的成员。一阶(递归)公理化理论是通过增加一阶句子/断定的递归可枚举集合作为公理，可以被公理化为一阶逻辑扩展的理论。这里的"..."叫做谓词并表达某种性质。谓词是适用于某些事物的表达。所以，表达"是黄色"或"喜欢椰菜"分别适用于是黄色或喜欢椰菜的那些事物。 一阶逻辑是区别于高阶逻辑的数理逻辑，它不允许量化性质。性质是一个物体的特性；所以一个红色物体被表述为有红色的特性。性质可以被当作物体只凭自身的一种构成(form)，它可以拥有其他性质。性质被认为有别于拥有它的物体。所以一阶逻辑不能表达下列陈述，"对于所有的性质 P，..." 或"存在着性质 P，..."。 但是，一阶逻辑足够强大了，它可以形式化全部的集合论和几乎所有的数学。把量化限制于个体(individual)使它难于用于拓扑学目的，但它是在数学底层经典的逻辑理论。它是比句子逻辑强比二阶逻辑弱的理论。

一阶逻辑的定义

谓词演算构成如下
- 生成规则(就是形成合式公式的递归定义)。
- 变换规则(就是推导定理的推理规则)。
- 公理或公理模式的(可能的可数的无限)集合。 有两种类型的公理: 逻辑公理，它是对于谓词演算有效的，和非逻辑公理，它是在特殊情况下为真的，就是说，在它所在的理论的标准解释中是真的。例如，非逻辑的皮亚诺公理在算术的符号主义标准解释下是真的，但是对于谓词演算它们不是有效的。 在公理的集合是无限的的时候，需要能判定给定的合式公式是否是一个公理的一个算法。进一步的，应当有可以判定一个推理规则的应用是否正确的算法。

词汇表

"词汇表"构成如下 # 大写字母 P, Q, R,... 是谓词变量。 # 小写字母 a, b, c,... 是(个别的)常量。 # 小写字母 x, y, z,... 是(个别的)变量。 # 小写字母 f, g, h,... 是函数变量。 # 表示逻辑算子的符号: ¬ (逻辑非)，\wedge (逻辑与)，\vee (逻辑或)，→ (逻辑条件) 和 ↔ (逻辑双条件)。 # 表示量词的符号: \forall (全称量词)，\exists (存在量词)。 # 左右圆括号。 一些符号可以被简略为原语(primitive)并被采纳为简写；比如 (P ↔ Q) 是 (P → Q) \wedge ( Q → P) 的简写。算子和量词的最小数目是三个(如果我们定义了算子或非或者与非则是两个)；例如，¬，\wedge 和 \forall 就足够了。项是一个常量、变量或 n≥0 个参数的函数符号。

生成规则

合式公式(wff)的集合按如下规则递归的定义: # 简单和复杂的谓词 如果 P 是 n 元(n ≥ 0)谓词，则 Pa_1,...,a_n 是合式的。如果 n ≤ 1，则 P 是原子。 # 归纳条款 I: 如果 φ 是 wff，则 ¬ φ 是 wff。 # 归纳条款 II: 如果 φ 和 ψ 是 wff，则 (\phi \wedge \psi)，(\phi \vee \psi)，(φ → ψ)和(φ ↔ ψ) 是 wff。 # 归纳条款 III: 如果 φ 是 包含变量 x 的一个自由实例的 wff，则 \forall x \, \varphi 和 \exists x \, \varphi 是 wff。(此后在 \forall x \, \varphi 和 \exists x \, \varphi 中x 的任何实例都被称为约束的 — 而不是自由的。) # 闭包条款: 其他东西都不是 wff。

变换(推理)规则

肯定前件充当推理的唯一规则。如果没有公理模式，则还需要一个一致代换规则。

演算

谓词演算是命题演算的扩展。如果命题演算被定义为十一个公理和一个推理规则(肯定前件)，不计算针对逻辑等价算子的额外定律在内，则谓词演算可以被定义为在其上添加四个补充的公理和一个补充的推理规则。

公理扩展

下列四个公理是谓词演算的特征:
- PRED-1: \forall x Z(x) \rightarrow Z(y)
- PRED-2: Z(y) \rightarrow \exists x Z(x)
- PRED-3: \forall x (W \rightarrow Z(x)) \rightarrow (W \rightarrow \forall x Z(x))
- PRED-4: \forall x (Z(x) \rightarrow W) \rightarrow (\exists x Z(x) \rightarrow W) 它们实际上是公理模式，因为其中的谓词字母 W 和 Z 可以被任何谓词字母所替代，而不改变这些公式的有效性。

推理规则

叫做全称普遍化的推理规则是谓词演算的特征。它可以陈述为 : \mathit \vdash Z(x), \mathit \vdash \forall x Z(x) 这里的 Z(x) 假定表示谓词演算的一个已证明的定理，而 ∀xZ(x) 是它针对于变量 x 的闭包。谓词字母 Z 可以被任何谓词字母所替代。 注意：全称普遍化类似于模态逻辑的必然性规则，它是 :\mathit \vdash P, \mathit \vdash \Box P

一阶逻辑的元逻辑定理

在公告板中列出了一些重要的元逻辑定理。 # 不像命题演算，一阶逻辑是不可判定性的。对于任意的公式 P，可以证实没有判定过程，判定 P 是否有效，(参见停机问题)。(结论独立的来自于邱奇和图灵。) # 有效性的判定问题是半可判定的。按哥德尔不完备定理所展示的，对于任何有效的公式 P, P 是可证明的。 # 单体谓词逻辑(就是说，谓词只有一个参数的谓词逻辑)是可判定的。

参见


- 哥德尔不完备定理
- 推理规则列表
- 数理逻辑

引用


- David Hilbert and Wilhelm Ackermann (1928). Grundzüge der theoretischen Logik (Principles of Theoretical Logic). Springer-Verlag, ISBN 0-8218-2024-9.
- [http://plato.stanford.edu/entries/logic-classical/ Article on classical logic] by Stewart Shapiro at the Stanford Encyclopedia of Philosophy, which covers the definition, model theory and soundness and completeness results for first-order logic characterised in a natural deduction style.
- [http://www.ltn.lv/~podnieks/ Introduction to mathematical logic] by Karl Podnieks.
- [http://us.metamath.org/index.html Metamath]: a project to construct mathematics using an axiomatic system based on propositional calculus, predicate calculus, and set theory category:数理逻辑 category:離散數學

高阶逻辑

在数学中，高阶逻辑在很多方面有别于一阶逻辑。 其一是变量类型出现在量化中；粗略的说，一阶逻辑中禁止量化谓词。允许这么做的系统请参见二阶逻辑。 高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型理论。高阶谓词是接受其他谓词作为参数的谓词。一般的，阶为 n 的高阶谓词接受一个或多个(n − 1)阶的谓词作为参数，这里的 n > 1。对高阶函数类似的评述也成立。 高阶逻辑更加富有表达力，但是它们的性质，特别是有关模型论的，使它们对很多应用不能表现良好。作为哥德尔的结论，经典高阶逻辑不容许(递归的公理化的)可靠的和完备的证明演算；这个缺陷可以通过使用 Henkin 模型来修补。

参见


- 高阶文法
- 有类型的lambda演算
- 直觉类型理论

外部链接


- [http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/AIencyclopedia/ A short article from the Encyclopedia of Artificial Intelligence]

文献


- Alonzo Church: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, Vol. 5, 1940, 56-68.
- Leon Henkin: Completeness in the theory of types. Journal of Symbolic Logic, Vol. 15, 1950, 81-91.
- Peter B. Andrews: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. 2nd edition, Academic Press 2002.
- J. Lambek, P. J. Scott: Introduction to Higher Order Categorical Logic. Cambridge University Press 1986. Category:数理逻辑 Category:计算机逻辑

数理逻辑

数理逻辑是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。 数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑（相对于哲学逻辑），又称元数学，后者的使用现已局限于证明论的某些方面。

历史

“数理逻辑”的名称由皮亚诺（Peano）首先给出，他又称其为符号逻辑。数理逻辑在本质上依然是亚里士多德的逻辑学，但从记号学的观点来讲，它是用抽象代数来记述的。 某些哲学倾向浓厚的数学家对用符号或代数方法来处理形式逻辑作过一些尝试，比如说莱布尼兹和兰伯特（Johann Heinrich Lambert）；但他们的工作鲜为人知，后继无人。直到19世纪中叶，乔治·布尔和其后的奥古斯都·德·摩根才提出了一种处理逻辑问题的系统性的数学方法（当然不是定量性的）。 亚里士多德以来的传统逻辑得到改革和完成，由此也得到了研究数学基本概念的合适工具。虽然这并不意味着1900年至1925年间的有关数学基础的争论已有了定论，但这“新”逻辑在很大程度上澄清了有关数学的哲学问题。 传统的逻辑研究（参见逻辑论题列表）较偏重于“论据的形式”，而当代数理逻辑的态度也许可以被总结为对于内容的组合研究。它同时包括“语形”（例如，从一形式语言把一个文字串传送给一编译器程序，从而转写为机器指令）和“语义”（在模型论中构造特定模型或全部模型的集合）。 数理逻辑的里程碑式著作有哥特洛布·弗雷格（Gottlob Frege）的《概念文字》（Begriffsschrift）和伯特兰·罗素的《数学原理》（Principia Mathematica）。

数理逻辑论的体系

数理逻辑的主要分支包括：模型论、证明论、递归函数论。有时还包括公理集合论。数理逻辑和计算机科学有许多重合之处，这是因为许多计算机科学的先驱者既是数学家、又是逻辑学家，比如说象阿兰·图灵。 程序语言学、语义学的研究从模型论衍生而来，而程序验证则从模型论的模型检测衍生而来。 柯里－霍华德同构（Curry-Howard isomorphism）给出“证明”和“程序”的等价性，这一结果与证明论有关，直觉逻辑和线性逻辑在此起了很大作用。λ演算以及其它演算和组合逻辑现在属于理想程序语言。 计算机科学在自动验证和自动寻找证明等技巧方面的成果对逻辑研究做出了贡献，比如说自动定理证明和逻辑编程。

一些基本结果

一些重要结果是：
- 一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是哥德尔完备性定理，虽然那个定理的通常陈述使它与算法之间的关系不明显。
- 有效的一阶公式的集合是不可计算的，也就是说，不存在检测普遍有效性的算法。尽管以下算法存在：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机，如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，公式是否有效仍是未知数。换句话说，这一集合是“递归可数的”，用更通俗的话来讲，是“半可判定的”。
- 普遍有效的二阶公式的集合甚至不是递归可数的。这是哥德尔不完备定理的一个结果。
- 勒文海姆-斯科伦定理（Löwenheim-Skolem theorem）。
- 相继式演算（sequent calculus）中的切割－消去法。
- 保罗·科恩（Paul Cohen）在1963年证明的连续统假设的独立性。

技术参考

一阶语言和结构

定义 一阶语言 \mathfrak\, 是一组独特的印刷上的符号，分类如下: # 等价符号 =\,；连结词 \lor\,，\lnot\,；全称量词 \forall\, 和圆括号 (\,，)\,。 # 变量符号的可数集合 \_^\infty\,。 # 常量符号的集合 \_\,。 # 函数符号的集合 \_\,。 # 关系符号的集合 \_\,。
所以，要指定一个语言，通常只指定一组常量符号、函数符号和关系符号就足够了，因为第一组符号是标准的。圆括号只充当形成符号的群组的目的，在公式中书写函数和关系的时候被非形式的使用。 这些符号就是符号。它们不代表任何东西。他们不意味任何事物。加入语义和语言学要点对数学语言的形式化是没有用的。 因为确实需要在这些形式化之外获得某些意义。在语言之上的模型的概念就提供着这种语义。
定义 在语言 \mathfrak\, 上的 \mathfrak\,-结构是由非空集合 A\, 构成的包(bundle)，它是结构的全集，包括了: # 对于来自 \mathfrak\, 的每个常量符号 c\,，有一个元素 c^ \in A\,。 # 对于来自 \mathfrak\, 的每个 n\,-元函数符号 f\,，有一个 n\,-元函数 f^ : A^n \longrightarrow A\,。 # 对于来自 \mathfrak\, 的每个 n\,-元关系符号 R\,，有一个在 A\, 上的 n\,-元关系，就是说一个子集 R^ \subseteq A^n\,。
在这个上下文中对这种结构使用模型这个词。但是理解它的动机或许是重要的，见下。

项、公式和句子

定义 \mathfrak\,-项是来自 \mathfrak\, 的符号的非空有限字符串 t\,，如
- t\, 是一个变量符号。
- t\, 是一个常量符号。
- t\, 是形如 f t_1 ... t_n\, 的字符串，这里的 f\, 是 n\,-元函数符号而 t_1\,, ..., t_n\, 是 \mathfrak\, 的项。
定义 \mathfrak\,-公式是来自 \mathfrak\, 的符号的非空有限字符串 \phi\,，如
- \phi\, 是形如 t_1 = t_2\, 的字符串，这里的 t_1\, 和 t_2\, 是 \mathfrak\, 的项。
- \phi\, 是形如 R t_1 ... t_n\, 的字符串，这里的 R\, 是 n\,-元关系符号而 t_1\,, ..., t_n\, 是 \mathfrak\, 的项。
- \phi\, 形如 \lnot(\alpha)\,，这里的 \alpha\, 是 \mathfrak\,-公式。
- \phi\, 形如 (\alpha \lor \beta)\,，这里的 \alpha\, 和 \beta\, 二者是 \mathfrak\,-公式。
- \phi\, 形如 (\forall y)(\alpha)\,，这里的 y\, 是来自 \mathfrak\, 的变量符号而 \alpha\, 是 \mathfrak\,-公式。
定义 由要么第一个要么第二个子句来特征描述的 \mathfrak\,-公式被称为原子。
定义 设 \phi\, 是一个 \mathfrak\,-公式。来自 \mathfrak\, 的变量符号 x\, 被称为在 \phi\, 中是自由的，如果
- \phi\, 是原子，而 x\, 出现在 \phi\, 中。
- \phi\, 形如 \lnot(\alpha)\,，而 x\, 在 \alpha\, 中是自由的。
- \phi\, 形如 (\alpha \lor \beta)\,，而 x\, 在 \alpha\, 或 \beta\, 中是自由的。
- \phi\, 形如 (\forall y)(\alpha)\,，这里的 x\, 和 y\, 不是同一个变量符号而 x\, 在 \alpha\, 中是自由的。
定义 句子是没有自由变量的公式。

指派函数

此后，\mathfrak\, 将指称一阶语言，\mathfrak\, 是 \mathfrak\,-结构，它下层的全集用 A\, 指称。每个公式都将被理解为 \mathfrak\,-公式。
定义 到 \mathfrak\, 的变量指派函数(v.a.f.)是自 \mathfrak\, 的变量集合到 A\, 的函数。
定义 设 s\, 是到 \mathfrak\, 的 v.a.f.。我们定义项指派函数(t.a.f.) \overline\,，自 \mathfrak\,-项的集合到 A\,，如:
- 如果 t\, 是变量符号 x\,，则 \overline(t) = s(x)\,。
- 如果 t\, 是常量符号 c\,，则 \overline(t) = c^\,。
- 如果 t\, 形如 f t_1 ... t_n\,，则 \overline(t) = f^(\overline(t_1), ..., \overline(t_n))\,。
定义 设 s\, 是到 \mathfrak\, 的 v.a.f.，假定 x\, 是一个变量而 a \in A\,。我们定义 v.a.f. s[x|a]\,，指称为 x\,-指派函数的修改 s\,，为
s[x|a](v) = \begin s(v) & \mbox v \ne x \\ a & \mbox v = x \end \,

逻辑满足

定义 设 \phi\, 是公式，并假定 s\, 是到 \mathfrak\, 的 v.a.f.。我们称 \mathfrak\, 通过指派 s\, 满足 \phi\, ，并写为 \mathfrak \models \phi[s]\,，如果:
- \phi\, 形如 t_1 = t_2\,，而 \overline(t_1) = \overline(t_2)\,。
- \phi\, 形如 R t_1 ... t_n\,，而 (\overline(t_1), ..., \overline(t_n)) \in R^\,。
- \phi\, 形如 \lnot(\alpha)\,，而 \mathfrak\mbox\not\models\mbox\alpha[s]\,。
- \phi\, 形如 (\alpha \lor \beta)\,，而 \mathfrak \models \alpha[s]\, 或者 \mathfrak \models \beta[s]\,。
- \phi\, 形如 (\forall y)(\alpha)\,，而对于每个元素 a \in A\,，\mathfrak \models \alpha[s[y|a]]\,。
定义 设 \phi\, 是公式，并对到 \mathfrak\, 的每个 v.a.f. s\, 假定 \mathfrak \models \phi[s]\,。则我们称 \mathfrak\, 建模 \phi\,，并写为 \mathfrak \models \phi\,。
定义 设 \Phi\, 是公式的集合，并对每个公式 \phi \in \Phi\, 假定 \mathfrak \models \phi\,，则我们称 \mathfrak\, 建模 \Phi\,，并写为 \mathfrak \models \Phi\,。
在 \phi\, 是句子的情况下，就是没有自由变量的公式，存在一个单一的 v.a.f.，对于它 \mathfrak \models \phi[s]\,，直接的蕴涵了 \mathfrak \models \phi\,。
定义 设 \phi\, 是一个句子，并假定 \mathfrak \models \phi\,。则我们称 \phi\, 为在 \mathfrak\, 中是真实的。

逻辑蕴含和真实

定义 设 \Psi\, 和 \Phi\, 是公式的集合。我们称 \Psi\, 为逻辑蕴涵 \Phi\,，并写为 \Psi \models \Phi\,，如果对于所有结构 \mathfrak\,， \mathfrak \models \Psi\, 蕴涵 \mathfrak \models \Phi\,。
作为简写，在处理单元素集合(singleton)的时候，我们经常写 \Psi \models \phi\, 替代 \Psi \models \\,。
定义 设\phi\, 是公式，并假定 \varnothing \models \phi\,。则我们称 \phi\, 是全集有效，或者简单有效，在这种情况下我们简单的写为 \models \phi\,。
假如公式 \phi\, 是有效的，实际上意味着所有 \mathfrak\,-结构 \mathfrak\, 建模 \phi\,。
定义 设 \phi\, 是一个句子，并假定 \models \phi\,。则我们称 \phi\, 为真实的。

变量代换

定义 设 u\, 是项，并假定 x\, 是变量，而 t\, 是另一个项。我们定义这个项 u_t^x\,，读做把 x\, 替换为 t\, 的 u\,，如下:
- 如果 u\, 是变量符号 x\,，则 u_t^x\, 被定义为是项 t\,。
- 如果 u\, 是不是 x\, 的变量符号，则 u_t^x\, 被定义为项 u\,。
- 如果 u\, 是常量符号，则 u_t^x\, 被定义为项 u\,。
- 如果 u\, 形如 f t_1 ... t_n\,，则 u_t^x\, 被定义为项 f _t^x ... _t^x\,。
定义 设 \phi\, 是公式，并假定 x\, 是变量，而 t\, 是项。我们定义公式 \phi_t^x\,，读做把 x\, 替换为 t\, 的 \phi\,，如下:
- 如果 \phi\, 形如 t_1 = t_2\,，则 \phi_t^x\, 被定义为公式 _t^x = _t^x\,。
- 如果 \phi\, 形如 R t_1 ... t_n\,，则 \phi_t^x\, 被定义为公式 R _t^x, ..., _t^x\,。
- 如果 \phi\, 形如 \lnot(\alpha)\,，则 \phi_t^x\, 被定义为公式 \lnot(\alpha_t^x)\,。
- 如果 \phi\, 形如 (\alpha \lor \beta)\,，则 \phi_t^x\, 被定义为公式 (\alpha_t^x \lor \beta_t^x)\,。
- 如果 \phi\, 形如 (\forall y)(\alpha)\,，则
  - 如果 x\, and y\, 是同一个变量符号，则 \phi_t^x\, 被定义为公式 \phi\,。
  - 否则 \phi_t^x\, 被定义为公式 (\forall y)(\alpha_t^x)\,。

可代换性

定义 设 \phi\, 是公式，并假定 x\, 是变量，而 t\, 是项。我们称 t\, 对 x\, 在 \phi\, 中是可代换的，如果:
- \phi\, 是原子。
- \phi\, 形如 \lnot(\alpha)\,，而 t\, 对 x\, 在 \alpha\, 中是可代换的。
- \phi\, 形如 (\alpha \lor \beta)\,，而 t\, 对 x\, 在 \alpha\, 和 \beta\, 二者中是可代换的。
- \phi\, 形如 (\forall y)(\alpha)\,，而
  - 要么 x\, 在 \phi\, 中不是自由变量。
  - 要么 y\, 在 t\, 中不出现，而 t\, 对 x\, 在 \alpha\, 中是可代换的。
项于变量的可代换性的概念相应于在代换在项或公式中完成之后保持真实性的概念。严格的说，代换总是允许的，但可代换性将是强制的，以此生成意义不被代换所破坏的公式。

引用


- A. S. Troelstra & H. Schwichtenberg (2000). Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science) (2nd ed.). Cambridge University Press. ISBN 0521779111.
- George Boolos & Richard Jeffrey (1989). Computability and Logic (3rd ed.). Cambridge University Press. ISBN 0521007585.
- Elliott Mendelson (1997). Introduction to Mathematical Logic (4th ed.) Chapman & Hall.
- A. G. Hamilton (1988). Logic for Mathematicians Cambridge University Press.

外部链接


- [http://www.uni-bonn.de/logic/world.html Mathematical Logic around the world]
- [http://home.swipnet.se/~w-33552/logic/home/index.htm Polyvalued logic]
- [http://www.cis.upenn.edu/~giorgi/cl.html Computability logic] 数理逻辑的新方向 - 从真理的理论到可计算性的理论。

参见条目


- 逻辑
- 可计算性逻辑
- 博弈语义学
- 可证明性逻辑
- 可解释性逻辑
- 相继式演算
- 直觉逻辑
- 谓词逻辑 Category:數理邏輯 ja:数理論理学

集合论

集合论（简称集论）是一门研究集合的数学理论。这里的集合指由一些抽象的数学对象构成的整体。集合、元素和成员关系是数学中最基本的概念。集论（加上逻辑和谓词演算）是数学的公理化基础之一，通过集合及成员关系来形式化地表示其它数学对象。 集合论可以用来表示一系列略有不同的概念：
- 朴素集合论是由19世纪末的德国数学家康托最早提出的集合论。
- 公理集合论是一个更加严格的理论，它是发现了原始集合论里的一些错误(如：罗素悖论)后而修正的。
- Z集合论由德国数学家Ernst Zermelo创立的一个公理集合论。
- ZF集合论是最常用的公理集合论，由Abraham Fraenkel和Thoralf Skolem扩展了Z集合论所得。
- 不同的逻辑系统有相应不同的集合（如模糊逻辑里的模糊集合）。
- 音乐集合理论可以被看成是集合论在音乐上的应用。
- ja:集合論

拓扑学


- 此條目談的是數學上的拓扑，其他含義請見消歧義頁面拓扑。 ---- 拓扑学，台灣叫拓樸學，是近代发展起来的一个研究连续性现象的数学分支。中文名称起源于希腊语Topology的音译。Topology原意为地志学，于19世纪中期由科学家引入，当时主要研究的是出于数学分析的需要而产生的一些几何问题。发展至今，拓扑学主要研究拓扑空间在拓扑变换下的不变性质和不变量。

分支学科


- 点集拓扑学又称为一般拓扑学
- 组合拓扑学
- 代数拓扑学
- 微分拓扑学
- 几何拓扑学 ja:位相幾何学 ko:위상수학 simple:Topology

皮亚诺公理

皮亚诺公理，也称皮亚诺公设，是数学家皮亚诺提出的关于自然数的五条公理系统。根据这五条公理可以建立起一阶算术系统，也称皮亚诺算术系统。

定理

皮亚诺的这五条公理用非形式化的方法叙述如下： #1是自然数； #每一个确定的自然数a，都有一个确定的后继数a' ，a' 也是自然数（一个数的后继数就是紧接在这个数后面的数，例如，1的后继数是2，2的后继数是3等等）； #如果b、c都是自然数a的后继数，那么b = c； #1不是任何自然数的后继数； #任意关于自然数的命题，如果证明了它对自然数1是对的，又假定它对自然数n为真时，可以证明它对n' 也真，那么，命题对所有自然数都真。(这条公理保证了数学归纳法的正确性) 若将0也视作自然数，则公理中的1要换成0。 更正式的定义如下： 一个戴德金-皮亚诺结构为一满足下列条件的三元组(X, x, f)：
- X是一集合， x为X中一元素，f是 X 到自身的映射
- x 不在 f的值域内.
- f 为一单射.
- 若A 为X的子集并满足:
  - x属于 A, 且
  - 若 a 属于 A, 则 f(a) 亦属于 A :则 A = X.

参见


- 自然数 Category:数论 Category:数理逻辑 ja:ペアノの公理 ko:페아노의 공리

算法

Category:代数 Category:算法 算法是指完成一个任务所需要的具体步骤和方法。也就是说给定初始状态或输入数据，经过计算机程序的有限次运算，能够得出所要求或期望的终止状态或输出数据。 算法常常含有重复的步骤和一些比较或逻辑判断。如果一个算法有缺陷，或不适合于某个问题，执行这个算法将不会解决这个问题。不同的算法可能用不同的时间、空间或效率来完成同样的任务。一个算法的优劣可以用空间复杂度与时间复杂度来衡量。

算法的历史

“算法”的中文名稱出自周髀算經；而英文名稱 Algorithm 来自于9世纪波斯数学家比阿勒·霍瓦里松的名字al-Khwarizmi，因為比阿勒·霍瓦里松在数学上提出了算法这个概念。“算法”原为"algorism"，意思是阿拉伯数字的运算法则，在18世纪演变为"algorithm"。 第一次编写算法是Ada Byron于1842年为巴贝奇分析机编写求解解伯努利方程的程序，因此Ada Byron被大多数人认为是世界上第一位程序员。因为巴贝奇(Charles Babbage)未能完成他的巴贝奇分析机，这个算法未能在巴贝奇分析机上执行。 因为"well-defined procedure"缺少数学上精确的定义，19世纪和20世纪早期的数学家、逻辑学家在定义算法上出现了困难。20世纪的英国数学家图灵提出了著名的图灵论题，并提出一种假想的计算机的抽象模型，这个模型被称为图灵机。图灵机的出现解决了算法定义的难题，图灵的思想对算法的发展起到了重要的作用。

算法的特征

#输入，一个算法必须有零个或多个输入量。 #输出，一个算法应有一个或多个输出量，输出量是算法计算的结果。 #确定性，算法的描述必须无歧义，以保证算法的执行结果是确定的。 #有穷性，算法必须在有限步骤内实现。注：此处“有限”不同于数学概念的“有限”，天文数字般的有限对于实际问题并无意义。 #有效性（亦称可行性），能够实现，算法中描述的操作都是可以通过已经实现的基本运算执行有限次来实现。

形式化算法

算法是计算机处理信息的本质，因为计算机程序本质上是一个算法来告诉计算机确切的步骤来执行一个指定的任务，如计算职工的薪水或打印学生的成绩单。 一般地，当算法在处理信息时，会从输入设备或数据的存储地址读取数据，把结果写入输出设备或某个存储地址供以后再调用。

算法的复杂度

算法的时间复杂度

算法的时间复杂度是指算法需要消耗的时间资源。一般来说，计算机算法是问题规模n的函数f（n），算法的时间复杂度也因此记做 T（n）=O（f（n）） 因此，问题的规模n越大，算法执行的时间的增长率与f（n）的增长率正相关，称作渐进时间复杂度（Asymptotic Time Complexity）。

算法的空间复杂度

算法的空间复杂度是指算法需要消耗的空间资源。其计算和表示方法与时间复杂度类似，一般都用复杂度的渐近性来表示。同时间复杂度相比，空间复杂度的分析要简单得多。

非確定性多項式時間(NP)

算法的实现

算法不单单可以用计算机程序来实现，也可以在神经网络、电路或者机械设备上实现。

例子一

这是算法的一个简单的例子。 我们有一串随机数列。我们的目的是找到这个数列中最大的数。如果将数列中的每一个数字看成是一颗豆子的大小,可以将下面的算法形象地称为“捡豆子”： # 首先将第一颗豆子放入口袋中。 # 从第二颗豆子开始检查，直到最后一颗豆子。如果正在检查的豆子比口袋中的还大，则将它捡起放入口袋中，同时丢掉原先口袋中的豆子。 # 最后口袋中的豆子就是所有的豆子中最大的一颗。 下面是一个形式算法，用近似于编程语言的伪代码表示 给定：一个数列“list"，以及数列的长度"length(list)" largest = list[1] for counter = 2 to length(list): if list[counter] > largest: largest = list[counter] print largest 符号说明:
- = 用于表示赋值。即：右边的值被赋予给左边的变量。
- List[counter]用于表示数列中的第counter项。例如：如果counter的值是5，那么List[counter]表示数列中的第5项。
- <= 用于表示“小于或等于”。

例子二

求两个自然数的最大公约数 设两个变量 M 和 N #如果 M < N，则交换 M 和 N #M 被 N 除，得到余数 R #判断 R＝0，正确则 N 即为“最大公约数”，否则下一步 #将 N 赋值给 M，将 R 赋值给 N，重做第一步。 用“BASIC 代码”表示－－ If M < N Then Swap M,N Do While R <> 0 R = M Mod N M = N N = R Loop Print N

算法设计和分析的基本方法


- 分治法
- 动态规划
- 贪心法（亦作饕餮法）

算法的分类


- 基本算法
  - 枚举
  - 搜索
    - 深度优先搜索
    - 广度优先搜索
    - 启发式搜索
    - 遗传算法
- 数据结构的算法
- 数论与代数算法
- 计算几何的算法
  - 凸包算法
- 图论的算法
  - 哈夫曼编码
  - 树的遍历
  - 最短路径算法
  - 最小生成树算法
  - 最小树形图
  - 网络流算法
  - 匹配算法
- 动态规划
- 其他
  - 数值分析
  - 加密算法
  - 排序算法
  - 检索算法
  - 随机化算法
  - 关于并行算法，请参阅并行计算一文。

参见


- 计算机科学课程列表 ja:アルゴリズム ko:알고리즘 th:อัลกอริทึม

逻辑非

逻辑非是布尔代数中一种一元运算。它的运算结果是将运算元的真值取反。 命题 p的非可以有几种写法：
- p (p 上加一横)
- ~p
- ¬p
- NOT p
- !p 以上可以读做 " p不成立"或者 "非 p"。 ~p 为真 当且仅当 p为假。 例如，如果p代表命题“今天星期六”，则它的非~p代表命题“今天不是星期六”。 category:布尔代数 ja:否定 th:นิเสธ

命题演算

在数理逻辑中命题演算或句子演算是一个形式演绎系统，其原子公式是命题变量。(相对于谓词逻辑，它是量化的并且它的原子公式是谓词函数；和模态逻辑，它可以是非真值泛函的。) 演算是用来证明有效的公式(就是说它的定理)和论证(argument)的逻辑系统。它是公理的集合(它可以为空或是可数无限集合)或公理模式(schemata)，和推导有效的推理的推导规则。形式文法(或语法)递归定义语言的表达式和合式(well-formed)公式(wff)。此外给出定义真值(truth)和求值(valuation)(或释义(interpretation))的语义。它允许我们确定哪个 wff 是有效的(也就是定理)。 在命题演算中语言由命题变量(或者叫占位符(placeholder))和句子算子(或者叫连结词)。wff 是任何原子公式或在句子操作符之上建造的公式。 在下文中我们描述一种标准命题演算。很多不同的公式系统存在，它们都或多或少等价但在下列方面不同：(1)它们的语言(就是说哪些操作符和变量是语言的一部分); (2) 它们有哪些(如果有的话)公理; (3)采用了哪些推理规则。

文法

语言的构成: # 字母表的大写字母，表示命题变量。它们是原子公式。惯例上，使用拉丁字母(A, B, C)或希腊字母(χ, φ, ψ)，但是不能混合使用。 # 表示连结词(connective)(或逻辑算子)的符号: ¬、∧、∨、→、↔。(我们可以使用更少的算子(和相应的符号)，因为一些算子是简写形式 — 例如，P → Q 等价于 ¬ P ∨ Q)。 # 左右圆括号: (，)。 合式公式(wff)的集合右如下规则递归的定义: # 基础: 字母表的字母(通常是大写的，如A、B、φ、χ 等)是 wff。 # 归纳条款 I: 如果 φ 是 wff，则 ¬ φ 是 wff。 # 归纳条款 II 如果 φ 和 ψ 是 wff，则 (φ ∧ ψ)、(φ ∨ ψ)、(φ → ψ) 和 (φ ↔ ψ) 是 wff。 # 闭包条款: 其他东西都不是 wff。 重复的应用这三个公式允许生成复杂的 wff。例如: # 通过规则 1，A 是 wff。 # 通过规则 2，¬ A 是 wff。 # 通过规则 1，B 是 wff。 # 通过规则 3，( ¬ A ∨ B ) 是 wff。

演算

为了简单化，我们使用自然演绎系统，它没有公理；或者等价的说，它有空的公理集合。 使用我们的演算的推导将用编号后的行的列表，在每行之上有一个单一的 wff 和一个断定(justification)的形式展示出来。任何前提(premise)都在定部，并带有 "p" 作为它们的断定。结论将在最后一行。推导将被看作完备的，条件是所有行都是通过正确的应用一个规则而从前面的行得出的。 (作为一种对比的方式，参见证明树)。

公理

我们的公理集合是空集。

推理规则

我们的命题演算有十个推理(inference)规则。这些规则允许我们从给定的一组假定为真的公式中推导出其他为真的公式。前八个简单的陈述我们可以从其他 wff 推论出(infer)特定的 wff。但是最后两个规则使用了假言(hypothetical)推理，这意味着在规则的前提中我们可以临时的假定一个(未证明的)假设(hypothesis)作为推导出的公式集合的一部分，来查看我们是否能推导出一个特定的其他公式。因为前八个规则不是这样而通常被描述为非假言规则，而最后两个就叫做假言规则。 ; 双重否定除去: 从 wff ¬ ¬ φ，我们可以推出 φ。 ; 合取介入: 从任何 wff φ 和任何 wff ψ，我们可以推出 ( φ ∧ ψ )。 ; 合取除去: 从任何 wff ( φ ∧ ψ )，我们可以推出 φ 和 ψ。 ; 析取介入: 从任何 wff φ，我们可以推出 (φ ∨ ψ) 和 (ψ ∨ φ)，这里的 ψ 是任何 wff。 ; 析取除去: 从 ( φ ∨ ψ )、( φ → χ ) 和 ( ψ → χ ) 形式的wff，我们可以推出 χ。 ; 双条件介入: 从 ( φ → ψ ) 和 ( ψ → φ ) 形式的 wff，我们可以推出 ( φ ↔ ψ )。 ; 双条件除去: 从 wff ( φ ↔ ψ )，我们可以推出 ( φ → ψ ) 和 ( ψ → φ )。 ; 肯定前件: 从 φ 和 ( φ → ψ ) 形式的 wff，我们可以推出 ψ。 ; 条件证明: 如果在假定假设 φ 的时候可以推导出 ψ，我们可以推出 ( φ → ψ )。 ; 反证证明: 如果在假定假设 φ 的时候可以推导出 ψ 和 ¬ ψ，我们可以推出 ¬ φ。

证明的例子

下面是(语法上的)证明的一个例子:
要证明: A \rightarrow A
证明:
解释 A \vdash A 为 "假定 A，推导出 A"。读 \vdash A \rightarrow A 为 "不假定任何东西，推导出 A 蕴涵 A" ，或者 "A 蕴涵 A 是重言式" ，或者 "A 蕴涵 A 是永真的"。

规则的可靠性和完备性

这组规则的关键特性是它们是可靠的和完备的。非形式的，这意味着规则是正确的并且不再需要其他规则。这些要求可以如下这样正式的提出。 我们定义真值指派为把命题变量映射到真或假的函数。非形式的，这种真值指派可以被理解为对事件的可能状态(或可能性世界)的描述，在这里特定的陈述是真而其他为假。公式的语义因而可以被形式化，通过对它们把那些"事件状态"认定为真的定义。 我们通过如下规则定义这种真值 A 在什么时候满足特定 wff:
- A 满足命题变量 P 当且仅当 A(P) = 真
- A 满足 ¬ φ 当且仅当 A 不满足 φ
- A 满足 (φ ∧ ψ) 当且仅当 A 满足 φ 与 ψ 二者
- A 满足 (φ ∨ ψ) 当且仅当 A 满足 φ 和 ψ 中至少一个
- A 满足 (φ → ψ) 当且仅当没有 A 满足 φ 但不满足 ψ 的事例
- A 满足 (φ ↔ ψ) 当且仅当 A 满足 φ 与 ψ 二者，或则不满足它们中的任何一个 通过这个定义，我们现在可以形式化公式 φ 被特定公式集合 S 蕴涵的意义。非形式的，就是在使给定公式集合 S 成立的所有可能情况下公式 φ 也成立。这导引出了下面的形式化定义: 我们说 wff 的集合 S 语义蕴涵(蕴涵：entail 或 imply)特定的 wff φ，条件是满足在 S 中的公式的所有真值指派也满足 φ。 最后我们定义语法蕴涵，φ 被 S 语法蕴涵，当且仅当我们可以在有限步骤内使用我们提出的上述推理规则推导出它。这允许我们精确的公式化推理规则的可靠性和完备性的意义: ; 可靠性 : 如果 wff 集合 S 语法蕴涵 wff φ，则 S 语义蕴涵 φ ; 完备性 : 如果 wff 集合 S 语义蕴涵 wff φ，则 S 语法蕴涵 φ 对上述规则集合这些都成立。

可靠性证明的梗概

(对于多数逻辑系统，这是相当"简单的"证明方向) 符号约定: 设 "G" 是涉及语句集合的变量。设 "A"、"B" 和 "C" 是涉及句子的变量。我们把 "G 语法蕴涵 A" 写成 "G 证明 A"。我们把 "G 语义蕴涵 A" 写成 "G 蕴涵 A"。 我们要展示: (A)(G)(如果 G 证明 A，则 G 蕴涵 A) 我们注意到 "G 证明 A" 有一个归纳定义，这给予我们直接的办法来证实(demonstrate)"如果 G 证明 A，则 . . ."形式的断言。所以我们的证明是用归纳法进行的。
- I. 基础。展示: 如果 A 是 G 的成员则 G 蕴涵 A
- [II. 基础。展示: 如果 A 是公理，则 G 蕴涵 A
- III. 归纳步骤: (a) 假定对于任意的 G 和 A，如果 G 证明 A 则 G 蕴涵 A。(如果需要的话，对 B、C 等做同样的假定) ::(b) 对于针对 A 的推论的规则的，导出一个新的句子 B 的每个可能的应用，展示 G 蕴涵 B。 (N.B. 对于上述演算基础步骤 II 可以省略，它是自然演绎系统而没有公理。基本上，它涉及展示每个公理都是(语义上)逻辑真理。) 基础步骤证实了对于任何 G 来自 G 的最简单的可证明的语句都被 G 所蕴涵。(这是简单的，因为集合蕴涵它的任何一个成员是语义事实，这是平凡的(trivial))。归纳步骤将有系统的覆盖所有的进一步的可证明的句子--通过考虑我们能够使用推理规则达成逻辑结论的每种情况--并展示如果一个新句子是可证明的，它也是在逻辑上被蕴涵的。(例如，我们可能有一个告诉我们从 "A" 可以推导出 "A 或 B"。在 III.(a) 中我们假定如果 A 是可证明的则是被蕴涵的。我们也知道如果 A 是可证明的，则 "A 或 B" 是可证明的。我们必须展示接着 "A 或 B" 也是被蕴涵的。我们求助于语义定义和我们所做的假定来完成。我们假定了 A 从 G 是可证明出来的。所以它也被 G 所蕴涵。所以使 G 全部为真的任何语义求值也使 A 为真。此外通过"或"的语义定义，使 A 为真的任何求值都使 "A 或 B" 为真。所以使 G 的全部为真的任何求值都使 "A 或 B" 为真。所以 "A 或 B"被蕴涵了。)一般的，归纳步骤将由有一定长度的，却是推论的所有规则的简单的逐个例的分析组成的，它展示每个"保持的"语义蕴涵。 通过可证明性的定义，除了 G 的成员、公理、或从规则得出的句子之外没有是可证明的；所以如果所有这些都是语义上被蕴涵的，则演绎演算是可靠的。

完备性证明的梗概

(这通常是非常困难的证明方向。) 我们接受同上面一样的符号约定。 我们要展示: 如果 G 蕴涵 A，则 G 证明 A。我们通过反证法来进行: 我们转而展示如果 G 不证明 A，则 G 不蕴涵 A。
- I. G 不证明 A。(假定)
- II. 如果 G 不证明 A，则我们可以构造一个(有限的)"最大化的集合" G
- ，它是 G 的超集并且不证明 A。
  - (a)在这个语言的所有句子上加置一个"次序"。(比如，字母表次序)，并把它们编号为 E1, E2, . . .
  - (b)归纳的定义集合(G0, G1 . . . )的一个序列(series) Gn 为如下 (i)G0=G。 (ii) 如果 证明 A，则 G(k+1)=Gk。 (iii) 如果 不证明 A，则 G(k+1)=
  - (c)定义 G
- 为所有 Gn 的并集。(就是说，G
- 在任何 Gn 中的所有句子的集合)。
  - (d) 可以容易的展示 (i) G
- 包含(是其超集) G (通过 (b.i))；(ii) G
- 不证明 A (因为如果它证明 A 则某些句子被增加到某个 Gn 上而导致它证明了 A; 但是这被定义所排除)；和 (iii) G
- 是(关于 A) "最大化的集合": 如果任何更多的句子不管怎样的被增加到 G
- ，它就会证明 A。(因为如果有可能增加任何更多的句子，再次根据定义，在构造 Gn 期间被遇到的时候它们就应当已经被增加进去了。)
- III. 如果 G
- 是(关于 A)的最大化集合，则它是"类真理的"。这意味着它包含句子 "A"，只在它不包含非-A 的句子的条件下; 如果它包含 "A" 并且包含 "如果 A 则 B"，则它也包含 "B"；以此类推。
- IV. 如果 G
- 是类真理的，则有这个语言的 "G
- -规范"求值: 它使在 G
- 中每个句子为真而在 G
- 之外的所有句子为假，而仍然遵守在这个语言的语义合成(composition)的法则。
- V. G
- -规范求值将使我们最初的集合 G 全部为真，而使 A 为假。
- VI. 如果有在其上 G 是真而 A 是假的求值，则 G 不(语义上)蕴涵 A。 Q.E.D.

可供选择的演算

有可能定义其他版本的命题演算，它通过公理的方式定义了多数逻辑算子的语法，并且它只使用一个推理规则。

公理

设 φ、χ 和 ψ 表示合式公式。(wff 自身将不包含任何希腊字母，而只包含大写罗马字母、连结算子和圆括号)。公理有
- THEN-1: φ → (χ → φ)
- THEN-2: (φ → (χ → ψ)) → ((φ → χ) → (φ → ψ))
- AND-1: φ ∧ χ → φ
- AND-2: φ ∧ χ → χ
- AND-3: φ → (χ → (φ ∧ χ))
- OR-1: φ → φ ∨ χ
- OR-2: χ → φ ∨ χ
- OR-3: (φ → ψ) → ((χ → ψ) → (φ ∨ χ → ψ))
- NOT-1: (φ → χ) → ((φ → ¬ χ) → ¬ φ)
- NOT-2: φ → (¬ φ → χ)
- NOT-3: φ ∨ ¬ φ 公理 THEN-2 可以被看作是"关于蕴涵的蕴涵的分配特性"。公理 AND-1 和 AND-2 对应于"合取除去"。在 AND-1 和 AND-2 之间的关系反映了合取算子的交换性。公理 AND-3 对应于"合取介入"。公理 OR-1 和 OR-2 对应于"析取介入"。在 OR-1 和 OR-2 之间的关系反映了析取算子的交换性。公理 NOT-1 对应于"反证法"。公理 NOT-2 说明了"从矛盾中可以推导出任何东西"。公理 NOT-3 叫做"排中律" (拉丁语 tertium non datur: "排除第三者")并反映了命题公式的语义求值: 公式可以有的真值要么是真要么是假。至少在经典逻辑中，没有第三个真值。直觉逻辑不接受公理 NOT-3。

推理规则

推理规则是肯定前件:
- \phi, \ \phi \rightarrow \chi \vdash \chi . 如果还使用双箭头的等价算子的话，则要增加如下"自然"推理规则:
- IFF-1: \phi \leftrightarrow \chi \vdash \chi \rightarrow \phi
- IFF-2: \phi \rightarrow \chi, \ \chi \rightarrow \phi \vdash \phi \leftrightarrow \chi

元推理规则

设示范被表示为相继式，假设在十字转门(turnstile)的左侧而结论在十字转门的右侧。则演绎定理可以被陈述如下: : 如果相继式 :: \phi_1, \ \phi_2, \ ... , \ \phi_n, \ \chi \vdash \psi : 已经被证实了，则也有可能证实相继式 :: \phi_1, \ \phi_2, \ ..., \ \phi_n \vdash \chi \rightarrow \psi 。 这个演绎定理(DT)自身没有公式化为命题演算: 它不命题演算的定理，而是关于命题演算的一个定理。在这个意义上，它是元定理，相当于关于命题演算可靠性和完备性的定理。 在另一方面，DT 对与简化语法上的证明过程是如此的有用以至于它看作和用做推理规则，同肯定前件一起使用。在这个意义上，DT 对应于自然条件证明推理规则，它是在本文中提出的第一个版本的命题演算的一部分。 DT 的逆定理也是有效的: : 如果相继式 :: \phi_1, \ \phi_2, \ ..., \ \phi_n \vdash \chi \rightarrow \psi : 已经被证实了，则也有可能正式相继式 :: \phi_1, \ \phi_2, \ ... , \ \phi_n, \ \chi \vdash \psi 实际上，DT 的逆定理的有效性相对于 DT 而言是平凡的: : 如果 :: \phi_1, \ ... , \ \phi_n \vdash \chi \rightarrow \psi : 则 :: 1: \phi_1, \ ... , \ \phi_n, \ \chi \vdash \chi \rightarrow \psi :: 2: \phi_1, \ ... , \ \phi_n, \ \chi \vdash \chi : 并且可以演绎自 (1) 和 (2) :: 3: \phi_1, \ ... , \ \phi_n, \ \chi \vdash \psi : 通过肯定前件的方式，Q.E.D. DT 的拟命题有着强有力的蕴涵: 它可以用来把公理转换成推理规则。例如，公理 AND-1, : \vdash \phi \wedge \chi \rightarrow \phi 可以通过演绎定理的逆定理的方式被转换成推理规则 : \phi \wedge \chi \vdash \phi 这是合取除去，是(在本文中)第一个版本的命题演算中使用的十个推理规则中的一个。

证明的例子

下面是(语法上)证明的一个例子，只涉及到公理 THEN-1 和 THEN-2:
要证明: A → A (蕴涵的自反性)。
证明: :1. (A → ((A → A) → A)) → ((A → (A → A)) → (A → A)) ::公理 THEN-2 通过 φ = A, χ = A → A, ψ = A :2. A → ((A → A) → A) ::公理 THEN-1 通过 φ = A, χ = A → A :3. (A → (A → A)) → (A → A) ::得自 (1) 和 (2) 通过肯定前件。 :4. A → (A → A) ::公理 THEN-1 通过 φ = A, χ = A :5. A → A ::得自 (3) 和 (4) 通过肯定前件。

其他逻辑演算

命题演算大概是在所有当前使用的逻辑演算中最简单的一种。(亚里士多德的"三段论"演算，在现代逻辑中在很大程度上被替代了，它与命题逻辑相比在某些方面更简单--但在其他方面更加复杂)。它可以按很多方式来扩展。 最直接的方式是开发一个更加复杂的逻辑演算，介入对所用于的句子的更精细的细节敏感的规则。在命题逻辑中的"原子句子"被分解成项、变量、谓词和量词的时候，它们就生成了一阶逻辑，或者叫做一阶谓词逻辑，它保持命题逻辑的所有规则并增加了一些新规则。(例如，从"所有的狗都是动物"我们可以推出"如果 Rover 是狗，则 Rover 是动物")。 通过一阶逻辑的工具，有可能公式化一些理论，要么带有显式的公理要么通过推理规则，而把它们自身当作逻辑演算。算术是其中最周知的理论；其他的还包括集合论和 mereology。 模态逻辑也提供了一种推理的变体，它不能在命题演算中捕获。例如，从"必然性的 p" 我们可以推出 p。从 p 我们可以推出 "可能性的 p"。 多值逻辑是允许句子有除了真和假之外的值的逻辑。(例如，都不和都是是标准的"额外值"；"连续统逻辑"允许每个句子有任何的在真和假之间的表示"真实程度"的有限的数值)。这些逻辑经常要求与命题逻辑非常不同的运算设备。

参见


- 布尔代数主题列表
- 哥德尔、埃舍尔、巴赫
- 布尔逻辑
- 弗雷格的命题演算

外部链接


- [http://www.iep.utm.edu/p/prop-log.htm Article on Propositional logic] at the Internet Encyclopedia of Philosophy
- [http://www.ltn.lv/~podnieks/mlog/ml2.htm Introduction to Mathematical Logic] Category:离散数学 Category:数理逻辑 th:แคลคูลัสเชิงประพจน์

模态逻辑

模态逻辑，或者叫(不很常见)内涵逻辑，是处理用模态如可能、或许、可以、一定、必然等限定的句子的逻辑分支。使用模态算子如可能或必然的任何逻辑系统因此就叫做模态逻辑。模态逻辑可以用语义的内涵性来描述其特征: 非模态逻辑都有复杂句子的真值由子句子的真值决定的特征。所以它们是外延性的。相反在模态逻辑中，这不成立: "George W. Bush 是美国总统" 和 "2 + 2 = 4" 是真的，但是 "George W. Bush 必然是美国总统" 是假的，而"2 + 2 = 4 是必然的" 是真的。 形式模态逻辑使用模态判决算子表示模态。模态算子的基本集合通常被指定为 \Box 和 \Diamond。在真势模态逻辑(就是说必然性和可能性的逻辑)中 \Box 表示必然性，而 \Diamond 表示可能性。句子被认定为
- 可能的 如果它可能为真(不管实际上是真是假);
- 必然的 如果它不可能为假;
- 偶然的 如果它不是必然为真，就是说，可能为真可能为假。偶然的真理是实际上为真，但可能曾经不是的真理。

形而上学和其他模态

真势和认识

模态逻辑最经常用来谈论所谓的真势模态: "...是必然的" 或者 "....是可能的" ，这些模态(包括形而上学模态和逻辑模态)最容易混淆于认识模态(来自希腊语 episteme, 知识): "...确实是真的" 和 "...(对给定的可获得的信息)或许是真的"。在普通的话语中这两种模态经常用类似的词来表达；下列对比可能有所帮助: 一个人 Jones 可以合理的同时说出: (1) "我确信 Bigfoot 不可能存在"，还有(2) "Bigfoot 存在的确是可能的"。Jones 通过(1)表达的意思是，对于给定的所有可获得的信息，Bigfoot 存在与否是没有疑问的。这是一个认识上的断言。通过(2)表达的意思是这个事物可能曾是其它样子的。他的意思不是 "就我所知而言，Bigfoot 可能存在" 。(所以这不矛盾于(1))。而是，他做了一个形而上学上的断定，即使他不知道，Bigfoot 存在仍是可能的。 在其他方面，Jones 可以说 (3) "哥德巴赫猜想可能为真，并也可能为假，还有(4) 如果它是真的，则它必然是真的，而不可能是假的。" 这里 Jones 的意思是，就他所知而言，它为真为假都是在认识上可能的(哥德巴赫猜想仍未被证明是真还是假)。但是如果有这么一个证明(至今仍未发现)，则哥德巴赫猜想为假在逻辑上是不可能的 -- 不会有一组数违背它。逻辑上的可能性是一种真势(alethic)可能性；(4)做了对这个数学论断已经为假是否可能的一个断言，而(3)只做了对就 Jones 所知而言这个论断被证实为假是否可能的一个断言，所以 Jones 还是不自相矛盾。 认识上的可能性还以一种非形而上学的方式关注真实世界。形而上学的可能性以可能曾是的方式关注世界，而认识上的可能性以(就我所知而言)可能正是的方式关注世界。比如，我想知道在离开前是否要带把伞。如果你告诉我 "外面可能在下雨" -- 在一种认识上可能的意义上--那么这会影响我是否带伞的决定。但是如果你告诉我 "外面下雨是可能的" -- 在一种形而上学上可能的意义上--那么我从这种大道理中没有得到任何启示。 大量的哲学文献关心真势而非认识模态。(实际上，其中大多数关心一种最广泛的真势模态，就是逻辑可能性)。这不是说真势可能性比我们日常用的认识可能性更重要(考虑上面决定是否带伞的例子)。只是说在哲学研究中的优先权不是日常生活中的重要性带来的。

道义和时态

言语中有一些类似的模式，尽管不大可能与真势模态混淆但仍密切的相关。其一是有关时间的谈论。明天可能会下雨，但也可能不下好像是合理的；在另一方面，如果昨天下雨了，如果实际上已经下了，则说"昨天可能没有下雨"就不是完全正确的。过去好像"固定的"或必然的，而将来在某种程度上不是。很多哲学家和逻辑学家认为这种推理不是很好；但是我们经常以这种方式谈话，所以最好有一种逻辑能捕获它的结构。类似的有关道德的谈论，或者说义务和规范一般好像也有模态结构。在 "你必须这么做" 和 "你可以这么做" 之间的区别看起来很像在"这是必然的和这是可能的"之间的区别。这种逻辑叫做道义逻辑，道义来自希腊语 "duty"。 值得注意的是，模态逻辑可以开发出实现多数这种方言；它们有公共逻辑机构的事实(使用"内涵"或非真值泛函的句子算子)使它们都是同一个东西的变体。认识逻辑被证实捕获于系统"S4"；道义逻辑捕获于系统"D"，时态逻辑捕获于"t"(小写的)，而真势逻辑被证实为"S5"

模态逻辑的释义

在模态逻辑的最常见解释中，你要考虑"所有逻辑上可能的世界"。如果一个陈述在所有可能的世界中是真的，则它是必然的真理。如果一个陈述碰巧在我们的世界中是真的，但不是在所有可能的世界中是真的，则它是偶然的真理。在某些(不是必须在我们自己的)可能的世界中是真的陈述叫做可能的真理。 这种"可能的世界"是否是解释模态逻辑的最佳方式，怎样在文字上接受这种方言，是形而上学的鲜活的问题。例如，可能的世界的方言可以把关于 Bigfoot 的断言翻译为"有某个可能的世界，在其中 Bigfoot 存在"。要主张 Bigfoot 的存在性是可能的，但不是现实的，你可以说"有某个可能的世界，在其中 Bigfoot 存在；但是在现实世界中，Bigfoot 不存在"。但是对使模态断言对我们负责的那个东西是什么仍是不清楚的。我们真的要宣称可能的世界的存在性吗？它在每一点都同我们的现实世界一样真实，却惟独不是现实的。David Lewis 强硬的说就是这样，可能的世界同我们自己的世界一样真实。这种立场叫做"模态现实主义"。不足为奇的，多数哲学家不愿意接受这种特别的学说，在搜寻一种可替代的方式来释义我们的模态断言所蕴含的本体论承诺。

形式化规则

有很多有不同性质的模态逻辑。在其中很多必然性和可能性的概念满足下列 de Morgan 定律的联系: :"X 是非必然的" 等价于 "非 X 是可能的"。 :"X 是非可能的" 等价于 "非 X 是必然的"。 尽管模态逻辑教科书比如 Hughes 和 Cresswell 的 "A New Introduction to Modal Logic" 覆盖了这个定律不成立的一些系统。 模态逻辑向命题逻辑的合式公式增加上必然性和偶然性。在一些记号中 "必然的 p" 使用"方块"( \Box p )表示，而"可能的 p" 使用"菱形"(\Diamond p)表示。无论是什么样的记号，两个算子是以相互定义的方式定义的:
- \Box p (必然的 p) 等价于 \neg \Diamond \neg p (非可能的非-p)
- \Diamond p (可能的 p) 等价于 \neg \Box \neg p (非必然的非-p) 因此，\Box 和 \Diamond 叫做对偶算子。 要建立模态逻辑的可用系统，必须向命题逻辑的增加什么公理是非常有争议的主题。得名于 Saul Kripke 的 K，只向经典命题逻辑公理体系增加了如下规则:
- 必然性规则: 如果 p 是 K 的定理，则 \Box p 也是。
- 分配律公理: 如果 \Box (p \rightarrow q) 则 (\Box p \rightarrow \Box q) (这也叫做公理 K) 这些规则缺乏从 p 的必然性到 p 的实际情况的公理，所以通常要补充上下列"自反性"公理，这就生成经常叫做 T 的一个系统。
- \Box p \rightarrow p (如果 p 是必然的，则 p 是事实) 这是多数但不是全部模态逻辑系统的规则。Jay Zeman 的书 "Modal Logic" 覆盖了没有这个规则的系统如 S1^0。 但 K 是一个弱模态逻辑。特别是留下了一个公开的问题，命题是必然的但只偶尔是必然的。如果 \Box p 是真的则 \Box \Box p 是真的不是 K 的定理，它是说，必然的真理必然是必然的。这可能不是 K 的大缺陷，因为这些好像是十分奇怪的问题，而试图解答它们的任何尝试都把我们卷入混乱的难题中。无论如何，对这种问题的不同解决方式生成了不同的模态逻辑系统。 今天最常见的系统是模态逻辑 S5，它通过增加使所有模态真理是必然的公理来粗壮的解答了这个问题: 例如，如果 p 是可能的，则 p 必然是可能的，如果 p 是必然的，则它必然是必然的。很多人认为它正当的根据是，它是在我们需要每个可能的世界相对于每个其他世界都是可能的时候所获得的系统。不过，模态逻辑的其他系统已经被公式化了，部分的因为 S5 不能很好的适合我们感兴趣的所有种类的形而上学模态。(若此则意味着可能的世界的谈论不能很好的适合这些种类的模态)。

模态逻辑的发展

尽管亚里士多德的逻辑几乎全部都关注直言三段论的理论，他的著作还包含在模态逻辑要点上的一些延伸讨论(比如他著名的在解释篇 § 9 中海战悖论)，并且它们与潜在性和时间有关连。遵从他的著作，经院学者为模态逻辑的严格理论开发出了根基，大多在关于本质和偶然的陈述的逻辑的注释的上下文中。在中世纪的作家中，在 William of Ockham 和 John Duns Scotus 的著作中找到了关于模态逻辑的一些最重要的工作。 形式模态逻辑的缔造者是 C. I. Lewis，他在专著 A Survey of Symbolic Logic (1918) 中介入了一个系统(后来叫做 S3)，并(同 C. H. Langford 一起)在书 Symbolic Logic (1932)中介入了系统 S1-S5。J. C. C. McKinsey 在 1941 年使用代数方法(带有算子的布尔代数)来证明 Lewis 的 S2 和 S4 的可判定性。Saul Kripke 从 1959 年开始为模态逻辑设计了关系语义或可能的世界语义。Vaughan Pratt 在 1976 年介入了动态逻辑。Amir Pnueli 在 1977 年提出使用时态逻辑来公式化频繁操作并发程序的行为。 时态逻辑，在 1957 年由 A. N. Prior 发明，与模态逻辑有密切的关联，因为增加了模态算子 [F] 和 [P]，分别意味着今后和至今，导致了时态逻辑的一个系统。 模态逻辑的风味包括: 命题动态逻辑(PDL)，命题线性时态逻辑(PLTL)，线性时态逻辑(LTL)，计算树逻辑(CTL)， Hennessy-Milner 逻辑，S1-S5 和 T。

引用


- M. Fitting and R.L. Mendelsohn (1998) First Order Modal Logic. Kluwer Academic Publishers.
- James Garson (2003) [http://plato.stanford.edu/entries/logic-modal Modal logic]. Entry in the Stanford Encyclopedia of Philosophy.
- Rod Girlie (2000) Modal Logics and Philosophy. Acumen (UK). The proof theory employs refutation trees (semantic tableaux). A good introduction to the varied interpretations of modal logic.
- Robert Goldblatt (1992) "Logics of Time and Computation", CSLI Lecture Notes No. 7, Centre for the Study of Language and Information, Stanford University, 2nd ed. (distributed by University of Chicago Press).
- Robert Goldblatt (1993) "Mathematics of Modality", CSLI Lecture Notes No. 43, Centre for the Study of Language and Information, Stanford University. (distributed by University of Chicago Press).
- G.E. Hughes and M.J. Cresswell (1968) An Introduction to Modal Logic, Methuen.
- G.E. Hughes and M.J. Cresswell (1984) A Companion to Modal Logic, Medhuen.
- G.E. Hughes and M.J. Cresswell (1996) A New Introduction to Modal Logic, Routledge.
- E.J. Lemmon (with Dana Scott), 1977, An Introduction to Modal Logic, American Philosophical Quarterly Monograph Series, no. 11 (ed. by Krister Segerberg), Basil Blackwell, Oxford.
- J. Jay Zeeman (1973) [http://www.clas.ufl.edu/users/jzeman/modallogic/ Modal Logic]. D. Reidel Publishing Company.

参见


- De dicto and de re
- 混合逻辑
- 内部代数
- 可解释性逻辑
- 可证明性逻辑
- Kripke语义

外部链接


- [http://www-formal.stanford.edu/jmc/mcchay69/node22.html A discussion of modal logic] by John McCarthy
- [http://www.earlham.edu/~peters/courses/logsys/nonstbib.htm Bibliography of Non-Standard Logics] by Peter Suber
- [http://www.cc.utah.edu/~nahaj/logic/structures/systems/index.html List of Logic Systems] List of most of the more popular modal logics.
- [http://aiml.net/ Advances in Modal Logic] (bi-annual international conference and book series in Modal Logic)
- [http://www.cass.net.cn/chinese/s14_zxs/facu/liuxinwen/02.htm 模态逻辑]，[新西兰] M·J·克雷斯韦尔，《哲学逻辑指南》，第7章，中国人民大学出版社，2005年

致谢

本文包含最初来自Free On-line Dictionary of Computing的一些材料，经过授权在 GFDL 下。 Category:逻辑 ja:様相論理学

阿隆佐·邱奇

阿隆佐·邱奇是美国数学家，1936年发表可计算函数的第一份精确定义，对算法理论的系统发展做出巨大贡献。邱奇在普林斯顿受教并工作四十年，曾任数学与哲学教授。1967年迁往加利福尼亚大学洛杉矶分校。 解决算法问题包括构造一个能解决某一指定集及其他相关集的算法，如果该算法无法构建，则表明该问题是不可解的。证明此种问题不可解性的定理是算法理论中的一大突破，邱奇的算法即为该类算法的首例。邱奇从英国数学家阿兰·图灵的论文出发证明了基本几何问题的算法不可解性。同时证明了预演逻辑中真命题全集的解法问题是不可解的。

外部连接

http://www.cartage.org.lb/en/themes/Biographies/MainBiographies/C/Church/1.html category:美国数学家 ja:アロンゾ・チャーチ ko:알론조 처치

图灵

阿兰·麦席森·图灵（Alan Mathison Turing）），英国数学家、邏輯學家，他被視為计算机之父。 1931年图灵进入剑桥大学国王学院，毕业后到美国普林斯顿大学攻读博士学位，二战爆发后回到剑桥，后曾协助军方破解德国的著名密码系统Enigma，帮助盟军取得了二战的胜利。 图灵对于人工智能的发展有诸多贡献，例如图灵曾写过一篇名为《机器会思考吗？》（Can Machine Think?）的论文，其中提出了一种用于判定机器是否具有智能的试验方法，即图灵试验。至今，每年都有试验的比赛。 此外，图灵提出的著名的图灵机模型为现代计算机的逻辑工作方式奠定了基础。 图灵患有严重的花粉过敏症。

孩童和年轻时代

图灵的父亲Julius Mathison Turing是一名英属印度的公务员。图灵的母亲Ethel1911年在印度的Chatrapur怀了孕。他们希望艾伦在英国出生，所以回到伦敦，住在帕丁顿（Paddington）。结果就在那里诞下了艾伦。父亲的公务员委任使他在艾伦小时候经常来往于英伦和印度。由于对于英属殖民地安全的忧虑，他把家庭留在英伦与朋友同住。图灵很小的时候就表现出它的天才，后来就更加显著。他说他在三个星期里自己学会阅读，而且，就对数字和智力游戏着迷。 六岁的时候，他的父母为他在一间叫圣迈克尔的（St. Michael's）日间学校注了册。女校长很快就注意到他的天才，随后Marlborough学院的许多教育家也注意到这点。1926年，他十四岁的时候转到了在多尔瑟(Dorset)的Sherborne寄宿学校。开学的第一天，刚好遇上了大罢工。图灵决心要赶上第一天的课，于是他独自从南桑普敦（Southampton）骑了六十英里的自行车去上学，途中还在一间旅社度过一宵。 图灵天生对科学的喜好并没有给他在Sherborne的老师留下好印象。他们对教育的定义是着重于人文学科而不是科学。虽然如此，图灵继续在他喜欢的学科表现出惊人的能力。还没有学过基础微积分，他就能够解答在他当时年龄来说是很高深的难题。 1928年，图灵十八岁，開始閱讀阿尔伯特·爱因斯坦的著作。他不但能够理解，而且能够从一段并没有明示的文字里推导出爱因斯坦的运动定律。

大学和可计算性的工作

阿尔伯特·爱因斯坦 图灵不愿意如他在科学和数学方面一样地努力去学习人文学科，他的期终考试曾经几次不及格，因此，他不能进入他的第一志愿三一学院，而是去了剑桥大学国王学院。他在哈代指导下学习。哈代是很受尊敬的数学家。从1931年到1934年，他是当时剑桥一个数学研究和教学中心的Sadleirian讲座教授。图灵在1935年成为国王学院研究员。 图灵在他的重要论文《论可计算数及其在判定问题上的应用》（On Computable Numbers, with an Application to the Entscheidungsproblem）(1936年5月28日提交）里，对哥德尔1931年在证明和计算的限制的结果作了重新论述，他用现在叫做图灵机的简单形式裝置代替了哥德尔的以通用算术为基础的形式语言。由于速度很慢，尽管没有一台图灵机会有实际用途，图灵还是证明了这样的机器有能力解决任何可想像的数学难题，如果这些难题是用一种算法来表达。现今，图灵机还是计算理论研究的中心课题。他继续证明了判定问题（Entscheidungsproblem）是没有答案的。他的证明首先展示了图灵机的停机问题(halting problem)是没有答案的，这是说不可能用一个算法来决定一台指定的图灵机是否会停机。尽管他的证明比阿隆佐·邱奇在λ演算方面相等的证明晚发表了几个月，图灵的著作是更易于理解和直观的。 他的通用（图灵）机的概念也是新穎的。这一通用机能够完成任何其他机器所能做的任务。这篇论文还介绍了可定义数的概念。 图灵在普林斯顿大学度过了1937年和1938年的大部分时间，在邱奇指导下学习。1938年，他取得了博士学位。他的论文介绍了超计算（hypercomputation）的概念。这里，图灵机给加上了启示器，因而，可以用于研究不能用算法解答的问题。 1939年图灵回到剑桥，聆听了维特根斯坦关于数学基本原理（foundations of mathematics）的讲座。他们激烈地争论，图灵为形式主义辩护，而维根斯坦則认为把数学抬得太高而且不能发现任何绝对真理。

早期的计算机研究：图灵试验

形式主义 1945年到1948年，图灵在国家物理实验室，负责自动计算引擎(ACE)的工作 。1949年，他成为曼切斯特大学计算机实验室的副主任，负责最早的真正的计算机---曼切斯特一号的软件工作。在这段时间，他继续作一些比较抽象的研究，如“计算机械和智能”。图灵在对人工智能的研究中，提出了一个叫做图灵试验的实验，尝试定出一个决定机器是否有感觉的标准。 1952年，图灵写了一个国际象棋程序。可是，当时没有一台计算机有足够的运算能力去执行这个程序，他就模仿计算机，每走一步要用半小时。他与一位同事下了一盘，结果程序输了。後來美國新墨西哥州洛斯阿拉莫斯國家實驗室的研究群根據圖靈的理論，在MANIAC上設計出世界上第一個電腦程序的象棋。

图案形成和数理生物学的研究

从1952年直到去世，图灵一直在数理生物学方面做研究。他在1952年发表了一篇论文《形態發生的化学基础》(The Chemical Basis of Morphogenesis)。他主要的兴趣是斐波那契葉序列，存在于植物结构的斐波那契數。他应用了反应-扩散公式，现在已经成为图案形成范畴的核心。他后期的论文都没有发表，一直等到1992年《艾伦·图灵选集》出版，这些文章才见天日。

迫害和逝世

1992年 因为图灵的同性恋倾向而遭到的迫害使得他的职业生涯尽毁。1952年，他的同性伴侣协同一名同谋一起闯进了图灵的房子实施盗窃。图灵为此而报警。但是警方的调查结果使得他被控以“明显的猥亵和性颠倒行为”（请参看鸡奸法）。他没有申辩，并被定罪。在著名的公审后，他被给予了两个选择：坐牢或荷尔蒙疗法。他选择了荷尔蒙注射，并持续了一年。在这段时间里，药物产生了包括乳房不断发育的副作用。1954年，图灵因食用浸过氰化物溶液的苹果死亡。很多人相信他的死是有意的，并判决他的死是自杀。但是他的母亲极力争论他的死是意外，因为他在实验室里不小心堆放了很多化学物品。

参见


- 图灵奖
- 著名同性恋和双性恋者

外部链接


- [http://www-history.mcs.st-andrews.ac.uk/history/Mathematicians/Turing.html MacTutor biography of Turing]
- [http://www.turing.org.uk/bio/part1.html A short biography of Turing]
- [http://www.idsia.ch/~juergen/turing.html An even shorter bio]
- [http://www.systemtoolbox.com/article.php?history_id=3 Alan Turing - Towards a Digital Mind: Part 1]
- [http://www.loebner.net/Prizef/TuringArticle.html Computing machinery and intelligence] Full text of article.
- [http://episte.math.ntu.edu.tw/articles/sm/sm_30_11_2/index.html 謎樣的計算機科學之父] Turing Turing Turing ja:アラン・チューリング ko:앨런 튜링 simple:Alan Turing th:แอลัน ทัวริง

哥德尔不完备定理

在数理逻辑中，哥德尔不完备定理是库尔特·哥德尔于1930年证明并发表的两条定理。简单地说，第一条定理指出：
任何一个相容的数学形式化理论中，只要它强到足以在其中定义自然数的概念，就可以在其中构造在体系中既不能证明也不能否证的命题。
这条定理是在数学界以外最著名的定理之一，也是误解最多的定理之一。形式逻辑中有一条定理也同样容易被错误表述。有许多命题听起来很像是哥德尔不完备定理，但事实上是错误的。稍后我们可以看到一些对哥德尔定理的误解。 把第一条定理的证明过程在体系内部形式化后，哥德尔证明了他的第二条定理。该定理指出：
任何相容的形式体系不能用于证明它本身的相容性。
这个结果破坏了数学中一个称为希尔伯特计划的哲学企图。大卫·希尔伯特(David Hilbert)提出，象实分析那样较为复杂的体系的相容性，可以用较为简单的体系中的手段来证明。最终，全部数学的相容性可以归结为基本算术的相容性。但哥德尔的第二条定理证明了基本算术的相容性不能在自身内部证明，因此当然就不能用来证明比它更强的系统的相容性了。

哥德尔不完备定理的意义

哥德尔定理是一阶逻辑的定理，故最终只能在这个框架内理解。在形式逻辑中，数学命题及其证明都是用一种符号语言描述的，在这里我们可以机械地检查每个证明的合法性，于是便可以从一组公理开始无可辩驳地证明一条定理。理论上，这样的证明可以在电脑上检查，事实上这样的合法性检查程序也已经有了。 为了这个过程得以进行，我们需要知道手头有什么样的公理。我们可以从一组有限的公理集开始，例如欧几里德几何。或者更一般地，我们可以允许无穷的公理列表，只要能机械地判断给定的命题是否一条公理就行。在计算机科学里面，这被称为公理的递归集。尽管无穷的公理列表听起来有些奇怪，实际上自然数的的通常理论中，称为皮亚诺公理的就是这么一样东西。 哥德尔的第一条不完备定理表明任何一个允许定义自然数的体系必定是不完全的：它包含了既不能证明为真也不能证明为假的命题。 存在不完备的体系这一事实本身并不使人感到特别惊讶。例如，在欧几里德几何中，如果把平行公设去掉，就得到一个不完备的体系。不完备的体系可能只意味着尚未找出所有必须的公理而已。 但哥德尔揭示的是在多数情况下，例如在数论或者实分析中，你永远不能找出公理的完整集合。每一次你将一个命题作为公理加入，将总有另一个命题出现在你的研究范围之外。 你可以加入无穷条公理（例如，所有真命题）到公理列表中，但你得到的公理列表将不再是递归集。给出任意一条命题，将没有机械的方法判定它是否是系统的一条公理。如果给出一个证明，一般来说也无法检查它是否正确。 在计算机科学的语言中，哥德尔定理有另一种表述方式。在一阶逻辑中，定理是递归可枚举的：你可以编写一个可以枚举出其所有合法证明的程序。你可以问是否可以将结论加强为递归的：你可以编写一个在有限时间内判定命题真假的程序吗？根据哥德尔定理，答案是一般来说不能。 這理論用在人工智慧上，則指出有些道理可能是我們能夠判別，但機器單純用logic推斷卻無法得知的道理。

不确定命题的例子

在形式系统中出现不确定命题本身不是了不得的事。 之后哥德尔和保尔·科恩得出的一些结果结合起来就给出了不确定命题（既不能证明也不能否证的命题）的一个实际例子：选择公理和连续统假设都是集合论的标准公理系统内的不确定命题。这个结果与不完全性定理无关。 在1973年，群论中的怀特海问题被证明是集合论中的不确定命题。 1977年，Kirby、Paris和Harrington证明了组合论中的一个命题，拉姆赛理论的某个版本，在皮阿诺公理给出的算术公理系统中是不确定的，但可以在集合论的一个更大体系中证明为真。 在计算机科学中用到的Kruskal的树问题，也是在皮亚诺公理中不确定而在集合论中可证明的。 Goodstein定理是一个关于自然数的相对简单的命题，它在皮亚诺算术中是不确定的。 Gregory Chaitin在算法信息论中构造了一个不确定命题，但事实上他只是证明了他自己理论的不完备性。

对哥德尔定理的一些误解

由于哥德尔的第一条定理太有名了，对它的误解越来越多。我们举出一些例子： # 该定理并不意味着任何有趣的公理系统都是不完备的。例如，欧几里德几何可以被公理化为一个完备的系统。（事实上，欧几里德的原创公理集已经非常接近于完备的系统。所缺少的公理是非常直观的，以至于直到出现了形式化证明之后才注意到需要它们） # 该定理仅假设公理系统允许你定义自然数的集合。系统仅仅包含自然数是不够的。你也要能在系统中用公理和一阶逻辑表达“x是自然数”这样的概念。有许多系统包含自然数，却是完备的。例如，实数和复数都有完备的公理化系统。

讨论和推论

不完备性的结论影响了数学哲学以及形式化主义（使用形式符号描述原理）中的一些观点。我们可以将第一定理解释为“我们永远不能发现一个万能的公理系统能够证明一切数学真理，而不能证明任何谬误”
以下对第二定理的另一种说法甚至更令人不安：
如果一个公理系统可以用来证明它自身的相容性，那么它是不相容的。