---
url: fol.semantics.evaluation
---

# 一阶逻辑 ▸ 语义 ▸ᐨ 取值的性质

这是一篇标题中带上标减号 (ᐨ) 的章节. 这表示这种章节不推荐线性阅读, 读者应该在需要时再回来查看. 因为这种章节只是一些枯燥引理的简单罗列, 而不包含动机的说明, 并且省去了大部分的自然语言证明. 读者应该在使用这些引理的章节中寻找动机, 并自行理解形式化的证明.

```agda
open import Foundation.Essential
open import FOL.Language.Base
module FOL.Semantics.EvaluationFacts (ℒ : Language) where

open import FOL.Syntax.Base ℒ
open import FOL.Semantics.Base ℒ
```

## 项取值的性质

**<u>引理</u>** 项的取值与替换的复合性质:
给变元替换表 `σ` 的值域中的项全部按赋值表 `𝓋` 取值, 得到一个新的赋值表 `𝓋 ⊨ₜ_ ∘ σ`, 用它对某项 `t` 取到的值等于先用 `σ` 替换 `t`, 再按 `𝓋` 取值.

**<u>证明</u>** 即证 `(𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ t ≡ 𝓋 ⊨ₜ t [ σ ]ₜ`. 使用项的结构归纳法.

当项是变元时, 简单化简可知两边相等. 当项是函数应用 `f $̇ t⃗` 时, 有归纳假设
`∀ t → t ∈⃗ t⃗ → (𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ t ≡ 𝓋 ⊨ₜ t [ σ ]ₜ`,

要证 `(𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ f $̇ t⃗ ≡ 𝓋 ⊨ₜ (f $̇ t⃗) [ σ ]ₜ`.

对两边化简, 等价于证
`fᴵ f ((𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ⃗ t⃗) ≡ fᴵ f (𝓋 ⊨ₜ⃗ t⃗ [ σ ]ₜ⃗)`.

用合同性 `cong` 同时消掉两边的 `fᴵ f`, 剩下的等式换成 `map⃗` 表达, 即证
`map⃗ ((𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ_) t⃗ ≡ map⃗ (𝓋 ⊨ₜ_) (map⃗ (_[ σ ]ₜ) t⃗)`.

由归纳假设可知上式的左边等于 `map⃗ (𝓋 ⊨ₜ_ ∘ _[ σ ]ₜ) t⃗`, 而这等于上式的右边. ∎

```agda
⊨ₜ-∘ : ⦃ _ : Interpretation D ⦄ →
  ∀ 𝓋 σ t → (𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ t ≡ 𝓋 ⊨ₜ t [ σ ]ₜ
⊨ₜ-∘ 𝓋 σ = term-elim (λ _ → refl) H where
  H : ∀ f t⃗ → (∀ t → t ∈⃗ t⃗ → (_⊨ₜ_ 𝓋 ∘ σ) ⊨ₜ t ≡ 𝓋 ⊨ₜ t [ σ ]ₜ) →
    (𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ f $̇ t⃗ ≡ 𝓋 ⊨ₜ (f $̇ t⃗) [ σ ]ₜ
  H f t⃗ IH = cong (fᴵ f) H2 where
    H2 : (𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ⃗ t⃗ ≡ 𝓋 ⊨ₜ⃗ t⃗ [ σ ]ₜ⃗
    H2 rewrite ⊨ₜ⃗≡map⃗ (𝓋 ⊨ₜ_ ∘ σ) t⃗ | ⊨ₜ⃗≡map⃗ 𝓋 (t⃗ [ σ ]ₜ⃗) | []ₜ⃗≡map⃗ t⃗ σ =
      map⃗ ((𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ_) t⃗       ≡⟨ map⃗-ext IH ⟩
      map⃗ (𝓋 ⊨ₜ_ ∘ _[ σ ]ₜ) t⃗       ≡⟨ map⃗-∘ _ _ _ ⟩
      map⃗ (𝓋 ⊨ₜ_) (map⃗ (_[ σ ]ₜ) t⃗) ∎
```

**<u>引理</u>** 赋值表插值与项提升的抵消性质:
往赋值表 `𝓋` 的头部插入任意对象 `x` 得到新赋值表 `x ∷ₙ 𝓋`, 在它之下, 提升后的项 `↑ₜ t` 的取值等于提升前的项 `t` 在 `𝓋` 下的取值.

**<u>证明</u>** 即证 `𝓋 ⊨ₜ t ≡ (x ∷ₙ 𝓋) ⊨ₜ ↑ₜ t`. 由 `↑ₜ` 的定义, 它即是替换 `# ∘ suc`. 由项的取值与替换的复合性质得证. ∎

