---
title: "任意の論理式に対する反映"
module: L.FormulaReflection
lang: ja
site: "Bedrock"
description: "任意の論理式に対する反映"
stage: "構成可能段階と公理"
reading_order: 34
canonical: https://bedrock.institute/ja/L.FormulaReflection.html
html: L.FormulaReflection.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/FormulaReflection.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantBounding, FOL.Manipulation.Relativization, FOL.Absoluteness, V.Hierarchy, L.Constructible, L.Ordinal, L.Axioms.Basic, L.Axioms.Separation, L.ExistentialReflection]
routes: [constructible-axioms]
translations: [https://bedrock.institute/en/L.FormulaReflection.md, https://bedrock.institute/zh/L.FormulaReflection.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 任意の論理式に対する反映

論理式全体の反映では、その構文に現れるすべての存在部分論理式へ答える必要があります。論理式に沿って共同の閉性条件と順序数の梯子を再帰的に作り、その論理式が構成可能宇宙全体と同じ真理値を持つ段階を得ます。

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

The proof is structural induction, and it needs two things of the stage. At an
unbounded quantifier it needs the previous chapter's closure, for the quantifier's
own matrix. At a bounded quantifier it needs the bound to lie in the stage, so
that anything the bound admits does too; that is the constants condition the
separation chapter already knows how to meet.

</details>

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

No single-matrix limit can serve all the matrices at once, because closure is not
inherited by larger stages: enlarging the stage admits more environments to
answer for. So the ladder is built jointly. One rung's step merges, over the
formula's structure, the single-matrix step of every matrix in it, together with
the stage holding the constants. The limit then answers for every matrix, and the
previous chapter's argument applies to each without being run again.

</details>

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊥̇
        ; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
```

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

lint-agda: keep (⊤̇ names the defining formula behind `LsetS`)

</details>

```agda
open import FOL.Manipulation.ConstantBounding using ( BoundedTm; BoundedFo )
open import FOL.Manipulation.Relativization using ( relativize; module Correct )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( ∅-ord; bound2 )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Axioms.Separation {ℓ} lem
  using ( Below′; liftFoTo; mkBoundedFo )
open import L.ExistentialReflection {ℓ} lem
  using ( Below; LsetEnv; pickStage; ClosedFor; module Ladder; module Single )

open import Cubical.Data.Unit using ( Unit*; tt* )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
import Cubical.Data.Empty as Empty
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )

open hPropStructure 𝒮ʟ using ( S )

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

## 段階そのものを要素にする

推移的な段階 `Lset σ` は、その全体を定義する恒真な論理式によって次の定義可能段階に現れます。この事実により、後の閉性構成は段階自身をより大きな段階の要素として保持できます。

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

The certificate is sealed, and only it: the stage as an element of the model is
the pair of the stage with the certificate, and the first component has to keep
reducing, since "lies in the bound" and "lies in the stage" are the same
statement only because it does. The certificate is a different matter. It unfolds
through definability into the smallness machinery, and it sits inside a constant,
so every consumer that mentions the constant in a type would carry that unfolding
along; a chapter that separates with a relativized formula takes minutes rather
than seconds without this one line.

</details>

```agda
module Cor (β : V ℓ) (oβ : IsOrd β) =
  Correct 𝒮ʟ id (LsetS β oβ)
```

## 段階が論理式に対して満たす条件

`Answers φ σ τ` は、`σ` から取った環境の下で `φ` の存在部分論理式が真なら、`τ` が対応する証人を含むことを構文に沿って記録します。この条件は `τ` を大きくすると保存されます。

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

A universal quantifier contributes the step for the *negated* matrix, because the
argument for it is by contradiction: to know that everything in the stage
satisfies the matrix is to know that nothing in L refutes it, and the refutation
is what has to be included in the stage.

</details>

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

These conditions only grow easier to satisfy as the rung grows, since each entry
is a membership and membership is inherited through an ordinal. That is what
lets the merges below raise the pieces to their join.

</details>

