一阶逻辑与完备性

一阶逻辑是关于对象和关系的量化陈述的形式语言，哥德尔完备性定理表明其证明系统精确地捕捉了在所有解释中都为真的语句。

Definition

一阶逻辑通过量词扩展了命题逻辑，这些量词涵盖了对象的域以及关系、函数和常量符号；完备性定理指出，一个语句当且仅当它是假定公理的逻辑推论时，才能在其证明系统中被推导出来。

Scope

本主题涵盖了一阶语言的语法、项、公式和语句，结构和满足度的语义，有效性和逻辑推论的概念，一阶逻辑的演绎系统，以及将可证明性与真理联系起来的可靠性和完备性定理。

Core questions

• 一阶逻辑的精确语法和语义是什么？
• 一个语句是某个理论的逻辑推论意味着什么？
• 为什么每个有效语句都是形式上可证明的？
• 完备性如何将证明系统与所有模型的类别联系起来？

Key theories

可靠性定理

证明系统中可推导出的每个语句在前提的所有模型中都为真，因此演绎系统从不证明错误的推论。

哥德尔完备性定理

反之，在理论的所有模型中都成立的每个语句都可以从该理论中推导出来，因此对于一阶逻辑而言，可证明性与逻辑推论是一致的。

亨金构造

通过直接从具有存在性语句见证的最大一致语句集构建模型来证明完备性，从而提供了一种构造模型的句法方法。

Clinical relevance

一阶逻辑是形式化数学理论的标准框架，完备性保证了所有模型共有的任何语义真理原则上都可以被证明，这为自动化定理证明和公理系统的基础充分性奠定了基础。

History

一阶逻辑起源于弗雷格的《概念文字》（Begriffsschrift），并由希尔伯特和阿克曼将其分离为一个独立的系统。哥德尔在他的1929年博士论文中证明了完备性，而亨金在1949年的构造则提供了一种使用最大一致集和存在性语句的见证的简化证明，这在今天已成为标准。

Key figures

• Gottlob Frege
• Kurt Goedel
• Leon Henkin
• Alfred Tarski

Seminal works

• enderton2001
• marker2002
• shoenfield1967

Frequently asked questions

完备性与哥德尔不完备性定理有何不同？

完备性是关于逻辑推论的：在理论的所有模型中为真的每个语句都是可证明的。不完备性是关于特定理论的：一个足够强的、一致的理论拥有在其预期模型中为真但无法证明的语句。两者关注不同的概念，并不冲突。

为什么一阶逻辑是标准选择？

它具有足够的表达力来形式化大多数数学，同时享有完备性和紧致性，而这些特性在二阶逻辑等更强的逻辑中则不成立。这种表达力与良好元理论性质之间的平衡使其成为默认的逻辑框架。