```agda
∷ₙ⊨ₜ↑ₜ : ⦃ _ : Interpretation D ⦄ →
  ∀ (x : D) 𝓋 t → 𝓋 ⊨ₜ t ≡ (x ∷ₙ 𝓋) ⊨ₜ ↑ₜ t
∷ₙ⊨ₜ↑ₜ x 𝓋 t = ⊨ₜ-∘ (x ∷ₙ 𝓋) (# ∘ suc) t
```

**<u>引理</u>** 项取值的外延性:
如果赋值表 `𝓋` 和 `𝓊` 逐点相等, 那么 `𝓋 ⊨ₜ_` 和 `𝓊 ⊨ₜ_` 逐点相等.

**<u>证明</u>** 用项的结构归纳法. 当项是变元时显然成立. 当项是函数应用 `f $̇ t⃗` 时, 有归纳假设
`∀ t → t ∈⃗ t⃗ → 𝓋 ⊨ₜ t ≡ 𝓊 ⊨ₜ t`,

要证 `𝓋 ⊨ₜ (f $̇ t⃗) ≡ 𝓊 ⊨ₜ (f $̇ t⃗)`.

化简并换成 `map⃗` 表达, 即证
`fᴵ f (map⃗ (𝓋 ⊨ₜ_) t⃗) ≡ fᴵ f (map⃗ (𝓊 ⊨ₜ_) t⃗)`.

由 `cong` 和归纳假设得证. ∎

```agda
⊨ₜ-ext : ⦃ _ : Interpretation D ⦄ →
  ∀ {𝓋 𝓊} → 𝓋 ≗ 𝓊 → 𝓋 ⊨ₜ_ ≗ 𝓊 ⊨ₜ_
⊨ₜ-ext {𝓋} {𝓊} eq = term-elim eq H where
  H : ∀ f t⃗ → (∀ t → t ∈⃗ t⃗ → 𝓋 ⊨ₜ t ≡ 𝓊 ⊨ₜ t) → 𝓋 ⊨ₜ (f $̇ t⃗) ≡ 𝓊 ⊨ₜ (f $̇ t⃗)
  H f t⃗ IH rewrite ⊨ₜ⃗≡map⃗ 𝓋 t⃗ | ⊨ₜ⃗≡map⃗ 𝓊 t⃗ = cong (fᴵ f) (map⃗-ext IH)
```

## 公式取值的性质

**<u>引理</u>** 公式取值的外延性:
如果赋值表 `𝓋` 和 `𝓊` 逐点相等, 那么对任意公式 `φ` 都有 `𝓋 ⊨ᵩ φ ↔ 𝓊 ⊨ᵩ φ`.

**<u>证明</u>** 对公式的结构归纳.

- 当公式是恒假 `⊥̇` 时:
    显然成立.
- 当公式是关系应用 `R $̇ t⃗` 时:
    要证 `Rᴵ R (map⃗ (𝓋 ⊨ₜ_) t⃗) holds ↔ Rᴵ R (map⃗ (𝓊 ⊨ₜ_) t⃗) holds`.
    由项取值的外延性, `𝓋 ⊨ₜ_` 和 `𝓊 ⊨ₜ_` 逐点相等, 所以 `map⃗ (𝓋 ⊨ₜ_) t⃗` 与 `map⃗ (𝓊 ⊨ₜ_) t⃗` 相等.
    由关于逻辑等价的合同性即证.
- 当公式是蕴含式 `φ →̇ ψ` 时:
    有归纳假设 `𝓋 ⊨ᵩ φ ↔ 𝓊 ⊨ᵩ φ` 以及 `𝓋 ⊨ᵩ ψ ↔ 𝓊 ⊨ᵩ ψ`,
    要证 `(𝓋 ⊨ᵩ φ → 𝓋 ⊨ᵩ ψ) ↔ (𝓊 ⊨ᵩ φ → 𝓊 ⊨ᵩ ψ)`.
    由归纳假设配合简单的命题逻辑推理即证.
- 当公式是全称量化式 `∀̇ φ` 时:
    要证 `(∀ x → (x ∷ₙ 𝓋) ⊨ᵩ φ) ↔ (∀ x → (x ∷ₙ 𝓊) ⊨ᵩ φ)`,
    只需证 `∀ x → (x ∷ₙ 𝓋) ⊨ᵩ φ ↔ (x ∷ₙ 𝓊) ⊨ᵩ φ`.
    递归使用本引理, 只需证 `x ∷ₙ 𝓋` 与 `x ∷ₙ 𝓊` 逐点相等.
    由于 `𝓋` 和 `𝓊` 逐点相等, 所以分别插入 `x` 后也逐点相等. ∎

