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

対話型目次 · 依存グラフ

この章の作業はすべて、単一の宇宙レベル ℓ の上で行われる。言語を解釈する二つの構造では、等号と所属がともに hProp (ℓ-suc ℓ) に値を取るため、充足の主張は命題であり、二つの主張はパスで比較できる。外側の世界はこのレベルの累積階層 V であり、内側の世界は L、つまり構成可能な集合への制限として得られるものである。

module L.Absoluteness {ℓ : Level} where

符号化の諸章が階層についての論理式を渡してくれたとき、同じことを L の内部で言いたくなるであろう。ここには二つの調整が必要である。論理式の定数は現在 V ℓ という型に属するが、L の中でこの論理式を読むには、各定数を制限された台の要素、すなわち集合と、それが構成可能であることの証拠の組に置き換えなければならない。さらに、元の論理式の充足は制限された構造ではなく周囲の構造で計算されていた。本章はこの二つを取り除く。しかも一度に一つの論理式ずつである。移送されるのは特定の φ と、その定数が選ばれた境界を守ること、そしてその形が Δ₀ であることを記録するデータである。

取り除きは二つの事実に依存する。それぞれ別の章で証明済みのものである。第一に、改名の機構は、任意の複雑さの論理式について、各定数が選んだ界を満たす証拠を伴う限り、定数を置き換えられる。ここで界として取るのは「ある段階に属する」ではなく「構成可能である」であり、証拠とは構成可能性の証明である。第二に、Δ₀ 絶対性は、有界論理式が推移的クラスの内側でも外側でも同じ意味を持つ、という主張である。この性質は一つ一つの論理式について、その式が Δ₀ であることを証明する帰納的な証拠の上の帰納法で確立される。任意の論理式に対する包括的な絶対性はなく、またあってはならない。非有界の量化子は、定義域が縮めば真偽を変えるからである。

この二つを合わせると移送定理が得られる。定数がすべて構成可能である Δ₀ 論理式は L の対象言語の中で読むことができ、二つの読み方は一致する。一致は真理値のパスであり、四段階で組み立てられ、証明自身は帰納を一切使わない。帰納はすでに、それぞれの元の章で、この章が受け取るデータのために使い果たされている。

論理式 φ の定数は周囲の解釈が選ぶ型に属し、証拠 h : BoundedFo InL φ は各定数が構成可能であることを述べる。改名はその定数を、周囲の集合と構成可能性の証明からなる対へ送る。しかもこの置き換えは、任意の複雑さの論理式に使える。非有界の量化子はそのまま連れて行かれる。定理 ⊨-map は定数の型を変える前後の充足を比較し、Δ₀ 絶対性は外側の構造と制限した構造を比較する。ただしそれは、論理式がみずからの Δ₀ の証拠を伴っていることをさらに要求する。

二つの世界に名前を付ける。周囲の構造は 𝒮ᵥ、すなわち階層 V ℓ 上の ZF 風の構造である。等号はパスで、所属は階層本来のものである。内側の構造は 𝒮ʟ、つまり 𝒮ᵥ を構成可能な集合のクラス isL に制限したものである。本章はすでに isL を、定数の満たすべき境界として選んでいる。絶対性の実例は、同じクラスに対してさらに一つ、それが推移的であることを要求し、isL-trans が記録するのはこの点である。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V )

二つの充足関係は同じ型 hProp (ℓ-suc ℓ) に値を取る。制限された台 S の元は、周囲の集合とその構成可能性の証拠の対である。周囲の定数は id により自分自身を表し、内側の定数はすでにそのような対なので、fst で周囲の集合を取り出せる。この二つの解釈が移送証明の両端である。

open hPropView 𝒮ʟ using ( S )

module SemV = FOL.Semantics 𝒮ᵥ
open SemV.At (V ℓ) id using () renaming ( _⊨_ to _⊨v_ )

絶対性の定理は一度だけ実例化される。境界としてすでに選ばれたクラス isL の上で、追加の入力 isL-trans がこのクラスが推移的であることを述べる。その Δ₀ の法則 abs₀ は、内側の言語の論理式とその Δ₀ の証拠を受け取り、内側と外側の充足の間の真理値のパスを返す。証拠は形式的な飾りではなく実引数である。この法則が使えるのは、Δ₀ の証拠が書き下された論理式に対して正確に限られ、その証拠が、絶対性の章で一度だけ行われた帰納に対して、この特定の論理式がどのように組み立てられているかを伝えるからである。以降、内側の充足関係には平易な _⊨_ の名が与えられる。表に立つ充足関係はこれ一つだからである。

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

境界は構成可能性

論理式を動かす前に、改名の機構にどの定数が適格で、それらが何になるかを知らせておく必要がある。この節の選択のすべてはその界にある。階層のある定数が適格であるのは、それが構成可能なときであり、台の要素として成るのは、定数とその構成可能性の証拠の対である。像を集合として読み戻せばもとの定数が得られるという往復の条件は、像が集合を第一成分として格納するため、refl で成り立つ。この実例で L について使われるのはこれだけで、それ以外のことは何も使われない。

定数をまったく含まない読み方は、証明なしに適格である。これに名を与えておく価値がある。構造に関する読み方のほとんどはまさにこの種のもので、変数と有界量化子だけによって語り、構成可能であるべきものが何もないからである。

界の述語こそ、この節の選択のすべてである。階層の定数 c が適格であるのは、命題 isL c が成り立つとき、すなわち c が構成可能階層のある序数の段階に属するときに限る。InL はこの命題値のクラスの基礎型を取り出すだけである。レベルがどこにあるかにも注意してほしい。isL c はレベル ℓ-suc ℓ の命題なので、InL はそのレベルの型に値を取る述語であり、集合の決定可能な性質ではない。

