完全な分出公理と置換公理

この章を読むか、読書案内と依存マップで別のルートを選べます。

読書案内 · 依存マップ

有界な分出公理は、Δ₀ 論理式で定義される構成可能な部分集合を作れますが、分出公理図式は任意の一階論理式を許します。本章では、分出する集合を含む段階で一つの論理式を反映することにより、この隔たりを埋めます。次に、始集合上の関数的関係のすべての値を一つの段階へ入れ、得られた完全な分出公理で集めることにより、完全な置換公理を証明します。本章で証明するのは、この二つの公理図式の欄です。ZF と ZFC のレコード全体は後の章で組み立てます。

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

古典的なパラメータは、ホスト側の原理 LEM だけです。指定された宇宙レベルで、各命題について証明か反駁のいずれかを返します。これはホスト側の選択公理ではなく、命題的切り詰めを受けた存在の任意の族から証人を選ぶ操作も与えません。また、後に集合論のモデル内で解釈される選択公理とも異なります。

open import Base.Prelude
open import Base.Classical using ( LEM )

lem : LEM (ℓ-suc ℓ) を固定します。このモジュールのすべての構成は、この一つのホスト側の仮定に相対的です。数学的な結論は、構成可能モデルにおける任意の一階論理式に対する分出公理図式と置換公理図式です。対象理論の選択公理は、ここでは仮定も証明もされません。排中律への依存は、後で使う最小段階と論理式の反映の定理を通して入ります。前者では条件を満たすより小さな段階が単に存在するかを判定し、後者では非有界全称量化子の逆向きで行列が成り立つかを判定します。

module L.Axioms.Full {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

議論では構文と意味論の間を行き来します。Formula S n の要素は、n 個の変数位置をもち、S の要素を定数とする対象言語の論理式です。con はそのような定数を論理式へ入れます。改名は変数が読む環境の位置を変え、それに対応する充足関係の定理を伴います。相対化は各非有界量化子を、選んだ定数で有界な量化子に置き換え、Δ₀-relativize は得られた論理式が有界であることを構造的に証明します。元の論理式と相対化された論理式の一致は反映から得られるのであり、構文変換だけからは得られません。

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( con; Formula; ∃̇∈ )
open import FOL.Manipulation.Renaming using ( renameFo; module Sat )
open import FOL.Manipulation.Relativization using ( relativize; Δ₀-relativize )
import FOL.Absoluteness

この言語には二つの構造による解釈があります。周囲の累積階層の構造 𝒮ᵥ は V ℓ のすべての集合を解釈し、𝒮ʟ の要素は構成可能性の証明を備えた集合です。添字 β に対し、Lset β は対応する構成可能段階です。その段階であることの証明から推移性が得られ、順序数添字どうしの厳密な所属に沿って Lset-mono が所属を上の段階へ移します。構成可能集合ごとに、stage はその集合を含む最小の順序数段階の添字を、順序数性と所属の証明とともに与えます。本章で使うのは後の二つの事実であり、最小性そのものではありません。

import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; Lset; Lset-layer; layer-trans; Lset-mono )
open import L.Stage {ℓ} lem using ( stage; stage-ord; stage-mem )

有界な分出公理と反映が、任意の論理式への橋渡しをします。有界な一変数論理式に対し、separateΔ₀ は必要な要素をもつ一意な構成可能集合を作ります。一つの任意の論理式 φ と一つの順序数 δ に対し、mkReflect は δ ∈ β を満たす順序数 β を作り、成分が Lset β に属する環境上で φ とその相対化を同一視します。これは指定された論理式とパラメータについての反映であり、Lset β が初等部分モデルであるという主張ではありません。置換公理のためには、FunctionalImage が、ある x ∈ˢ a と関係するすべての y を含む一つの順序数段階を与え、LsetS がその段階を対象言語の定数として表します。

open import L.Axioms.Separation {ℓ} lem
  using ( module FunctionalImage; separateΔ₀ )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.FormulaReflection {ℓ} lem using ( mkReflect )

いくつかのホスト側の構成により、意味論上の一致が正確なパスになります。⇔toPath は命題値の真理の間の双方向の含意をパスに変え、関数外延性は各点でのパスから述語を同一視します。hProp の添字付き存在は命題的切り詰めを受けています。置換公理の証明では、PT.rec はそのような存在を別の命題へだけ除去し、PT.map は証人を切り詰めの外へ出さずに変換します。どちらの操作も、始域の要素を大域的に選びません。

open import Cubical.Data.Unit using ( tt* )
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )

𝒮ʟ の台 S は、V ℓ の集合と、その構成可能性の証明からなります。その等しさと所属関係は基礎にある集合だけを見るので、x ∈ˢ a は、後で段階の推移性と組み合わせる外側の所属を与えます。対象言語の論理式はこの台にわたって量化するため、その定数と環境の各成分は、モデル内にとどまるために必要な構成可能性の証明を保っています。

open hPropStructure 𝒮ʟ

ホスト側の述語 Q : S → hProp (ℓ-suc ℓ) に対し、SetOf Q は、モデルの要素 b と、各点でのパス (x ∈ˢ b) ≡ Q x の組からなる型です。したがって isContr (SetOf Q) は強い一意存在を表します。その中心が実際の実現集合を与え、収縮が他のすべての実現者を中心と同一視します。Q は、対象言語の論理式の充足関係から作られる場合でも、ホスト側の関数です。中心からの射影は、すでにあるデータを取り出すだけで、記述原理を使いません。

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

絶対性の構成は、同じ構文に対して 𝒮ᵥ での外側の読みと 𝒮ʟ での内側の読みを与えます。ここでは内側の関係 _⊨ᵐ_ を _⊨_ と改名します。したがって γ ⊨ φ は、それ自体がホスト側の命題であり、有限環境 γ のもとで対象言語の論理式 φ が構成可能構造において真であることを述べます。任意のホスト側の述語を構文へ代入することとは異なります。

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )

後で使う二つの変数順序を比較するため、定数を恒等関数で解釈して、𝒮ʟ における改名の意味論を具体化します。Ren.Agrees は各点で、改名された変数位置と別の環境の対応する位置が同じ成分を読むことを述べます。この一致が与えられると、Ren.⊨-rename は、改名後の論理式の充足関係を、並べ替えた環境における元の論理式の充足関係と同一視します。

module Ren = Sat 𝒮ʟ id

二つの補助道具

最初の局所補題は、基礎にある集合についての推移性を記録します。x ∈ y かつ y ∈ Lset β ならば、各構成可能段階は推移的集合なので x ∈ Lset β です。ここで変数は V ℓ の要素であり、この補題は x の構成可能性の証明を作りません。後で使うときには x : S がすでにその証明をもち、transIn は反映に必要な段階への所属だけを与えます。

private
  transIn : (β : V ℓ) {x y : V ℓ} → ⟨ x ∈ y ⟩ → ⟨ y ∈ Lset β ⟩ → ⟨ x ∈ Lset β ⟩
  transIn β = layer-trans (Lset-layer β)

置換公理では、一つの二変数論理式を二通りの環境順序で使います。モデルでの主張 (y ∷ x ∷ []) ⊨ φ では、像 y がスロット零、始域の要素 x がスロット一に置かれます。しかし、存在量化子が始域の要素を束縛した後、その本体は (x ∷ y ∷ []) で評価され、新たに束縛された x がスロット零に置かれます。関数 swap は Fin 2 のこの二つの位置だけを交換し、数学的関係の向きを逆にするものではありません。

  swap : Fin 2 → Fin 2
  swap zero    = suc zero
  swap (suc _) = zero

論理式の改名を swap に適用して swapFo を得ます。φ が像を位置零、始域の要素を位置一で読むなら、swapFo φ は始域の要素を先に置いた環境で評価できます。これは自由変数位置の構文的な並べ替えであり、その意味論上の根拠は改名の正しさから別に得られます。

  swapFo : Formula S 2 → Formula S 2
  swapFo = renameFo swap

具体的な要素 x と z に対し、二つの環境はこの転置のもとで各点ごとに一致します。位置零では、swap は x ∷ z ∷ [] の第二成分 z を読み、位置一では x を読みます。したがって必要な二つのパスはいずれも refl に計算され、二成分の環境に対する Ren.Agrees の証明が完成します。

  swapAgrees : (x z : S) → Ren.Agrees swap (x ∷ z ∷ []) (z ∷ x ∷ [])
  swapAgrees x z zero       = refl
  swapAgrees x z (suc zero) = refl

改名の正しさから、置換公理で使う正確な意味論的変換が得られます。(x ∷ z ∷ []) ⊨ swapFo φ は (z ∷ x ∷ []) ⊨ φ と同じ命題です。x を始域の要素、z を像と読むと、左辺は有界存在量化子が作る順序であり、右辺はモデルが要求する像を先に置く順序です。このパスは通常の輸送により両方向に使えます。

  ⊨-swap : (φ : Formula S 2) (x z : S)
         → ((x ∷ z ∷ []) ⊨ swapFo φ) ≡ ((z ∷ x ∷ []) ⊨ φ)
  ⊨-swap φ x z = Ren.⊨-rename swap φ (x ∷ z ∷ []) (z ∷ x ∷ []) (swapAgrees x z)