```agda
Answers : ∀ {n} (φ : Formula S n) (σ : V ℓ) (oσ : IsOrd σ) (τ : V ℓ)
        → Type (ℓ-suc ℓ)
Answers (t ∈̇ u)  σ oσ τ = Unit*
Answers (t ≐ u)  σ oσ τ = Unit*
Answers (φ ∧̇ ψ)  σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ
Answers (φ ∨̇ ψ)  σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ
Answers (φ ⇒̇ ψ)  σ oσ τ = Answers φ σ oσ τ × Answers ψ σ oσ τ
Answers ⊥̇        σ oσ τ = Unit*
Answers (∃̇ φ)    σ oσ τ = ⟨ Single.Fstep φ σ oσ ∈ τ ⟩ × Answers φ σ oσ τ
Answers (∀̇ φ)    σ oσ τ = ⟨ Single.Fstep (¬̇ φ) σ oσ ∈ τ ⟩ × Answers φ σ oσ τ
Answers (∀̇∈ t φ) σ oσ τ = Answers φ σ oσ τ
Answers (∃̇∈ t φ) σ oσ τ = Answers φ σ oσ τ

Answers-mono : {τ τ' : V ℓ} → ⟨ τ ∈ τ' ⟩ → IsOrd τ'
             → ∀ {n} (φ : Formula S n) (σ : V ℓ) (oσ : IsOrd σ)
             → Answers φ σ oσ τ → Answers φ σ oσ τ'
Answers-mono h o (t ∈̇ u)  σ oσ _        = tt*
Answers-mono h o (t ≐ u)  σ oσ _        = tt*
Answers-mono h o (φ ∧̇ ψ)  σ oσ (a , b) =
  Answers-mono h o φ σ oσ a , Answers-mono h o ψ σ oσ b
Answers-mono h o (φ ∨̇ ψ)  σ oσ (a , b) =
  Answers-mono h o φ σ oσ a , Answers-mono h o ψ σ oσ b
Answers-mono h o (φ ⇒̇ ψ)  σ oσ (a , b) =
  Answers-mono h o φ σ oσ a , Answers-mono h o ψ σ oσ b
Answers-mono h o ⊥̇        σ oσ _        = tt*
Answers-mono {τ} h o (∃̇ φ) σ oσ (F , a) =
  o .fst {x = τ} {y = Single.Fstep φ σ oσ} F h , Answers-mono h o φ σ oσ a
Answers-mono {τ} h o (∀̇ φ) σ oσ (F , a) =
  o .fst {x = τ} {y = Single.Fstep (¬̇ φ) σ oσ} F h , Answers-mono h o φ σ oσ a
Answers-mono h o (∀̇∈ t φ) σ oσ a        = Answers-mono h o φ σ oσ a
Answers-mono h o (∃̇∈ t φ) σ oσ a        = Answers-mono h o φ σ oσ a
```

## 共同の一段階

論理式の各構成子について、その部分論理式が要求する解答段階を一つの順序数上界へまとめます。存在量化子では母式への一段階の反映も加え、論理式全体の要求を同時に満たします。

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

Each shape is written once, over an arbitrary payload with an arbitrary way of
raising it, so the recursion itself is ten one-line clauses and the ordinal
bookkeeping is not restated at each. The alternative, which is what one writes
first, is three parallel recursions of ten clauses each computing the ordinal,
its ordinality, and the rung's membership in it; they all traverse the same tree
and project the same bounds.

</details>

