---
title: "符号化された対に沿う階数降下"
module: L.Coding.Descent
lang: ja
site: "Bedrock"
description: "符号化された対に沿う階数降下"
stage: "内部の符号化：式と定義域"
reading_order: 45
canonical: https://bedrock.institute/ja/L.Coding.Descent.html
html: L.Coding.Descent.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Descent.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy, V.Coding, L.Rank]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.Descent.md, https://bedrock.institute/zh/L.Coding.Descent.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 符号化された対に沿う階数降下

後では符号に対して整礎再帰を行い、各段階で与えられた符号の直下の成分を処理します。再帰が整礎であるためには、符号からその成分へと狭義に減少する尺度が必要です。所属関係はそれを与えてくれません。Kuratowski 対は `pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆` と定義されるので、`b` のような成分に届くには、中間の非順序対 `⁅ a , b ⁆` を経なければならず、この中間集合そのものは符号ではありません。したがって所属に関する帰納は、符号についての仮定をそれらの間へ運ぶことができません。

階数ならできます。階数は所属に沿って狭義に増加し、その値は順序数であり、順序数の所属は推移的です。そこで有限の所属の連鎖は一つの順序数の比較へと縮み、再帰は符号そのものではなく**階数**に関する整礎帰納によって正当化できます。本章が組み立てるのはまさにこの比較です。順序対の各側ごとに一段階、さらにそれを合成して、対になったペイロードの各側から外側のタグ付き符号への 4 段階の降下を得ます。

数学的な舞台は累積階層です。その台 `S`、命題値をとる所属 `∈ˢ`、そして集合論的演算をひとまとめにした構造 `𝒮ᵥ` です。降下を証明する前に一つ、準備をはっきりさせておきます。整礎再帰には狭義の尺度が必要で、後で使う尺度は von Neumann の階数です。これはランクの章で定義され研究されています。そこでは `rank-mono` が階数が所属に沿って狭義に増加することを、`rank-ord` がすべての階数が順序数であることを記録しています。

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

open import Base.Prelude

module L.Coding.Descent {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

具体的な難しさは符号の形から読み取れます。`pr a b` の成分は `pr a b` の直接の要素ではありません。それは非順序対 `⁅ a , b ⁆` の中に包まれ、後者はさらに外側の非順序対の 2 つの要素の一つです。所属が与えるのは 1 本の辺ではなく複数段階の連鎖であり、連鎖の環となる集合はまったく符号の構造を持たないものです。この連鎖の代わりとなるのが、各所属の辺を階数を通して翻訳し、それを合成して得られる順序数どうしの狹義の不等式です。

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Rank {ℓ} using ( rank; rank-mono; rank-ord )

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
```

この比較には階層からの 3 つの材料を使います。非順序対 `⁅ u , v ⁆`、非順序対への所属を命題として特徴づける対の公理 `pairing-ax`、そして根底の集合としての所属と構造化された所属 `∈ˢ` とを相互に変換する `∈∈ₛ` です。和型 `_⊎_` は 2 つの成分の明示的な選択を運びます。左には `inl`、右には `inr` です。ここで選択を「単に存在する」ではなく明示的に保つことが重要なのは、降下の証明が対のどちらの成分へ降りるのかを指摘しなければならないからです。

```agda
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s )
```

重要なのは、推移性を使える場所の区別です。任意の集合の所属を推移的とはみなしません。各所属の辺を `rank-mono` で階数どうしの関係へ移した後にはじめて、中間の対象が順序数となり、`rank-ord` がその狭義の不等式を合成するための推移性を与えます。

```agda
open hPropStructure 𝒮ᵥ
```

## 階数を下げる基本段階

降下の議論は 2 つの再利用可能な事実に立っています。第 1 は非順序対への所属の辺です。`w` が `u` か `v` に明示的に等しいなら、`w` は `⁅ u , v ⁆` に属します。第 2 は階数の段階です。1 本の所属の辺 `x ∈ˢ y` と `y` から `z` への階数降下があれば、`x` から `z` への階数降下が得られます。両者を合わせると、所属の連鎖が一つの順序数の比較に変わります。しかも任意の集合について成り立ち、特定の対の式に限定されません。

対の公理は `⁅ u , v ⁆` の所属を切り詰められた選言として特徴づけます。「要素が `u` に等しいか `v` に等しい」という選言全体が切り詰められています。補題 `pair∈` は、切り詰めを外した逆向きを与えます。明示的な和 `w ≡ u ⊎ w ≡ v` を受け取り、`∣ h ∣₁` を `pairing-ax` の切り詰められた側に挿入し、`∈∈ₛ` で変換して、`⟨ w ∈ˢ ⁅ u , v ⁆ ⟩` の証明を返します。これがまさに降下の証明に必要な方向です。どちらの成分へ降りるかが指摘されていれば、場合分けなしに所属が従います。合成の段階 `trans≺` が次に階数への翻訳を行います。`rank-ord z` により `rank z` は順序数であり、`rank z` の下での所属は推移的なので、`rank x ∈ˢ rank y` と `rank y ∈ˢ rank z` は `rank x ∈ˢ rank z` に合成されます。第 1 の仮定は `x ∈ˢ y` に `rank-mono x y` を施したものです。推移性を使うのは順序数としての階数についてであって、任意の集合の所属について推移性を仮定することは決してない、と注意してください。

```agda
pair∈ : (u v w : S) → (w ≡ u) ⊎ (w ≡ v) → ⟨ w ∈ˢ ⁅ u , v ⁆ ⟩
pair∈ u v w h = ∈∈ₛ {a = w} {b = ⁅ u , v ⁆} .snd (pairing-ax u v w .snd ∣ h ∣₁)

