---
title: "Lévy 階層"
module: FOL.LevyHierarchy
lang: ja
site: "Bedrock"
description: "Lévy 階層"
stage: "一階論理"
reading_order: 9
canonical: https://bedrock.institute/ja/FOL.LevyHierarchy.html
html: FOL.LevyHierarchy.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/LevyHierarchy.lagda.md
prerequisites: [Base.Prelude, FOL.Syntax]
routes: [common-foundations]
translations: [https://bedrock.institute/en/FOL.LevyHierarchy.md, https://bedrock.institute/zh/FOL.LevyHierarchy.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Lévy 階層

一階論理式には二つの量化の仕方があります。「$t$ に属するすべての $x$ について」という有界な量化と、宇宙全体にわたる非有界な量化です。Lévy 階層は、論理式の構文的な複雑さを非有界量化子で測ります。**Δ₀** 論理式は有界量化子しか使わず、Σ₁ 論理式は Δ₀ の核の前に非有界な存在量化子の列を、Π₁ 論理式は非有界な全称量化子の列を前置します。これらのクラスへの所属が重要なのは、後の章で Δ₀ 絶対性を証明し、構成可能宇宙上で量化子の形に関する構造的帰納による定義可能性の議論を進めるからです。論理式をそのたびに調べる代わりに、本章では分類そのものをデータにします。**証拠**とは論理式で添字付けられた帰納的なデータであり、任意の定数域 `K` に対して使えるので、論理式は自分の構文とともに複雑さのクラスの証明を帯同できます。本章は Δ₀ の証拠、有界論理式を認識するブール判定器、そしてすべての有限レベル Σₙ/Πₙ への拡張を構成します。

本章は計算から証明への一本の橋に依拠します。型 `Bool` は `true` と `false` の二つの値を持ち、`_and_` は二つのブール値の結果を連言します。演算 `Bool→Type` はブール値を型へ送ります。`true` は一点型に、`false` は空な型に対応します。したがって `Bool→Type b` に元が存在するのは `b` が `true` のときちょうどです。この仕組みにより、計算の結果が後で証明義務を兼ねられます。プログラムはまず構文についてのブール的な問いを判定し、「答えが `true` になった」という主張はそれ自体が元を持てる型になるのです。

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

module FOL.LevyHierarchy where

open import Base.Prelude
open import Cubical.Data.Bool using ( Bool; true; false; _and_; Bool→Type )
```

分類の対象となる論理式は、`FOL.Syntax` の対象言語に由来します。項、原子関係 `_∈̇_` と `_≐_`、結合子、そして二組の異なる量化子の形式です。有界量化子 `∀̇∈` と `∃̇∈` は界限を言語内の項として名指ししますが、`∀̇_` と `∃̇_` は界限なしに量化します。二種の量化子が構文上区別されていることこそ、この分類全体を可能にする前提です。以下で定義される各族はいずれも `Formula K n` で添字付けられるため、ここでのLévy 階層は意味論的な値ではなく構文そのもの上の述語です。

```agda
open import Cubical.Data.Unit using ( tt )
open import FOL.Syntax using
  ( Term; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
```

## Δ₀ の証拠

`Δ₀` は論理式で添字付けられた帰納的族です。`Δ₀ φ` の元は、`φ` に現れる量化子がすべて有界であることの、明示的なデータとしての証拠です。定義は許容される論理式の形ごとに一つの構成子を持ち、非有界な `∃̇` と `∀̇` には構成子を与えません。この不在こそが分類です。この族は、ある宇宙レベル `ℓc` の定数域 `K` をパラメータとするほかは構文だけで決まるため、同じ証拠の型が任意の定数域で使えます。

Δ₀ の族を導く不変量は次のとおりです。有界量化子は有界性を保ち、非有界量化子はこれを壊す。宣言はこれを、任意のアリティ `n` の論理式で添字付けられた帰納的族 `Δ₀` として実現します。`K` と同じ宇宙レベルに住むので、証拠は小さなデータです。`t ∈̇ u` のような原子論理式はそのまま受け入れられます。量化子をまったく含まないため、`δ-∈` (および等式版の `δ-≐`) は引数を取りません。次にこのクラスは二項結合子の下で閉じ、`δ-∧` と `δ-∨` はそれぞれ複合論理式の両成分に対する証拠を要求します。

```agda
data Δ₀ {ℓc} {K : Type ℓc} : ∀ {n} → Formula K n → Type ℓc where
  δ-∈  : ∀ {n} {t u : Term K n} → Δ₀ (t ∈̇ u)
  δ-≐  : ∀ {n} {t u : Term K n} → Δ₀ (t ≐ u)
  δ-∧  : ∀ {n} {φ ψ : Formula K n} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ∧̇ ψ)
  δ-∨  : ∀ {n} {φ ψ : Formula K n} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ∨̇ ψ)