分出公理

完全な分出公理は、有界性の仮定を置かず、すべての一変数対象言語論理式 φ : Formula S 1 を量化します。その目標は、a に属し、かつ φ を満たす x だけを要素とするモデル内の集合が一意に存在することです。証明は相対化された論理式に有界な分出公理を適用し、実現者全体の可縮な型を sym Q≡ に沿って輸送します。したがって一意性は separateΔ₀ から得られ、反映の後で証明し直す必要はありません。

hasSeparationL : (a : S) (φ : Formula S 1)
               → isContr (SetOf (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)))
hasSeparationL a φ =
  subst (λ Q → isContr (SetOf Q)) (sym Q≡)
    (separateΔ₀ a (relativize c φ) (Δ₀-relativize c φ))

まず、反映を使う段階の中にパラメータ a が入るよう準備します。その基礎にある集合の最小段階添字を sa とし、stage-ord がこの添字の順序数性を証明します。sa を与えて mkReflect φ を適用すると、順序数 β、厳密な所属 sa ∈ β、および Lset β に入るすべての環境について φ とその相対化の充足命題を結ぶパスが得られます。ここで sa を渡すことには意味があります。反映段階は初めからこの添字を含むように作られるのであり、後から拡大されるのではありません。

  where
  sa  = stage (fst a) (a .snd)
  R   = mkReflect φ sa (stage-ord (fst a) (a .snd))
  β   = R .fst
  oβ  = R .snd .fst

添字 β、基礎にある集合 Lset β、モデルの要素 c は、それぞれ異なる対象です。証明 oβ : IsOrd β により、LsetS β oβ はその段階を構成可能性の証明と組にして、要素 c : S にします。これは relativize が必要とする形です。新しい量化子の境界は対象言語の定数なので、段階は周囲の集合として使うだけでなく、モデルの内部で表されなければなりません。

  c   = LsetS β oβ

これでパラメータを反映段階へ入れられます。stage-mem は fst a ∈ Lset sa を与え、反映のデータは順序数の厳密な所属 sa ∈ β を与えます。構成可能階層の単調性により、この二つから fa∈β : fst a ∈ Lset β が得られます。ここで a を順序数と同一視してはいません。sa と β は添字であり、fst a は上の段階へ入れられる集合です。

  fa∈β : ⟨ fst a ∈ Lset β ⟩
  fa∈β = Lset-mono {α = β} {β = sa} (R .snd .snd .fst)
           (stage-mem (fst a) (a .snd))

反映を適用できるのは、成分が Lset β に属する環境だけなので、分出公理の述語にある所属の連言が本質的な役割を果たします。x ∈ˢ a が与えられると、推移性によりこの事実と fa∈β から fst x ∈ Lset β が得られ、tt* が一成分環境の空の末尾に対する自明な条件を与えます。そこで R の反映成分を使うと、x における φ の充足関係から、その相対化の充足関係へのパス bridge が得られます。a の外にある任意の x : S については、比較を主張しません。

  bridge : (x : S) → ⟨ x ∈ˢ a ⟩
         → ((x ∷ []) ⊨ φ) ≡ ((x ∷ []) ⊨ relativize c φ)
  bridge x x∈a = R .snd .snd .snd (x ∷ []) (transIn β x∈a fa∈β , tt*)

残る仕事は、二つのホスト側の述語を比較することです。どちらの方向でも、共通の所属証明 x ∈ˢ a はそのまま保ち、充足関係の証明だけを bridge またはその逆向きに沿って輸送します。⇔toPath はこの二つの写像を x における命題値の間のパスに変え、funExt が各点でのパスを Q≡ へまとめます。これは述語の等しさです。ここでは存在の命題的切り詰めを除去せず、候補集合について外延性を使う議論も行いません。

  Q≡ : (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))
     ≡ (λ x → (x ∈ˢ a) ⊓ ((x ∷ []) ⊨ relativize c φ))
  Q≡ = funExt (λ x → ⇔toPath
    (λ { (x∈a , h) → x∈a , subst ⟨_⟩ (bridge x x∈a) h })
    (λ { (x∈a , h) → x∈a , subst ⟨_⟩ (sym (bridge x x∈a)) h }))

像を収める段階

