---
title: "集合の定義可能な部分集合"
module: L.Definability
lang: ja
site: "Bedrock"
description: "集合の定義可能な部分集合"
stage: "構成可能段階と公理"
reading_order: 24
canonical: https://bedrock.institute/ja/L.Definability.html
html: L.Definability.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Definability.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, V.Hierarchy, V.Smallness]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.Definability.md, https://bedrock.institute/zh/L.Definability.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 集合の定義可能な部分集合

集合 `A` に対して、演算子 `Def A` は、`A` 上の制限構造における一階論理式と `A` の有限個のパラメータで定義される `A` の部分集合をちょうど集めます。その所属定理は、後の構成可能性の議論で使う論理式、環境、充足関係を取り出します。

本章を支える設計上の要点が二つあります。第一に、論理式は `A` の小さな要素型 `⟪ A ⟫` を定数域として取るので、「`A` からのパラメータ」が型そのものによって強制されます。第二に、充足は制限構造 `𝒮ᵥ ↾ (∈ A)` 上の**内側**の意味論で読まれ、量化子の範囲は `A` の要素だけに限られます。これが教科書で「`(A, ∈)` **の中で**定義可能」と言う意味であり、前の章々の本質的小ささがここで効きます。すべての論理式の評価は小さな型になるので、`Def A` は集合であり、レベルの引き下げは一切不要です。

この章の問いは次のものです。集合 `A` に対して、一階の論理式を `(A, ∈)` の中で解釈したとき、どの部分集合が取り出せるでしょうか。答えは一つの演算子 `Def A` に集められ、それ自体が周囲の階層の集合になります。すべては一つの宇宙レベル ℓ を固定して行われ、これにより `Def A` は `A` と同じレベルの集合として存在できる大きさを保ちます。

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

open import Base.Prelude

module L.Definability {ℓ : Level} where

open import FOL.ZFStructure using ( ZFStructure; Transitive )
```

論理式は帰納的な対象言語から来ます。`Formula K n` は、定数が型 `K` で添字づけられ、自由変数の `n` 個のスロットを持ち、原子論理式は構造の所属と等号の関係から組み立てられます。`K = ⟪ A ⟫`、つまり `A` の小さな要素型を選べば、「`A` からのパラメータ」は構成そのものによって成り立ちます。すべての定数は `A` の要素を名指すからです。有界断片 `Δ₀` は、充足の内側と外側の読みを比べる際に後で効きます。定数の対応付けと改名は、論理式を定数域の間で移し、その移動に沿って充足を輸送する操作です。

```agda
open import FOL.Syntax using ( Formula; var; con; _∈̇_; ⊤̇ )
open import FOL.LevyHierarchy using ( Δ₀ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
open import FOL.Manipulation.Relabelling using ( mapΔ₀; ⊨-map )
import FOL.Absoluteness
```

「`(A, ∈)` **の中で**定義可能」とは、量化子が `A` の要素の上だけで動くことを意味します。したがって充足は、クラス `x ↦ x ∈ˢ A` に制限した構造で取られなければならず、周囲の階層で取るのではありません。この章はレベル ℓ の階層が担う周囲の構造 `𝒮ᵥ` の上で作業します。台は `S`、所属は `∈ₛ` です。`A` への制限と制限された世界の小ささは小ささの章から来ます。クラス、制限された台と同値な小さな型、定数の解釈を与えると、制限された構造を組み立て直し、そこではすべての論理式が小さな命題に評価されることを証明します。ここでの制限のクラスは「`A` への所属」そのものです。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Smallness {ℓ} using ( module InnerSmall )

open import Cubical.Foundations.Equiv
  using ( _≃_; equivFun; invEq; invEquiv; compEquiv; propBiimpl→Equiv )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
```

本質的小ささこそが、充足を集合の添字にできる根拠です。各論理式は `(A, ∈)` の中で**小さな**命題に評価されるので、式を満たす `A` の要素は小さな型で添字づけられ、階層の構成子 `sett` が小さな索引型と索引写像から集合を作ります。一つの論理式が定義する部分集合も `Def` 自身も、この方法で構成されます。すると `sett` の所属は切断された存在の命題にすぎず、命題値の目標に向かうとき切断は命題へ消去されるだけで、選ばれた証人は得られません。構成のこの形が、本章の経路に基づく仕様を生みます。

```agda
open import Cubical.Data.Sigma using ( Σ-cong-equiv-snd )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( sett )
```

最後に、真理値の語彙です。結合子と量化子は `hProp (ℓ-suc ℓ)` の命題に直接作用するので、充足は `hProp (ℓ-suc ℓ)` に値を取ります。`⟨ p ⟩` は `hProp` の根底にある命題を取り出します。この種の命題の相等は経路なので、所属についての仕様は命題としての経路で述べられ、経路の連結によって証明されます。これが整えば、次の節は一つの集合 `A` を固定し、その定義可能部分集合を定義します。

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber; presentation
        ; isEmb⟪_⟫↪; _⊆_; extensionality )