```

含意 `δ-⇒` と、量化子を持たない偽 `δ-⊥` が、量化子を含まない形を完成させます。決定的な行は有界量化子です。`δ-∀∈` と `δ-∃∈` はアリティ `suc n` の本体 `φ` に対する証拠を受け取り、`∀̇∈ t φ` あるいは `∃̇∈ t φ` の証拠を返します。界限は項 `t` です。こうして有界性は有界量化子をそのまま通過します。同じくらい決定的なのは、この一覧に欠けているものです。非有界な `∃̇` や `∀̇` に触れる構成子は一つもありません。`∃̇ (x₀ ∈̇ x₁)` のように非有界量化子を含む論理式はどの構成子にも当てはまらず、その添字での `Δ₀` の元は決して組み立てられません。この拒否こそが分類であり、分類についての定理ではありません。

```agda
  δ-⇒  : ∀ {n} {φ ψ : Formula K n} → Δ₀ φ → Δ₀ ψ → Δ₀ (φ ⇒̇ ψ)
  δ-⊥  : ∀ {n} → Δ₀ {n = n} ⊥̇
  δ-∀∈ : ∀ {n} {t : Term K n} {φ : Formula K (suc n)} → Δ₀ φ → Δ₀ (∀̇∈ t φ)
  δ-∃∈ : ∀ {n} {t : Term K n} {φ : Formula K (suc n)} → Δ₀ φ → Δ₀ (∃̇∈ t φ)

δ-¬ : ∀ {ℓc} {K : Type ℓc} {n} {φ : Formula K n} → Δ₀ φ → Δ₀ (¬̇ φ)
```

否定と真理に特別な扱いは要りません。それらは原始的ではないからです。この構文では `¬̇ φ` は `φ ⇒̇ ⊥̇` として、`⊤̇` は `⊥̇ ⇒̇ ⊥̇` として定義されています。含意と偽がすでに証拠を持つため、定義された論理式の有界性は `δ-⇒` 構成子から従います。派生証拠 `δ-¬ d` は証拠 `d` を `δ-⊥` とまとめ、`δ-⊤` は含意の両辺に `δ-⊥` を置きます。これらは既存の族についての補題であって新しい構成子ではなく、後のコードが新たな場合分けなしに否定された論理式や自明な論理式を証明できるようにします。

```agda
δ-¬ d = δ-⇒ d δ-⊥