InL : V ℓ → Type (ℓ-suc ℓ)
InL c = ⟨ isL c ⟩

部分的な定数写像は点ごとに固定される。源の定数は、すでに共通の世界 V ℓ の中で集合であるため id で読まれ、先の定数、つまり台 S の要素は fst で読まれる。部分的な割り当ては、証拠 p : InL c を伴う各適格な定数 c を対 c , p へ送る。三角条件は (c , p) .fst が c であることを要求し、これは refl で成り立つ。したがって唯一の正しさの義務は計算によって果たされ、L から入ってきたデータは証拠 p だけだったことになる。

module ToL = Relabel {K = V ℓ} {K' = S} {W = V ℓ}
  id (λ p → p .fst) InL (λ c p → c , p) (λ c p → refl)

この具体化では、liftFo は、定数が InL を満たす任意の複雑さの論理式に使え、各定数を周囲の集合とその構成可能性の証拠の対へ置き換える。そして Δ₀-liftFo h dφ は、元の論理式の Δ₀ の証拠 dφ を、持ち上げられた論理式の Δ₀ の証拠へ変える。transferFo が用いる双方向の法則 abs₀ が充足を比較するのは Δ₀ 論理式に限られるため、証拠は伴って運ばれねばらず、その運搬を可能にするのがまさにこの改名である。

open ToL public using ( liftFo; Δ₀-liftFo )

移送

この節の問いはこうである。定数が構成可能な、階層についての Δ₀ の主張は、L の内側で成り立つことと外側で成り立つこととが、いつまさに一致するのか。答えが transferFo であり、模型の側から外へ向かって読む四つのパスの連結として証明される。第一段階だけが絶対性の帰納を使う。その帰納は Δ₀ の証拠の上で、みずからの章の中ですでに一度完了しており、ここでは目の前の持ち上げられた論理式において呼び出されるだけである。残りの三段階は改名の簿記であり、定数はここではじめて顧みられ、何も変わっていないことが分かる。

この簿記の一箇所には、説明を加える価値がある。最後の段階にある恒等的な改名は無駄ではない。定数上の恒等写像による像は、その写像が再帰的に適用されるため、論理式を定義的に等しいものにはしない。しかしその意味は等しく、それこそ改名の定理が f = id で述べていることである。

この主張が等しいと置くのは、先験的には異なる世界に住む二つの充足の判断である。左辺では環境 γ は S の要素、すなわち構成可能性の証明を伴う集合からなり、γ ⊨ liftFo φ h は定数が L へと改名された論理式の L 内での充足である。右辺では同じ環境が map (λ p → p .fst) で項ごとに射影され、元の論理式 φ が周囲の階層の中で評価される。両辺とも同じ hProp の命題なので、主張される一致は単一のパスであって、含意ではない。

transferFo : ∀ {n} (φ : Formula (V ℓ) n) (h : BoundedFo InL φ) → Δ₀ φ
           → (γ : Vec S n) → (γ ⊨ liftFo φ h) ≡ ((map (λ p → p .fst) γ) ⊨v φ)

第一段階は解釈する構造を取り替えるだけで、構文はそのままである。絶対性は、内側の Δ₀ の証拠 Δ₀-liftFo h dφ とともに適用され、持ち上げられた論理式の L における充足を、同じ論理式の、射影後の環境での階層における充足へ書き換える。第二段階は f = (λ p → p .fst) とした改名の定理 ⊨-map で、持ち上げられた論理式の定数と環境の変数の、射影の下での解釈を処理する。定数と環境の各成分を fst を通して読んでも、この論理式の述べることは変わらないのである。二つの段階は内側の世界の作られ方と一致し、sym が第二を連鎖に必要な向きで提示する。

transferFo φ h dφ γ =
    abs₀ (Δ₀-liftFo h dφ) γ
  ∙ sym (⊨-map 𝒮ᵥ (λ p → p .fst) id (liftFo φ h) (map (λ p → p .fst) γ))

残りの二段階が定数に関わり、合わせて改名が何も変えていないことを述べる。正しさの法則 liftFo-correct は構文の水準のパス mapFo (liftFo φ h) .fst ≡ mapFo id φ を与える。三角条件が各定数で成り立っていたため、改名後の論理式を fst に沿って世界へ押し込んだものは、元の論理式を id に沿って押し込んだものと同じになる。続いて合同が、このパスを固定された環境と充足の記号の下へ動かす。最後に f = id の ⊨-map が、論理式とその恒等像が同じ意味を持つと述べ、連鎖は閉じる。L の内側の充足は φ の周囲の充足に等しいのである。

  ∙ cong (λ ψ → (map (λ p → p .fst) γ) ⊨v ψ) (ToL.liftFo-correct φ h)
  ∙ ⊨-map 𝒮ᵥ id id φ (map (λ p → p .fst) γ)

まとめ

liftFo は、定数が構成可能である限り、階層についての任意の複雑さの論理式を L の対象言語へ運ぶ。transferFo は Δ₀ の証拠の存在をさらに要求し、そのとき二つの読み方が一致すると述べる。したがってこのページの同値は Δ₀ に限られる。Δ₀ の外では、絶対性の章が二つの一方向の法則、Σ₁ の真理が上向きに保存されることと Π₁ の真理が下向きに保存されることを証明しており、これら二つの隣接するクラスにそれぞれ適用される。どちらの結果も、L の内側で何を述べられるかの制限ではない。そちらの分出と置換の論理式のスキーマは、任意の複雑さの論理式を受け取る。制限されるのは、階層から直接どの結論を引き出せるかである。無制限の形で書く方が容易な述語は、この経路を通さず、模型の上に直接、無制限に書かれるべきである。