---
title: "定義可能冪集合の Δ₀ 記述"
module: L.GCH.DefinablePowerSetDescription
lang: ja
site: "Bedrock"
description: "定義可能冪集合の Δ₀ 記述"
stage: "GCH の証明"
reading_order: 101
canonical: https://bedrock.institute/ja/L.GCH.DefinablePowerSetDescription.html
html: L.GCH.DefinablePowerSetDescription.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/DefinablePowerSetDescription.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Definability, L.Coding.Model, L.Coding.SatisfactionBridge, L.Coding.DefinablePowerSet, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Coding.Satisfaction, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.CodeAlphabet, L.GCH.SatisfactionDescription]
routes: [gch-descriptions]
translations: [https://bedrock.institute/en/L.GCH.DefinablePowerSetDescription.md, https://bedrock.institute/zh/L.GCH.DefinablePowerSetDescription.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
open import Base.Classical using ( LEM )
```

宇宙レベル `ℓ` と実例 `lem : LEM (ℓ-suc ℓ)` を固定する。このモジュールのすべての結果は、最後の健全性と完全性を含め、ちょうどこの仮定のもとで成り立つ。

```agda
module L.GCH.DefinablePowerSetDescription {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

```agda
open import FOL.ZFStructure using ( module hPropView )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; _⇒̇_; ∃̇∈; ∀̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( prAtL; container )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst; defSet-Sat )
open import L.Coding.DefinablePowerSet {ℓ} lem using ( envOne )
open import L.Coding.CodeSet {ℓ} lem using ( keyS; key∈AllCodes )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table; val-at )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
open import L.Coding.Quantification {ℓ} using
  ( sh; i0; i1; i3; i6; f0; f1; down
  ; sndEx; sndAll; sndEx-out; sndAll-in; fillSnd; useSnd
  ; pr-out; pr-in; sndS )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )
open import L.GCH.SatisfactionDescription {ℓ} lem using ( satAt; module SatRead; module Match )
```

この章の課題は、構成可能な台の要素をパラメータとして許した一階定義可能部分集合の集まりを、有界論理式で認識することである。この集まりは定義可能冪集合 `𝒟ₒ` であり、完全な内部冪集合ではない。内部の記述が正しくなるには、数項のタグ、符号領域、充足関係表がそれぞれ意図した意味をもつ必要がある。

この構成では、排中律を本書で唯一の明示的な古典的仮定として用いる。それでも命題的切り詰めは全体に残る。存在証明は、ある論理式や表の値が存在することを示しても、それを大域的に選び出さない。

対象言語での記述は、意図的に有界に保つ。所属原子式、連言、含意、有界存在量化子、有界全称量化子だけから組み立て、後で `checkΔ₀` がこの構文上の形を検査する。外から与えた論理式を、符号化された充足構成での解釈と比較する際には、定数の写像も用いる。

意図する出力は `𝒟ₒ W`、すなわち `W` 上の制限構造で `W` の要素をパラメータとして定義できる部分集合の集まりである。二つの所属方向を証明すれば、外延性によって候補の出力をこの集合と同一視できる。順序対の符号は、環境、論理式の鍵、表の項目を表す。

論理式 `ψ` に対し、充足構成はどの一項環境が `ψ` を満たすかを記録する。橋渡し定理は、そこから `W` の中で切り出される部分を、`ψ` が定義する部分集合と同一視する。実際の符号集合は `ψ` から作られる鍵を含み、実際の充足関係表の関数性がその鍵での値を定める。これらを使えるのは、候補の符号集合と表を `satAt` が保証した後だけである。復号が一意になるわけでも、部分集合の定義論理式が選ばれるわけでもない。

記述に現れる量化子はすべて、環境にすでにある集合によって有界でなければならない。以下の補助量化子は、その範囲内で順序対の符号の二成分を表す。二方向の補題によって、対象言語での充足と対応する意味論的な証人との間を行き来できる。

`Tags` は、指定された十個の枠を数項 0 から 9 と解釈する。特に以下の節では、タグ 0 で一項環境を、タグ 1 でアリティ 1 の鍵を認識する。別の述語 `satAt` はさらに強く、候補のコード領域と表が、その台上のアルファベットと再帰的な充足構成を実現していることを保証する。

環境は構成可能集合からなる有限ベクトルで表す。積は切り出し関係を定める二つの所属条件を組み合わせる。それらが命題であるため、選択を導入することなく、切り詰められた証人をその条件へ消去できる。

証明では、点ごとの所属の同値を集合の等しさへ繰り返し変換する。所属は命題値なので、どちらの所属方向を示すときにも、単に存在する符号・論理式・表示を消去できる。周囲の集合の要素を台の要素として読む必要があるときは、`∈-asFiber` が表示の添字を復元する。

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈-asFiber )
```

タグとして使うフォン・ノイマン数項は累積階層の中にある。特に 0 は一変数環境の唯一の項目を示し、1 はここで扱う論理式のアリティを示す。

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_ )
```

構成可能集合の台を `S` と書く。`S` の要素は基礎の集合とその構成可能性の証明書からなるので、論理式の有界な証人は意図したモデルの内部にとどまる。

```agda
open hPropView 𝒮ʟ using ( S )
```

構成可能集合の有限環境で対象言語の論理式が充足されることを `γ ⊨ φ` と書く。この記法の背後にある絶対性によって、後の意味論的な議論では、この内部の読みを周囲の累積階層における通常の所属と比較できる。

```agda
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _⊨ᵐ_ )
open AbsL using () renaming ( _⊨ᵐ_ to _⊨_ )
```

単項環境は、一つの枠の上の二つの有界の節で記述される。符号化された集合 `e` のすべての要素が、タグ 0 と値 `z` の順序対であり、`e` の中にその対に等しい要素が存在する、というものである。全称の節がほかのすべての要素を排除し、存在の節が空集合を排除する。

```agda
singleOf : ∀ {j} → Fin j → Fin j → Fin j → Formula S j
singleOf e N0 z = ∀̇∈ (var e) (prAtL i0 (sh 1 N0) (sh 1 z)) ∧̇ ∃̇∈ (var e) (prAtL i0 (sh 1 N0) (sh 1 z))
```

定義可能部分集合の節には二つの連言肢がある。第一は、符号化された集合 `x` のすべての要素が `w` に属し、その一項環境が値 `y` に属することを述べる。第二は、`w` の要素 `z` のうち、その一項環境が `y` に属するものはすべて `x` に属することを述べる。合わせると、`x` が値 `y` によって `w` から切り出されることが分かる。

```agda
definesB : ∀ {j} → Fin j → Fin j → Fin j → Fin j → Formula S j
definesB x w y N0 =
    ∀̇∈ (var x) ((var i0 ∈̇ var (sh 1 w)) ∧̇ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1))
  ∧̇ ∀̇∈ (var w) (∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⇒̇ (var i0 ∈̇ var (sh 1 x)))
```

所属の節は候補の値の要素を走る。各要素について要求するのは、候補領域 `C` にタグ 1 との対の形をした要素 `c` があり、表の項目が `c` と値 `y` を対にし、その `y` が当の要素を `w` から切り出すことだけである。この段階の `c` は鍵の形をしているにすぎない。後で `satAt` を仮定して初めて、実際の論理式の鍵として復号できる。

```agda
memAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
memAt v w T C N =
  ∀̇∈ (var v) (∃̇∈ (var (sh 1 C)) (sndEx i0 (sh 2 (N f1))
    (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))))))
```

被覆の節は逆向きの条件を与える。`C` の要素 `c` がタグ 1 の鍵の形をもつなら、`c` での表の値 `y` と、`y` によって切り出される候補出力の要素 `x` が単に存在することを要求する。したがって候補領域の鍵形の要素をすべて覆うが、それらを実際のアリティ 1 の論理式の鍵すべてと同一視するには、やはり `satAt` が必要である。

```agda
allAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
allAt v w T C N =
  ∀̇∈ (var C) (sndAll i0 (sh 1 (N f1))
    (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))))
```

論理式 `defAt` は、所属の節と被覆の節を連言で結ぶ。それだけでは候補出力を候補のコード領域と表に関係づけるにすぎない。正しい `Tags` と `satAt` のデータを合わせると、二つの節が、出力は `𝒟ₒ W` であることを示す二つの包含になる。

```agda
opaque
  defAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → Fin m) → Formula S m
  defAt v w T C N = memAt v w T C N ∧̇ allAt v w T C N
```

通常の議論ではこの定義を不透明に保ち、後の証明が長い構文展開ではなく、二つの包含という数学的なインターフェースを使うようにする。展開するのは、有界性の確認と二方向の読みの証明に必要な局所的な範囲だけである。

```agda
opaque
  unfolding defAt
```

Δ₀ の証拠は、構造的な検査によって産み出される。論理式が使うのは、変数・所属・連言・含意・有界の量化子だけである。証明されるのは論理式の形であって、記述の正しさではない。

```agda
  Δ₀-defAt : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) → Δ₀ (defAt v w T C N)
  Δ₀-defAt v w T C N = checkΔ₀ (defAt v w T C N) tt
```

記述の読みは、それを二つの連言支に分解する。

```agda
  defAt-out : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m)
            → ⟨ γ ⊨ defAt v w T C N ⟩ → ⟨ γ ⊨ memAt v w T C N ⟩ × ⟨ γ ⊨ allAt v w T C N ⟩
  defAt-out v w T C N γ h = h
```

記述の埋めは、二つの連言支を再び対にする。

```agda
  defAt-in : ∀ {m} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m)
           → ⟨ γ ⊨ memAt v w T C N ⟩ → ⟨ γ ⊨ allAt v w T C N ⟩ → ⟨ γ ⊨ defAt v w T C N ⟩
  defAt-in v w T C N γ h1 h2 = h1 , h2
```

最初の意味論的な計算では `singleOf` を扱う。符号化された集合 `E` と値 `Z` を固定し、指定されたタグが実際に 0 を表すと仮定する。この仮定の下で、二つの有界な節が集合の等式 `E = envOne Z` と同値であることを示す。

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

```agda
module _ {j : ℕ} (e N0 z : Fin j) (δ : Vec S j) (q0 : (lookup N0 δ) .fst ≡ # 0) where
```

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

```agda
  private
    E = (lookup e δ) .fst
    Z = (lookup z δ) .fst
```

単項の節の読みから、符号化された集合が値の正準な単項環境と等しいことが得られる。順方向では、符号化された集合のすべての要素が、数項ゼロと値の順序対であり、対のアトムの妥当性に沿って運ばれる。

```agda
  singleOf-out : ⟨ δ ⊨ singleOf e N0 z ⟩ → E ≡ envOne Z
  singleOf-out (hall , hex) = extensionalV (λ y → ⇔toPath (fwd y) (bwd y))
    where
    fwd : (y : V ℓ) → ⟨ y ∈ E ⟩ → ⟨ y ∈ envOne Z ⟩
    fwd y hy = ∣ lift zero , sym (pr-out i0 (sh 1 N0) (sh 1 z) (down (lookup e δ) y hy ∷ δ) (hall (down (lookup e δ) y hy) hy)
```

逆向きの包含では、正準な一項環境の要素から始める。存在側の連言肢が符号化された集合のある要素を与え、その対の等式と既知のタグ 0 によって、その要素を最初に与えた要素と同一視できる。この等式に沿って所属を移送すれば、元の要素が符号化された集合に属することが得られる。

```agda
                                 ∙ cong (λ a → pr a Z) q0) ∣₁
    bwd : (y : V ℓ) → ⟨ y ∈ envOne Z ⟩ → ⟨ y ∈ E ⟩
    bwd y = rec₁ ((y ∈ E) .snd)
      (λ { (lift zero , qy) → rec₁ ((y ∈ E) .snd)
        (λ { (y' , (y'∈ , hy')) →
```

`envOne Z` の要素は順序対 `pr (# 0) Z` である。したがってタグの枠を数項 0 に書き換えると、この要素は `singleOf` が要求する順序対と同一視される。要素そのものが `Z` と同一視されるわけではない。

```agda
          subst (λ u → ⟨ u ∈ E ⟩)
            (pr-out i0 (sh 1 N0) (sh 1 z) (y' ∷ δ) hy' ∙ cong (λ a → pr a Z) q0 ∙ qy) y'∈ })
        hex
         ; (lift (suc ()) , _) })
```

逆に、符号化された集合が正準な一項環境に等しいと仮定する。その環境の唯一の添字は 0 なので、各要素は必要な順序対の形をもち、残る後者添字の場合は不可能性で閉じる。正準な 0 番の項目が有界存在の証人を与え、仮定した等式に沿う移送がその所属を与える。

```agda
  singleOf-in : E ≡ envOne Z → ⟨ δ ⊨ singleOf e N0 z ⟩
  singleOf-in q =
      (λ y hy → pr-in i0 (sh 1 N0) (sh 1 z) (y ∷ δ)
         (rec₁ (setIsSet (y .fst) (pr ((lookup N0 δ) .fst) Z))
           (λ { (lift zero , qy) → sym qy ∙ cong (λ a → pr a Z) (sym q0) ; (lift (suc ()) , _) })
```

要素に名前が与えられ、その所属が運ばれる。そして存在の証人は、ゼロの数項と値の対を、タグの等式に逆らってまとめる。

```agda
           (subst (λ u → ⟨ y .fst ∈ u ⟩) q hy)))
    , ∣ yS , ( subst (λ u → ⟨ pr (# 0) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁
             , pr-in i0 (sh 1 N0) (sh 1 z) (yS ∷ δ) (cong (λ a → pr a Z) (sym q0)) ) ∣₁
    where
    yS : S
```

名前のついた要素は、数項ゼロと値の対の、符号化された集合の中での提示である。

```agda
    yS = down (lookup e δ) (pr (# 0) Z) (subst (λ u → ⟨ pr (# 0) Z ∈ u ⟩) (sym q) ∣ lift zero , refl ∣₁)
```

</div>
</details>

集合 `X`・台 `Wv`・値 `Y` の間の切り出しの関係は、各点での双方向である。`X` のすべての要素は `Wv` に属しその単項環境が `Y` の中にあり、`Wv` の要素のうちその単項環境が `Y` の中にあるものはすべて `X` に属する。量化は構成可能な集合の上を行われるので、この関係は構成可能な台の上で述べられる。

```agda
Cuts : (X Wv Y : V ℓ) → Type (ℓ-suc ℓ)
Cuts X Wv Y = ((z : S) → ⟨ z .fst ∈ X ⟩ → ⟨ z .fst ∈ Wv ⟩ × ⟨ envOne (z .fst) ∈ Y ⟩)
            × ((z : S) → ⟨ z .fst ∈ Wv ⟩ → ⟨ envOne (z .fst) ∈ Y ⟩ → ⟨ z .fst ∈ X ⟩)
```

対象言語の節を数学的な切り出し関係と比較するため、`x`、`w`、`y`、タグ 0 の枠を固定する。それぞれの解釈を `X`、`Wv`、`Y` と名付ける。タグの等式があるからこそ、`singleOf` は正準な一項環境を表せる。

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

```agda
module _ {j : ℕ} (x w y N0 : Fin j) (δ : Vec S j) (q0 : (lookup N0 δ) .fst ≡ # 0) where
```

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

```agda
  private
    X = (lookup x δ) .fst
    Wv = (lookup w δ) .fst
    Y = (lookup y δ) .fst
```

`Y` は構成可能集合なので、一項環境が `Y` に属するという証明から、その環境を表す台の要素を得られる。この表示があるため、`definesB` の有界存在量化子は `Y` の実際の要素を証人にできる。

```agda
    YS = lookup y δ
```

単項の節の存在量化を読むと、それが、正準な単項環境の値の中での所属に変換される。証人は値の要素であり、単項の節が、符号化された項目をその索引の正準な環境と同一視する。

```agda
    one-out : (z : S) → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⟩ → ⟨ envOne (z .fst) ∈ Y ⟩
    one-out z = rec₁ ((envOne (z .fst) ∈ Y) .snd)
      (λ { (e , (e∈ , he)) → subst (λ u → ⟨ u ∈ Y ⟩) (singleOf-out i0 (sh 2 N0) i1 (e ∷ z ∷ δ) q0 he) e∈ })
```

存在量化の埋めは逆である。正準な単項環境は値の中で提示され、単項の節は延長された環境のもとで埋められる。

```agda
    one-in : (z : S) → ⟨ envOne (z .fst) ∈ Y ⟩ → ⟨ (z ∷ δ) ⊨ ∃̇∈ (var (sh 1 y)) (singleOf i0 (sh 2 N0) i1) ⟩
    one-in z h = ∣ down YS (envOne (z .fst)) h , (h , singleOf-in i0 (sh 2 N0) i1 (down YS (envOne (z .fst)) h ∷ z ∷ δ) q0 refl) ∣₁
```

定義可能部分集合の節を読むと、切り出し関係の二つの方向が得られる。第一の連言肢は、`X` の各要素が `Wv` に属し、その一項環境が `Y` に属することを与える。第二の連言肢は、この二つの事実から `X` への所属を戻す。

```agda
  definesB-out : ⟨ δ ⊨ definesB x w y N0 ⟩ → Cuts X Wv Y
  definesB-out (h1 , h2) = (λ z hz → h1 z hz .fst , one-out z (h1 z hz .snd)) , (λ z hw he → h2 z hw (one-in z he))
```

逆に、`Cuts X Wv Y` の二つの各点的な方向から、対象言語における定義可能部分集合の節の二つの連言肢を満たせる。上の内部変換は、有界な一項環境の証人と、正準な一項環境が `Y` に属することとの間を正確に行き来する。

```agda
  definesB-in : Cuts X Wv Y → ⟨ δ ⊨ definesB x w y N0 ⟩
  definesB-in (o , i) = (λ z hz → o z hz .fst , one-in z (o z hz .snd)) , (λ z hw he → i z hw (one-out z he))
```

</div>
</details>

## 有界部分集合の各節を読む

完全な読みのモジュールは、四つの集合、すなわち提案された値・台・表・コードの定義域に名前を与える。

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

```agda
module Read {m : ℕ} (v w T C : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m) (tg : Tags γ N) where
```

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

```agda
  private
    Vv = (lookup v γ) .fst
    Wv = (lookup w γ) .fst
    Tv = (lookup T γ) .fst
```

コードの定義域の底の集合と、タグ一の背後にある数項が名付けられる。所属の節が選ぶのは、タグ一と第二成分の対の形のコードだからである。

```agda
    Cv = (lookup C γ) .fst
    N1v = (lookup (N f1) γ) .fst
```

所属の節の読みは、提案された値の各要素に対して、切り詰められた記録を与える。定義域の中の、タグ一とある成分の対として分解される符号、その符号をある値と対にする表の項目、そしてその要素と値の間の切り出しの関係である。記録は切り詰めのもとで存在し、符号や値は選ばれない。

```agda
  mem-out : ⟨ γ ⊨ memAt v w T C N ⟩ → (x : S) → ⟨ x .fst ∈ Vv ⟩
          → ∥ Σ[ c ∶ S ] Σ[ p ∶ S ] Σ[ y ∶ S ]
              (⟨ c .fst ∈ Cv ⟩ × ((c .fst ≡ pr (# 1) (p .fst)) × (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × Cuts (x .fst) Wv (y .fst)))) ∥₁
  mem-out h x x∈ = rec₁ squash₁
    (λ { (c , (c∈ , hc)) → rec₁ squash₁
```

所属の節を読むには、まず候補の符号領域から鍵の形をした要素 `c` を取り出し、次に `c` と値 `y` を対にする表の項目を取り出す。対の仕様が符号化された第二成分を結果に現れる意味論的な等式へ変え、タグの等式が形式的なタグを実際の数項 1 へ書き換える。

```agda
      (λ { (p , s , (ec , he)) → rec₁ squash₁
        (λ { (e , (e∈ , hy)) → map₁
          (λ { (y , s' , (ee , hd)) →
            c , p , y , ( c∈ , ( ec ∙ cong (λ a → pr a (p .fst)) (tg f1)
                        , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
```

最も内側の存在は、`definesB-out` を通して読まれ、要素と表の項目の値 `y` の間の切り出しの関係を産み出す。

```agda
                          , definesB-out i6 (sh 7 w) i0 (sh 7 (N f0)) (y ∷ s' ∷ e ∷ p ∷ s ∷ c ∷ x ∷ γ) (tg f0) hd ) ) ) })
          (sndEx-out i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))) (e ∷ p ∷ s ∷ c ∷ x ∷ γ) hy) })
        he })
      (sndEx-out i0 (sh 2 (N f1)) (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0))))) (c ∷ x ∷ γ) hc) })
    (h x x∈)
```

所属の節の埋めは逆の構成である。各要素に対して切り詰められた記録を産み出す関数を受け取り、節の充足を組み立てる。

```agda
  mem-in : ((x : S) → ⟨ x .fst ∈ Vv ⟩
            → ∥ Σ[ c ∶ S ] Σ[ p ∶ S ] Σ[ y ∶ S ]
                (⟨ c .fst ∈ Cv ⟩ × ((c .fst ≡ pr (# 1) (p .fst)) × (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × Cuts (x .fst) Wv (y .fst)))) ∥₁)
         → ⟨ γ ⊨ memAt v w T C N ⟩
  mem-in g x x∈ = map₁
```

逆に、候補出力の各要素に対して、このような切り詰められた意味論的記録が与えられているとする。等式 `c = pr (# 1) p` は有界論理式が要求するアリティ一の形を与え、`pr(c,y)` の表への所属は表の項目の有界な表示を与える。

```agda
    (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) →
      let ec' : c .fst ≡ pr N1v (p .fst)
          ec' = ec ∙ cong (λ a → pr a (p .fst)) (sym (tg f1))
          δ4 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ x ∷ γ
          eS = down (lookup T γ) (pr (c .fst) (y .fst)) e∈
```

続いて七つの枠からなる環境を組み立て、`definesB-in` によって切り出し関係を定義可能部分集合の節へ戻す。

```agda
          δ7 = y ∷ container eS c y refl .fst ∷ eS ∷ δ4
      in c , ( c∈ , fillSnd i0 (c ∷ x ∷ γ) (lookup (N f1) γ) p ec'
                 (∃̇∈ (var (sh 4 T)) (sndEx i0 i3 (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))))
                 ∣ eS , ( e∈ , fillSnd i0 (eS ∷ δ4) c y refl (definesB i6 (sh 7 w) i0 (sh 7 (N f0)))
                              (definesB-in i6 (sh 7 w) i0 (sh 7 (N f0)) δ7 (tg f0) cuts) i3 refl ) ∣₁
```

鍵の形、表の項目、切り出し条件を符号化した後、外側の有界量化子が、この切り詰められたまとまりを候補出力の元の要素に適用する。したがって、この意味論的記録から所属の節全体の充足を再構成できる。

```agda
                 (sh 2 (N f1)) refl ) })
    (g x x∈)
```

覆いの節の読みは、タグ一と `p` の対として分解される符号 `c` を取り、単に、`c` における表の値 `y` と、`y` によって切り出される集合 `x` を与える。

```agda
  all-out : ⟨ γ ⊨ allAt v w T C N ⟩ → (c p : S) → ⟨ c .fst ∈ Cv ⟩ → c .fst ≡ pr (# 1) (p .fst)
          → ∥ Σ[ y ∶ S ] Σ[ x ∶ S ] (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × (⟨ x .fst ∈ Vv ⟩ × Cuts (x .fst) Wv (y .fst))) ∥₁
  all-out h c p c∈ ec = rec₁ squash₁
    (λ { (e , (e∈ , hy)) → rec₁ squash₁
      (λ { (y , s' , (ee , hx)) → map₁
```

証明は、表の項目と三つの枠の存在量化を消去する。そして定義可能な部分集合の節の読みが、要素と表の値の間の切り出しの関係を産み出す。

```agda
        (λ { (x , (x∈ , hd)) →
          y , x , ( subst (λ u → ⟨ u ∈ Tv ⟩) ee e∈
                  , ( x∈ , definesB-out i0 (sh 7 w) i1 (sh 7 (N f0)) (x ∷ y ∷ s' ∷ e ∷ δ3) (tg f0) hd ) ) })
        hx })
      (sndEx-out i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))) (e ∷ δ3) hy) })
```

逆向きの構成では、符号領域の要素 `c` を固定し、それが `pr (# 1) p` として表される場合を調べる。意味論的な覆いの仮定は、命題的切り詰めの下で表の値と、その値が切り出す部分集合を与える。これらの証人が、その表示に対する有界な結論を満たす。

```agda
    (useSnd i0 (c ∷ γ) (lookup (N f1) γ) p ec'
      (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0))))))
      (sh 1 (N f1)) refl (h c c∈))
    where
    ec' : c .fst ≡ pr N1v (p .fst)
```

形式的なタグを使う等式は、`Tags` によって必要なアリティ一の等式へ変換される。補助的な容器は、成分と符号を有界量化子の範囲内に保つだけであり、意味論的な証人に選択や一意性を加えるものではない。

```agda
    ec' = ec ∙ cong (λ a → pr a (p .fst)) (sym (tg f1))
    δ3 : Vec S (3 + m)
    δ3 = p ∷ container c (lookup (N f1) γ) p ec' .fst ∷ c ∷ γ
```

したがって覆いの節を満たす際には、候補の符号領域の要素のうち、アリティ一の鍵の形で表示されたものをすべて扱う。その各表示に対し、意味論的な仮定が命題的切り詰めの下で、表の値、それが切り出す候補出力の要素、および両者の所属を与える。後で `satAt` を加えるまでは、これらが実際の論理式の鍵であるとは主張しない。

```agda
  all-in : ((c p : S) → ⟨ c .fst ∈ Cv ⟩ → c .fst ≡ pr (# 1) (p .fst)
            → ∥ Σ[ y ∶ S ] Σ[ x ∶ S ] (⟨ pr (c .fst) (y .fst) ∈ Tv ⟩ × (⟨ x .fst ∈ Vv ⟩ × Cuts (x .fst) Wv (y .fst))) ∥₁)
         → ⟨ γ ⊨ allAt v w T C N ⟩
  all-in g c c∈ = sndAll-in' (λ p s s∈ p∈ ec →
    map₁ (λ { (y , x , (e∈ , (x∈ , cuts))) →
```

最も内側の有界存在量化子には、切り出された集合 `x` と、`x` が値の集合に属する証明、さらに `definesB` で符号化したばかりの `Cuts` の証拠が渡される。これで逆向きの翻訳が完成する。表の項目とそれが切り出す部分集合についての意味論的な証人から所属の条項の充足が得られ、存在データはすべて命題的切り詰めの中に保たれる。

```agda
      let eS = down (lookup T γ) (pr (c .fst) (y .fst)) e∈
          δ6 = y ∷ container eS c y refl .fst ∷ eS ∷ p ∷ s ∷ c ∷ γ
      in eS , ( e∈ , fillSnd i0 (eS ∷ p ∷ s ∷ c ∷ γ) c y refl (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0))))
                       ∣ x , (x∈ , definesB-in i0 (sh 7 w) i1 (sh 7 (N f0)) (x ∷ δ6) (tg f0) cuts) ∣₁ i3 refl ) })
      (g c p c∈ (ec ∙ cong (λ a → pr a (p .fst)) (tg f1))))
```

覆いの条項にも同じ二段の存在選択がある。充足関係表の値と、その値が作業集合から切り出す部分集合である。両者を合わせた外向きの読み出しに名前を付けることで、次の議論では、この単に存在する一対の証人を一つの命題値のまとまりとして扱える。

```agda
    where
    sndAll-in' = sndAll-in i0 (sh 1 (N f1))
      (∃̇∈ (var (sh 3 T)) (sndEx i0 i3 (∃̇∈ (var (sh 6 v)) (definesB i0 (sh 7 w) i1 (sh 7 (N f0)))))) (c ∷ γ)
```

</div>
</details>

## 有界な記述の正しさ

ここから、有界な記述を実際の定義可能性の演算と比較する。この比較には `defAt` の充足だけでは足りない。数を表すタグが意図した値をもち、作業集合の枠が `W` を表し、さらに `satAt` が符号集合と充足関係表に本来の充足意味論を保証していなければならない。

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

```agda
module DefRead {m : ℕ} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m) (W : S)
  (qw : (lookup w γ) .fst ≡ W .fst) (tg : Tags γ N) (hs : ⟨ γ ⊨ satAt T w C E N ⟩) where
```

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

```agda
  open Alphabet W
  open Match W
```

先に得た二つの読み出しが必要な橋を与える。`SatRead` は、記述された符号領域と表を、`W` 上の実際の符号と充足値に対応させる。`Read` は `defAt` を二つの意味論的な切り出し条件として読む。その上で `DefOf (W .fst)` が、復号されたアリティ一の各論理式を `W` の一つの部分集合として解釈する。

```agda
  private module SR = SatRead T w C E N γ W qw tg hs
  private module RD = Read v w T C N γ tg
  private module DA = DefOf (W .fst)
  private
    Vv = (lookup v γ) .fst
    Wv = (lookup w γ) .fst
```

表の枠と符号の枠が表す基礎の集合を、それぞれ `Tv` と `Cv` と書く。`satAt` の役割はまさに、これら記述された集合への所属と、実際の充足関係表および符号領域への所属とを相互に変換できるようにすることである。

```agda
    Tv = (lookup T γ) .fst
    Cv = (lookup C γ) .fst
```

対応 `toS` は、アルファベットの上の論理式のすべての定数を、`S` の対応する定数へ付け替え、周囲の充足で判定できる論理式を作る。

```agda
    toS : Formula Ab 1 → Formula S 1
    toS = mapFo (asConst W)
```

表の値の補題は、論理式のキーで記録された値が、付け替えられた論理式の明示的な充足集合に等しいと言う。証明は、表の外向きの射影と、一様な充足の値の同定とを合成する。

```agda
    valOf : (ψ : Formula Ab 1) (c y : S) → c .fst ≡ (keyS W ψ) .fst → ⟨ pr (c .fst) (y .fst) ∈ Tv ⟩
          → y .fst ≡ (Sat W (toS ψ)) .fst
    valOf ψ c y qc h = SR.T-out c y h .snd ∙ cong (λ p → p .fst) (val-at W W ψ c (SR.T-out c y h .fst) qc)
```

中心となる橋は論理式を一つずつ扱う。`Cuts` が、`x` は `W` の要素のうち、その一変数環境が `ψ` の充足集合に属するものからちょうど成ると述べるなら、`x` は特定の定義可能部分集合 `DA.defSet ψ` に等しくなる。この等式は、所属の両方向を示して外延性から得られる。

```agda
    cut≡ : (ψ : Formula Ab 1) (x : S) → Cuts (x .fst) Wv ((Sat W (toS ψ)) .fst) → DA.defSet ψ ≡ x .fst
    cut≡ ψ x (o , i) = extensionalV (λ z → ⇔toPath (fwd z) (bwd z))
      where
      fwd : (z : V ℓ) → ⟨ z ∈ DA.defSet ψ ⟩ → ⟨ z ∈ x .fst ⟩
      fwd z = rec₁ ((z ∈ x .fst) .snd)
```

第一の方向では、`DA.defSet ψ` への所属から、命題的切り詰めの下で `W` の要素の表示が得られる。充足の橋によって、その表示の一変数環境は `ψ` の充足集合に入り、`Cuts` の内向きの半分が、表示された集合を `x` に入れる。

```agda
        (λ { ((q , hq) , e) →
          i (down W z (subst (λ u → ⟨ u ∈ W .fst ⟩) e (ι∈ q)))
            (subst (λ u → ⟨ z ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ W .fst ⟩) e (ι∈ q)))
            (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) e
              (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁)) })
```

もう一方の方向では `z ∈ x` から始める。`Cuts` の外向きの半分は、`z ∈ W` と、その一変数環境が充足集合に属することの両方を与える。第一の事実は `∈-asFiber` によって、`W` の表示の実際の添字と、そこから `z` へ戻るパスに変換される。

```agda
      bwd : (z : V ℓ) → ⟨ z ∈ x .fst ⟩ → ⟨ z ∈ DA.defSet ψ ⟩
      bwd z hz =
        let zS = down x z hz
            zW = subst (λ u → ⟨ z ∈ u ⟩) qw (o zS hz .fst)
            fib = ∈-asFiber {a = z} {b = W .fst} zW
```

その表示のパスに沿って環境の所属を移し、`defSet-Sat` を逆向きに適用する。これにより表示が `DA.defSet ψ` に属することが分かり、同じパスに沿って戻せば `z ∈ DA.defSet ψ` が得られて、外延的な等式が完成する。

```agda
        in subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
             (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
               (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) (sym (fib .snd)) (o zS hz .snd)))
```

逆に、`DA.defSet ψ` がすでに `x` に等しいとする。`Cuts` を再構成するには、`x` の要素を `DA.defSet ψ` の要素へ書き換え、定義可能部分集合への所属を展開する。すると、その集合を `W` の要素として表すデータと、対応する一変数環境が充足集合に属する証明が同時に得られる。

```agda
    cuts-of : (ψ : Formula Ab 1) (x : S) → DA.defSet ψ ≡ x .fst → Cuts (x .fst) Wv ((Sat W (toS ψ)) .fst)
    cuts-of ψ x e = o , i
      where
      o : (z : S) → ⟨ z .fst ∈ x .fst ⟩ → ⟨ z .fst ∈ Wv ⟩ × ⟨ envOne (z .fst) ∈ (Sat W (toS ψ)) .fst ⟩
      o z hz = rec₁ (isProp× ((z .fst ∈ Wv) .snd) ((envOne (z .fst) ∈ (Sat W (toS ψ)) .fst) .snd))
```

この所属を展開すると、`W` の中の表示と、`defSet-Sat` を通じて、その一変数環境が必要な充足集合に属することが得られる。表示と元の要素との等式に沿って、二つの結論をどちらも `x` のその要素へ戻す。

```agda
        (λ { ((q , hq) , eq) →
            subst (λ u → ⟨ z .fst ∈ u ⟩) (sym qw) (subst (λ u → ⟨ u ∈ W .fst ⟩) eq (ι∈ q))
          , subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) eq (subst ⟨_⟩ (defSet-Sat W ψ q) ∣ (q , hq) , refl ∣₁) })
        (subst (λ u → ⟨ z .fst ∈ u ⟩) (sym e) hz)
      i : (z : S) → ⟨ z .fst ∈ Wv ⟩ → ⟨ envOne (z .fst) ∈ (Sat W (toS ψ)) .fst ⟩ → ⟨ z .fst ∈ x .fst ⟩
```

`Cuts` の内向きの半分では、`W` の表示された要素から始め、その一変数環境が `ψ` を満たすと仮定する。充足の橋がこれを `DA.defSet ψ` への所属に変え、仮定した等式 `DA.defSet ψ = x .fst` がその要素を `x` に入れる。

```agda
      i z hw he =
        let fib = ∈-asFiber {a = z .fst} {b = W .fst} (subst (λ u → ⟨ z .fst ∈ u ⟩) qw hw)
        in subst (λ u → ⟨ z .fst ∈ u ⟩) e
             (subst (λ u → ⟨ u ∈ DA.defSet ψ ⟩) (fib .snd)
               (subst ⟨_⟩ (sym (defSet-Sat W ψ (fib .fst)))
```

最後の輸送は、選んだ要素の表示とその基礎の集合を揃えるだけである。したがって `cut≡` と `cuts-of` を合わせると、`ψ` に対する `Cuts` 述語は、一つの定義可能部分集合 `DA.defSet ψ` との等しさに対応する。どちらの向きも定義論理式の一意性を主張しない。

```agda
                 (subst (λ u → ⟨ envOne u ∈ (Sat W (toS ψ)) .fst ⟩) (sym (fib .snd)) he)))
```

これで健全性を正確に述べられる。作業集合の枠が `W` と同一視され、数を表すタグが正しく、`satAt` が符号集合と充足関係表を正しく保証しているという前提の下で、`defAt` の充足は値の枠をちょうど `𝒟ₒ (W .fst)` に定める。ここで `𝒟ₒ` が集めるのは、`W` の要素をパラメータに使える一階論理式で定義される `W` の部分集合であり、完全な内部冪集合ではない。

```agda
  def-sound : ⟨ γ ⊨ defAt v w T C N ⟩ → Vv ≡ 𝒟ₒ (W .fst)
  def-sound hd = extensionalV (λ x → ⇔toPath (fwd x) (bwd x))
    where
    hm = defAt-out v w T C N γ hd .fst
    ha = defAt-out v w T C N γ hd .snd
```

順方向の包含では、所属の節が命題的切り詰めの下で、鍵の形をした符号、充足関係表の項目、その項目が切り出す部分集合を記述する条件を与える。`satAt` が候補の符号領域を実際のものと対応させた後、`decodeAll` は、符号が必要な第二成分をもつアリティ一の論理式が単に存在することだけを与える。続いて表の値の補題が、その項目の値をこの論理式の充足集合と同一視する。

```agda
    fwd : (x : V ℓ) → ⟨ x ∈ Vv ⟩ → ⟨ x ∈ 𝒟ₒ (W .fst) ⟩
    fwd x hx = rec₁ ((x ∈ 𝒟ₒ (W .fst)) .snd)
      (λ { (c , p , y , (c∈ , (ec , (e∈ , cuts)))) → rec₁ ((x ∈ 𝒟ₒ (W .fst)) .snd)
        (λ { (ψ , qp) →
          𝒟ₒ-intro (W .fst) x ∣ ψ , cut≡ ψ xS
```

`Cuts` の事実が、表の値の同定に沿って、復号された論理式の充足集合の中へ運ばれ、定義可能冪集合の導入が、切り出された集合を `𝒟ₒ` の中に置く。切り詰められた論理式の復号は、命題値の導入の中で消費される。

```agda
            (subst (λ u → Cuts x Wv u) (valOf ψ c y (ec ∙ cong (pr (# 1)) qp) e∈) cuts) ∣₁ })
        (decodeAll c (SR.C-out c c∈) 1 (p .fst) ec) })
      (RD.mem-out hm xS hx)
      where
      xS : S
```

値の枠は、所属の条項の外向きの読み出しのために、台の要素として提示される。

```agda
      xS = down (lookup v γ) x hx
```

逆向きの包含では、`𝒟ₒ (W .fst)` への所属から得られるのは、命題的に切り詰められた論理式 `ψ` と等式 `DA.defSet ψ = x` だけである。所属命題への消去の内部で、`defAt` の覆いの側が、この一時的な証人 `ψ` から作った鍵に対し、表の値と、値の枠に属する集合 `x'` を与える。

```agda
    bwd : (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (W .fst) ⟩ → ⟨ x ∈ Vv ⟩
    bwd x hx = rec₁ ((x ∈ Vv) .snd)
      (λ { (ψ , e) → rec₁ ((x ∈ Vv) .snd)
        (λ { (y , x' , (e∈ , (x'∈ , cuts))) →
          subst (λ u → ⟨ u ∈ Vv ⟩)
```

切り出しの等式が、表の値の同定に沿って運ばれて、切り出された集合の基礎の集合を復元し、輸送がそれを値の枠の中へ置く。

```agda
            (sym (cut≡ ψ x' (subst (λ u → Cuts (x' .fst) Wv u) (valOf ψ (keyS W ψ) y refl e∈) cuts)) ∙ e)
            x'∈ })
        (RD.all-out ha (keyS W ψ) (sndS (keyS W ψ) (# 1) (cd ψ) refl) (SR.C-in (keyS W ψ) (key∈AllCodes W ψ)) refl) })
      (𝒟ₒ-inv (W .fst) x hx)
```

完全性は同じ同値関係を逆向きにたどる。作業集合の同一視、正しいタグ、`satAt` を引き続き仮定すると、値の枠と `𝒟ₒ (W .fst)` との等式から `defAt` の充足を構成できる。二つの連言項はそれぞれ、列挙された各集合に定義論理式があることと、アリティ一の各論理式が定める部分集合が必ず現れることを示す。

```agda
  def-complete : Vv ≡ 𝒟ₒ (W .fst) → ⟨ γ ⊨ defAt v w T C N ⟩
  def-complete qv = defAt-in v w T C N γ mem all
    where
```

それぞれの論理式の表の項目は、すでに定義された再帰の表から選ばれる。その表は、表の中での所属と、明示的な充足集合との同定の両方を保証する。

```agda
    entry : (ψ : Formula Ab 1) → Σ[ y ∶ S ] (⟨ pr ((keyS W ψ) .fst) (y .fst) ∈ Tv ⟩ × (y .fst ≡ (Sat W (toS ψ)) .fst))
    entry ψ = Table.val W W (keyS W ψ) (key∈AllCodes W ψ)
            , ( SR.T-in (keyS W ψ) (key∈AllCodes W ψ)
              , cong (λ p → p .fst) (val-at W W ψ (keyS W ψ) (key∈AllCodes W ψ) refl) )
```

所属の連言項では、値の枠の要素を `𝒟ₒ (W .fst)` へ移し、`𝒟ₒ-inv` で展開する。定義論理式は命題的切り詰めの下でのみ存在する。その内部で論理式の鍵、対応する表の項目、必要な `Cuts` の証拠を組み立てるが、定義論理式を大域的に選んだり、標準的なデータとして保持したりはしない。

```agda
    mem : ⟨ γ ⊨ memAt v w T C N ⟩
    mem = RD.mem-in (λ x x∈ → map₁
      (λ { (ψ , e) →
        keyS W ψ , sndS (keyS W ψ) (# 1) (cd ψ) refl , entry ψ .fst
        , ( SR.C-in (keyS W ψ) (key∈AllCodes W ψ)
```

ここで用いる表の値は、再帰的な充足関係表がこの論理式の鍵に対してすでに定めた値である。その値と明示的な充足集合との等式に沿って `cuts-of` を移せば、切り出しの証拠が得られる。この一時的な論理式の証人は終始 `map₁` の内部にあり、得られる所属の証人も命題的に切り詰められたままである。

```agda
          , ( refl
            , ( entry ψ .snd .fst
              , subst (λ u → Cuts (x .fst) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ x e) ) ) ) })
      (𝒟ₒ-inv (W .fst) (x .fst) (subst (λ u → ⟨ x .fst ∈ u ⟩) qv x∈)))
```

覆いの連言項は、符号の領域の中の、アリティ一のキーそれぞれに対して証明される。対の分解が明示的に名指される。

```agda
    all : ⟨ γ ⊨ allAt v w T C N ⟩
    all = RD.all-in (λ c p c∈ ec → map₁
      (λ { (ψ , qp) →
        let qc : c .fst ≡ (keyS W ψ) .fst
            qc = ec ∙ cong (pr (# 1)) qp
```

与えられたアリティ一の鍵に対し、復号は、その第二成分を符号にもつ論理式 `ψ` が単に存在することだけを与える。定義可能部分集合 `DA.defSet ψ` は導入によって `𝒟ₒ (W .fst)` に属し、仮定した等式に沿う輸送で値の枠に入る。復号は一意な論理式や標準的な論理式を選ばない。

```agda
            xS : S
            xS = down (lookup v γ) (DA.defSet ψ)
                   (subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (W .fst) (DA.defSet ψ) ∣ ψ , refl ∣₁))
        in entry ψ .fst , xS
         , ( subst (λ u → ⟨ pr u ((entry ψ .fst) .fst) ∈ Tv ⟩) (sym qc) (entry ψ .snd .fst)
```

充足関係表は、復号された論理式の鍵に対応する値を与え、`cuts-of` は、その値が作業集合からちょうど `DA.defSet ψ` を切り出すことを示す。先ほど得た所属と合わせれば、これらのデータは覆いの条項を満たす。`decodeAll` の結果は命題的に切り詰められ、この命題値の条項にだけ消去されるので、構成は存在だけを記録し、復号された論理式を保持しない。

```agda
           , ( subst (λ u → ⟨ DA.defSet ψ ∈ u ⟩) (sym qv) (𝒟ₒ-intro (W .fst) (DA.defSet ψ) ∣ ψ , refl ∣₁)
             , subst (λ u → Cuts (DA.defSet ψ) Wv u) (sym (entry ψ .snd .snd)) (cuts-of ψ xS refl) ) ) })
      (decodeAll c (SR.C-out c c∈) 1 (p .fst) ec))
```

</div>
</details>

公開される健全性の向きは、後で実際に使う正確なインターフェースを示す。作業集合の枠が `W` を表し、`Tags` が数の枠を固定し、`satAt` が符号と充足のデータを保証すれば、`defAt` から `𝒟ₒ (W .fst)` との等しさが従う。したがって、この有界論理式が意図した意味をもつのは、このように整えられた背景の中である。

```agda
def-sound : ∀ {m} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m) (W : S)
          → (lookup w γ) .fst ≡ W .fst → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
          → ⟨ γ ⊨ defAt v w T C N ⟩ → (lookup v γ) .fst ≡ 𝒟ₒ (W .fst)
def-sound v w T C E N γ W qw tg hs = DefRead.def-sound v w T C E N γ W qw tg hs
```

公開される完全性の向きは同じ仮定をもち、含意を逆にする。`𝒟ₒ (W .fst)` との等しさから `defAt` の充足が再構成される。二つの定理を合わせると、各要素の代表論理式を選ぶことも、完全な内部冪集合と同一視することもなく、定義可能部分集合の集まりが特徴づけられる。

```agda
def-complete : ∀ {m} (v w T C E : Fin m) (N : Fin 10 → Fin m) (γ : Vec S m) (W : S)
             → (lookup w γ) .fst ≡ W .fst → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
             → (lookup v γ) .fst ≡ 𝒟ₒ (W .fst) → ⟨ γ ⊨ defAt v w T C N ⟩
def-complete v w T C E N γ W qw tg hs = DefRead.def-complete v w T C E N γ W qw tg hs
```