open ZFStructure 𝒮ᵥ
```

## 演算子

以下のすべては一つの集合 `A` に相対的 so、本節はモジュール `DefOf A` の中で進みます。制限のクラスは「`A` への所属」であり、本質的小ささの証人 `e` はライブラリの `presentation` です。小さな要素型 `⟪ A ⟫` は、同値の違いを除いて、制限された台そのものです (小さい方の所属を点ごとに大きい方へ置き換えるだけです)。定数の解釈 `ι` は、定数つまり `⟪ A ⟫` の添字を、制限された台の対応する要素へ送ります。その第一成分は定義上、その要素そのものです。

クラス `M` は各集合 `x` に命題 `x ∈ˢ A` を割り当てるので、制限された台 `Σ[ x ∈ S ] (x ∈ᶜ M)` は要素ごとに、`A` の要素と「それが要素である証拠」の対です。同値 `e` はこの台が本質的に小さいことを示します。第一因子は `presentation A` の逆で、索引写像のファイバーに「だけ」落ちている `A` の要素を `⟪ A ⟫` の添字と同一視します。第二因子は各 `v` について、小さい方の所属 `v ∈ₛ A` と大きい方の所属 `v ∈ˢ A` を両方向に変換します。これらは命題なので、点ごとの変換は正当です。

```agda
module DefOf (A : S) where

  M : S → hProp (ℓ-suc ℓ)
  M x = x ∈ˢ A

  e : ⟪ A ⟫ ≃ (Σ[ x ∈ S ] (x ∈ᶜ M))
  e = compEquiv (invEquiv (presentation A))
```

定数の解釈 `ι` は、同値 `e` を関数として読んだものにすぎません。論理式の定数域は `⟪ A ⟫` 自身になるので、言語の定数とは `A` の要素への添字であり、`ι` はそれを制限された台へ復号します。`ι m` の第一射影は定義上、基礎となる集合 `⟪ A ⟫↪ m` であり、所属の証明はこの事実をそのまま使います。

```agda
        (Σ-cong-equiv-snd (λ v →
          propBiimpl→Equiv (snd (v ∈ₛ A)) (snd (v ∈ˢ A))
            (∈∈ₛ {a = v} {b = A} .snd) (∈∈ₛ {a = v} {b = A} .fst)))

  ι : ⟪ A ⟫ → Σ[ x ∈ S ] (x ∈ᶜ M)
  ι = equivFun e
```

このデータに対して `InnerSmall` を開くと、世界が組み立て直されます。「`A` への所属」に制限した構造 `𝒮M`、その充足関係 `⊨ᵐ`、そして `⟪ A ⟫` 上のすべての論理式が小さな命題に評価されるという定理 `⊨ᵐ-small` です。public に開くことで、後の章は内側の充足をまさにこれらの名前で読みます。以降、「充足する」とは常にこの内側の関係を指し、量化子は `A` の要素に限られます。

```agda
  open InnerSmall M ⟪ A ⟫ e {K = ⟪ A ⟫} ι public
