Bedrock相対化
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップ相対化は、各非有界量化子を選んだ定数で有界化します。変換後の論理式は Δ₀ であり、その通常の充足関係は、元の論理式の非有界量化子を選んだ集合の要素だけにわたらせる意味論と一致します。本章は三つの要素をこの順に構築します。すなわち、書き換え演算子そのもの、その出力が Lévy 階層の Δ₀ クラスに属することの証拠 (有界論理式の定義は階層の章を参照)、そして書き換えの意味を選んだ集合の上の有界量化と同一視する正当性定理です。議論は一般的に保たれています。論理式は任意の型 K の定数を持つことができ、意味論も構造 𝒮 を通じて命題宇宙 hProp ℓ に値をとれます。
舞台を整えます。論理式は任意の型 K の定数を含むことができ、充足関係は構造 𝒮 を通じて命題宇宙 hProp ℓ に値をとれます。非有界量化子を含む論理式、たとえば ∃̇ (x ∈̇ y) を考えてください。これは宇宙全体の中に y に属する要素があるかと問います。定数 c が与えられると、相対化はこの量化子に境界 con c を補って書き換えます。結果は ∃̇∈ (con c) (x ∈̇ y) であり、y に属する要素のうち、定数 c の指すものに属するものがあるかだけを問います。論理式の他の部分はまったく変わりません。この書き換えは純粋に構文的なものです。書き換え後の論理式が依然として本来の意図を表すかどうかは別の意味論的な問題であり、正当性の節で扱います。
{-# OPTIONS --cubical --safe --guardedness #-} module FOL.Manipulation.Relativization where open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure )
一箇所で一つの非有界量化子を書き換えるのは容易です。ここでの課題は、すべての論理式の任意の深さでこれを統一的に行い、後の管理も保つことです。本章の三つの要素は三つの問いに答えます。第一に、演算子 relativize c が置き換えそのものを行い、既に有界な量化子とその境界には触れません。第二に、証拠 Δ₀-relativize は出力が Lévy 階層の Δ₀ クラスに属すること、すなわちそこに現れる量化子がすべて有界であることを保証します (有界論理式の定義は階層の章にあります)。第三に、定理 relativize-correct が二つの読みを結びます。定数の任意の解釈のもとで、書き換え後の論理式の通常の充足は、元の論理式の非有界量化子を c の指す集合だけにわたらせる読みと一致します。
open import FOL.Syntax using ( con; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ ) import FOL.Semantics
演算子
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; _^_ )
境界は一度だけ名付けられます。A = ι c、すなわち選んだ定数が表示する台の要素です。関係 γ ⊨ᴬ φ は環境 γ : S ^ n と同じアリティ n の論理式 φ を取り、標準の充足と同様に命題宇宙 hProp ℓ の命題を返します。上付きの ᴬ は量化子が A に相対化されていることを示します。続く節のうち、標準と異なるのは非有界量化子の節だけです。
open At K ι using ( _⊨_; ⟦_⟧ ) A : S A = ι c infix 6 _⊨ᴬ_ _⊨ᴬ_ : ∀ {n} → S ^ n → Formula K n → hProp ℓ
最初の五つの節は標準の意味論をそのまま写します。原子式は、指示 ⟦ t ⟧ γ と ⟦ u ⟧ γ に対する構造の命題値をとる所属と等号になり、結合子は論理演算 ⊓、⊔、⇒ になり、偽は ⊥ になります。これは意図的です。これらの形では相対化すべきものがなく、これらの節を標準のものと定義的に同一にしておくことが、対応する正当性のケースを refl で証明できる理由になります。再帰はここでも構造的であり、⊨ᴬ は全関数です。
γ ⊨ᴬ (t ∈̇ u) = ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ γ ⊨ᴬ (t ≐ u) = ⟦ t ⟧ γ ≈ˢ ⟦ u ⟧ γ γ ⊨ᴬ (φ ∧̇ ψ) = (γ ⊨ᴬ φ) ⊓ (γ ⊨ᴬ ψ) γ ⊨ᴬ (φ ∨̇ ψ) = (γ ⊨ᴬ φ) ⊔ (γ ⊨ᴬ ψ) γ ⊨ᴬ (φ ⇒̇ ψ) = (γ ⊨ᴬ φ) ⇒ (γ ⊨ᴬ ψ)
量化子の節が二つの意味論が分かれる場所です。非有界な存在量化子に対する γ ⊨ᴬ (∃̇ φ) は、添字付きの結合 ∃[ x ] (x ∈ˢ A) ⊓ ((x ∷ γ) ⊨ᴬ φ) です。すべての台の要素 x をわたり、命題であるガード x ∈ˢ A を連言します。双対に、非有界な全称量化子は含意のガード x ∈ˢ A ⇒ _ を伴う ∀[ x ] P x を使います。有界な節はもともと量化子を項に制限しており、その項は元の環境 γ で評価されます。ガードは A ではなく ⟦ t ⟧ γ を用い、それ以外は標準の読みと正確に一致します。ここでは定義に現れる演算だけを述べています。抽象的な命題演算は、ガードを二値判定にする法則を仮定していません。
γ ⊨ᴬ ⊥̇ = ⊥ γ ⊨ᴬ (∃̇ φ) = ∃[ x ∶ S ] (x ∈ˢ A) ⊓ ((x ∷ γ) ⊨ᴬ φ) γ ⊨ᴬ (∀̇ φ) = ∀[ x ∶ S ] (x ∈ˢ A) ⇒ ((x ∷ γ) ⊨ᴬ φ) γ ⊨ᴬ (∀̇∈ t φ) = ∀[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⇒ ((x ∷ γ) ⊨ᴬ φ) γ ⊨ᴬ (∃̇∈ t φ) = ∃[ x ∶ S ] (x ∈ˢ ⟦ t ⟧ γ) ⊓ ((x ∷ γ) ⊨ᴬ φ)
正当性は一つの構造帰納法で示されます。relativize c φ の標準的な意味は、φ の A-有界な意味と等しいのです。原子式のケースは refl であり、演算子が実際に変更する二つの量化子の節は、⟦ con c ⟧ γ が A であるため、∃̇∈ (con c) _ の標準的な意味論が対応する節へと計算によって展開される箇所そのものです。残りはすべて合同性です。結論は単なる同値でなく命題宇宙 hProp ℓ の中のパスなので、二つの命題はそのまま同一視され、後の議論でそれに沿って輸送できます。
この命題は論理式 φ と環境 γ の両方に対して量化し、命題宇宙 hProp ℓ の中のパスを主張します。relativize c が原子式を触っていないため、左辺 γ ⊨ (t ∈̇ u) はちょうど命題 ⟦ t ⟧ γ ∈ˢ ⟦ u ⟧ γ に計算され、これは定義上 γ ⊨ᴬ (t ∈̇ u) そのものです。等号と偽も同様なので、これらのケースは追加の段階なしに、定義的等価を意味する refl で証明されます。結合子のケースは対応する論理演算に cong₂ を適用します。部分の結果が一致するので、結合された命題も一致します。
relativize-correct : ∀ {n} (φ : Formula K n) (γ : S ^ n) → (γ ⊨ relativize c φ) ≡ (γ ⊨ᴬ φ) relativize-correct (t ∈̇ u) γ = refl relativize-correct (t ≐ u) γ = refl relativize-correct (φ ∧̇ ψ) γ = cong₂ _⊓_ (relativize-correct φ γ) (relativize-correct ψ γ)
存在量化のケースが核心です。左辺の relativize c (∃̇ φ) は ∃̇∈ (con c) φ′ であり、有界な存在量化の標準的意味論は ∃[ x ] (x ∈ˢ ⟦ con c ⟧ γ) ⊓ ((x ∷ γ) ⊨ φ′) です。しかし ⟦ con c ⟧ γ は A = ι c に計算されるため、拡張環境 x ∷ γ での帰納法の仮定により内部の ⊨ φ′ を ⊨ᴬ φ に置き換えると、この式は定義的に ∃̇ φ の ᴬ 節になります。形式的には、funExt がすべての x にわたる各点ごとの一致を添字族の一致に変え、cong がそれをガード x ∈ˢ A ⊓ _ を通して輸送し、外側の cong (λ P → ∃[ x ] P x) が族の一致をその結合の一致へ持ち上げます。全称量化のケースは ∀[ x ] P x と ⇒ を用いた双対です。
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 c が元の境界の項 t を保持し、⊨ᴬ も量化子を ⟦ t ⟧ γ でガードするため、ガードは決して変わりません。x ∷ γ での帰納法の仮定を通して本体の充足を変換するだけで、同じ funExt、内側の cong、外側の cong (λ P → ∃[ x ] P x) か cong (λ P → ∀[ x ] P 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 →
10 個のケースがすべて扱われ、再帰は φ に対するものなので、証明はすべての論理式と環境に対して完了します。これで本章の議論は閉じます。相対化は純粋に構文的な変換であり、その出力は Δ₀ であり、命題をとる任意の ZF 構造におけるその標準的な意味は選んだ集合に制限された量化です。したがって後の章では、定義可能性の条件を集合 A に相対化し、Δ₀ 論理式を用いて作業し、その充足を A の内部での量化から直接読み取れます。そのすべてがこの一つの帰納に支えられています。
cong (λ q → (x ∈ˢ ⟦ t ⟧ γ) ⊓ q) (relativize-correct φ (x ∷ γ))))
まとめ
relativize は Δ₀ 論理式を作り、Δ₀-relativize はその複雑さの上界を記録し、relativize-correct はその意味を選んだ集合の内部での量化と同定します。この三つを合わせると、任意の論理式を一つの集合に制限するという標準的な集合論の手法が得られます。構文的には集合を名指す定数で量化子を有界化し、意味論的にはここで証明した一つの帰納がそれを担います。この先では、Δ₀ の証拠が絶対性の議論に供給され、正当性のパスにより、定義可能性を解析する際に相対化された論理式の充足を A の上の有界量化に置き換えられます。