```agda
private
  Box : (σ : V ℓ) (P : V ℓ → Type (ℓ-suc ℓ)) → Type (ℓ-suc ℓ)
  Box σ P = Σ[ τ ∈ V ℓ ] (IsOrd τ × ⟨ σ ∈ τ ⟩ × P τ)

  Raise : (P : V ℓ → Type (ℓ-suc ℓ)) → Type (ℓ-suc ℓ)
  Raise P = {τ τ' : V ℓ} → ⟨ τ ∈ τ' ⟩ → IsOrd τ' → P τ → P τ'

  unitBox : (σ : V ℓ) (oσ : IsOrd σ) → Box σ (λ _ → Unit*)
  unitBox σ oσ = b .fst , (b .snd .fst , (b .snd .snd .fst , tt*))
    where b = bound2 σ σ oσ oσ

  joinBox : {σ : V ℓ} {P Q : V ℓ → Type (ℓ-suc ℓ)} → Raise P → Raise Q
          → Box σ P → Box σ Q → Box σ (λ τ → P τ × Q τ)
  joinBox {σ} rP rQ (τ₁ , (o₁ , (s₁ , p))) (τ₂ , (o₂ , (_ , q))) =
    b .fst
    , ( ob
      , ( ob .fst {x = τ₁} {y = σ} s₁ (b .snd .snd .fst)
        , ( rP (b .snd .snd .fst) ob p , rQ (b .snd .snd .snd) ob q ) ) )
    where
    b  = bound2 τ₁ τ₂ o₁ o₂
    ob = b .snd .fst

  addBox : {σ : V ℓ} {P : V ℓ → Type (ℓ-suc ℓ)} → Raise P
         → (F : V ℓ) → IsOrd F → Box σ P → Box σ (λ τ → ⟨ F ∈ τ ⟩ × P τ)
  addBox {σ} rP F oF (τ , (oτ , (s , p))) =
    b .fst
    , ( ob
      , ( ob .fst {x = τ} {y = σ} s (b .snd .snd .snd)
        , ( b .snd .snd .fst , rP (b .snd .snd .snd) ob p ) ) )
    where
    b  = bound2 F τ oF oτ
    ob = b .snd .fst

  raiseAns : ∀ {n} (φ : Formula S n) (σ : V ℓ) (oσ : IsOrd σ)
           → Raise (Answers φ σ oσ)
  raiseAns φ σ oσ h o = Answers-mono h o φ σ oσ

gstep : ∀ {n} (φ : Formula S n) (σ : V ℓ) (oσ : IsOrd σ) → Box σ (Answers φ σ oσ)
gstep (t ∈̇ u)  σ oσ = unitBox σ oσ
gstep (t ≐ u)  σ oσ = unitBox σ oσ
gstep (φ ∧̇ ψ)  σ oσ = joinBox (raiseAns φ σ oσ) (raiseAns ψ σ oσ)
                        (gstep φ σ oσ) (gstep ψ σ oσ)
gstep (φ ∨̇ ψ)  σ oσ = joinBox (raiseAns φ σ oσ) (raiseAns ψ σ oσ)
                        (gstep φ σ oσ) (gstep ψ σ oσ)
gstep (φ ⇒̇ ψ)  σ oσ = joinBox (raiseAns φ σ oσ) (raiseAns ψ σ oσ)
                        (gstep φ σ oσ) (gstep ψ σ oσ)
gstep ⊥̇        σ oσ = unitBox σ oσ
gstep (∃̇ φ)    σ oσ = addBox (raiseAns φ σ oσ)
                        (Single.Fstep φ σ oσ) (Single.Fstep-ord φ σ oσ)
                        (gstep φ σ oσ)
gstep (∀̇ φ)    σ oσ = addBox (raiseAns φ σ oσ)
                        (Single.Fstep (¬̇ φ) σ oσ) (Single.Fstep-ord (¬̇ φ) σ oσ)
                        (gstep φ σ oσ)
gstep (∀̇∈ t φ) σ oσ = gstep φ σ oσ
gstep (∃̇∈ t φ) σ oσ = gstep φ σ oσ
```

## 共同の梯子

共同の一段階を自然数回反復し、その極限を取ります。有限段階ごとの解答条件が単調性によって極限へ移るため、極限段階は論理式のすべての部分に対して閉じます。

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

Two readings come off the step for free, because they were built into it. The
extra ordinal is in the first rung, hence under the limit. And at every rung, the
whole tree of memberships holds against the next rung, which is the answering
hypothesis in the form the induction wants.

</details>

```agda
module Mk {n : ℕ} (φ₀ : Formula S n) (κ : V ℓ) (oκ : IsOrd κ)
          (bdd : BoundedFo (Below′ κ) φ₀) where

  private
    jstep : (σ : V ℓ) (oσ : IsOrd σ)
          → Box σ (λ τ → ⟨ κ ∈ τ ⟩ × Answers φ₀ σ oσ τ)
    jstep σ oσ = addBox (raiseAns φ₀ σ oσ) κ oκ (gstep φ₀ σ oσ)

  Gₙ : ℕ → V ℓ
  Gₙ-ord : (N : ℕ) → IsOrd (Gₙ N)
  Gₙ zero        = ∅
  Gₙ (suc N)     = jstep (Gₙ N) (Gₙ-ord N) .fst
  Gₙ-ord zero    = ∅-ord
  Gₙ-ord (suc N) = jstep (Gₙ N) (Gₙ-ord N) .snd .fst

  Gₙ-step : (N : ℕ) → ⟨ Gₙ N ∈ Gₙ (suc N) ⟩
  Gₙ-step N = jstep (Gₙ N) (Gₙ-ord N) .snd .snd .fst

  module Lad = Ladder Gₙ Gₙ-ord Gₙ-step

  β : V ℓ
  β = Lad.top

  oβ : IsOrd β
  oβ = Lad.top-ord

  κ∈β : ⟨ κ ∈ β ⟩
  κ∈β = oβ .fst {x = Gₙ 1} {y = κ}
          (jstep ∅ ∅-ord .snd .snd .snd .fst) (Lad.G∈top 1)

  answersAt : (N : ℕ) → Answers φ₀ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N))
  answersAt N = jstep (Gₙ N) (Gₙ-ord N) .snd .snd .snd .snd
```

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

