---
title: "定義可能な冪集合を表す論理式"
module: L.Coding.DefinablePowerSet
lang: ja
site: "Bedrock"
description: "定義可能な冪集合を表す論理式"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 69
canonical: https://bedrock.institute/ja/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/zh/L.Coding.DefinablePowerSet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 定義可能な冪集合を表す論理式

本章では論理式のコードと一様な充足関係を組み合わせ、台の定義可能な冪集合への所属を表す一階述語を定義し、その述語が自由変数一つの論理式で定義される部分集合をちょうど選び出すことを示します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

This is the step the whole route exists for. Every chapter before it built a
component at a carrier the caller *holds*: a set of `L`, named in a
formula as a constant. The internal hierarchy cannot hold its stage that way. Its
graph binds the stage, because a graph may not name the object it defines, and a
set enters a formula only by being named. So the description of the definable
powerset has to be speakable **under that binder**, with the carrier occupying a
slot of the ambient environment and nothing else.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

What the description says is what the operator is. `u` is the definable powerset
of the carrier when its members are exactly the sets carved out of the carrier by
a formula: there merely is a code `c` over the carrier and a value `v`, the value
is what the satisfaction recursion records at that code, and `u`'s member is the
set of members of the carrier whose one-entry environment lies in `v`. Three
conjuncts, and each is a chapter already delivered, read at a slot rather than at
a constant.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

One shape correction is forced and it is worth stating before the formula
appears. The code and the value are bound by **adjacent** existentials, with no
conjunct between them. Nested through an intervening conjunct the two hypotheses
land at different environments, and the route would acquire a weakening lemma it
otherwise never needs: the same formula, the same conjunct count, the same depth,
and a lemma's worth of difference.

</details>

```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` が両方向を証明します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Definability at arity one asks whether a formula holds of a single member, and
the satisfaction recursion answers at *environments*, so the two are joined by
the environment that assigns that member to the only variable there is. An
environment is its graph, and a graph of length one is a single pair: the numeral
zero with the value.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

That makes the reader one line. "The set at this slot has exactly the pairs
`(0, y)` as members" is `extAt` applied to the tag reader, and the tag
reader already delivers the equation between underlying sets, so nothing has to
be proved about pairs here at all.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Its two directions are hand-written over the one-element index type, and that is
a measurement rather than a taste. Reading a membership in a one-entry set back
is a two-case split, one case impossible; through a library round trip between
finite functions and vectors the same statement walled a chapter at over eight
minutes, and the chapter that met it wrote its two clauses by hand instead. This
one does the same.

</details>

```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` は、コード `w` に対応する充足関係の値 `v` に一項目環境が属する要素を、`x` がちょうど含むことを表します。三つの読取り補題が両方向とその同値性を示します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The third conjunct, alone, at three slots: the member, the carrier and the value
the satisfaction recursion recorded. It says that the member is the set of those
members of the carrier whose one-entry environment lies in that value, which is
the definable subset spelled out with the recursion in the place of satisfaction.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The condition is a conjunction rather than one clause because the carrier's bound
is not implied by the rest. A member of the recursion's value is an environment,
not a set of the carrier, so the second half alone would say nothing about where
the member came from; the definable subset is cut out of the carrier and the
formula has to say so.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Its two directions are `extAt`'s own two, and the existential inside the
condition is read by the previous section. Nothing here inspects the value, which
is why this section knows nothing about codes.

</details>

```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` の台の要素であることを認識します。導入・除去補題はこの論理式と明示的に符号化された論理式を相互に移します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Two conjuncts, both already proved, and this is only where they meet: the
argument is a key at arity one, and it has a closed, shaped witness at the
carrier the slot holds. The first is what tells the decode which arity to answer
at; the second is what the decode runs on. Neither names a set, so the pair can
be stated under any binder.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The pinned predicate of the code-set chapter is this same pair with one binder on
top, and that binder is the only thing separating a predicate a stage can hold
from a predicate a bound variable can carry.

</details>

```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` はその値の一意性を示します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The satisfaction recursion's graph was generalized to take its carrier as a slot,
and its two halves are the existence and uniqueness the recursion was built from,
restated at that slot and at a variable environment. Nothing is proved here that
was not proved then: existence hands over the subformula slot, the table over it,
   and the ten clauses, all three of which take the ambient environment as an
argument already; uniqueness reads the graph's own bound index set and table back
and applies the pinning theorem at the carrier the graph bound.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Both are stated with the code and the value reached by equations rather than
named, which is the law the value theorems were written under: naming a key puts
its construction inside a satisfaction, and the same statement then costs minutes
instead of seconds.

