---
title: "可定义幂集的公式"
module: L.Coding.DefinablePowerSet
lang: zh
site: "Bedrock"
description: "可定义幂集的公式"
stage: "内部编码：表与统一满足关系"
reading_order: 69
canonical: https://bedrock.institute/zh/L.Coding.DefinablePowerSet.html
html: L.Coding.DefinablePowerSet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/DefinablePowerSet.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Definability, L.Axioms.Basic, L.Coding.Model, L.Coding.Expressions, L.Coding.Environment, L.Coding.FormulaRecovery, L.Coding.CodeSet, L.Coding.SatisfactionGraph, L.Coding.EnvironmentTower, L.Coding.Quantification, L.Coding.PinnedRecursion, L.Coding.SatisfactionTable, L.Coding.SlotClosure, L.Coding.Satisfaction, L.Coding.SatisfactionBridge, L.Coding.UniformSatisfaction]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.DefinablePowerSet.md, https://bedrock.institute/ja/L.Coding.DefinablePowerSet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 可定义幂集的公式

本章把公式编码与一致满足关系结合起来，定义一个表示属于载体可定义幂集的一阶谓词，并证明该谓词恰好选出由单自由变元公式定义的子集。

这就是整条路线为之存在的那一步。在它之前的每一章，构造的都是调用方**持有**的载体上的一个组件：`L` 的一个集合，在公式里被点名为常元。内部层级无法那样持有自己的层。它的图把层绑定起来，因为一个图不能点名它所定义的那个对象，而集合进入公式的唯一方式是被点名。故可定义幂集的描述必须能**在那层绑定之下**表述出来，其中载体只占周遭环境的一个位置，此外没有别的。

那条描述所说的，就是这个算子本身。`u` 是载体的可定义幂集，其诸成员恰是「由一条公式在载体中定义出的那些集合」：仅仅存在载体之上的一个码 `c` 与一个取值 `v`，该取值就是满足关系那场递归在那个码处所记录的东西，而 `u` 的那个成员是「其单条目环境落在 `v` 中的载体诸成员」之集。三个合取项，而每一个都是某章早已给出的东西，只是读在一位上、不读在常元上。

有一处形状上的修正是必须的，值得在公式出现之前先讲。码与取值由**相邻的**两个存在量词绑定，中间不隔任何合取项。若中间隔一个合取项再嵌套，那两条假设就会落在不同的环境上，于是这条路线将平白多出一条它永远用不着的弱化引理：同一条公式、同样的合取项数目、同样的深度，差别恰好是多出一条引理。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Coding.DefinablePowerSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _∈̇_; _∧̇_; ∃̇_ )
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; IsOrd; Lset; 𝒟ₒ; 𝒟ₒ-intro; 𝒟ₒ-inv )
open import L.Definability {ℓ} using ( module DefOf )
open import L.Axioms.Basic {ℓ} using ( 𝒟ₒ→isL; LsetS )
open import L.Coding.Model {ℓ} using ( domAt-out )
open import L.Coding.Expressions {ℓ} using ( extAt; extAt-out; extAt-in; extAt-in-both; tagAtL; tagAtL-adequate )
open import L.Coding.Environment {ℓ} using ( env )
open import L.Coding.FormulaRecovery {ℓ} using ( keyOf; keyOf-fst )
open import L.Coding.CodeSet {ℓ} lem
  using ( keyArityAtL; keyArityAtL-in; keyArityAtL-out; hasWitnessAt
        ; codeS; keyS; witnessAt-in; witnessAt-out )
open import L.Coding.SatisfactionGraph {ℓ} lem
  using ( satGraphAt; GraphWitAt; graphAt-in; graphAt-out
        ; Bi; Ti; Ci; Ei; NN; ev; numν )
open import L.Coding.EnvironmentTower {ℓ} lem using ( module Tower )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds )
open import L.Coding.SatisfactionTable {ℓ} lem
  using ( keyʟ; slot; satTable; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
open import L.Coding.SatisfactionBridge {ℓ} lem using ( asConst; defSet-Sat )
open import L.Coding.UniformSatisfaction {ℓ} lem using ( keyBridge; fr; frTags; frTow; frDom )

open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )

open hPropStructure 𝒮ʟ

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

## 只有一个条目的环境

`envOne v` 是把唯一自由变元赋值为 `v` 的图。公式 `envOneAt e y` 恰好识别该图，而 `envOneAt-in` 与 `envOneAt-out` 证明两个方向。

