Bedrockこの章を読むか、対話型目次と依存グラフで別のルートを選べます。
対話型目次 · 依存グラフ宇宙レベル ℓ を固定し、lem : LEM (ℓ-suc ℓ) を仮定する。この仮定は該当するレベルの各命題に判定を与え、以下の構成の明示的なパラメータとして保たれる。
module L.Coding.SatisfactionGraphSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
W を構成可能集合とし、論理式の定数が値を取るアルファベットと、環境の各成分が値を取る範囲の両方に用いる。一様な充足関係の構成は、AllCodes W の各論理式符号に、その論理式を満たす環境の集合を割り当てる。本章では、この割り当て自身が L の内部にグラフを持つことを証明する。その要素は、論理式符号と対応する充足集合の順序対である。数学的な要点は置換公理である。一様なグラフ論理式は各符号の上で一意な値を持つので、集合 AllCodes W 上の像を一つの集合に集められる。
このような構成可能集合 W を固定し、符号化に必要な命題のレベルで排中律を仮定する。順序対は周囲の階層で構成されるが、定義域、値、グラフはいずれも構成可能な論域 S に属する。
定義域 AllCodes W は、W のアルファベット上の整形式な論理式符号からなる構成可能集合である。論理式の構文がグラフ論理式の型を与え、依存対の外延性が後に、解とその充足証明からなる依存対の一意性を示す。
累積階層の所属は切り詰められた存在を表すため、任意のグラフ要素の最終的な特徴づけも切り詰められた形になる。論域 S は構成可能構造 𝒮ʟ のもので、その各要素は周囲の集合と構成可能性の証明からなる。
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
open hPropView 𝒮ʟ using ( S )
ここで使う充足関係は、制限構造 𝒮ᵥ ↾ isL、すなわち構成可能構造 𝒮ʟ 上の内側の意味論である。定数はその論域上の恒等写像で解釈される。したがって _⊨_ は、論理式が L で満たされることを直接に表し、本章では周囲の意味論との比較定理を使わない。
module AbsSF = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _⊨ᵐ_ )
open AbsSF using () renaming ( _⊨ᵐ_ to _⊨_ )
固定した W に対し、一様な構成の二つのパラメータをこの同じ集合で具体化する。したがって、符号のアルファベットと環境の値域はいずれも W である。Table.graph W W は AllCodes W のすべての要素に一様に適用される二項論理式であり、値の関係を記述する。Table.val W W x mx は、特定の符号 x におけるその一意な値である。
module SatGraph (W : S) where
論理式符号 x とその所属証明 mx に対し、この一意な値を valOf x mx と書く。等式 valOf≡ は、それを定義上 Table.val W W x mx と同一視する。この記法により、グラフを集める対象の数学的な関数、すなわち定義域の要素をその充足集合へ送る関数が明確になる。
opaque
valOf : (x : S) → ⟨ x .fst ∈ (AllCodes W) .fst ⟩ → S
valOf x mx = Table.val W W x mx
valOf≡ : (x : S) (mx : ⟨ x .fst ∈ (AllCodes W) .fst ⟩) → valOf x mx ≡ Table.val W W x mx
valOf≡ x mx = refl
gr を一つの二項論理式 Table.graph W W とする。第一の自由な位置には充足集合の候補が、第二の位置には論理式符号が入る。したがって、この論理式が定める関係は、符号と値の間のグラフ関係の候補である。
private
opaque
unfolding valOf
gr : Formula S 2
gr = Table.graph W W
二つの事実により gr は関数的になる。存在性は、表の値とその論理式符号について gr が成り立つことを述べ、証人は Table.funct から得る。一意性は、同じグラフ論理式を満たす任意の y が valOf x mx に等しいことを述べ、表の一意性定理を対称にして得る。
defines' : (x : S) (mx : ⟨ x .fst ∈ (AllCodes W) .fst ⟩) → ⟨ (valOf x mx ∷ x ∷ []) ⊨ gr ⟩
defines' x mx = Table.funct W W x mx .fst .snd
only' : (x : S) (mx : ⟨ x .fst ∈ (AllCodes W) .fst ⟩) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ gr ⟩ → y ≡ valOf x mx
only' x mx y h = sym (Table.val-uniq W W x mx y h)
各論理式符号について、gr の解の型は可縮である。その中心は、値 valOf x mx と、この値が gr を満たす証明 defines' からなる依存対である。別の解 (y , h) があれば、only' がまず二つの値を同一視する。残る成分は同じ命題の証明なので、Σ≡Prop が値の等しさを完全な依存対の等しさへ持ち上げる。この可縮性こそ、置換に必要な関数性の前提である。
M : Recursion
M = record
{ dom = AllCodes W ; graph = gr
; funct = λ x mx → (valOf x mx , defines' x mx)
, λ { (y , h) → Σ≡Prop (λ w → ((w ∷ x ∷ []) ⊨ gr) .snd) (sym (only' x mx y h)) } }
これで、構成可能集合 AllCodes W 上の関数的関係 gr に置換を適用できる。順序対 pr (x .fst) ((valOf x mx) .fst) が一つの構成可能集合に集められ、これを pairs と書く。したがってグラフは L の内部にある。定義域と各値が構成可能であり、置換がそれらの対関係を一つの集合にするからである。
module G = MapGraph M using ( F; F-in; pair-out )
opaque
pairs : S
pairs = G.F
AllCodes W の各論理式符号は、グラフの順序対を一つ与える。具体的に pairs-in は、基礎となる符号と基礎となる充足集合の順序対が pairs に属することを証明する。
pairs-in : (x : S) (mx : ⟨ x .fst ∈ (AllCodes W) .fst ⟩) → ⟨ pr (x .fst) ((valOf x mx) .fst) ∈ pairs .fst ⟩
pairs-in = G.F-in
逆に、順序対 pr (x .fst) (y .fst) が pairs に属すると仮定する。置換像のファイバーは命題値なので、切り詰められた証人を、x が AllCodes W に属し、y がそこでの一意な値に等しいことを述べる依存対へ消去できる。これが pairs-out の切り詰めなしの結論である。
pairs-out : (x y : S) → ⟨ pr (x .fst) (y .fst) ∈ pairs .fst ⟩
→ Σ[ mx ∶ ⟨ x .fst ∈ (AllCodes W) .fst ⟩ ] (y .fst ≡ (valOf x mx) .fst)
pairs-out = G.pair-out
pairs の任意の要素が、最初から順序対として表示されているとは限らない。そのため、一般の像定理が与える特徴づけは切り詰められている。すなわち、論理式符号 x、所属証明 mx、その要素を x と値の順序対として表示する等式が単に存在する。これが pairs-shape であり、切り詰めは置換像への所属から受け継がれる。
pairs-shape : (e : S) → ⟨ e .fst ∈ pairs .fst ⟩
→ ∥ Σ[ x ∶ S ] Σ[ mx ∶ ⟨ x .fst ∈ (AllCodes W) .fst ⟩ ] (e .fst ≡ pr (x .fst) ((valOf x mx) .fst)) ∥₁
pairs-shape e h = MapGraph.F-out M (e .fst) h
したがって pairs は、論理式の定数と環境の値がともに W から取られる一様な充足関係の内部グラフである。一様な値の存在と一意性が関係を関数的にし、置換がその関係を L の集合にし、三つの所属定理が、表示された順序対と任意の要素の両方についてこの集合を特徴づける。