この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

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

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

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

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

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

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

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

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

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )

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

open hPropView 𝒮ʟ

ホスト側の述語 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 (a .fst) (a .snd)
  R   = mkReflect φ sa (stage-ord (a .fst) (a .snd))
  β   = R .fst
  oβ  = R .snd .fst

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

  c   = LsetS β oβ

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

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

反映を適用できるのは、成分が Lset β に属する環境だけなので、分出公理の述語にある所属の連言が本質的な役割を果たす。x ∈ˢ a が与えられると、推移性によりこの事実と fa∈β から x .fst ∈ Lset β が得られ、_ が一成分環境の空の末尾に対する自明な条件を与える。そこで 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 は小さな表示 ⟪ a .fst ⟫ にわたる。各小さな添字が表す要素について中心の最小段階を取り、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 は各点のパスを述語の等式へまとめる。順方向は、命題的切り詰めを受けた始域の要素から始まる。ここで rec₁ がその証人を調べられるのは、行き先が BoundedImage y の基礎にある命題だからであり、(BoundedImage y) .snd がまさにそのことを証明する。証人はこの命題の中でだけ使われ、切り詰められていないデータとして返されることはない。

    Q≡ : Image ≡ BoundedImage
    Q≡ = funExt (λ y → ⇔toPath (into y) (out y))
      where
      into : (y : S) → ⟨ Image y ⟩ → ⟨ BoundedImage y ⟩
      into y = rec₁ ((BoundedImage y) .snd) λ { (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 φ の充足を含んでいる。map₁ は同じ始域の要素と所属の証明を命題的切り詰めの内側に保ったまま、⊨-swap φ x y に沿う輸送によって最後の成分を y ∷ x ∷ [] における φ の充足へ変える。得られるのは Image y である。これと順方向の含意から Q≡ が証明され、上の定義式の冒頭にある輸送が、完全な分出公理で得た集合を、完全な置換公理が要求する一意な集合へ変える。この比較では証人を一つも選び出していない。

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

まとめ

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