元数一处的可定义性，问的是一条公式对单个成员是否成立，而满足关系那场递归是在**环境**处作答的；把两者接起来的，正是「把那个成员指派给仅有的那一个变元」的环境。环境就是它的图，而长度为一的图只是一个对：数码零配上那个取值。

于是读式只有一行。「这一位上的集合，其成员恰是诸对 `(0, y)`」就是 `extAt` 施于标签读式，而标签读式本来就给出底集之间的那条等式，故这里完全不必再证任何关于对的事。

定义的两个方向都在那个单元素索引类型上手工写出，这是基于实测的取舍，而非风格偏好。把「属于一个单条目集合」解码回来，只需一次两分支的情形分析，其中一支不可能出现；若改走库里「有穷函数与向量」的路线，同一条陈述曾使某一章的处理耗时超过八分钟，遇到它的那一章于是改为手写两条子句。本章沿用这一做法。

```agda
envOne : V ℓ → V ℓ
envOne y = env {1} (λ _ → y)

envOneAt : ∀ {n} → Fin n → Fin n → Formula S n
envOneAt e y = extAt e (tagAtL zero 0 (suc y))

module _ {n : ℕ} (e y : Fin n) (γ : S ^ n) where
  private
    E : S
    E = lookup e γ

    v : V ℓ
    v = fst (lookup y γ)

    readEntry : (z : S) → ⟨ fst z ∈ envOne v ⟩ → fst z ≡ pr (# 0) v
    readEntry z = PT.rec (setIsSet (fst z) (pr (# 0) v))
      (λ { (lift zero , q) → sym q ; (lift (suc ()) , _) })

    entry∈ : (z : S) → fst z ≡ pr (# 0) v → ⟨ fst z ∈ envOne v ⟩
    entry∈ z q = ∣ lift zero , sym q ∣₁

  envOneAt-in : fst E ≡ envOne v → ⟨ γ ⊨ envOneAt e y ⟩
  envOneAt-in q = extAt-in-both e (tagAtL zero 0 (suc y)) γ fwd bwd
    where
    fwd : (z : S) → ⟨ fst z ∈ fst E ⟩ → ⟨ (z ∷ γ) ⊨ tagAtL zero 0 (suc y) ⟩
    fwd z z∈ = subst ⟨_⟩ (sym (tagAtL-adequate zero 0 (suc y) (z ∷ γ)))
      (readEntry z (subst (λ w → ⟨ fst z ∈ w ⟩) q z∈))

    bwd : (z : S) → ⟨ (z ∷ γ) ⊨ tagAtL zero 0 (suc y) ⟩ → ⟨ fst z ∈ fst E ⟩
    bwd z h = subst (λ w → ⟨ fst z ∈ w ⟩) (sym q)
      (entry∈ z (subst ⟨_⟩ (tagAtL-adequate zero 0 (suc y) (z ∷ γ)) h))

  envOneAt-out : ⟨ γ ⊨ envOneAt e y ⟩ → fst E ≡ envOne v
  envOneAt-out h = extensionalV (λ w → ⇔toPath (sub₁ w) (sub₂ w))
    where
    sub₁ : (w : V ℓ) → ⟨ w ∈ fst E ⟩ → ⟨ w ∈ envOne v ⟩
    sub₁ w w∈ = entry∈ wS (subst ⟨_⟩
        (tagAtL-adequate zero 0 (suc y) (wS ∷ γ))
        (extAt-out e (tagAtL zero 0 (suc y)) γ h wS w∈))
      where
      wS : S
      wS = w , isL-trans {x = fst E} {y = w} w∈ (snd E)

    sub₂ : (w : V ℓ) → ⟨ w ∈ envOne v ⟩ → ⟨ w ∈ fst E ⟩
    sub₂ w = PT.rec (snd (w ∈ fst E))
        (λ { (lift zero , q) →
               subst (λ u → ⟨ u ∈ fst E ⟩) (keyOf-fst 0 (lookup y γ) ∙ q) hasKey
           ; (lift (suc ()) , _) })
      where
      hasKey : ⟨ fst (keyOf 0 (lookup y γ)) ∈ fst E ⟩
      hasKey = extAt-in e (tagAtL zero 0 (suc y)) γ h (keyOf 0 (lookup y γ))
        (subst ⟨_⟩
          (sym (tagAtL-adequate zero 0 (suc y) (keyOf 0 (lookup y γ) ∷ γ)))
          (keyOf-fst 0 (lookup y γ)))
```