```

内側の充足 `⊨ᵐ` とその小ささが手に入れば、演算子は直接定義できます。`smallSat φ m` はメンバー `m` における `φ` の真理値で、一つ下の宇宙に住みます。`defSet φ` は `φ` が `A` から定義する部分集合で、`φ` が選ぶ要素たちの上の `sett` です。そして `Def A` はそれら全体の集まりで、論理式そのものを添字とします。論理式は `Type ℓ` の帰納的データなので、正当な小さな添字です。これこそ**構文を索引集合として使う**という発想です。

圧縮 `smallSat` は二段階の評価をまとめます。`⊨ᵐ-small φ (ι m ∷ [])` は対で、第一成分は内側の充足の命題と同値な小さな命題、第二成分がその同値です。環境 `ι m ∷ []` の項目が一つなのは、`φ` の自由変数のスロットが一つで、それを要素 `m` が `ι` を通じて埋めるからです。それとは独立に、`φ` に現れる任意の定数は定数の解釈 `ι` を通して解釈されるので、`A` のどんな要素でも名指せます。パラメータは定数を通じて入り、変数の項は単一の自由スロットをどこで評価するかを固定するだけです。根底の命題 `⟨ smallSat φ m ⟩` は、`φ` が `(A, ∈)` の中で `m` において成り立つことを、`sett` の添字に適した小さな形で言います。

```agda
  smallSat : Formula ⟪ A ⟫ 1 → ⟪ A ⟫ → hProp ℓ
  smallSat φ m = ⊨ᵐ-small φ (ι m ∷ []) .fst

  defSet : Formula ⟪ A ⟫ 1 → S
  defSet φ = sett (Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩) (λ p → ⟪ A ⟫↪ (p .fst))

  Def : S
```

定義可能部分集合 `defSet φ` は、索引型 `Σ[ m ∈ ⟪ A ⟫ ] ⟨ smallSat φ m ⟩` で提示されます。索引とはメンバー `m` と「`φ` が `m` で成り立つ」ことの証明の対であり、索引写像はその対を集合 `⟪ A ⟫↪ m` へ送ります。切断の規律に注意してください。証明の成分は証明であって選ばれたデータではなく、`defSet φ` の所属はそのような証明が「だけ」存在することを要求します。最後に `Def` は同じ構成を一段上で繰り返し、論理式そのものを索引族とします。各索引はある `defSet φ` に「だけ」ヒットします。論理式は `Type ℓ` に住むので索引型は小さく、結果は再び階層の集合になります。

```agda
  Def = sett (Formula ⟪ A ⟫ 1) defSet
```

## 所属の特徴付け

`Def` も各 `defSet φ` も `sett` で構成されるので、その所属は**定義上**「索引族にだけヒットすること」を意味します。`Def` については証明はまったく不要です。`Def` の要素はある `defSet φ` である「だけ」だからです。定義可能部分集合には二つの仕様があります。その要素は `A` の中にとどまること、そして要素 `⟪ A ⟫↪ m` が `defSet φ` に属するのは**内側の世界が `m` で `φ` を充足するときちょうどそのときに限る**ことです。これが文字どおり「定義可能部分集合」の意味であり、圧縮 `smallSat` は符号化にすぎず、同値がそれを保ちます。

第一の仕様は、各 `defSet φ` が `A` に含まれると言います。`defSet φ` の要素は、ある証明付きの索引 `(m , _)` から「だけ」来ており、索引付けされた集合を `y` と同一視する経路 `q` を伴います。`A` への所属は命題なので、切断は命題へ消去できます。その証明が既知の事実 `⟪ A ⟫↪ m ∈ˢ A` を `q` に沿って輸送し、`y ∈ˢ A` を得ます。既知の事実そのものは、小さい方の所属 `⟪ A ⟫↪ m ∈ₛ A` を `∈∈ₛ` を通して変換したものです。

```agda
  defSet⊆A : (φ : Formula ⟪ A ⟫ 1) (y : S) → ⟨ y ∈ˢ defSet φ ⟩ → ⟨ y ∈ˢ A ⟩
  defSet⊆A φ y = PT.rec (snd (y ∈ˢ A)) λ { ((m , _) , q) →
    subst (λ v → ⟨ v ∈ˢ A ⟩) q
          (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = A} .snd (∈ₛ⟪ A ⟫↪ m)) }

  private
```

第二の仕様は本章の核心で、含意の対ではなく命題としての経路で述べられます。`⟪ A ⟫↪ m` が `defSet φ` に属するという命題は、内側の充足の命題 `(ι m ∷ []) ⊨ᵐ φ` と等しいのです。補助定義 `decode` は `smallSat` を完全な対に展開し直し、第二成分の同値を両方向から使えるようにします。また private の単射性補題に注意してください。`⟪ A ⟫↪` は `⟪ A ⟫` から台への埋め込みなので、その値の間の経路は添字の間の経路から来ます。これにより集合の経路から `m' ≡ m` を復元します。

