Structurae & Interpretationes 结构与解释
〔定义 2.1〕:
设 S 为符号集,S–结构(S-structure)是具有下述性质的二元组 A=(A,a):
(α) A 是非空集合,称为 A 的论域(domain)或全集(universe);
(β) a 是定义于 S 的映射,满足以下条件:
(1) 对任一 n 元关系符号 R∈S,a(R) 为 A 上的 n 元关系;
(2) 对任一 n 元函数符号 f∈S,a(f) 为 A 上的 n 元函数;
(3) 对任一常元 c∈S,a(c) 为 A 的元素.
后文将 a(R),a(f),a(c) 分别记为 RA,fA,cA 或 RA,fA,cA.结构 A,B,⋯ 的论域相应地记作 A,B,⋯.结构 A=(A,a) 中的映射 a 将会写成符号集中对应符号的值列表,如 {R,f,c}–结构记作 A=(A,RA,fA,cA).
〔定义 2.2〕:
设 A 为 S–结构,映射 β:{vn∣n∈N}→A 将变元映射为 A 中的元素,称为 A 的一个赋值(assignment).
S–解释(interpretation)I 是指含有一个 S–结构 A 与其中的一个赋值 β 的二元组 (A,β) .
若 β 是 A 的一个赋值,a∈A 且 x 为变元,则 βax 表示将 x 映射为 a,而将与 x 相异的元素如同 β 一样映射的赋值,即
βax(y):={a,y=x,β(y),otw.对于 I=(A,β),记 Iax=(Aax,β).
Relatio Satisfactionis Consequentiaeque 满足关系与推论关系
〔定义 2.3〕:
定义 I=(A,β) 为 S–解释,函数 I(t) 将每个项 t 映射为 A 的元素,即
(α) 对变元 v,I(v):=β(v);(β) 对常元 c,I(c):=cA;
(γ) 对 n 元函数符号 f∈S,以及项 t1,⋯,tn,I(ft1⋯tn)=fA(I(t1),⋯,I(tn)).
对公式 φ 归纳,可如下定义关系「I 是 φ 的模型(model)」,其中 I 是任意的解释.「I 是 φ 的模型」可以等价地称为「I 满足(satisfies)φ」或「φ 在 I 中成立(holds)」,并记作 I⊨φ.
〔定义 2.4〕:
I⊨t1≡t2:iffI(t1)=I(t2)I⊨Rt1⋯tn:iffRAI(t1)⋯I(tn)I⊨¬φ:iffI⊨φ不成立I⊨(φ∧ψ):iffI⊨φ且I⊨ψI⊨(φ∨ψ):iffI⊨φ或I⊨ψI⊨(φ→ψ):iff若I⊨φ则I⊨ψI⊨(φ↔ψ):iffI⊨φ当且仅当I⊨ψI⊨∀xφ:iff对所有a∈A,Iax⊨φI⊨∃xφ:iff存在a∈A使得Iax⊨φ
易知,I⊨φ 当且仅当 φ 在 I 解释下为真命题.
对于 S–公式集合 Φ,若对任意 φ∈Φ,均有 I⊨φ,则称 I 是 Φ 的模型(I 满足 Φ),并记作 I⊨Φ.
〔定义 2.5〕:
令 Φ 为公式集合,φ 为公式.φ 是 Φ 的推论(consequence),当且仅当满足 Φ 的所有解释亦满足 φ,记作 Φ⊨φ.
设 ψ 为公式,{ψ}⊨φ 简记作 ψ⊨φ.
〔定义 2.6〕:
公式 φ 是有效的(valid),当且仅当 ∅⊨φ,记作 ⊨φ.因此公式有效当且仅当其在所有解释下均成立.
公式 φ 是可满足的(satisfiable),当且仅当存在满足 φ 的解释,记作 Satφ.公式集合 Φ 是可满足的,当且仅当对于任意 φ∈Φ,均有 Satφ,记作 SatΦ.
〔引理 2.a〕:
对于任意公式集合 Φ 及任意公式 φ,Φ⊨φ 当且仅当 SatΦ∪{¬φ} 不成立.
特别地,φ 有效当且仅当 {¬φ} 不可满足.
〔证明〕:
Φ⊨φ
当且仅当所有满足 Φ 的解释亦满足 φ,
当且仅当不存在满足 Φ 而不满足 φ 的解释,
当且仅当不存在满足 Φ∪{¬φ} 的解释,
当且仅当 SatΦ∪{¬φ} 不成立.
■