## 识别编码所定义的子集

`DefinesAt x w v` 表示 `x` 恰好包含如下元素：其单条目环境属于编码 `w` 所对应的满足关系值 `v`。三条读取引理分别给出两个方向及其等价。

单独取出第三个合取项来看，它涉及三样东西：那个成员、载体，以及满足关系递归所记录的取值。它说的是：那个成员恰是「其单条目环境落在该取值之中」的那些载体成员之集，也就是把可定义子集逐字写出，只是用递归取值代替了满足关系。

那个条件是一个合取而非单独一条子句，因为「属于载体」这一点不能由其余部分推出。递归取值的成员是一个环境，不是载体的子集，故仅凭后半句，对那个成员来自何处毫无说明；可定义子集本就取自载体，公式必须把这一点明确说出。

它的两个方向就是 `extAt` 自身的两个方向，条件中的存在量词由上一节读出。这里的任何步骤都不去查看那个取值，正因如此，本节无须涉及码的具体内容。

```agda
DefinesAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
DefinesAt x w v = extAt x ( (var zero ∈̇ var (suc w))
                          ∧̇ ∃̇ ( envOneAt zero (suc zero)
                               ∧̇ (var zero ∈̇ var (suc (suc v))) ) )

module _ {n : ℕ} (x w v : Fin n) (γ : S ^ n) where
  private
    inner : Formula S (suc n)
    inner = ∃̇ (envOneAt zero (suc zero) ∧̇ (var zero ∈̇ var (suc (suc v))))

    body : Formula S (suc n)
    body = (var zero ∈̇ var (suc w)) ∧̇ inner

    Holds : S → Type (ℓ-suc ℓ)
    Holds z = ⟨ fst z ∈ fst (lookup w γ) ⟩
              × ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩

    readInner : (z : S) → ⟨ (z ∷ γ) ⊨ inner ⟩
              → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
    readInner z = PT.rec (snd (envOne (fst z) ∈ fst (lookup v γ))) step
      where
      step : Σ[ E ∈ S ] ⟨ (E ∷ z ∷ γ)
               ⊨ (envOneAt zero (suc zero) ∧̇ (var zero ∈̇ var (suc (suc v)))) ⟩
           → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
      step (E , (hE , E∈)) = subst (λ u → ⟨ u ∈ fst (lookup v γ) ⟩)
        (envOneAt-out zero (suc zero) (E ∷ z ∷ γ) hE) E∈

    fillInner : (z : S) → ⟨ envOne (fst z) ∈ fst (lookup v γ) ⟩
              → ⟨ (z ∷ γ) ⊨ inner ⟩
    fillInner z h =
      ∣ E , (envOneAt-in zero (suc zero) (E ∷ z ∷ γ) refl , h) ∣₁
      where
      E : S
      E = envOne (fst z)
        , isL-trans {x = fst (lookup v γ)} {y = envOne (fst z)} h
            (snd (lookup v γ))

  DefinesAt-out : ⟨ γ ⊨ DefinesAt x w v ⟩
                → (z : S) → ⟨ fst z ∈ fst (lookup x γ) ⟩ → Holds z
  DefinesAt-out h z z∈ = hz .fst , readInner z (hz .snd)
    where
    hz : ⟨ (z ∷ γ) ⊨ body ⟩
    hz = extAt-out x body γ h z z∈

  DefinesAt-in : ⟨ γ ⊨ DefinesAt x w v ⟩
               → (z : S) → Holds z → ⟨ fst z ∈ fst (lookup x γ) ⟩
  DefinesAt-in h z (hw , hv) =
    extAt-in x body γ h z (hw , fillInner z hv)

  DefinesAt-both : ((z : S) → ⟨ fst z ∈ fst (lookup x γ) ⟩ → Holds z)
                 → ((z : S) → Holds z → ⟨ fst z ∈ fst (lookup x γ) ⟩)
                 → ⟨ γ ⊨ DefinesAt x w v ⟩
  DefinesAt-both f g = extAt-in-both x body γ
    (λ z z∈ → f z z∈ .fst , fillInner z (f z z∈ .snd))
    (λ z h → g z (h .fst , readInner z (h .snd)))
```

## 识别变元载体上的编码