</details>

```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` は一般の台でこの記述を解釈するために必要な構成可能性の条件を記録します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The three conjuncts, under two adjacent existentials, under one extension: `u` is
the set of exactly those `x` for which there merely are a code `c` over the
carrier and a value `v` such that the recursion records `v` at `c` and `x` is
what `v` defines. That is the definable powerset, said in the object language,
with the carrier at a slot throughout.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The side condition is about what an object-language quantifier can reach. Every
existential in the description ranges over `L`, so the set the description picks
out can only contain constructible sets. If some definable subset of the carrier
were not constructible, the description would still be satisfied, by the set of
the constructible ones, and it would then hold of something that is not the
definable powerset. `DefOK` is exactly the absence of that gap.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

A carrier the caller holds needs no such condition **stated**, because a caller
that holds the carrier holds the theorem about it too. A carrier at a slot is
whatever the ambient environment puts there, and no theorem about it is available
under the binder, so the fact has to travel as a hypothesis and be discharged
where the slot is filled. It is a hypothesis of the elimination only: the
introduction is given that `u` **is** the definable powerset, and `u` is an
element of `L`, so its members are constructible already and the condition it
would have needed is implied by its own hypothesis.

</details>

```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` はそのような証人から対応する定義可能部分集合との等式を復元します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The two halves of the description at a single formula, which is what the
adequacy is assembled from. Supplying the three conjuncts for a formula `ψ` is
supplying its key for the code and the recursion's value for the value; reading
them back is decoding the code to a formula, pinning the value to the recursion's
own, and then reading the third conjunct as a set identity.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Everything here is stated at a **variable** carrier reached by an equation, and
that is what keeps the stage out of the proof. The instantiation at a stage is an
equation the caller supplies, and neither `Lset` nor an ordinal appears
anywhere below.

</details>

```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` は明示的な定義論理式から出発します。両者を合わせて完全な記述の導入・除去仕様を証明します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Assembling and describing are the per-member halves, and the two readings are
those under `extAt`'s own two directions. The introduction says that the
definable powerset satisfies the description: every member of it is a definable
subset, and the three conjuncts are supplied for the formula that defines it.
The elimination says that nothing else does, and it is the direction the side
condition is for, since a set the description holds of has to be re-entered
member by member, and each member either is an element of `L` or is absent
altogether.

</details>

```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` がその段階の定義可能な冪集合を直接定義することを示します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The instantiation is just one equation. A stage is an element of
`L`, its definable subsets are constructible because a stage is constructible one
stage later, and those two facts are what the successor identity delivers at
every stage at once. So the side condition is discharged for good, and what is
left is an equivalence of truth values: at a carrier holding a stage, the
description holds of a set exactly when that set **is** the definable powerset of
that stage. It holds of `𝒟ₒS` and of nothing else.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Neither statement mentions the stage as anything but the value of a slot, which
is what the internal hierarchy needs: the description will be spoken under a
binder, and the equation the caller supplies is the only thing that connects it
to a stage at all.

</details>

```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)
```

## まとめ

本章で得た有界論理式は、構成可能段階上で、その段階の要素をパラメータとしてその段階上で定義できる部分集合全体をちょうど外延とします。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

`DefAt` is the definable powerset described in the object language at a
carrier that is a slot, and `DefAt-in` and `DefAt-out` are its two
readings: the operator satisfies the description, and under `DefOK`
nothing else does. `DefAt-stage` instantiates both readings at a stage, where
the side condition is discharged once and for all and the description becomes an
equation between truth values.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Three chapters meet here and not one of them is re-proved. The code predicate is
read at a slot, the satisfaction graph is read at a slot, and the definable
subset is read through the bridge that says the recursion's value is satisfaction
over the carrier. What is new is only the joining: `envOneAt`, one line,
because an environment of length one is a single pair, and `DefinesAt`,
which is `extAt` over a two-part condition.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Two measurements are worth recording. The adjacency correction was adopted before
the first line was written and it cost nothing, so no weakening lemma exists
anywhere on this route. And the one difficulty met while writing was not in the
mathematics at all: the code predicate's elimination at a pinned carrier, with
the truncation's payload left to inference, ran past 140 seconds and was
terminated there, while the same two lines with the payload type written out
check in two seconds. Every `PT.rec` here names its payload, and that is
why this chapter checks in half a minute rather than not at all.

</details>