```agda
    ⟪⟫↪-inj : {m' m : ⟪ A ⟫} → ⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m → m' ≡ m
    ⟪⟫↪-inj {m'} {m} = isEmbedding→Inj isEmb⟪ A ⟫↪ m' m

  defSet-mem : (φ : Formula ⟪ A ⟫ 1) (m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ defSet φ) ≡ ((ι m ∷ []) ⊨ᵐ φ)
  defSet-mem φ m = ⇔toPath fwd bwd
```

順方向は、所属が「だけ」与えるものを展開します。証明 `h` が `smallSat φ m'` を示す索引 `(m' , h)` と、`⟪ A ⟫↪ m' ≡ ⟪ A ⟫↪ m` となる経路 `q` です。単射性が `q` を `m' ≡ m` に変え、それに沿って `h` を輸送すれば `smallSat φ m` の証明が得られます。次に `decode` の第二成分、つまり小さな命題と内側の充足との同値が、この証明を目標の命題へ変換します。部品はすべて使われます。切断が索引を、埋め込みが添字の間の経路を、輸送が証明の移動を、同値が復号を担います。

```agda
    where
    decode = ⊨ᵐ-small φ (ι m ∷ [])
    fwd : ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩ → ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩
    fwd = PT.rec (snd ((ι m ∷ []) ⊨ᵐ φ)) λ { ((m' , h) , q) →
      invEq (decode .snd) (subst (λ k → ⟨ smallSat φ k ⟩) (⟪⟫↪-inj q) h) }
```

逆方向は短くて済みます。同値は逆にも走るからです。`hφ : (ι m ∷ []) ⊨ᵐ φ` が与えられれば、同値を適用して `smallSat φ m` の証明を得て、自明な経路 `refl` とともに索引 `(m , 証明)` を取ります。結果は `∣_∣₁` で切断されますが、所属が要求するのはそれだけです。両方向を合わせて、内側の充足と定義可能部分集合への所属との、約束された正確な対応が得られます。

```agda
    bwd : ⟨ (ι m ∷ []) ⊨ᵐ φ ⟩ → ⟨ ⟪ A ⟫↪ m ∈ˢ defSet φ ⟩
    bwd hφ = ∣ (m , equivFun (decode .snd) hφ) , refl ∣₁
```

## Def は細分するが要素を失わない

推移性を仮定する前でも、二つの事実が `Def A` の位置を定めます。恒真論理式は `A` 全体を定義するので、`A` 自身が `Def A` の要素です。また、`Def A` の各要素は `A` の部分集合です。この段階ではまだ `A ⊆ Def A` を主張していません。次節では推移性のもとで `A` の各要素を個別に定義し、このより強い包含を証明します。

private の補助 `A-mem` は大きい方の所属の証明をファイバーの形に変換します。`A` の要素 `y` は、`⟪ A ⟫↪ m ≡ y` を満たすある添字 `m` から「だけ」来ており、`∈-asFiber` がファイバーをデータとして返す (切断はそれが消費する所属の証明の中にある) ので、`let` で対を分解できます。二つの集合の等しさは `extensionality` で示すので、両方向の包含を確立すれば十分です。

```agda
  private
    A-mem : (y : S) → ⟨ y ∈ˢ A ⟩ → Σ[ m ∈ ⟪ A ⟫ ] (⟪ A ⟫↪ m ≡ y)
    A-mem y y∈ = ∈-asFiber {a = y} {b = A} y∈

  defSet⊤≡A : defSet ⊤̇ ≡ A
  defSet⊤≡A = extensionality (defSet ⊤̇) A (sub₁ , sub₂)
```

容易な方向は、今証明した包含を再利用します。`defSet ⊤̇` の集合論的な要素 `y` は、`sett` の所属の定義を通して切断された索引を与え、`defSet⊆A` が `y` を `A` の中に置き、変換 `∈∈ₛ` が命題を包含 `⊆` が期待する形に整えます。ここでは `⊤̇` の意味は一切使わず、この半分はすべての `defSet φ` で成り立ちます。

```agda
    where
    sub₁ : ⟨ defSet ⊤̇ ⊆ A ⟩
    sub₁ y y∈ₛ = ∈∈ₛ {a = y} {b = A} .fst
      (defSet⊆A ⊤̇ y (∈∈ₛ {a = y} {b = defSet ⊤̇} .snd y∈ₛ))
    sub₂ : ⟨ A ⊆ defSet ⊤̇ ⟩
```