`isCodeAt c w` 识别 `c` 是否为某个单自由变元公式的键，且该公式的常元都属于槽位 `w` 处的载体。引入与消去引理在此公式和显式编码公式之间转换。

两个合取项都已证明，这里只把它们结合起来：其一说实参是元数一处的一个键，其二说该键在「该槽位所持载体」上具有一个既封闭又成形的见证。前者确定解码所用的元数，后者提供解码所依据的数据。二者都不点名具体集合，因此可以在任意绑定之下陈述。

码集那一章所固定的那条谓词，就是这一对再加上一层绑定；而这层绑定正是「一层所能支撑的谓词」与「一个被绑定变元所能携带的谓词」之间唯一的差别。

```agda
isCodeAt : ∀ {n} → Fin n → Fin n → Formula S n
isCodeAt c w = keyArityAtL c 1 ∧̇ hasWitnessAt w c

module _ (A : S) where
  codeAt-in : ∀ {n} (c w : Fin n) (γ : S ^ n)
            → fst (lookup w γ) ≡ fst A
            → (ψ : Formula ⟪ fst A ⟫ 1) → fst (lookup c γ) ≡ fst (keyS A ψ)
            → ⟨ γ ⊨ isCodeAt c w ⟩
  codeAt-in c w γ qw ψ qc =
    keyArityAtL-in c 1 γ (codeS A ψ) qc , witnessAt-in A w c γ ψ qw qc

  codeAt-out : ∀ {n} (c w : Fin n) (γ : S ^ n)
             → fst (lookup w γ) ≡ fst A
             → ⟨ γ ⊨ isCodeAt c w ⟩
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ]
                   (fst (lookup c γ) ≡ fst (keyS A ψ))) ∥₁
  codeAt-out c w γ qw (hk , hw) =
    PT.rec squash₁ step (keyArityAtL-out c 1 γ hk)
    where
    step : Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# 1) (fst z))
         → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ]
               (fst (lookup c γ) ≡ fst (keyS A ψ))) ∥₁
    step (z , qz) = witnessAt-out A w c γ qw hw 1 z qz
```

## 变元载体上的满足关系

给定一条公式，其常元取自槽位 `w` 中载体的成员，`graphAt-holds` 在图中给出该公式的键与一致满足关系的取值，`graphAt-unique` 则证明此取值唯一。

满足关系递归的图已被推广为把满足关系那场递归中的载体取作一个位，其两半正是该递归赖以建立的存在性与唯一性，只是重新陈述于这个位上，并落到一个变元环境上。这里没有证明任何此前未证的事：存在性给出子公式槽、其上的那张表，以及十条子句，而这三者本来就把周遭环境取作实参；唯一性把图自身绑定的索引集与表读出，再在图所绑定的那个载体上施用钉住定理。

两者都以等式给出码与取值，而不是点名键；这正是诸取值定理写作时遵循的规则：一旦点名一个键，它的构造就会被并入一个满足关系，同一条陈述的验证时间于是从几秒变成几分钟。

```agda
module _ (B : S) where
  private
    toB : ∀ {n} → Formula ⟪ fst B ⟫ n → Formula S n
    toB = mapFo (asConst B)

  graphAt-holds : ∀ {m n} (ψ : Formula ⟪ fst B ⟫ m) (w c v : Fin n) (γ : S ^ n)
                → fst (lookup w γ) ≡ fst B
                → fst (lookup c γ) ≡ fst (keyʟ (toB ψ))
                → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
                → ⟨ γ ⊨ satGraphAt w c v ⟩
  graphAt-holds {m} {n} ψ w c v γ qw qc qv = graphAt-in w c v γ
    ∣ numν
    , (Tower.tower B
    , (slot B φ
    , (satTable B φ
    , (B
    , (sym qw
    , (frTags B φ γ
    , (frTow B φ γ
    , (slotClosed B φ (Tower.tower B ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
         ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)
    , (frDom B φ γ
    , (entry
    , SlotHolds.holds B Ti Bi Ci Ei NN (fr B φ γ) refl
        (frTags B φ γ) (frTow B φ γ) ψ refl refl)))))))))) ∣₁
    where
    φ : Formula S m
    φ = toB ψ

    entry : ⟨ pr (fst (lookup c γ)) (fst (lookup v γ)) ∈ fst (satTable B φ) ⟩
    entry = subst2 (λ a b → ⟨ pr a b ∈ fst (satTable B φ) ⟩)
      (sym qc) (sym qv) (entry-in B φ)

  graphAt-unique : ∀ {m n} (ψ : Formula ⟪ fst B ⟫ m) (w c v : Fin n) (γ : S ^ n)
                 → fst (lookup w γ) ≡ fst B
                 → fst (lookup c γ) ≡ fst (keyʟ (toB ψ))
                 → ⟨ γ ⊨ satGraphAt w c v ⟩
                 → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
  graphAt-unique {m} {n} ψ w c v γ qw qc h =
    PT.rec (setIsSet (fst (lookup v γ)) (fst (Sat B (toB ψ)))) step
      (graphAt-out w c v γ h)
    where
    step : GraphWitAt w c v γ → fst (lookup v γ) ≡ fst (Sat B (toB ψ))
    step (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12)))))))))))
      = SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) B (eb ∙ qw) tg hE hc h12
          ψ (subst (λ u → ⟨ u ∈ fst C ⟩) (qc ∙ sym (keyBridge B ψ))
               (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup c γ) (lookup v γ) ha))
          (lookup v γ)
          (subst (λ u → ⟨ pr u (fst (lookup v γ)) ∈ fst T ⟩)
             (qc ∙ sym (keyBridge B ψ)) ha)
```

