---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# 集合の定義可能な部分集合

```agda
open import Base.Prelude
```

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

```agda
module L.Definability {ℓ : Level} where
```

```agda
open import FOL.ZFStructure using ( ZFStructure; module hPropView )
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
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Smallness {ℓ} using ( module InnerSmall )
```

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

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

```agda
open import Cubical.Data.Sigma using ( Σ-cong-equiv-snd )
```

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

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

```agda
open import Cubical.Foundations.Equiv
  using ( invEquiv; compEquiv; propBiimpl→Equiv )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
```

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

```agda
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` を両方向に変換する。これらは命題なので、点ごとの変換は正当である。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

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

</summary>
<div class="submodule-fold-content">

```agda
  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 ((v ∈ₛ A) .snd) ((v ∈ˢ A) .snd)
            (∈∈ₛ {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 = rec₁ ((y ∈ˢ A) .snd) λ { ((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 = rec₁ (((ι m ∷ []) ⊨ᵐ φ) .snd) λ { ((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 φ` である「だけ」である。目標は命題から積を作った命題なので、`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 = rec₁ (isPropΠ λ y → isPropΠ λ _ → (y ∈ˢ A) .snd)
    (λ { (φ , 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` のすべての要素が定数として使え、`ι` がそれを制限された台へ復号するからである。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

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

</summary>
<div class="submodule-fold-content">

```agda
    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∈ₛ = rec₁ ((y ∈ₛ ⟪ A ⟫↪ mₐ) .snd)
        (λ { ((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 ∷ [])
```

</div>
</details>

</div>
</details>

## まとめ

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