δ-⊤ : ∀ {ℓc} {K : Type ℓc} {n} → Δ₀ {K = K} {n = n} ⊤̇
δ-⊤ = δ-⇒ δ-⊥ δ-⊥
```

## 具体的な論理式を判定する

論理式を一つずつ構成子のリストと突き合わせて読む必要はありません。関数 `bounded` は構文を走査し、非有界な量化子に出会わないときにちょうど `true` を返し、`checkΔ₀` はこのブール値が `true` になったという主張を実際の `Δ₀` の証拠へ変換します。証明された方向は一方向です。ブール値の成功が証拠を与えます。この定義が逆方向の判定手続きであるとは主張せず、完全性の結果もここでは証明しません。

不変量が機械的に検査できるなら、Δ₀ の証拠を手で組み立てる必要はありません。関数 `bounded` は論理式をたどって `Bool` を報告します。原子論理式と偽はそのまま `true` を返し、各二項結合子は `_and_` で二つの部分論理式の結果を連言します。この段階の検査は、Δ₀ が受け入れる形を論理式の構成子ごとに一つの再帰で写しているにすぎません。

```agda
bounded : ∀ {ℓc} {K : Type ℓc} {n} → Formula K n → Bool
bounded (t ∈̇ u) = true
bounded (t ≐ u) = true
bounded (φ ∧̇ ψ) = bounded φ and bounded ψ
bounded (φ ∨̇ ψ) = bounded φ and bounded ψ
```

ここで不変量が本領を発揮します。二つの非有界量化子はどちらも `false` を返すため、論理式のどこかに非有界量化子が一度現れれば、部分論理式がどうであれ検査全体が失敗します。有界量化子は逆で、再帰はそのまま本体へ進みます。界限 `t` は構文の項であり、量化子を隠せないからです。規則 `bounded (∀̇∈ t φ) = bounded φ` は、有界性を通過させた Δ₀ の構成子の計算上の対応物です。

```agda
bounded (φ ⇒̇ ψ) = bounded φ and bounded ψ
bounded ⊥̇ = true
bounded (∃̇ φ) = false
bounded (∀̇ φ) = false
bounded (∀̇∈ t φ) = bounded φ
```

連言におけるブール値 `true` は一度に二つのことを意味するので、プライベートな補助関数 `and-out` がそれを分解します。`a b : Bool` と `Bool→Type (a and b)` の元が与えられると、`Bool→Type a` と `Bool→Type b` それぞれの元の組を返します。`a` が `false` のとき、入力は空な型 `Bool→Type false` に属さねばならず、この場合は荒謬パターン `()` で片付きます。`a` が `true` のときは、単位元 `tt` が第一の連言肢を証明し、与えられた `h` がそのまま第二の連言肢になります。

```agda
bounded (∃̇∈ t φ) = bounded φ

private
  and-out : (a b : Bool) → Bool→Type (a and b) → Bool→Type a × Bool→Type b
  and-out false b ()
  and-out true b h = tt , h
```

ブール的な判定が証拠に変わるのが関数 `checkΔ₀` です。この関数は論理式 `φ` と `Bool→Type (bounded φ)` の元を受け取ります。後者が存在するのは走査が `true` と計算したときに限られ、関数は実際の `Δ₀ φ` の証拠を返します。原子論理式の場合は対応する構成子を直接返し、仮定 `h` は使われません。連言の場合、`bounded (φ ∧̇ ψ)` は `bounded φ and bounded ψ` と計算されるので、`and-out` が `h` を連言肢ごとの二つの証明 `p .fst` と `p .snd` に分解し、再帰呼び出しが下位の証拠を供給して `δ-∧` が組み立て直します。

```agda
checkΔ₀ : ∀ {ℓc} {K : Type ℓc} {n} (φ : Formula K n) → Bool→Type (bounded φ) → Δ₀ φ
checkΔ₀ (t ∈̇ u) h = δ-∈
checkΔ₀ (t ≐ u) h = δ-≐
checkΔ₀ (φ ∧̇ ψ) h = δ-∧ (checkΔ₀ φ (p .fst)) (checkΔ₀ ψ (p .snd))
  where p = and-out (bounded φ) (bounded ψ) h
```

選言と含意は同じ動きを繰り返します。それぞれ `and-out` で `h` を分解し、二つの再帰呼び出しを実行して、`δ-∨` か `δ-⇒` で組み立て直します。偽は `δ-⊥` だけで足ります。これらの節により、Δ₀ が受け入れる量子化を含まないすべての形について、ブール値の結果から証拠への道が用意されました。

```agda
checkΔ₀ (φ ∨̇ ψ) h = δ-∨ (checkΔ₀ φ (p .fst)) (checkΔ₀ ψ (p .snd))
  where p = and-out (bounded φ) (bounded ψ) h
