相対化

相対化は、各非有界量化子を選んだ定数で有界化する。変換後の論理式は Δ₀ であり、その通常の充足関係は、元の論理式の非有界量化子を選んだ集合の要素だけにわたらせる意味論と一致する。本章は三つの要素をこの順に構築する。すなわち、書き換え演算子そのもの、その出力が Lévy 階層の Δ₀ クラスに属することの証拠 (有界論理式の定義は階層の章を参照)、そして書き換えの意味を選んだ集合の上の有界量化と同一視する正当性定理である。議論は一般的に保たれている。論理式は任意の型 K の定数を持つことができ、意味論も構造 𝒮 を通じて命題宇宙 hProp ℓ に値をとれる。

舞台を整える。論理式は任意の型 K の定数を含むことができ、充足関係は構造 𝒮 を通じて命題宇宙 hProp ℓ に値をとれる。非有界量化子を含む論理式、たとえば ∃̇ (x ∈̇ y) を考えてほしい。これは宇宙全体の中に y に属する要素があるかと問う。定数 c が与えられると、相対化はこの量化子に境界 con c を補って書き換える。結果は ∃̇∈ (con c) (x ∈̇ y) であり、y に属する要素のうち、定数 c の指すものに属するものがあるかだけを問う。論理式の他の部分はまったく変わらない。この書き換えは純粋に構文的なものである。書き換え後の論理式が依然として本来の意図を表すかどうかは別の意味論的な問題であり、正当性の節で扱う。

一箇所で一つの非有界量化子を書き換えるのは容易である。ここでの課題は、すべての論理式の任意の深さでこれを統一的に行い、後の管理も保つことである。本章の三つの要素は三つの問いに答える。第一に、演算子 relativize c が置き換えそのものを行い、既に有界な量化子とその境界には触れない。第二に、証拠 Δ₀-relativize は出力が Lévy 階層の Δ₀ クラスに属すること、すなわちそこに現れる量化子がすべて有界であることを保証する (有界論理式の定義は階層の章にある)。第三に、定理 relativize-correct が二つの読みを結ぶ。定数の任意の解釈のもとで、書き換え後の論理式の通常の充足は、元の論理式の非有界量化子を c の指す集合だけにわたらせる読みと一致する。

演算子

relativize c は原子論理式と既に有界な量化子を変えず、∃̇ と ∀̇ を con c で有界な量化子へ置き換える。境界は定数なので、変数をずらさずに束縛子の下へ入れる。定義は 10 個の論理式構成子に対する単純な再帰であり、コードを読む前に不動点となる構文的不変量を述べておく価値がある。相対化の後は、結果のすべての量化子が有界であり、導入される境界は con c の出現だけだということである。

シグニチャはデータを固定する。任意の定数記号の型 K から定数 c を一つと、アリティ n の論理式 φ を取り、同じアリティの別の論理式を返す。原子式、三つの二項結合子、そして偽に対する節はまったく書き換えを行わず、部分論理式に再帰して結合子の構造を保つだけである。したがって相対化は深さを保ち、構造的に変更しうるのは量化子の節だけである。

relativize : ∀ {ℓ} {K : Type ℓ} (c : K) {n} → Formula K n → Formula K n
relativize c (t ∈̇ u)  = t ∈̇ u
relativize c (t ≐ u)  = t ≐ u
relativize c (φ ∧̇ ψ)  = relativize c φ ∧̇ relativize c ψ
relativize c (φ ∨̇ ψ)  = relativize c φ ∨̇ relativize c ψ

非有界な二つの節が要点すべてを担う。∃̇ φ は ∃̇∈ (con c) φ′ へ、∀̇ φ は ∀̇∈ (con c) φ′ へ変わる。ここで φ′ は本体の相対化であり、量化子は今や定数 con c の要素の上だけをわたる。既に有界な二つの節は、元の境界の項 t をそのまま保つ。それはすでに量化子を制限しているからで、相対化されるのは本体だけである。境界の con c は変数ではなく項なので、新しく束縛した値で環境を拡張してもまったく乱されない。変換のどこでも de Bruijn 流の再索引付けは不要である。

relativize c (φ ⇒̇ ψ)  = relativize c φ ⇒̇ relativize c ψ
relativize c ⊥̇        = ⊥̇
relativize c (∃̇ φ)    = ∃̇∈ (con c) (relativize c φ)
relativize c (∀̇ φ)    = ∀̇∈ (con c) (relativize c φ)
relativize c (∀̇∈ t φ) = ∀̇∈ t (relativize c φ)

