形式陈述
给定一阶语言 公理库 一阶逻辑语法 First-order syntax 以符号表、项、原子公式、联结词和量词归纳生成一阶公式的语法系统。 L ,一个 L -结构 M 包含非空论域 M ,并对签名中的每个非逻辑符号指定解释:
常元 c 解释为元素 c M ∈ M 。
n 元函数符号 f 解释为全函数 公理库 函数 Function · Map · Mapping 由定义域、陪域和单值图共同组成,并把每个输入送到唯一输出的映射。 f M : M n → M 。
n 元关系符号 R 解释为有限元关系 公理库 关系 Relation · Binary relation 带源集与目标集的二元关系,其底层关系图是 A×B 的子集。 R M ⊆ M n 。
若等号属于逻辑符号,它必须解释为论域上的真实相等关系。常元也可统一看成零元函数:M 0 是只含空元组的单元素集合,从它到 M 的函数正好选出一个元素。
结构不为变量固定值;解释含变量的项与公式还需要变量赋值 公理库 变量赋值 Variable assignment 把每个变量映射到结构论域元素、供项求值与量词语义使用的函数。 s 。结构也不必满足任何尚未指定的公理。“L -结构”只要求符号解释类型正确;“理论 T 的模型”才要求满足 T 的全部公理。
直觉
语言给出可使用的名字和输入位置,结构为这些位置填入具体对象、运算与关系。函数符号 + 本身不携带普通加法的规律;把它解释为别的二元全函数仍得到合法结构,只是可能不再满足交换律等公理。
同一个论域可以配上不同结构,同一个语言也可以在不同论域上解释。因此比较两份公式的真假前,既要确认符号解释,也要确认量词究竟遍历哪些对象。符号的字形相同,并不意味着其数学含义已经固定。
例子与边界
在一个有限结构中完整求值
取语言 L = { c , f , R } ,其中 c 是常元,f 是一元函数符号,R 是二元关系符号。令
M = { 0 , 1 , 2 } , c M = 0 , f M ( a ) = a + 1 ( mod 3 ) , 并令 R M = { ( 0 , 1 ) , ( 1 , 2 ) , ( 2 , 0 ) } 。于是 f ( f ( c ) ) 的值是 2 ,R ( f ( c ) , f ( f ( c ) ) ) 为真,因为 ( 1 , 2 ) 在解释关系中。
句子 ∀ x R ( x , f ( x ) ) 为真:依次取 x = 0 , 1 , 2 ,得到关系中的三个有序对。句子 ∃ x f ( x ) = x 为假,因为三个输出分别为 1 , 2 , 0 ,没有不动点。若把同一语言中的 f 改为恒等函数,这个存在句就变真,说明真假随结构而变。
代数语言与关系语言
群语言使用常元 e 、二元乘法和一元逆元;任何群都给出这种语言的结构,但任意解释这些符号并不自动得到群。环语言中的 0 , 1 , + , ⋅ 可解释为整数、有限域或矩阵环的相应运算;若采用含一元负号的签名,还须给出它的解释。它们共享形成规则,却可能满足不同句子。
图语言只需二元关系 E ,但任意 E ⊆ M 2 可能带自环且不对称。若要简单无向图,还要加上 ∀ x ¬ E ( x , x ) 与 ∀ x ∀ y ( E ( x , y ) → E ( y , x ) ) 。序语言的 < 同理:结构定义并不强制它真的满足序公理。
全函数与非空论域
标准一阶函数解释必须处处有值且留在论域内。例如实数上的倒数在 0 无定义,不能原样解释一元函数符号;可改用二元关系表达 x y = 1 ,或明确定义零点的额外取值并在公理中限制非零输入。
本页采用非空论域。若有常元,空论域本来就无法解释它;即使语言没有常元,允许空结构也会改变量词规律,例如 ∀ x P ( x ) 可以空真而 ∃ x P ( x ) 为假。因此允许空结构是一项语义约定的变化。
推论与应用
结构与赋值共同决定满足关系 公理库 满足关系 Satisfaction relation · Tarski semantics 用对公式构造的递归定义刻画结构与赋值何时满足一阶公式。 :先递归求项值,再判断关系成员资格,最后处理联结词和量词。句子没有自由变量,所以最终真值不依赖赋值。
一阶理论 公理库 一阶理论 First-order theory 同一一阶语言中一组句子及其模型类所构成的理论。 筛选满足特定公理的结构。子结构、同构、初等嵌入和超积则比较或构造结构:其中同构要同时保留全部符号解释,初等嵌入还要求保持任意一阶公式的真假。这些不同层次不能仅由论域集合之间的函数替代。
Ehrenfeucht–Fraïssé 博弈 公理库 Ehrenfeucht–Fraïssé 博弈 Ehrenfeucht–Fraïssé games · Ehrenfeucht-Fraisse games · EF games 用有限轮部分同构博弈刻画有界量词秩的一阶不可区分性,并构造有限线性序的应答策略。 用有限轮选点比较两个结构:每轮只要求所选元组保持部分同构,却能精确刻画有界量词秩公式的真假一致。在纯序语言中,七点序和八点序虽不同构,应答者仍能赢三轮;差异是否可见,取决于允许的公式观察深度。
参考资料
Anand Pillay, Lecture Notes — Model Theory (Math 411) , University of Notre Dame, 2002,§1,pp.1–3 :单类与多类结构、函数关系解释、理论模型。
Jeremy Avigad, Robert Y. Lewis, Floris van Doorn, Logic and Proof , 在线版 3.18.4(访问于 2026),§§10.1–10.3 :解释、项求值、量词与论域。