各 x ∈ˢ a に対し、仮定は関係する値の依存和 Σ y , (y ∷ x ∷ []) ⊨ φ を可縮にします。その中心が一つの値を与え、収縮が関係するすべての値を中心と同一視するので、この段階ではホスト側の選択公理を使いません。FunctionalImage は小さな表示 ⟪ fst a ⟫ にわたります。各小さな添字が表す要素について中心の最小段階を取り、boundingOrd がそれらすべてを一つの順序数 βimg で上から抑えます。任意の x ∈ˢ a が与えられると、∈-asFiber は小さな添字と、その表示値が x の基礎にある集合に等しいというパスを返します。そのパスに沿って関係を添字が表す始域の要素へ移し、可縮性によって選ばれた中心を関係する各 y と同一視し、その等しさに沿って共通の段階上界を移します。この構成の最小段階を求める操作は依然として lem に依存しますが、選択公理は使いません。

module Images (a : S) (φ : Formula S 2)
              (fc : (x : S) → ⟨ x ∈ˢ a ⟩
                  → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩)) where
  open FunctionalImage a (λ x y → (y ∷ x ∷ []) ⊨ φ) fc public

置換公理

hasReplacementL の仮定は、a の各要素上の値のファイバーを可縮にし、その結論は像の述語を実現するモデル内の集合の型を可縮にします。これは異なる二つの一意性です。前者は各始域の要素に一つの値を与え、後者はそれらすべてをちょうど集める一つの集合を与えます。像の述語にある始域の要素の存在は命題的切り詰めを受けているため、存在するという事実だけを記録し、選ばれた要素を外へ出しません。opaque の境界が変えるのは Agda の定義上の簡約だけであり、この主張も仮定も変えません。

opaque
  hasReplacementL : (a : S) (φ : Formula S 2)
                → ((x : S) → ⟨ x ∈ˢ a ⟩
                     → isContr (Σ[ y ∈ S ] ⟨ (y ∷ x ∷ []) ⊨ φ ⟩))
                → isContr (SetOf (λ y → ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)))

置換公理の証明に必要な二つの材料が、これでそろいました。各点での可縮なファイバーから、Images は a の要素と関係するすべての値を含む一つの順序数段階を与えます。その段階において一変数論理式 imageFo に完全な分出公理を適用すると、BoundedImage を実現する集合からなる可縮型が得られます。以下で証明するパス Q≡ は、この述語を段階条件のない像の述語 Image と同一視します。したがって sym Q≡ に沿って輸送すれば、必要な可縮型 SetOf Image が得られます。これは任意の論理式 φ に対する完全な置換公理であり、前章の有界な置換公理の定理を適用したものではありません。

後に L.Model は、hasSeparationL と hasReplacementL を L⊨ZF の十二の欄のうち二つとして用います。その ZF レコードを組み立てた後で初めて、hasChoiceL L⊨ZF が L⊨ZFC を作るための対象理論の選択の欄を与えます。ここで lem : LEM (ℓ-suc ℓ) は古典的なホスト側の仮定であり、fc は定理に明記された各点での一意存在の仮定です。fc がすでに含む中心を射影するのにホスト側の選択公理は必要ありません。後で得られる選択の欄は結論であって、この証明の前提ではありません。

  hasReplacementL a φ fc =
    subst (λ Q → isContr (SetOf Q)) (sym Q≡)
      (hasSeparationL (LsetS βimg βimg-ord) imageFo)
    where
    open Images a φ fc

置換公理が要求する述語を、モデルの公理と同じ変数順序で直接述べます。候補 y が Image に属すのは、ある x ∈ˢ a について、像を先、始域の要素を後に置いた環境 y ∷ x ∷ [] で φ が成り立つとき、またそのときに限ります。hProp の添字付き存在は命題的切り詰めを用います。適切な始域の要素が存在するという事実は保ちますが、それがどの要素かは忘れます。したがって SetOf Image の可縮性が述べるのは、ちょうどこれらの像を要素とするモデル内の集合が一意に存在することであり、像集合そのものの要素が一つしかないということではありません。

    Image : S → hProp (ℓ-suc ℓ)
    Image y = ∃[ x ∶ S ] (x ∈ˢ a) ⊓ ((y ∷ x ∷ []) ⊨ φ)

同じ条件を分出公理によって得るには、それを一変数の対象言語論理式として表す必要があります。imageFo の有界存在量化子は定数 a の要素にわたります。始域の証人 x を導入すると、本体は環境 x ∷ y ∷ [] で評価されます。φ が想定する環境は y ∷ x ∷ [] なので、本体には swapFo φ を置き、⊨-swap が、この位置交換によって意図した関係が保たれることを証明します。a によって有界なのは、新たに加えたこの存在量化子だけです。φ は非有界な量化子を含み得るので、imageFo は Δ₀ 論理式とは限らず、完全な分出公理によって扱う必要があります。

    imageFo : Formula S 1
    imageFo = ∃̇∈ (con a) (swapFo φ)

