周囲の論理式から L 上の論理式へ

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

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

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

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

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

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

open import Base.Prelude

module L.Absoluteness {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )

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

open import FOL.Syntax using ( Formula )
open import FOL.LevyHierarchy using ( Δ₀ )
open import FOL.Manipulation.ConstantBounding using ( BoundedFo; module Relabel )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
import FOL.Absoluteness

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

import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )

open import Cubical.Data.Vec using ( map )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V )

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

open hPropStructure 𝒮ʟ using ( S )

module SemV = FOL.Semantics 𝒮ᵥ
open SemV using ( _^_ )
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 へ送ります。三角条件は fst (c , p) が c であることを要求し、これは refl で成り立ちます。したがって唯一の正しさの義務は計算によって果たされ、L から入ってきたデータは証拠 p だけだったことになります。

module ToL = Relabel {K = V ℓ} {K' = S} {W = V ℓ}
  id 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 fst で項ごとに射影され、元の論理式 φ が周囲の階層の中で評価されます。両辺とも同じ hProp の命題なので、主張される一致は単一のパスであって、含意ではありません。

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

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

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

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

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

まとめ

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