逆方向は「真」の意味を使います。`⊤̇` はすべてのメンバーで成り立つので、`defSet-mem ⊤̇ m` は `⟪ A ⟫↪ m ∈ˢ defSet ⊤̇` を、どんな要素でも証明できる命題と同一視します。ここではそれを恒等関数として与えます。したがって `A` の各要素 `y` は、`⟪ A ⟫↪ m` である「だけ」なので、ファイバーの経路に沿って `defSet ⊤̇` の中へ輸送されます。`subst ⟨_⟩` の中の `sym (defSet-mem ⊤̇ m)` に注意してください。この定理は命題としての経路なので、目標が必要とするどちらの方向にも証明を輸送できます。

```agda
    sub₂ y y∈ₛ =
      let (m , q) = A-mem y (∈∈ₛ {a = y} {b = A} .snd y∈ₛ)
      in subst (λ v → ⟨ v ∈ₛ defSet ⊤̇ ⟩) q
           (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet ⊤̇} .fst
             (subst ⟨_⟩ (sym (defSet-mem ⊤̇ m)) (λ z → z)))
```

双対の包含 `Def∋⊆A` は、`Def A` の各要素が `A` の部分集合であると言います。その前提はそれ自体が切断です。`x` はある `defSet φ` である「だけ」です。目標は命題から積を作った命題なので、`PT.rec` が切断を消去できます。そして、`x` を `defSet φ` と同一視する経路に沿って `y ∈ˢ x` を逆方向に輸送し、`defSet φ` の包含を適用します。`A ∈ Def` を与える `defSet⊤≡A` と合わせて状況は完結します。`Def` は `A` を要素として含み、含むのは `A` の部分集合だけです。

```agda
  Def∋⊆A : (x : S) → ⟨ x ∈ˢ Def ⟩ → (y : S) → ⟨ y ∈ˢ x ⟩ → ⟨ y ∈ˢ A ⟩
  Def∋⊆A x = PT.rec (isPropΠ λ y → isPropΠ λ _ → snd (y ∈ˢ A))
    (λ { (φ , q) y y∈x → defSet⊆A φ y (subst (λ s → ⟨ y ∈ˢ s ⟩) (sym q) y∈x) })
```

## 推移性の下で A ⊆ Def A

`A` が推移的なら、`A` の各**要素** `a` 自身も定義可能です。モデルの章で交わりを作ったのと同じ二つの記号による構成、すなわち原子論理式「その変数は `a` の要素である」を使います。分離が暗黙に課す「∈ A」の条件を埋めるのがまさに推移性です。`a` の要素はすでに `A` の要素なので、原子式が切り出すのはちょうど `a` です。よって `A ⊆ Def A` であり、落とされる要素はありません。前節と合わせると、`Def` の反復は蓄積するだけであり、これは構成可能階層がまさに要求する性質です。

この議論は `A` の推移性を明示的な仮定として取ります。原子論理式 `atom mₐ` は `var zero ∈̇ con mₐ` で、自由変数のスロットが一つと、要素 `mₐ` を名指す単一の定数からなります。`⟪ A ⟫` を定数域として使うという設計判断がここでも効きます。`A` のすべての要素が定数として使え、`ι` がそれを制限された台へ復号するからです。

```agda
  module Refine (Atrans : Transitive 𝒮ᵥ M) where

    atom : ⟪ A ⟫ → Formula ⟪ A ⟫ 1
    atom mₐ = var zero ∈̇ con mₐ

    atom-mem : (mₐ m : ⟪ A ⟫)
             → (⟪ A ⟫↪ m ∈ˢ defSet (atom mₐ)) ≡ (⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ)
```

この原子式への所属定理の特殊化は直接です。環境は単一のパラメータ `m` に固定されており、原子式の意味論により `var zero ∈̇ con mₐ` の内側の真理値は、制限された世界の中の所属 `⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ` にほかなりません。制限された所属は基礎となる集合の周囲の所属で定義されるので、この原子式は実際に `⟪ A ⟫↪ mₐ` の要素を選びます。残る仕事は、提示された集合 `defSet (atom mₐ)` がその要素と等しいことを示すことだけです。

```agda
    atom-mem mₐ m = defSet-mem (atom mₐ) m

    defSet-atom≡ : (mₐ : ⟪ A ⟫) → defSet (atom mₐ) ≡ ⟪ A ⟫↪ mₐ
    defSet-atom≡ mₐ = extensionality (defSet (atom mₐ)) (⟪ A ⟫↪ mₐ) (sub₁ , sub₂)
      where
      sub₁ : ⟨ defSet (atom mₐ) ⊆ ⟪ A ⟫↪ mₐ ⟩
```

