一阶逻辑 二阶逻辑 类型论

一阶逻辑（First-order logic）是数学家、哲学家、语言学家使用的一种形式演绎系统。它有很多名字包括：一阶谓词演算、低等谓词演算、一阶逻辑的语言或谓词逻辑。不像自然语言如英语，FOL使用由数学结构来解释的完全无歧义的形式语言。一阶逻辑是通过允许在给定论域的个体上的量化而扩展命题逻辑的演绎系统。例如，在FOL中可陈述“所有个体都有性质P”。

命题逻辑处理简单的陈述性命题，一阶逻辑补充覆盖了谓词和量化。例如下列句子：“苏格拉底是男人”，“柏拉图是男人”。在命题逻辑中，它们是两个无关的命题，比如指示为p和q。但是在一阶逻辑中，这两个句子将由同一个性质联系起来：Man（x），这裡的Man（x）意味着x是个男人。在x = 苏格拉底时我们得到了第一个命题p，而在x = 柏拉图时我们得到了第二个命题q。这种构造在介入了量词的时候允许更加强力的逻辑，比如“对于所有x...”。例如，“对于所有x，如果Man（x）则...”。没有量词的话，所有在FOL中的有效论证在命题逻辑中也有效，反之亦然。

一阶理论构成自公理的集合（通常有限的或递归可枚举的）和给定底层可演绎性关系从它们可演绎出的那些陈述。“一阶理论”通常意味着某个公理集合和“与之在一起的完备（和可靠）的一阶逻辑公理化”，它闭合在FOL的规则之下。（对任何这种系统FOL将引出同样的抽象可演绎性关系，所以我们在头脑中不需要有固定的公理化系统。）一阶语言有足够的表达能力来形式化两个重要的数学理论：ZFC集合论和皮亚诺算术。但是一阶语言不能无条件的表达可数性的概念，即使它在一阶理论ZFC中在ZFC符号论的预期释义下是可表达的。这种想法可以用二阶逻辑无条件的表达。