これで場合分けが完了する。10 個の構成子がすべて扱われ、再帰は入力の論理式に対して構造的であるため、relativize c φ はすべての論理式に対して定義される。有界な二つの節は単に再帰するだけなので、φ に元からあった有界量化子は自分の境界を持ったまま残り、新たな境界は非有界量化子の相対化による像そのものである。

relativize c (∃̇∈ t φ) = ∃̇∈ t (relativize c φ)

非有界量化子はすべて有界化され、他は何も変わらないため、結果には ∃̇ や ∀̇ の構成子がまったく現れない。Lévy 階層の章の用語で言えば、それこそが Δ₀ であることの意味である。帰納的族 Δ₀ は許容される形ごとに一つの構成子を持ち、非有界量化子には何も持たない。関数 Δ₀-relativize は φ に対する再帰でそのような証拠を組み立て、構成子ごとに一行を要する。

この命題はすべての論理式 φ に対して量化し、ブール値のフラグではなく帰納的族の中の証拠 Δ₀ (relativize c φ) を作る。原子式に対しては、証拠 δ-∈ と δ-≐ がそのまま与えられる。原子論理式は量化子をまったく含まないため、Δ₀ への所属は直ちに得られる。結合子の節は δ-∧、δ-∨、δ-⇒ で証拠を組み合わせ、二項演算の下でのこのクラスの閉性の規則を写している。

Δ₀-relativize : ∀ {ℓ} {K : Type ℓ} (c : K) {n} (φ : Formula K n) → Δ₀ (relativize c φ)
Δ₀-relativize c (t ∈̇ u)  = δ-∈
Δ₀-relativize c (t ≐ u)  = δ-≐
Δ₀-relativize c (φ ∧̇ ψ)  = δ-∧ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)
Δ₀-relativize c (φ ∨̇ ψ)  = δ-∨ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)

偽は量化子を含まないため δ-⊥ で足りる。決定的な行はここでも量化子である。relativize が非有界量化子を有界化した箇所では、Δ₀-relativize は相対化された本体への証拠に対し、有界量化のために用意された構成子 δ-∃∈ か δ-∀∈ を適用する。元の論理式の有界量化子も、自分の本体に対して同じ扱いを受ける。いずれの場合も帰納法の仮定が部分論理式の証拠を与え、構成子がそれを外側の結合子や量化子を通して持ち上げる。

Δ₀-relativize c (φ ⇒̇ ψ)  = δ-⇒ (Δ₀-relativize c φ) (Δ₀-relativize c ψ)
Δ₀-relativize c ⊥̇        = δ-⊥
Δ₀-relativize c (∃̇ φ)    = δ-∃∈ (Δ₀-relativize c φ)
Δ₀-relativize c (∀̇ φ)    = δ-∀∈ (Δ₀-relativize c φ)
Δ₀-relativize c (∀̇∈ t φ) = δ-∀∈ (Δ₀-relativize c φ)

10 個のケースがすべて扱われ、φ に対する再帰によりすべての入力に証拠が存在することが保証される。これが本章の約束の構文的な半分である。相対化された論理式は直観的に有界というだけでなく、後の絶対性や定義可能性の議論が直接消費できる明示的な Δ₀ の証拠を帯同する。

Δ₀-relativize c (∃̇∈ t φ) = δ-∃∈ (Δ₀-relativize c φ)

正当性

比較用の意味論は元の論理式を解釈し、非有界量化子だけを選んだ境界の値へ制限する。構造帰納法により、これは相対化した論理式の通常の意味論とちょうど一致する。ここには二つの意味論が登場する。FOL.Semantics からの標準的な γ ⊨ _ と、ここで定義する補助関係 γ ⊨ᴬ _ である。後者はすべての結合子、原子式、有界量化子で標準のものと一致し、∃̇ と ∀̇ でのみ異なり、束縛変数が選んだ集合に属するという条件を付け加える。証明すべき定理はパス (γ ⊨ relativize c φ) ≡ (γ ⊨ᴬ φ) なので、二つの関係は同一性の型をもつ型に値をとらねばならない。これが、モジュールが命題値の構造 𝒮 と定数の解釈 ι をパラメータとする理由である。