完全な分出公理は共通の段階を表すモデル内の集合に適用されるので、それが実現する述語は二つの条件を含みます。第一の条件は y を Lset βimg に置き、第二の条件は y が imageFo を満たすと述べます。第一の連言は分出公理が加える領域の条件であり、論理式のすべての量化子を有界にするものではありません。真に像となる値については、range∈βimg がすでにすべてを共通の段階へ入れているため、この条件は余分です。残る証明は、この段階条件を加えても除いても、像の述語の外延が変わらないことを示します。

    BoundedImage : S → hProp (ℓ-suc ℓ)
    BoundedImage y = (y ∈ˢ LsetS βimg βimg-ord) ⊓ ((y ∷ []) ⊨ imageFo)

等式 Q≡ は各点での議論から得られます。候補 y ごとに、into y と out y が Image y と BoundedImage y の間の二つの含意を与えます。⇔toPath はそれらを命題値の間のパスにし、funExt は各点のパスを述語の等式へまとめます。順方向は、命題的切り詰めを受けた始域の要素から始まります。ここで PT.rec がその証人を調べられるのは、行き先が BoundedImage y の基礎にある命題だからであり、snd (BoundedImage y) がまさにそのことを証明します。証人はこの命題の中でだけ使われ、切り詰められていないデータとして返されることはありません。

    Q≡ : Image ≡ BoundedImage
    Q≡ = funExt (λ y → ⇔toPath (into y) (out y))
      where
      into : (y : S) → ⟨ Image y ⟩ → ⟨ BoundedImage y ⟩
      into y = PT.rec (snd (BoundedImage y)) λ { (x , (x∈a , h)) →

この許された命題への除去の内部で、始域の要素を x とし、x ∈ˢ a と (y ∷ x ∷ []) ⊨ φ の証明があるとします。値域についての定理 range∈βimg は y を共通の段階へ入れ、第一の連言を与えます。第二の連言では、同じ x を命題的切り詰めの中へ再び包みます。パス ⊨-swap φ x y の逆向きに沿う輸送は、y ∷ x ∷ [] における φ の充足を、x ∷ y ∷ [] における swapFo φ の充足へ移します。後者はちょうど imageFo の本体です。このように、この枝は始域の要素を切り詰めから結果として取り出すことなく、BoundedImage y の二つの部分を構成します。

        range∈βimg x x∈a y h
        , ∣ x , (x∈a , subst ⟨_⟩ (sym (⊨-swap φ x y)) h) ∣₁ }

逆向きの含意では、段階への所属の成分をそのまま捨てます。imageFo の充足はすでに、命題的切り詰めの下に、始域の要素 x、それが a に属すことの証明、そして x ∷ y ∷ [] における swapFo φ の充足を含んでいます。PT.map は同じ始域の要素と所属の証明を命題的切り詰めの内側に保ったまま、⊨-swap φ x y に沿う輸送によって最後の成分を y ∷ x ∷ [] における φ の充足へ変えます。得られるのは Image y です。これと順方向の含意から Q≡ が証明され、上の定義式の冒頭にある輸送が、完全な分出公理で得た集合を、完全な置換公理が要求する一意な集合へ変えます。この比較では証人を一つも選び出していません。

      out : (y : S) → ⟨ BoundedImage y ⟩ → ⟨ Image y ⟩
      out y (_ , h) = PT.map (λ { (x , (x∈a , h')) →
        x , (x∈a , subst ⟨_⟩ (⊨-swap φ x y) h') }) h

まとめ

完全な分出公理と完全な置換公理は、二つの還元から得られます。まず、始集合を含む段階内の環境上で指定された論理式を反映し、その真理値を Δ₀ 相対化の真理値へ移します。すると、有界な分出公理から完全な分出公理が得られます。次に、各点で可縮な値のファイバー、始集合の小さな表示、順序数による上界を用いて、関係するすべての値を一つの段階へ入れます。完全な分出公理がその像を集め、完全な置換公理を与えます。二つの結果は、古典的なパラメータ LEM (ℓ-suc ℓ) だけを保ち、ホスト側の選択公理を使いません。これらは後に L⊨ZF の分出と置換の欄を満たします。本章自体は ZF や ZFC のレコード全体を組み立てません。