trans≺ : (x y z : S) → ⟨ x ∈ˢ y ⟩ → ⟨ rank y ∈ˢ rank z ⟩ → ⟨ rank x ∈ˢ rank z ⟩
trans≺ x y z x∈y ry∈rz = rank-ord z .fst (rank-mono x y x∈y) ry∈rz
```

## タグ付きコードのペイロードへ降りる

2 つの基本段階が手もとにあれば、符号化された対の降下は Kuratowski 対の形を読むだけで得られます。`pr a b` の成分 `x` が符号全体に届くには 2 本の所属の辺を経ます。`x` は `⁅ a , b ⁆` に属し、`⁅ a , b ⁆` は `pr a b` に属する。そこで `pair-component≺` は任意の成分についてこの 2 段階の降下を証明し、タグには何の条件も課しません。第 2 成分に限定すると `payload≺`、すなわちペイロードからそのタグ付き符号への降下が得られます。タグ `c` のもとの対になったペイロード `pr a b` にはもう一度の合成が要りますが、ここで両側は実際に異なります。`leftPart` はまずペイロードの内側の第 1 成分へ降り、それからペイロード降下と合成します。`rightPart` はペイロード降下を 2 回施すだけです。通じてタグ `c` は任意の集合であり、数項である必要も、そこへ降りることもありません。

2 本の辺は明示的に供給されます。第 1 は与えられた選択 `h : x ≡ a ⊎ x ≡ b` を `pair∈ a b x h` で使います。第 2 の選択は `inr refl` です。非順序対 `⁅ a , b ⁆` は定義的に外側の対の右の要素なので、`pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl)` がその所属を証明し、`rank-mono` がそれを階数の不等式 `rank ⁅ a , b ⁆ ∈ˢ rank (pr a b)` に変えます。そして `trans≺` が両者を合成します。途中の集合 `⁅ a , b ⁆` がこの証明の内部にしか現れないことに注意してください。`pair-component≺` の命題は符号と選ばれた成分以外に何も言及しません。特殊化 `payload≺` は再び `inr refl` によって `z` を `pr c z` の右成分と読み、任意のタグ `c` に対するペイロードからそのタグ付き符号への降下を与えます。

```agda
pair-component≺ : (a b x : S) → (x ≡ a) ⊎ (x ≡ b) → ⟨ rank x ∈ˢ rank (pr a b) ⟩
pair-component≺ a b x h = trans≺ x ⁅ a , b ⁆ (pr a b) (pair∈ a b x h)
  (rank-mono ⁅ a , b ⁆ (pr a b) (pair∈ ⁅ a ⁆s ⁅ a , b ⁆ ⁅ a , b ⁆ (inr refl)))

payload≺ : (c z : S) → ⟨ rank z ∈ˢ rank (pr c z) ⟩
payload≺ c z = pair-component≺ c z z (inr refl)
```

タグのもとの両補題は、順序数 `rank (pr c (pr a b))` において合成されます。使うのは `rank-ord` の推移性のフィールドです。両者の非対称性は入れ子の構造を反映しています。`leftPart` では目標 `a` はペイロードの内側の第 1 成分なので、第 1 の辺は `pair-component≺ a b a (inl refl)` で、`rank a ∈ˢ rank (pr a b)` を与えます。第 2 の辺はペイロード降下 `payload≺ c (pr a b)` です。`rightPart` では目標 `b` はペイロード自身の第 2 成分なので、両方の辺がペイロード降下です。`payload≺ a b` が `b` から `pr a b` へ、次に `payload≺ c (pr a b)` がペイロードから外側のタグ付き符号へ。どちらの場合も結論は同じ形、`rank a` または `rank b` が `rank (pr c (pr a b))` に属する、であり、これは後のタグ付き符号上の整礎再帰が各直下の成分に要求する尺度の減少そのものです。

```agda
leftPart : (c a b : S) → ⟨ rank a ∈ˢ rank (pr c (pr a b)) ⟩
leftPart c a b = rank-ord (pr c (pr a b)) .fst
  (pair-component≺ a b a (inl refl)) (payload≺ c (pr a b))

rightPart : (c a b : S) → ⟨ rank b ∈ˢ rank (pr c (pr a b)) ⟩
rightPart c a b = rank-ord (pr c (pr a b)) .fst (payload≺ a b) (payload≺ c (pr a b))
```