Reading these conditions back off gives closure. At a rung, the tree gives that the matrix's
step function lies inside the next rung, and the previous chapter gives that the matrix's
answering stage is inside its step function; ordinal transitivity composes them
into the answering hypothesis, and the ladder's closure follows.

</details>

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

Two auxiliary facts let the induction start: membership in a stage is
inherited downward, since a stage is transitive, and a term's value lies in the
stage, a constant because it was registered and a variable because the
environment lies there.

</details>

```agda
  private
    closureOf : {k : ℕ} (ψ : Formula S (suc k))
              → ((N : ℕ) → ⟨ Single.Fstep ψ (Gₙ N) (Gₙ-ord N) ∈ Gₙ (suc N) ⟩)
              → ClosedFor β ψ
    closureOf ψ lands = Lad.closure ψ
      (λ N ms → Gₙ-ord (suc N) .fst
                  {x = Single.Fstep ψ (Gₙ N) (Gₙ-ord N)}
                  {y = pickStage ψ (LsetEnv (Gₙ N) (Gₙ-ord N) ms)}
                  (Single.pickLand ψ (Gₙ N) (Gₙ-ord N) ms) (lands N))

  open Cor β oβ using ( _⊨ᴬ_; relativize-correct )

  private
    transβ : {x y : V ℓ} → ⟨ x ∈ y ⟩ → ⟨ y ∈ Lset β ⟩ → ⟨ x ∈ Lset β ⟩
    transβ = layer-trans (Lset-layer β)

    lookupInLayer : ∀ {m} (i : Fin m) (γ : S ^ m) → Below β γ
                  → ⟨ fst (lookup i γ) ∈ Lset β ⟩
    lookupInLayer zero    (a ∷ γ) (ha , _)  = ha
    lookupInLayer (suc i) (a ∷ γ) (_  , hγ) = lookupInLayer i γ hγ

    tmInLayer : ∀ {m} (t : Term S m) (γ : S ^ m) → Below β γ
              → BoundedTm (Below′ β) t → ⟨ fst (⟦ t ⟧ γ) ∈ Lset β ⟩
    tmInLayer (con c) γ _  h = h
    tmInLayer (var i) γ bγ _ = lookupInLayer i γ bγ
```

## 帰納法

論理式の構造帰納法により、閉じた段階での充足関係を `L` 全体での充足関係と比較します。原子と結合子は直接従い、量化子では解答条件が必要な証人を段階内へ反映します。

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

The existential case is the one from the previous chapter. Downward, a witness from the stage is a
witness in L, and the hypothesis transfers it. Upward is the case of closure: the truth of the
existential in L is, by definition, the satisfiability the closure lemma consumes,
so closure returns a witness already inside the stage, and the hypothesis applies to
that one instead. Note which witness is used: not the one L happened to supply,
but the one closure chose. That is why no circularity arises here, and why the
stage never has to be a fixed point of anything.

</details>

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

The universal case is the existential case for the negated matrix, argued by contradiction.
If some element of L failed the matrix, that failure would be a witness for the negated
matrix, so closure would produce one inside the stage; but the hypothesis asserts that
everything in the stage satisfies the matrix, a contradiction. Deciding
whether the element fails is where the excluded middle enters the induction, and
it is the only place.

</details>