## 可定义幂集的描述

`DefAt u w` 表示 `u` 的每个成员都由某个单自由变元编码及其图中取值在槽位 `w` 的载体上定义。`DefOK` 记录对一般载体解释该描述所需的可构造性条件。

三个合取项，压在两个相邻的存在量词之下，再压在一次外延之下：`u` 恰是那些 `x` 之集，对它们仅仅存在载体之上的一个码 `c` 与一个取值 `v`，使得那场递归在 `c` 处记录的是 `v`，而 `x` 就是 `v` 所定义的东西。这就是可定义幂集，用对象语言说出来，而载体自始至终待在一位上。

那个旁条件关乎对象语言的量词能取到哪些对象。描述里的每个存在量词都在 `L` 上取值，故这条描述所刻画的集合只能包含可构造集。若载体的某个可定义子集不可构造，这条描述仍会被满足，只是满足它的将是「诸可构造者之集」，于是它对一个并非可定义幂集的东西成立。`DefOK` 所说的正是这一缺口不会出现。

能在调用处取得载体的调用方无须**写出**这样的条件，因为持有载体的调用方同时掌握关于它的定理。处于一位上的载体则是周遭环境放在那里的任何东西，在那层绑定之下没有关于它的定理可用，故这个条件必须作为假设随证明传递，并在该位被填上之处解除。这个条件只附加在消去那一半：引入方向被给定 `u` **就是**可定义幂集，且 `u` 是 `L` 的元素，故其成员本就可构造，它本会需要的那个条件由它自身的假设蕴含。

```agda
private
  sh3 : ∀ {n} → Fin n → Fin (suc (suc (suc n)))
  sh3 i = suc (suc (suc i))

DefBody : ∀ {n} → Fin n → Formula S (suc (suc (suc n)))
DefBody w = isCodeAt (suc zero) (sh3 w)
            ∧̇ ( satGraphAt (sh3 w) (suc zero) zero
              ∧̇ DefinesAt (suc (suc zero)) (sh3 w) zero )

DefAt : ∀ {n} → Fin n → Fin n → Formula S n
DefAt u w = extAt u (∃̇ (∃̇ (DefBody w)))

DefOK : S → Type (ℓ-suc ℓ)
DefOK A = (x : V ℓ) → ⟨ x ∈ 𝒟ₒ (fst A) ⟩ → ⟨ isL x ⟩
```

## 单个定义公式的两个方向

对固定的单自由变元公式，`fill` 为其可定义子集构造见证，证明它满足 `DefAt`；`read` 则从这类见证恢复出与相应可定义子集的相等。

描述的两半落在单独一条公式上，充分性正是由它们组合而成的。对一条公式 `ψ`，那三个合取项分别把它的键供给码、把递归的取值供给取值；反过来读取时，则把码解码成一条公式，把取值与递归自身的取值对上，再把第三个合取项读作一条集合等式。

此处的一切都陈述在**变元**载体上，只经过一条等式，而正是这一点把层挡在证明之外。在某一层处的实例化只是调用方提供的一条等式，而 `Lset` 与序数在下文任何地方都不出现。