checkΔ₀ (φ ⇒̇ ψ) h = δ-⇒ (checkΔ₀ φ (p .fst)) (checkΔ₀ ψ (p .snd))
  where p = and-out (bounded φ) (bounded ψ) h
checkΔ₀ ⊥̇ h = δ-⊥
```

残りの節が議論を閉じます。非有界量化子については、`bounded (∃̇ φ)` と `bounded (∀̇ φ)` はどちらも `false` と計算されるため、仮定 `h` は空な型 `Bool→Type false` に属さねばなりません。そのような元は存在しないからこそ、荒謬パターン `()` がこの場合を受け止められます。有界量化子については、`bounded (∀̇∈ t φ)` は `bounded φ` と計算されるので、`h` はそのまま本体に渡され、再帰の結果を `δ-∀∈` か `δ-∃∈` で包みます。全体として、これらの節はすべての論理式に対して `bounded φ ≡ true → Δ₀ φ` を確立します。計算上の成功が証拠を与えるのです。項 `t` と `u` は結果に影響せず、逆向きの主張はここではどこにも行われません。

```agda
checkΔ₀ (∃̇ φ) ()
checkΔ₀ (∀̇ φ) ()
checkΔ₀ (∀̇∈ t φ) h = δ-∀∈ (checkΔ₀ φ h)
checkΔ₀ (∃̇∈ t φ) h = δ-∃∈ (checkΔ₀ φ h)
```

## Σ₁ と Π₁

論理式が非有界に量化できるなら、次の自然な問いは、いくつの、どの種の非有界量化子を含んでよいかです。Σ₁ と Π₁ はちょうど一つの列について答えます。Σ₁ の証拠は、Δ₀ の証拠であるか、本体に対する Σ₁ の証拠に非有界な存在量化子をもう一つ施したものです。つまり Σ₁ の証拠は自分自身の上に重なる型をなし、Δ₀ の核の上の任意に有限な存在量化子の列を記録します。Π₁ は同じ構成で極性を逆にしたものです。どちらのクラスも二種の量化子の交替を許さず、各束縛子はアリティ `suc n` の本体を消費してアリティ `n` の論理式を生みます。ここでの二つの族は独立に定義されており、次の節が同じ考えをレベルで添字付けられた一様な階層へ組み替えます。

この重なりは `Σ₁` の二つの構成子にはっきり現れます。基底 `σ-Δ₀` は任意の Δ₀ の証拠をそのまま埋め込むので、すべての有界論理式は追加の量化子なしで Σ₁ に数えられます。ステップ `σ-∃` は非有界な存在量化子を一つ前置きし、アリティ `suc n` の本体に対する Σ₁ の証拠から `∃̇ φ` の証拠を作ります。`σ-∃` を繰り返せば有限個の存在量化子の列ができ、その列は `σ-Δ₀` の核で終わらねばならず、途中で全称量化子を入れる道はありません。

```agda
data Σ₁ {ℓc} {K : Type ℓc} : ∀ {n} → Formula K n → Type ℓc where
  σ-Δ₀ : ∀ {n} {φ : Formula K n} → Δ₀ φ → Σ₁ φ
  σ-∃  : ∀ {n} {φ : Formula K (suc n)} → Σ₁ φ → Σ₁ (∃̇ φ)
```

`Π₁` はその鏡像です。`π-Δ₀` は同じ Δ₀ の基底を共有し、`π-∀` は非有界な全称量化子を一つ前置きします。ここでも本体のアリティは `suc n` です。二つの族は量化子の極性を逆にした同じ重ね方で作られており、この極性の違いこそ、後に絶対性の議論が証拠から読み取るものです。

```agda
data Π₁ {ℓc} {K : Type ℓc} : ∀ {n} → Formula K n → Type ℓc where
  π-Δ₀ : ∀ {n} {φ : Formula K n} → Δ₀ φ → Π₁ φ
  π-∀  : ∀ {n} {φ : Formula K (suc n)} → Π₁ φ → Π₁ (∀̇ φ)
