形式陈述

一阶语言由关系符号、函数符号、常量、变量、逻辑联结词以及量词 $\forall,\exists$$\mathrm{\forall },\mathrm{\exists }$ 组成。一个结构 $\mathcal M$$\mathcal{M}$ 给出论域并解释非逻辑符号；赋值确定变量后，满足关系写作 $\mathcal M\models\varphi$$\mathcal{M}\models \phi$。

直觉

命题逻辑把句子看成不可拆分的真假块；一阶逻辑可以进入句子内部，讨论对象及其关系，例如“每个节点都有一条出边”。

例子与边界

$\forall x\,\exists y\,(x<y)$$\mathrm{\forall }x\mathrm{\exists }y(x<y)$ 表示没有最大元素。一阶逻辑只能量化论域中的对象，不能直接量化所有子集或关系；后者属于二阶逻辑。

推论与应用

群、序、图和集合论都可用一阶语言公理化；数据库查询、程序验证与 SMT 求解也大量使用其片段。

参考资料

• Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Chapter 2.
• Wilfrid Hodges, A Shorter Model Theory, Chapter 1.