```agda
module _ (A : S) where
  private
    module DA = DefOf (fst A)

    toS : Formula ⟪ fst A ⟫ 1 → Formula S 1
    toS ψ = mapFo (asConst A) ψ

    defined-membership : (ψ : Formula ⟪ fst A ⟫ 1) (y : V ℓ)
                       → (y ∈ DA.defSet ψ)
                       ≡ ((y ∈ fst A) ⊓ (envOne y ∈ fst (Sat A (toS ψ))))
    defined-membership ψ y = ⇔toPath out inn
      where
      at : ⟨ y ∈ fst A ⟩ → (y ∈ DA.defSet ψ) ≡ (envOne y ∈ fst (Sat A (toS ψ)))
      at hy = cong (λ u → u ∈ DA.defSet ψ) (sym e)
        ∙ defSet-Sat A ψ m ∙ cong (λ u → envOne u ∈ fst (Sat A (toS ψ))) e
        where
        m = ∈-asFiber {a = y} {b = fst A} hy .fst
        e = ∈-asFiber {a = y} {b = fst A} hy .snd
      out : ⟨ y ∈ DA.defSet ψ ⟩ → ⟨ y ∈ fst A ⟩ × ⟨ envOne y ∈ fst (Sat A (toS ψ)) ⟩
      out h = DA.defSet⊆A ψ y h , subst ⟨_⟩ (at (DA.defSet⊆A ψ y h)) h
      inn : ⟨ y ∈ fst A ⟩ × ⟨ envOne y ∈ fst (Sat A (toS ψ)) ⟩ → ⟨ y ∈ DA.defSet ψ ⟩
      inn (hy , h) = subst ⟨_⟩ (sym (at hy)) h

  fill : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
       → (z : S) (ψ : Formula ⟪ fst A ⟫ 1) → DA.defSet ψ ≡ fst z
       → ⟨ (Sat A (toS ψ) ∷ keyS A ψ ∷ z ∷ γ) ⊨ DefBody w ⟩
  fill {n} w γ qw z ψ qz = hcode , (hgraph , hdef)
    where
    δ : S ^ (suc (suc (suc n)))
    δ = Sat A (toS ψ) ∷ keyS A ψ ∷ z ∷ γ

    hcode : ⟨ δ ⊨ isCodeAt (suc zero) (sh3 w) ⟩
    hcode = codeAt-in A (suc zero) (sh3 w) δ qw ψ refl

    hgraph : ⟨ δ ⊨ satGraphAt (sh3 w) (suc zero) zero ⟩
    hgraph = graphAt-holds A ψ (sh3 w) (suc zero) zero δ qw
               (keyBridge A ψ) refl

    Holds : S → Type (ℓ-suc ℓ)
    Holds y = ⟨ fst y ∈ fst (lookup w γ) ⟩
              × ⟨ envOne (fst y) ∈ fst (Sat A (toS ψ)) ⟩

    agrees : (y : S) → (fst y ∈ fst z)
           ≡ ((fst y ∈ fst (lookup w γ)) ⊓ (envOne (fst y) ∈ fst (Sat A (toS ψ))))
    agrees y = cong (λ X → fst y ∈ X) (sym qz)
      ∙ defined-membership ψ (fst y)
      ∙ cong (λ X → (fst y ∈ X) ⊓ (envOne (fst y) ∈ fst (Sat A (toS ψ)))) (sym qw)

    into : (y : S) → ⟨ fst y ∈ fst z ⟩ → Holds y
    into y = subst ⟨_⟩ (agrees y)

    back : (y : S) → Holds y → ⟨ fst y ∈ fst z ⟩
    back y = subst ⟨_⟩ (sym (agrees y))

    hdef : ⟨ δ ⊨ DefinesAt (suc (suc zero)) (sh3 w) zero ⟩
    hdef = DefinesAt-both (suc (suc zero)) (sh3 w) zero δ into back

  read : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
       → (z c v : S) → ⟨ (v ∷ c ∷ z ∷ γ) ⊨ DefBody w ⟩
       → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
  read {n} w γ qw z c v (hcode , (hgraph , hdef)) =
    PT.rec squash₁ step (codeAt-out A (suc zero) (sh3 w) δ qw hcode)
    where
    δ : S ^ (suc (suc (suc n)))
    δ = v ∷ c ∷ z ∷ γ

    step : Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (fst c ≡ fst (keyS A ψ))
         → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
    step (ψ , qc) = ∣ ψ , extensionalV (λ y → ⇔toPath (into y) (back y)) ∣₁
      where
      qv : fst v ≡ fst (Sat A (toS ψ))
      qv = graphAt-unique A ψ (sh3 w) (suc zero) zero δ qw
             (qc ∙ keyBridge A ψ) hgraph

      into : (y : V ℓ) → ⟨ y ∈ DA.defSet ψ ⟩ → ⟨ y ∈ fst z ⟩
      into y hy = DefinesAt-in (suc (suc zero)) (sh3 w) zero δ hdef
        (y , isL-trans (DA.defSet⊆A ψ y hy) (snd A))
        (subst (λ X → ⟨ y ∈ X ⟩) (sym qw) (h .fst)
        , subst (λ X → ⟨ envOne y ∈ X ⟩) (sym qv) (h .snd))
        where h = subst ⟨_⟩ (defined-membership ψ y) hy

      back : (y : V ℓ) → ⟨ y ∈ fst z ⟩ → ⟨ y ∈ DA.defSet ψ ⟩
      back y hy = subst ⟨_⟩ (sym (defined-membership ψ y))
        (subst (λ X → ⟨ y ∈ X ⟩) qw (h .fst)
        , subst (λ X → ⟨ envOne y ∈ X ⟩) qv (h .snd))
        where
        h = DefinesAt-out (suc (suc zero)) (sh3 w) zero δ hdef
          (y , isL-trans hy (snd z)) hy
```