```agda
  reflectFo : ∀ {m} (χ : Formula S m)
            → ((N : ℕ) → Answers χ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N)))
            → BoundedFo (Below′ β) χ
            → (γ : S ^ m) → Below β γ → (γ ⊨ χ) ≡ (γ ⊨ᴬ χ)

  private
    reflect∃ : ∀ {m} (χ : Formula S (suc m)) → ClosedFor β χ
             → ((N : ℕ) → Answers χ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N)))
             → BoundedFo (Below′ β) χ
             → (γ : S ^ m) → Below β γ → (γ ⊨ (∃̇ χ)) ≡ (γ ⊨ᴬ (∃̇ χ))
    reflect∃ χ cl an bd γ bγ = ⇔toPath fwd bwd
      where
      fwd : ⟨ γ ⊨ (∃̇ χ) ⟩ → ⟨ γ ⊨ᴬ (∃̇ χ) ⟩
      fwd ex = PT.map
        (λ { (q , (fq∈ , satq)) →
             q , (fq∈ , subst ⟨_⟩ (reflectFo χ an bd (q ∷ γ) (fq∈ , bγ)) satq) })
        (cl γ bγ ex)
      bwd : ⟨ γ ⊨ᴬ (∃̇ χ) ⟩ → ⟨ γ ⊨ (∃̇ χ) ⟩
      bwd = PT.map
        (λ { (x , (x∈A , satx)) →
             x , subst ⟨_⟩ (sym (reflectFo χ an bd (x ∷ γ) (x∈A , bγ))) satx })

    reflect∀ : ∀ {m} (χ : Formula S (suc m)) → ClosedFor β (¬̇ χ)
             → ((N : ℕ) → Answers χ (Gₙ N) (Gₙ-ord N) (Gₙ (suc N)))
             → BoundedFo (Below′ β) χ
             → (γ : S ^ m) → Below β γ → (γ ⊨ (∀̇ χ)) ≡ (γ ⊨ᴬ (∀̇ χ))
    reflect∀ χ cl an bd γ bγ = ⇔toPath fwd bwd
      where
      fwd : ⟨ γ ⊨ (∀̇ χ) ⟩ → ⟨ γ ⊨ᴬ (∀̇ χ) ⟩
      fwd h x x∈A =
        subst ⟨_⟩ (reflectFo χ an bd (x ∷ γ) (x∈A , bγ)) (h x)
      bwd : ⟨ γ ⊨ᴬ (∀̇ χ) ⟩ → ⟨ γ ⊨ (∀̇ χ) ⟩
      bwd H x = decide (lem ((x ∷ γ) ⊨ χ))
        where
        decide : (⟨ (x ∷ γ) ⊨ χ ⟩ ⊎ (⟨ (x ∷ γ) ⊨ χ ⟩ → Empty.⊥))
               → ⟨ (x ∷ γ) ⊨ χ ⟩
        decide (inl yes) = yes
        decide (inr no)  = PT.rec (snd ((x ∷ γ) ⊨ χ)) collide
          (cl γ bγ ∣ x , (λ yes → lift (no yes)) ∣₁)
          where
          collide : Σ[ q ∈ S ] (⟨ fst q ∈ Lset β ⟩ × ⟨ (q ∷ γ) ⊨ (¬̇ χ) ⟩)
                  → ⟨ (x ∷ γ) ⊨ χ ⟩
          collide (q , (fq∈ , refute)) = Empty.rec
            (lower (refute (subst ⟨_⟩
              (sym (reflectFo χ an bd (q ∷ γ) (fq∈ , bγ))) (H q fq∈))))

  reflectFo (t ∈̇ u)  an bd γ bγ = refl
  reflectFo (t ≐ u)  an bd γ bγ = refl
  reflectFo (χ ∧̇ ψ)  an bd γ bγ =
    cong₂ _⊓_ (reflectFo χ (λ N → an N .fst) (bd .fst) γ bγ)
              (reflectFo ψ (λ N → an N .snd) (bd .snd) γ bγ)
  reflectFo (χ ∨̇ ψ)  an bd γ bγ =
    cong₂ _⊔_ (reflectFo χ (λ N → an N .fst) (bd .fst) γ bγ)
              (reflectFo ψ (λ N → an N .snd) (bd .snd) γ bγ)
  reflectFo (χ ⇒̇ ψ)  an bd γ bγ =
    cong₂ _⇒_ (reflectFo χ (λ N → an N .fst) (bd .fst) γ bγ)
              (reflectFo ψ (λ N → an N .snd) (bd .snd) γ bγ)
  reflectFo ⊥̇        an bd γ bγ = refl
  reflectFo (∃̇ χ)    an bd γ bγ =
    reflect∃ χ (closureOf χ (λ N → an N .fst)) (λ N → an N .snd) bd γ bγ
  reflectFo (∀̇ χ)    an bd γ bγ =
    reflect∀ χ (closureOf (¬̇ χ) (λ N → an N .fst)) (λ N → an N .snd) bd γ bγ
  reflectFo (∀̇∈ t χ) an bd γ bγ = ⇔toPath fwd bwd
    where
    tInβ : ⟨ fst (⟦ t ⟧ γ) ∈ Lset β ⟩
    tInβ = tmInLayer t γ bγ (bd .fst)
    fwd : ⟨ γ ⊨ (∀̇∈ t χ) ⟩ → ⟨ γ ⊨ᴬ (∀̇∈ t χ) ⟩
    fwd h x x∈t = subst ⟨_⟩
      (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ)) (h x x∈t)
    bwd : ⟨ γ ⊨ᴬ (∀̇∈ t χ) ⟩ → ⟨ γ ⊨ (∀̇∈ t χ) ⟩
    bwd h x x∈t = subst ⟨_⟩
      (sym (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ))) (h x x∈t)
  reflectFo (∃̇∈ t χ) an bd γ bγ = ⇔toPath fwd bwd
    where
    tInβ : ⟨ fst (⟦ t ⟧ γ) ∈ Lset β ⟩
    tInβ = tmInLayer t γ bγ (bd .fst)
    fwd : ⟨ γ ⊨ (∃̇∈ t χ) ⟩ → ⟨ γ ⊨ᴬ (∃̇∈ t χ) ⟩
    fwd = PT.map (λ { (x , (x∈t , h)) → x , (x∈t , subst ⟨_⟩
      (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ)) h) })
    bwd : ⟨ γ ⊨ᴬ (∃̇∈ t χ) ⟩ → ⟨ γ ⊨ (∃̇∈ t χ) ⟩
    bwd = PT.map (λ { (x , (x∈t , h)) → x , (x∈t , subst ⟨_⟩
      (sym (reflectFo χ an (bd .snd) (x ∷ γ) (transβ x∈t tInβ , bγ))) h) })
```

