---
title: "意味論"
module: FOL.Semantics
lang: ja
site: "Bedrock"
description: "意味論"
stage: "一階論理"
reading_order: 8
canonical: https://bedrock.institute/ja/FOL.Semantics.html
html: FOL.Semantics.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Semantics.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax]
routes: [common-foundations]
translations: [https://bedrock.institute/en/FOL.Semantics.md, https://bedrock.institute/zh/FOL.Semantics.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 意味論

対象言語は記号とその組み合わせの規則からなり、現時点で記号は何も表示しません。`∈̇` や `_≐_` を読めるようにするには、何を供給しなければならないのでしょうか。構造は、変数が何の上を動くかと、二つの原始的な述語がそこで何を意味するかを決めます。解釈は各定数記号に台の要素を割り当て、環境は利用できる各変数位置に現在の値を与えます。これらのデータが固定されると、構造的再帰によってすべての項に台の要素が、すべての論理式に命題が割り当てられます。本章を貫くのは、記号とその表示という一つの区別です。記号 `∈̇` は構文に属し、それが意味するようになるのは構造の関係 `∈ˢ` であり、両者は異なる層に住んでいます。

```agda
{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure )

module FOL.Semantics {ℓ} (𝒮 : ZFStructure ℓ) where
```

一つの構造 `𝒮 : ZFStructure ℓ` を固定します。これは前章のモデル論的データ、すなわち h-集合である台 `S` と、二つの台の要素を `hProp ℓ` の命題に送る等号 `≈ˢ` と所属 `∈ˢ` です。すべての論理式の解釈はこの同じ命題の宇宙に着地します。したがって集合についての主張は、文字どおり、証明を要素として持つ命題になります。これらのフィールド以外に、構造の内容は使いません。`ZFStructure` というレコード自体は集合論の公理を含まず、意味論の定義にも集合論の公理は要りません。

```agda
open import FOL.Syntax using
  ( Term; con; var
  ; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

open ZFStructure 𝒮
```

レコードのフィールドは今や固有の名前でスコープに入っています。`S` が台を、`∈ˢ` と `≈ˢ` が二つの関係を表し、したがって `x ∈ˢ y` は `x` と `y` についての構造の所属命題と読みます。対象言語の構成子もスコープにあり、各種の記号には意味論の側に明確な対応物があります。定数記号には台の要素が一つ必要であり、定数域から `S` への関数によって一度に固定されます。変数の位置には、使用のたびに変わりうる値が必要で、それを供給するのが環境です。原子論理式には二つの関係のいずれかが必要です。結合子と量化子には集合論はまったく要らず、「基礎語彙」の命題上の論理演算 `⊓`、`⊔`、`⇒`、`∀[ x ] P x`、`∃[ x ] P x` がそこに収まります。解釈は合成的です。項や論理式の意味は、その構成子と、直接の構成部分の意味から定まります。

## 環境

アリティ `n` の項は位置 `0` から `n - 1` までを参照でき、**環境** `γ` はその各位置に台の要素を一つ割り当てます。`S ^ 2` の環境には二つの成分があり、`var zero` と `var (suc zero)` が参照できますが、個々の項や論理式はその一方だけ、両方、あるいはどちらも使わないこともあります。したがって長さ `n` が定めるのは利用できる位置の範囲であって、実際に現れる変数の個数ではありません。束縛も同じ原理で働きます。量化子が台からの候補を取り上げるとき、環境はその要素を先頭に置いて拡張され、本体は位置 `zero` でそれを読みます。

環境の型は `S ^ n` と表記し、伝統的な上付きの $S^n$ に対応させます。`_^_` は「冪」と読みますが、単なる記法です。その定義は `Vec A n`、すなわち長さが型の一部になっている順序付きベクトルです。ここでは依存型が実際の仕事を担っています。論理式のアリティと環境の長さは食い違いようがなく、不一致ならそもそも正しい組み合わせが成立しません。演算 `lookup` は `Fin n` の位置にある成分を返し、`x ∷ γ` は先頭に一つ成分を付け加え、それまでの成分を後続の位置へ移します。

```agda
infixl 30 _^_

_^_ : ∀ {ℓ''} → Type ℓ'' → ℕ → Type ℓ''
A ^ n = Vec A n
```

## 評価と充足

意味論を運ぶのは二つの判断です。`⟦ t ⟧ γ` は項 `t` が環境 `γ` のもとで表示する台の要素を、`γ ⊨ φ` は論理式 `φ` が `γ` のもとで成立することを述べる命題を表します。どちらも固定された定数解釈 `ι : K → S` に対して定義されます。定数は `ι` から値を得て、変数は `γ` とともに変わり続けます。量化子が現れると、この分離がただちに効いてきます。束縛は変数の値を変えますが、定数記号の表示は変わりません。

解釈と環境は、互いに異なる二つの問いに答えます。定数 `con k` はどの環境を与えても `ι k` を表示し、変数 `var i` はどの解釈を固定しても `lookup i γ` を表示します。したがって環境が項の評価に関わるのは変数の場合だけで、定数記号の意味はつねに `ι` が固定します。この二つの場合で項の評価は尽くされます。

定数域 `K` と解釈 `ι : K → S` を固定します。この解釈のもとで、項の評価は項と環境を `S` の要素へ送り、充足関係は論理式と環境を命題へ送ります。充足関係は論理式の構造に沿って再帰的に定まります。原子式は構造の二つの関係を、結合子は「基礎語彙」の命題演算を、偽は空命題を用い、量化子は台の上を動きます。有界量化子では、限界の表示が、量化される要素の満たすべき所属条件を定めます。

```agda
module At {ℓc} (K : Type ℓc) (ι : K → S) where
```

この節を支えるのは二つの定義で、その型が何であるかを物語っています。評価 `⟦_⟧` は項と環境を台の要素へ写します。充足 `_⊨_` は環境と論理式を `hProp ℓ` の命題、すなわち任意の二要素が等しい型へ写します。そのような型の要素は証明です。したがって充足は単なる判定ではなく命題であり、定義は各式と各環境に対して、意味される命題がちょうどどれであるかを計算します。アリティ `n` は両方の型に現れるため、長さの合う環境だけが論理式に適用できます。論理式と環境の間の規律は、今や型そのものが強制します。

```agda
  ⟦_⟧ : ∀ {n} → Term K n → S ^ n → S
  ⟦ con k ⟧ γ = ι k
  ⟦ var i ⟧ γ = lookup i γ

  infix 6 _⊨_

  _⊨_ : ∀ {n} → S ^ n → Formula K n → hProp ℓ
```

原子的な所属は二つの項を評価し、それらを構造に渡します。主張は、二つの表示についての構造の所属命題になります。等号の原子は `≈ˢ` について同様です。ここで、点付きの記号がついに意味を持ちます。`∈̇` は `∈ˢ` として読まれ、構文より一つ下の層に降ります。命題的な三つの節は完全にホストの側にとどまります。連言は `⊓` で、選言は `⊔` で、含意は `⇒` で解釈され、いずれも命題上の演算です。連言の証明は証明の対であり、含意の証明は前件の証明を後件の証明へ変える関数です。この三つの節に集合論はまったく現れず、ホストの命題論理が部分公式の表示する命題に施されるだけです。

```agda
  γ ⊨ (t ∈̇ u)  = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
  γ ⊨ (t ≐ u)  = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ
  γ ⊨ (φ ∧̇ ψ)  = (γ ⊨ φ) ⊓ (γ ⊨ ψ)
  γ ⊨ (φ ∨̇ ψ)  = (γ ⊨ φ) ⊔ (γ ⊨ ψ)
  γ ⊨ (φ ⇒̇ ψ)  = (γ ⊨ φ) ⇒ (γ ⊨ ψ)
```

偽には環境は不要です。`⊥̇` は空命題 `⊥` として読まれます。量化子は、台がついに登場する場所です。非有界の `∃̇ φ` は台の上の存在量化を表します。すなわち、`S` のある要素 `x` が拡張環境 `x ∷ γ` のもとで本体を成立させる、という命題です。対になる `∀̇ φ` は全称量化を表し、その証明は各 `x : S` に `x ∷ γ` のもとでの本体の証明を割り当てる関数です。本体の内側では位置 `zero` が候補 `x` を保持し、`γ` の成分は後続の位置へ移っています。外側の論理式で自由だった変数は末尾から読まれます。命題的切り詰めにより、存在量化はそのような要素が存在することを記録するだけで、要素そのものをデータとして運びません。

有界の形はもう一つの成分を加えます。限界の表示への所属です。`∀̇∈ t φ` は、`⟦ t ⟧ γ` への所属が本体を含意することを要求します。したがって `⟦ t ⟧ γ` のすべての元が `φ` を満たします。`∃̇∈ t φ` は、元でありかつ本体を満たす要素を求めます。それぞれの環境がどこで使われるかに注意してください。限界 `t` は新しい束縛の外側にあり、元の `γ` で評価されます。拡張 `x ∷ γ` を見るのは本体だけです。この二つの節こそ、「`t` のすべての元が `φ` を満たす」「`t` のある元が `φ` を満たす」という読みの意味論的内容です。

```agda
  γ ⊨ ⊥̇        = ⊥
  γ ⊨ (∃̇ φ)    = ∃[ x ∶ S ] (x ∷ γ) ⊨ φ
  γ ⊨ (∀̇ φ)    = ∀[ x ∶ S ] (x ∷ γ) ⊨ φ
  γ ⊨ (∀̇∈ t φ) = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ φ)
  γ ⊨ (∃̇∈ t φ) = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ φ)
```

## まとめ

意味は合成的に与えられます。項は台の要素を表示し、それを決めるのは定数解釈と環境です。アリティ `n` の論理式は、利用できる位置を使い切るかどうかにかかわらず、`S ^ n → hProp ℓ` 型の関数を定めます。原子式は構造の二つの関係に問い合わせ、結合子はホストの命題演算を適用します。量化子は先頭に置かれた新しい位置を台の上に動かし、有界の形は拡張の外で限界の表示への所属を確かめ、拡張の内で本体を解釈します。どの節も構造的再帰の一段です。構成が使うのは台 `S` と二つの関係 `∈ˢ`、`≈ˢ` であり、証明 `isSetS` も集合論の公理も使いません。