一阶逻辑(First-Order Logic)

一阶逻辑(First-Order Logic)又称谓词逻辑,是数理逻辑中的核心形式系统。它在命题逻辑的基础上引入个体变量、谓词、函数以及全称与存在两个量词,使人们能够表达关于对象及其相互关系的一般性陈述,例如所有人都会死这类含量词的命题。

概述

一阶逻辑区分对象层面的个体与描述个体性质和关系的谓词。它只允许对个体变量使用量词,而不能对谓词或集合直接量化,这一限制正是一阶与更高阶逻辑的分界。凭借清晰的语法和语义,一阶逻辑成为形式化数学理论的标准框架,许多公理系统如集合论都在其中表述。

核心特点

• 量词:全称量词表示对所有个体成立,存在量词表示至少有一个个体成立。
• 语法与语义分离:语法给出合式公式的构造规则,语义通过解释与论域赋予真值。
• 可靠且完备:哥德尔完备性定理表明,一阶逻辑中语义有效的公式恰好都是可形式推导的。
• 半可判定:有效性问题是可枚举但不可判定的,这与丘奇和图灵关于判定问题的结果一致。

应用场景

一阶逻辑是数学基础的通用语言,几乎所有形式化数学都以它为底层框架。在计算机科学中,它用于形式规约、程序验证、数据库查询和知识表示;关系数据库的查询理论与关系演算就以一阶逻辑为基础。在人工智能中,它是经典知识表示与自动推理系统的核心工具。

常见问题

问:一阶逻辑和命题逻辑有何区别?答:命题逻辑只处理整体命题的真假组合,一阶逻辑则深入命题内部,能谈论个体、性质、关系并使用量词,表达力强得多。

问:为什么它是半可判定而非可判定?答:有效的公式总能被证明系统逐一枚举出来,但对于无效公式,没有算法能在有限步内一律判定,故整体不可判定。