```agda
⊨ᵩ-ext : ⦃ _ : Interpretation D ⦄ →
  ∀ {𝓋 𝓊} → 𝓋 ≗ 𝓊 → ∀ φ → 𝓋 ⊨ᵩ φ ↔ 𝓊 ⊨ᵩ φ
⊨ᵩ-ext eq ⊥̇ = ↔-refl
⊨ᵩ-ext eq (R $̇ t⃗) = ↔-cong (λ t → Rᴵ R t holds) (map⃗-cong (⊨ₜ-ext eq) t⃗)
⊨ᵩ-ext eq (φ →̇ ψ) = ↔-cong-→ (⊨ᵩ-ext eq φ) (⊨ᵩ-ext eq ψ)
⊨ᵩ-ext {𝓋} {𝓊} eq (∀̇ φ) = ↔-cong-Π λ x → ⊨ᵩ-ext (H x) φ where
  H : ∀ x → x ∷ₙ 𝓋 ≗ x ∷ₙ 𝓊
  H x zero = refl
  H x (suc n) = eq n
```

**<u>引理</u>** 公式的取值与替换的复合性质:
给变元替换表 `σ` 的值域中的项全部按赋值表 `𝓋` 取值, 得到一个新的赋值表 `𝓋 ⊨ₜ_ ∘ σ`, 用它对某公式 `φ` 取值等于先用 `σ` 替换 `φ`, 再按 `𝓋` 取值.

**<u>证明</u>** 对公式的结构归纳.

- 当公式是恒假 `⊥̇` 时:
    显然成立.
- 当公式是关系应用 `R $̇ t⃗` 时:
    与引理 `⊨ₜ-∘` 中函数应用 `f $̇ t⃗` 情况类似的方法可证.
- 当公式是蕴含式 `φ →̇ ψ` 时:
    与引理 `⊨ᵩ-ext` 中蕴含式的情况类似的方法可证.
- 当公式是全称量化式 `∀̇ φ` 时:
    留作练习. ∎

```agda
⊨ᵩ-∘ : ⦃ _ : Interpretation D ⦄ →
  ∀ 𝓋 φ σ → (𝓋 ⊨ₜ_ ∘ σ) ⊨ᵩ φ ↔ 𝓋 ⊨ᵩ φ [ σ ]ᵩ
⊨ᵩ-∘ 𝓋 ⊥̇ σ = ↔-refl
⊨ᵩ-∘ 𝓋 (R $̇ t⃗) σ = ↔-cong (λ t → Rᴵ R t holds) H where
  H = map⃗ ((𝓋 ⊨ₜ_ ∘ σ) ⊨ₜ_) t⃗       ≡⟨ map⃗-cong (⊨ₜ-∘ 𝓋 σ) t⃗ ⟩
      map⃗ (𝓋 ⊨ₜ_ ∘ _[ σ ]ₜ) t⃗       ≡⟨ map⃗-∘ _ _ _ ⟩
      map⃗ (𝓋 ⊨ₜ_) (map⃗ (_[ σ ]ₜ) t⃗) ∎
⊨ᵩ-∘ 𝓋 (φ →̇ ψ) σ = ↔-cong-→ (⊨ᵩ-∘ 𝓋 φ σ) (⊨ᵩ-∘ 𝓋 ψ σ)
⊨ᵩ-∘ 𝓋 (∀̇ φ) σ = ↔-cong-Π λ x →
  (x ∷ₙ (𝓋 ⊨ₜ_) ∘ σ) ⊨ᵩ φ               ↔⟨ ⊨ᵩ-ext (H x) φ ⟩
  ((x ∷ₙ 𝓋) ⊨ₜ_ ∘ (# 0 ∷ₙ ↑ₜ ∘ σ)) ⊨ᵩ φ ↔⟨ ⊨ᵩ-∘ (x ∷ₙ 𝓋) φ (# 0 ∷ₙ ↑ₜ ∘ σ) ⟩
  (x ∷ₙ 𝓋) ⊨ᵩ φ [ # 0 ∷ₙ ↑ₜ ∘ σ ]ᵩ      ↔∎
  where
  H : ∀ x → x ∷ₙ (𝓋 ⊨ₜ_) ∘ σ ≗ (x ∷ₙ 𝓋) ⊨ₜ_ ∘ (# 0 ∷ₙ ↑ₜ ∘ σ)
  H x zero = refl
  H x (suc n) = ∷ₙ⊨ₜ↑ₜ x 𝓋 (σ n)
```