```

## 一般の Lévy 階層

非有界量化子の固定された一つの列は、最初の段にすぎません。一般のLévy 階層は、非有界量化子の極性が何回交替するかで論理式を分级し、本章はこの分级を相互に定義された二つの帰納的族 `Σₙ` と `Πₙ` で符号化します。それぞれ自然数のレベル `k` を帯びます。添字 `k` は証拠そのものが供給する上界です。レベル `k` の証拠は最大 `k` 回の交替を使えますが、ちょうど `k` 回使う必要はありません。Δ₀ 論理式がすべてのレベルで埋め込まれるからです。暗黙の `n` は依然として論理式のアリティであり、`k` と混同してはならない別の管理項目です。各族は固定レベルで自分の極性の非有界量化子の下で閉じ、`σ-Π` と `π-Σ` が族をまたいで添字を上げる二つの交互ステップです。

交替とはまさに族の乗り換えですから、二つの族は互いを参照せねばならず、一つの `mutual` ブロックで宣言されます。`Σₙ` は論理式の添字の前にレベルの添字 `k` を帯びます。基底 `σ-Δ₀` は Δ₀ 論理式をどのレベル `k` にも置けるので、レベルが正確な回数ではなく上界を記録する理由がここにあります。交互ステップ `σ-Π` は `Πₙ k` の証拠を `Σₙ (suc k)` へ引き上げ、極性を越える代償としてレベルを一段支払います。最後に `σ-∃` はレベル `suc k` の証拠に同じレベルで存在量化子をもう一つ施して延ばし、本体のアリティ `suc n` は `n` に縮みます。

```agda
mutual
  data Σₙ {ℓc} {K : Type ℓc} : ℕ → ∀ {n} → Formula K n → Type ℓc where
    σ-Δ₀ : ∀ {k n} {φ : Formula K n} → Δ₀ φ → Σₙ k φ
    σ-Π  : ∀ {k n} {φ : Formula K n} → Πₙ k φ → Σₙ (suc k) φ
    σ-∃  : ∀ {k n} {φ : Formula K (suc n)} → Σₙ (suc k) φ → Σₙ (suc k) (∃̇ φ)
```

`Πₙ` は同じ相互定義ブロックで双対の形で宣言されます。`π-Δ₀` はすべてのレベルで Δ₀ を埋め込み、`π-Σ` は `Σₙ k` の証拠を `Πₙ (suc k)` へ引き上げ、`π-∀` はレベル `suc k` を非有界な全称量化子の下で閉じます。二つの族を合わせると、核がレベルの許す回数だけ交替する有限個の量化子の列が記録されます。前節で独立に定義された Σ₁/Π₁ の族は、形の上で `Σₙ 1` と `Πₙ 1`、すなわち `suc zero` に対応します。レベル 0 では Δ₀ の構成子しか使えず、量化子の構成子はいずれも `suc k` を要求するからです。

```agda
  data Πₙ {ℓc} {K : Type ℓc} : ℕ → ∀ {n} → Formula K n → Type ℓc where
    π-Δ₀ : ∀ {k n} {φ : Formula K n} → Δ₀ φ → Πₙ k φ
    π-Σ  : ∀ {k n} {φ : Formula K n} → Σₙ k φ → Πₙ (suc k) φ
    π-∀  : ∀ {k n} {φ : Formula K (suc n)} → Πₙ (suc k) φ → Πₙ (suc k) (∀̇ φ)
```

## まとめ

Lévy 階層は帰納的な証拠として表されました。Δ₀ の証拠は構成上、非有界量化子を排除し、Σ₁ と Π₁ は一方の極性からなる有限列を加え、相互定義された Σₙ と Πₙ の族は、さらに高い交替レベルを論理式のアリティとは別に制限します。各証拠は許される外側の形を明らかにするので、後の帰納法では有界、存在、全称の場合を分けて扱えます。