順方向の包含は、`y ∈ˢ defSet (atom mₐ)` の切断された索引を消去します。索引は、メンバーと「原子式がそこで成り立つ」ことの証明 `h` の対 `(m , h)` であり、さらに索引写像からの経路 `q` を伴います。`atom-mem` により証明 `h` は周囲の意味での所属 `⟪ A ⟫↪ m ∈ˢ ⟪ A ⟫↪ mₐ` に変わり、`∈∈ₛ` がそれを `⟪ A ⟫↪ mₐ` の集合論的な要素へ変換します。`q` に沿った輸送で完成です。これは、平凡な「`A` への所属」の代わりに原子式の意味を置いた、`defSet⊆A` の証明の鏡像です。

```agda
      sub₁ y y∈ₛ = PT.rec (snd (y ∈ₛ ⟪ A ⟫↪ mₐ))
        (λ { ((m , h) , q) →
          subst (λ v → ⟨ v ∈ₛ ⟪ A ⟫↪ mₐ ⟩) q
            (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = ⟪ A ⟫↪ mₐ} .fst
              (subst ⟨_⟩ (atom-mem mₐ m) ∣ (m , h) , refl ∣₁)) })
```

逆方向の包含は、推移性が登場する場所です。`y ∈ˢ ⟪ A ⟫↪ mₐ` が与えられれば、それを周囲の所属 `y∈a` に展開します。`A` の推移性は「`A` の要素の要素は再び `A` の要素」と言うもので、ここでは `⟪ A ⟫↪ mₐ ∈ˢ A` という証人 `mₐ-as` とともに適用されます。よって `y ∈ˢ A` となり、ファイバー分解は `⟪ A ⟫↪ m ≡ y` を満たす添字 `m` を渡し、`defSet (atom mₐ)` の要素として提示できます。

```agda
        (∈∈ₛ {a = y} {b = defSet (atom mₐ)} .snd y∈ₛ)
      sub₂ : ⟨ ⟪ A ⟫↪ mₐ ⊆ defSet (atom mₐ) ⟩
      sub₂ y y∈ₛ =
        let y∈a     = ∈∈ₛ {a = y} {b = ⟪ A ⟫↪ mₐ} .snd y∈ₛ
            y∈A     = Atrans {x = ⟪ A ⟫↪ mₐ} {y = y} y∈a mₐ-as
```

締めくくりに、得られた添字 `m` が実際に自身で原子式を満たすことを示します。ファイバーの経路に沿って `y∈a` を逆向きに輸送すると所属が `⟪ A ⟫↪ mₐ` の内側に入り、`atom-mem` を `sym` で逆向きに読んで、それが `smallSat (atom mₐ) m` の証明に変わります。最後の `q` に沿った輸送が `defSet (atom mₐ)` に着地します。両方の包含で、集合の等しさが得られます。ここでの輸送はどれも、集合や命題の経路に沿って**証明**を運ぶもので、新しいデータを作ることはありません。

```agda
            (m , q) = ∈-asFiber {a = y} {b = A} y∈A
        in subst (λ v → ⟨ v ∈ₛ defSet (atom mₐ) ⟩) q
             (∈∈ₛ {a = ⟪ A ⟫↪ m} {b = defSet (atom mₐ)} .fst
               (subst ⟨_⟩ (sym (atom-mem mₐ m))
                 (subst (λ v → ⟨ v ∈ˢ ⟪ A ⟫↪ mₐ ⟩) (sym q) y∈a)))
```

この等式が手に入れば、`Def` への所属まであと切断一つです。`a ∈ˢ A` が与えられれば、その所属のファイバー分解は `⟪ A ⟫↪ mₐ ≡ a` を満たす添字 `mₐ` を与えます。ここではファイバーがデータなので、`let` で対を開き `mₐ` に名前を付けられます。

```agda
        where
        mₐ-as : ⟨ ⟪ A ⟫↪ mₐ ∈ˢ A ⟩
        mₐ-as = ∈∈ₛ {a = ⟪ A ⟫↪ mₐ} {b = A} .snd (∈ₛ⟪ A ⟫↪ mₐ)

    A⊆Def : (a : S) → ⟨ a ∈ˢ A ⟩ → ⟨ a ∈ˢ Def ⟩
    A⊆Def a a∈ =
```

