Lévy 階層

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

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

open import Cubical.Data.Bool using ( _and_; Bool→Type )

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

Δ₀ の証拠

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

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

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₁) のように非有界量化子を含む論理式はどの構成子にも当てはまらず、その添字での Δ₀ の元は決して組み立てられない。この拒否こそが分類であり、分類についての定理ではない。

  δ-⇒  : ∀ {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 を δ-⊥ とまとめ、δ-⊤ は含意の両辺に δ-⊥ を置く。これらは既存の族についての補題であって新しい構成子ではなく、後のコードが新たな場合分けなしに否定された論理式や自明な論理式を証明できるようにする。

δ-¬ d = δ-⇒ d δ-⊥

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

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

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

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

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 φ は、有界性を通過させた Δ₀ の構成子の計算上の対応物である。

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 のときは、単位元 _ が第一の連言肢を証明し、与えられた h がそのまま第二の連言肢になる。

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 に分解し、再帰呼び出しが下位の証拠を供給して δ-∧ が組み立て直す。

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 を分解し、二つの再帰呼び出しを実行して、δ-∨ か δ-⇒ で組み立て直す。偽は δ-⊥ だけで足りる。これらの節により、Δ₀ が受け入れる量子化を含まないすべての形について、ブール値の結果から証拠への道が用意された。

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 は結果に影響せず、逆向きの主張はここではどこにも行われない。

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

Σ₁ と Π₁

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

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

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

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

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 に縮む。

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 を要求するからである。

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