**<u>引理</u>** 赋值表插值与公式提升的抵消性质:
往赋值表 `𝓋` 的头部插入任意对象 `x` 得到新赋值表 `x ∷ₙ 𝓋`, 在它之下, 提升后的公式 `↑ φ` 的取值等于提升前的公式 `φ` 在 `𝓋` 下的取值.

**<u>证明</u>** 即证 `𝓋 ⊨ᵩ φ ↔ (x ∷ₙ 𝓋) ⊨ᵩ ↑ φ`. 由 `↑` 的定义, 它即是替换 `# 0 ∘ suc`. 由公式的取值与替换的复合性质得证. ∎

```agda
∷ₙ⊨ᵩ↑ : ⦃ _ : Interpretation D ⦄ →
  ∀ (x : D) 𝓋 φ → 𝓋 ⊨ᵩ φ ↔ (x ∷ₙ 𝓋) ⊨ᵩ ↑ φ
∷ₙ⊨ᵩ↑ x 𝓋 φ = ⊨ᵩ-∘ (x ∷ₙ 𝓋) φ (# ∘ suc)
```

**<u>引理</u>** 公式应用的取值:
如果在头部插入了项 `t` 取值的赋值表 `𝓋 ⊨ₜ t ∷ₙ 𝓋` 下公式 `φ` 的取值成立, 那么在 `𝓋` 下公式应用 `φ [ t ]₀` 的取值也成立.

**<u>证明</u>** 由公式取值的外延性, 前提 `(𝓋 ⊨ₜ t ∷ₙ 𝓋) ⊨ᵩ φ` 可转化为 `(𝓋 ⊨ₜ_ ∘ (t ∷ₙ #)) ⊨ᵩ φ`, 再用公式的取值与替换的复合性质即得 `𝓋 ⊨ᵩ φ [ t ]₀`. ∎

```agda
φ[t]-intro : ⦃ _ : Interpretation D ⦄ →
  ∀ 𝓋 φ t → (𝓋 ⊨ₜ t ∷ₙ 𝓋) ⊨ᵩ φ → 𝓋 ⊨ᵩ φ [ t ]₀
φ[t]-intro 𝓋 φ t H = ⊨ᵩ-∘ 𝓋 φ (t ∷ₙ #) .⇒ H2 where
    H2 : (𝓋 ⊨ₜ_ ∘ (t ∷ₙ #)) ⊨ᵩ φ
    H2 = ⊨ᵩ-ext eq φ .⇒ H where
      eq : ∀ n → (𝓋 ⊨ₜ t ∷ₙ 𝓋) n ≡ 𝓋 ⊨ₜ (t ∷ₙ #) n
      eq zero = refl
      eq (suc n) = refl
```

## 有效性的性质

**<u>引理</u>** 有效性的结合:
有效的 `φ` 与有效的 `Γ` 可以结合成有效的 `φ ∷ Γ`.

**<u>证明</u>** 即证 `𝓋 ⊨ᵩ φ → 𝓋 ⊨͆ᵩ Γ → 𝓋 ⊨͆ᵩ (φ ∷ Γ)`. 其中 `𝓋 ⊨͆ᵩ φ ∷ Γ` 又可以展开为 `∀ ξ → ξ ∈͆ φ ∷ Γ → 𝓋 ⊨ᵩ ξ`. 讨论 `ξ ∈͆ φ ∷ Γ`.

- 当 `ξ` 等于 `φ` 时, 由前提即证.
- 当 `ξ` 是 `Γ` 中的元素时, 由 `𝓋 ⊨͆ᵩ Γ` 即证. ∎

```agda
_⊨∷_ : ⦃ _ : Interpretation D ⦄ →
  ∀ {𝓋 φ Γ} → 𝓋 ⊨ᵩ φ → 𝓋 ⊨͆ᵩ Γ → 𝓋 ⊨͆ᵩ (φ ∷ Γ)
(𝓋⊨φ ⊨∷ 𝓋⊨Γ) φ (here refl) = 𝓋⊨φ
(𝓋⊨φ ⊨∷ 𝓋⊨Γ) ξ (there ξ∈Γ) = 𝓋⊨Γ ξ ξ∈Γ
```

---
> 知识共享许可协议: [CC-BY-NC-SA 4.0](https://creativecommons.org/licenses/by-nc-sa/4.0/deed.zh)  
> [GitHub](https://github.com/choukh/MetaLogic/blob/main/src/FOL/Semantics/EvaluationFacts.lagda.md) | [GitHub Pages](https://choukh.github.io/MetaLogic/FOL.Semantics.EvaluationFacts.html) | [语雀](https://www.yuque.com/ocau/metalogic/fol.semantics.evaluation)  
> 交流Q群: 893531731