`Def` の要素 `defSet (atom mₐ)` は `⟪ A ⟫↪ mₐ` と等しく、その等しさとファイバーの経路 `q` を合成すれば `defSet (atom mₐ) ≡ a` が得られます。論理式とこの等式の対を切断 `∣_∣₁` で包むと、`Def` への所属が要求するもの、つまり定義した部分集合が `a` であるような論理式が「だけ」存在することが、ちょうど得られます。こうして `A` のすべての要素は `Def` に残り、前節と合わせて、この演算子は精化だけを行います。

```agda
      let (mₐ , q) = ∈-asFiber {a = a} {b = A} a∈
      in ∣ atom mₐ , defSet-atom≡ mₐ ∙ q ∣₁
```

### 外部から読む定義可能性

名前を与える価値のある帰結が一つあります。構成可能性の段階の証明はこれに繰り返し依拠するからです。`defSet φ` への所属は**内側**の世界 `(A, ∈)` での命題ですが、これからの議論は周囲の階層で行われます。Δ₀ 論理式については二つの読みが一致します。これが絶対性定理です。絶対性はクラスの要素について述べられる一方、`defSet` は小さな索引型について述べられるので、残るのはそのずれの処理だけです。定数の改名がこのずれを埋め、証明全体は三段階の経路になります。`defSet` の仕様、論理式の改名、そして絶対性です。

このためには `A` が推移的でなければならず、だからこそこの補題はこのこの議論に置かれています。階層のどの段階も推移的です。

絶対性のモジュールは、周囲の構造、クラス `M`、推移性の仮定の上で具体化され、制限された構造 `Abs.𝒮M`、外側の充足 `Abs.⊨ᵛ`、そして Δ₀ 絶対性 `Abs.abs₀` を与えます。この命題は、`φ` が Δ₀ であることを証明する証拠 `d` を取り、命題としての経路を主張します。`⟪ A ⟫↪ m` が `defSet φ` に属するという命題は、論理式 `mapFo ι φ` が**周囲**の構造で環境 `⟪ A ⟫↪ m ∷ []` のもとで充足されることと等しいのです。右辺の論理式は定数を `ι` を通して写すので、`A` の要素を名指す、周囲の台の上の論理式になります。

```agda
    module Abs = FOL.Absoluteness.Single 𝒮ᵥ M Atrans

    abs-defSet : (φ : Formula ⟪ A ⟫ 1) → Δ₀ φ → (m : ⟪ A ⟫)
               → (⟪ A ⟫↪ m ∈ˢ defSet φ)
                 ≡ ((⟪ A ⟫↪ m ∷ []) Abs.⊨ᵛ (mapFo ι φ))
    abs-defSet φ d m =
```

証明は三つの経路を連結します。第一に、`defSet-mem` は定義可能部分集合への所属を、`ι m` における `φ` の内側の充足として読みます。第二に、`⊨-map` (対称の方向なので `sym`) は、定数を `ι` を通して改名しても真理値が変わらないと言います。`ι` が内側の世界の定数の解釈にほかならないからです。残るのは、改名された論理式 `mapFo ι φ` の内側の充足です。第三に、`abs₀` がその Δ₀ 論理式の内側の充足を、周囲の構造での外側の充足へ輸送します。推移性を使うのはこの一段階だけです。この結果により、後の章は定義可能部分集合への所属を、内側だけではなく周囲の命題として扱えます。

```agda
        defSet-mem φ m
      ∙ sym (⊨-map Abs.𝒮M ι id φ (ι m ∷ []))
      ∙ Abs.abs₀ (mapΔ₀ ι d) (ι m ∷ [])
```

## まとめ

`Def A` は、内側の世界 `(A, ∈)` で `A` からのパラメータ付きの論理式によって定義される `A` の部分集合の集合です。構文が索引集合として働き、内側の充足が意味を与え、本質的小ささが必要な宇宙レベルを賄います。仕様 `defSet-mem` は「定義可能」の意味を直接述べ、この演算子は精化だけを行います。推移性の下では `A ⊆ Def A` (`A⊆Def`) であり、`Def A` の要素は `A` の部分集合です (`Def∋⊆A`)。次の章はこの一歩を宇宙へと反復します。