## 读取并组装描述

`describe` 按满足关系的值读取 `DefAt` 的见证，而 `assemble` 从显式定义的公式出发。两者合起来证明完整描述的引入与消去规格。

装配与描述是处理逐成员情形的两半，两种读法就是把它们分别放到 `extAt` 自身的两个方向上。引入方向说：可定义幂集满足这条描述，即它的每个成员都是一个可定义子集，而那三个合取项由「定义它的那条公式」给出。消去方向说：别的东西都不满足；这里正是那个旁条件起作用的地方，因为一个满足描述的集合要逐成员地重新进入，而每个成员要么是 `L` 的元素，要么根本不在其中。

```agda
  private
    describe : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
             → (z : S) → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
    describe w γ qw z = PT.rec squash₁ viaCode
      where
      Target : Type (ℓ-suc ℓ)
      Target = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁

      viaValue : (c : S)
               → Σ[ v ∈ S ] ⟨ (v ∷ c ∷ z ∷ γ) ⊨ DefBody w ⟩ → Target
      viaValue c (v , hv) = read w γ qw z c v hv

      viaCode : Σ[ c ∈ S ] ⟨ (c ∷ z ∷ γ) ⊨ ∃̇ (DefBody w) ⟩ → Target
      viaCode (c , hc) = PT.rec squash₁ (viaValue c) hc

    assemble : ∀ {n} (w : Fin n) (γ : S ^ n) → fst (lookup w γ) ≡ fst A
             → (z : S)
             → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)) ∥₁
             → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
    assemble w γ qw z = PT.rec (snd ((z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)))) step
      where
      step : Σ[ ψ ∈ Formula ⟪ fst A ⟫ 1 ] (DA.defSet ψ ≡ fst z)
           → ⟨ (z ∷ γ) ⊨ ∃̇ (∃̇ (DefBody w)) ⟩
      step (ψ , qψ) = ∣ keyS A ψ , ∣ Sat A (toS ψ) , fill w γ qw z ψ qψ ∣₁ ∣₁

  DefAt-in : ∀ {n} (u w : Fin n) (γ : S ^ n)
           → fst (lookup w γ) ≡ fst A
           → fst (lookup u γ) ≡ 𝒟ₒ (fst A)
           → ⟨ γ ⊨ DefAt u w ⟩
  DefAt-in {n} u w γ qw qu = extAt-in-both u Φ γ f g
    where
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (DefBody w))

    f : (z : S) → ⟨ fst z ∈ fst (lookup u γ) ⟩ → ⟨ (z ∷ γ) ⊨ Φ ⟩
    f z z∈ = assemble w γ qw z
      (𝒟ₒ-inv (fst A) (fst z) (subst (λ X → ⟨ fst z ∈ X ⟩) qu z∈))

    g : (z : S) → ⟨ (z ∷ γ) ⊨ Φ ⟩ → ⟨ fst z ∈ fst (lookup u γ) ⟩
    g z hz = subst (λ X → ⟨ fst z ∈ X ⟩) (sym qu)
      (𝒟ₒ-intro (fst A) (fst z) (describe w γ qw z hz))

  DefAt-out : ∀ {n} (u w : Fin n) (γ : S ^ n) → DefOK A
            → fst (lookup w γ) ≡ fst A
            → ⟨ γ ⊨ DefAt u w ⟩
            → fst (lookup u γ) ≡ 𝒟ₒ (fst A)
  DefAt-out {n} u w γ ok qw h =
    extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))
    where
    Φ : Formula S (suc n)
    Φ = ∃̇ (∃̇ (DefBody w))

    sub₁ : (y : V ℓ) → ⟨ y ∈ fst (lookup u γ) ⟩ → ⟨ y ∈ 𝒟ₒ (fst A) ⟩
    sub₁ y y∈ = 𝒟ₒ-intro (fst A) y (describe w γ qw yS (extAt-out u Φ γ h yS y∈))
      where
      yS : S
      yS = y , isL-trans {x = fst (lookup u γ)} {y = y} y∈ (snd (lookup u γ))

    sub₂ : (y : V ℓ) → ⟨ y ∈ 𝒟ₒ (fst A) ⟩ → ⟨ y ∈ fst (lookup u γ) ⟩
    sub₂ y y∈ = extAt-in u Φ γ h yS (assemble w γ qw yS (𝒟ₒ-inv (fst A) y y∈))
      where
      yS : S
      yS = y , ok y y∈
```