二つの読みを比較するために、台 S をもつ命題値の ZF 構造 𝒮、各定数記号に台の要素を割り当てる解釈 ι、そして注目の定数 c を固定する。標準の意味論 γ ⊨ _ と項の評価 ⟦_⟧ は、与えられた ι に対して FOL.Semantics から得られる。この節はこれらのデータに伴う関係 γ ⊨ᴬ _ を加える。これは元の論理式を標準の意味論どおりに解釈するが、非有界量化子だけを一つの台の要素 A、すなわち選んだ定数の表示 ι c に制限する。原子式、結合子、偽、有界量化子では伴う関係は標準の意味論と一致するはずであり、異なるのは無界量化が A の内部での量化に置き換わる箇所だけである。議論は 𝒮 の命題値関係を直接用いる。

module Correct {ℓ} (𝒮 : ZFStructureₕ ℓ)
               {ℓc} {K : Type ℓc} (ι : K → ZFStructure.S 𝒮) (c : K) where

open ZFStructure 𝒮
open module Sem = FOL.Semantics 𝒮 using ( module At )

open At K ι using ( _⊨_; ⟦_⟧ )

A : S
A = ι c

infix  _⊨ᴬ_
_⊨ᴬ_ : ∀ {n} → Vec S n → Formula K n → hProp ℓ

γ ⊨ᴬ (t ∈̇ u)  = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ
γ ⊨ᴬ (t ≐ u)  = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ
γ ⊨ᴬ (φ ∧̇ ψ)  = (γ ⊨ᴬ φ) ⊓ (γ ⊨ᴬ ψ)
γ ⊨ᴬ (φ ∨̇ ψ)  = (γ ⊨ᴬ φ) ⊔ (γ ⊨ᴬ ψ)
γ ⊨ᴬ (φ ⇒̇ ψ)  = (γ ⊨ᴬ φ) ⇒ (γ ⊨ᴬ ψ)

γ ⊨ᴬ ⊥̇        = ⊥
γ ⊨ᴬ (∃̇ φ)    = ∃[ x ∶ S ] (x ∈ˢ A) ⊓ ((x ∷ γ) ⊨ᴬ φ)
γ ⊨ᴬ (∀̇ φ)    = ∀[ x ∶ S ] (x ∈ˢ A) ⇒ ((x ∷ γ) ⊨ᴬ φ)
γ ⊨ᴬ (∀̇∈ t φ) = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ᴬ φ)
γ ⊨ᴬ (∃̇∈ t φ) = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ᴬ φ)

relativize-correct : ∀ {n} (φ : Formula K n) (γ : Vec S n)
                   → (γ ⊨ relativize c φ) ≡ (γ ⊨ᴬ φ)
relativize-correct (t ∈̇ u)  γ = refl
relativize-correct (t ≐ u)  γ = refl
relativize-correct (φ ∧̇ ψ)  γ = cong₂ _⊓_ (relativize-correct φ γ) (relativize-correct ψ γ)

relativize-correct (φ ∨̇ ψ)  γ = cong₂ _⊔_ (relativize-correct φ γ) (relativize-correct ψ γ)
relativize-correct (φ ⇒̇ ψ)  γ = cong₂ _⇒_ (relativize-correct φ γ) (relativize-correct ψ γ)
relativize-correct ⊥̇        γ = refl
relativize-correct (∃̇ φ)    γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →
  cong (λ q → (x ∈ˢ A) ⊓ q) (relativize-correct φ (x ∷ γ))))

relativize-correct (∀̇ φ)    γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
  cong (λ q → (x ∈ˢ A) ⇒ q) (relativize-correct φ (x ∷ γ))))
relativize-correct (∀̇∈ t φ) γ = cong (λ P → ∀[ x ∶ S ] P x) (funExt (λ x →
  cong (λ q → (x ∈ˢ ⟦ t ⟧ γ) ⇒ q) (relativize-correct φ (x ∷ γ))))
relativize-correct (∃̇∈ t φ) γ = cong (λ P → ∃[ x ∶ S ] P x) (funExt (λ x →

  cong (λ q → (x ∈ˢ ⟦ t ⟧ γ) ⊓ q) (relativize-correct φ (x ∷ γ))))

まとめ

relativize は Δ₀ 論理式を作り、Δ₀-relativize はその複雑さの上界を記録し、relativize-correct はその意味を選んだ集合の内部での量化と同定する。この三つを合わせると、任意の論理式を一つの集合に制限するという標準的な集合論の手法が得られる。構文的には集合を名指す定数で量化子を有界化し、意味論的にはここで証明した一つの帰納がそれを担う。この先では、Δ₀ の証拠が絶対性の議論に供給され、正当性のパスにより、定義可能性を解析する際に相対化された論理式の充足を A の上の有界量化に置き換えられる。