## 反映定理

任意の論理式、出発段階、そこから取った環境に対し、より大きな順序数段階を構成します。その段階は論理式について閉じ、制限構造での真理値が `L` 全体での真理値と一致します。

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

Packaged, the theorem takes the formula and any ordinal the caller wants inside
the stage, and returns a stage containing it. The extra ordinal is not a
convenience: the certificate is not inherited by larger stages, so a caller
cannot enlarge the stage afterwards to fit the set it is working with. It has to
say up front what must fit, and the joint step carries it.

</details>

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

The package is sealed, and this is the seal that matters most in the book so far.
Transparent, the stage it names unfolds through the joint step, the bounding
lemma and the excluded middle at every rung; a consumer that mentions the stage
in a type, as both consumers do, would drag that whole unfolding into every
conversion check, and the next chapter simply does not finish. Sealed, the stage
is a name, and the four things a consumer needs of it are the four the package
already states.

</details>

```agda
  reflectRel : (γ : S ^ n) → Below β γ
             → (γ ⊨ φ₀) ≡ (γ ⊨ relativize (LsetS β oβ) φ₀)
  reflectRel γ bγ =
    reflectFo φ₀ answersAt (liftFoTo κ∈β φ₀ bdd) γ bγ
    ∙ sym (relativize-correct φ₀ γ)

opaque
  mkReflect : ∀ {n} (φ : Formula S n) (δ : V ℓ) → IsOrd δ
            → Σ[ β ∈ V ℓ ] Σ[ oβ ∈ IsOrd β ]
                (⟨ δ ∈ β ⟩
                 × ((γ : S ^ n) → Below β γ
                    → (γ ⊨ φ) ≡ (γ ⊨ relativize (LsetS β oβ) φ)))
  mkReflect φ δ oδ = M.β , (M.oβ , (δ∈β , M.reflectRel))
    where
    bdd : Σ[ σ ∈ V ℓ ] (IsOrd σ × BoundedFo (Below′ σ) φ)
    bdd = mkBoundedFo φ
    b : Σ[ τ ∈ V ℓ ] (IsOrd τ × ⟨ bdd .fst ∈ τ ⟩ × ⟨ δ ∈ τ ⟩)
    b = bound2 (bdd .fst) δ (bdd .snd .fst) oδ
    module M = Mk φ (b .fst) (b .snd .fst)
                  (liftFoTo (b .snd .snd .fst) φ (bdd .snd .snd))
    δ∈β : ⟨ δ ∈ M.β ⟩
    δ∈β = M.oβ .fst {x = b .fst} {y = δ} (b .snd .snd .snd) M.κ∈β
```

## まとめ

論理式の全存在部分式に対する解答条件を一つの梯子へ統合すると、任意の有限な論理式を反映する段階が得られます。主定理はこの段階での評価と `L` 全体での評価を同定します。

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

The classical cost is unchanged: the excluded middle, in the descent, in deciding
satisfiability, and once more in the universal case here. No choice, and no
well-ordering of L.

</details>