## 可构造层上的可定义幂集

当载体为可构造层时，其公式编码与一致满足关系对象已经属于 `L`，因此 `DefOK` 自动成立。所得特化直接表明 `DefAt` 定义该层的可定义幂集。

该实例化只需一条等式。层是 `L` 的元素，其可定义子集也可构造 (因为层在下一层可构造)；后继恒等式在每层同时给出这两点。因此旁条件一次得到解除，剩下的是真值之间的等价：在持有该层的载体上，这条描述对某个集合成立，当且仅当该集合**就是**此层的可定义幂集。它对 `𝒟ₒS` 成立，对其他集合都不成立。

两条陈述都只把那一层当作某一位的取值提到，而这正是内部层级所需要的：那条描述将在一层绑定之下被说出，而调用方提供的那条等式，是唯一把它与某一层联系起来的东西。

```agda
DefAt-stage : (β : V ℓ) (oβ : IsOrd β) → ∀ {n} (u w : Fin n) (γ : S ^ n)
            → fst (lookup w γ) ≡ Lset β
            → (γ ⊨ DefAt u w)
              ≡ ( (fst (lookup u γ) ≡ 𝒟ₒ (Lset β))
                , setIsSet (fst (lookup u γ)) (𝒟ₒ (Lset β)) )
DefAt-stage β oβ u w γ qw = ⇔toPath
  (DefAt-out (LsetS β oβ) u w γ (𝒟ₒ→isL β oβ) qw)
  (DefAt-in (LsetS β oβ) u w γ qw)
```

## 小结

本章得到一个有界公式；在可构造层上，其外延恰为可用该层中的参数在该层上定义的子集全体。

`DefAt` 是可定义幂集在对象语言中相对于槽位载体的描述，`DefAt-in` 与 `DefAt-out` 是它的两条读式：该算子满足描述；在 `DefOK` 条件下，其他对象都不满足。`DefAt-stage` 把两条读式实例化到一层；在那里旁条件一次得到解除，描述也化为真值之间的等式。

三章在此汇合，没有一章需要重证。码谓词读在一个位置上，满足关系的图也读在一个位置上，而可定义子集经由那座桥读出，桥的内容是「递归的取值就是载体之上的满足关系」。新增的只有接合处：`envOneAt`，一行，因为长度为一的环境只是一个对；以及 `DefinesAt`，它就是 `extAt` 施于一个两部分的条件。

有两处测量值得记录。相邻那处更正在第一行写下之前就已采纳，未付出额外代价，故这条路线上任何地方都不存在弱化引理。写作期间唯一的困难根本不在数学里：码谓词在固定载体处的消去，若把截断的载荷交给推断，要跑 140 秒并在那里被终止；而同样两行，把载荷的类型显式写出，两秒即检查完毕。此处每一次 `PT.rec` 都指明了自己的载荷，这正是本章能在半分钟内、而不是根本无法检查完的原因。