数えられた始集合から Skolem 包を数える

この和は、二つの集合の内部の和である。

D : S
D = cupʟ D₁ D₂

左側の要素は、和の左の規則によって含められる。

in₁ : (z : S) → ⟨ z .fst ∈ D₁ .fst ⟩ → ⟨ z .fst ∈ D .fst ⟩
in₁ z = cupʟ-inl D₁ D₂ (z .fst)

右側の要素は対称的に含められる。

in₂ : (z : S) → ⟨ z .fst ∈ D₂ .fst ⟩ → ⟨ z .fst ∈ D .fst ⟩
in₂ z = cupʟ-inr D₁ D₂ (z .fst)

z ∈ D₁ ∪ D₂ なら、z が左側または右側に属することだけが得られる。この選言は命題的に切り詰められている。所属は、ある提示添字が z を名指すことを保つが、具体的な添字は保たないからである。

out : (z : S) → ⟨ z .fst ∈ D .fst ⟩ → ∥ ⟨ z .fst ∈ D₁ .fst ⟩ ⊎ ⟨ z .fst ∈ D₂ .fst ⟩ ∥₁
out z = cupʟ-out D₁ D₂ (z .fst)

D = D₁ ∪ D₂ と書く。どちらか一方の集合の要素は D に属し、D の各要素からは、二つの集合のいずれかに由来するという切り詰められた証明が得られる。

open Union2 D₁ D₂ public using ( D; in₁; in₂; out )

それぞれの符号化された単射は、その底にある関数と、グラフが符号化の言う通りにちょうど成立する証明を抽出する。

module X₁ = Extract E₁ D₁ (c₁ .fst) ((c₁ .snd) .fst) using ( toFun; toFun-graph )
module X₂ = Extract E₂ D₂ (c₂ .fst) ((c₂ .snd) .fst) using ( toFun; toFun-graph )

Mem z は z が和集合の定義域 D に属するという命題である。入力にこの証明を添えることで、場合分けされた関数を評価するために必要な定義域の証拠がちょうど得られる。

Mem : S → Type (ℓ-suc ℓ)
Mem z = ⟨ z .fst ∈ D .fst ⟩

左の定義域への所属は排中律で判定でき、この判定こそ、タグ付きの単射を作るための場合分けである。

Case : S → Type (ℓ-suc ℓ)
Case z = Dec ⟨ z .fst ∈ D₁ .fst ⟩

排中律は、和のすべての要素が左の定義域から来たかどうかを判定する。

decide : (z : S) → Case z
decide z = FOL.Semantics.decideMembership 𝒮ᵥ lem (z .fst) (D₁ .fst)

左の定義域に属さない要素は、右の定義域に属する。和の中の所属は二つの側に分かれ、左側は仮定された失敗と矛盾する。

off : (z : S) → Mem z → (⟨ z .fst ∈ D₁ .fst ⟩ → ⊥₀) → ⟨ z .fst ∈ D₂ .fst ⟩
off z m nmem = rec₁ ((z .fst ∈ D₂ .fst) .snd)
  (λ { (inl h) → ⊥₀-rec (nmem h) ; (inr h) → h }) (out z m)

それぞれの側の値はタグ付きの像である。数項のタグ 0 か 1 を、抽出された関数の値と対にする。こうして二つの単射は、重ならないタグ付きの値域に着地する。

val : (z : S) → Mem z → Case z → S
val z m (yes h) = prʟ (nn ) (X₁.toFun (z , h))
val z m (no nmem) = prʟ (nn ) (X₂.toFun (z , off z m nmem))

z ∈ D に対し、関数 fn は z ∈ D₁ かどうかを判定する。左の場合は (0,E₁(z)) を返し、補集合にあたる右の場合は (1,E₂(z)) を返す。

fn : (z : S) → Mem z → S
fn z m = val z m (decide z)

周囲での意味 Wit y z には二つの分岐がある。左の分岐では z ∈ D₁ であり、(z,v) ∈ E₁ を満たす v が単に存在して、y の底集合が (0,v) に等しくなる。

Wit : (y z : S) → Type (ℓ-suc ℓ)
Wit y z =
    (⟨ z .fst ∈ D₁ .fst ⟩
      × ∥ Σ[ v ∶ S ] (Holds E₁ z v × (y .fst ≡ pr (# ) (v .fst))) ∥₁)
  ⊎ ((⟨ z .fst ∈ D₁ .fst ⟩ → ⊥₀)

右の分岐では z ∉ D₁ であり、(z,v) ∈ E₂ を満たす v が単に存在して、底集合について y = (1,v) となる。異なるタグにより、別々の分岐から得た出力が等しくなることはない。

      × ∥ Σ[ v ∶ S ] (Holds E₂ z v × (y .fst ≡ pr (# ) (v .fst))) ∥₁)

グラフは二つの枠をもつ論理式として書かれる。D₁ への所属と最初の符号の上の存在量化の連言、あるいはその所属の否定と第二の符号の上の存在量化の連言である。存在量化子の内側では、単射された値とタグの等式が符号化のアトムである。

opaque
  fo : Formula S 
  fo = ((var i1 ∈̇ con D₁) ∧̇ ∃̇ (appC E₁ i2 i0 ∧̇ tagAtL i1  i0))
     ∨̇ ((¬̇ (var i1 ∈̇ con D₁)) ∧̇ ∃̇ (appC E₂ i2 i0 ∧̇ tagAtL i1  i0))

二つの符号化のアトムを読むには、その妥当性の補題を使う。適用のアトムの充足は所属 Holds E z v になり、タグのアトムの充足は、y とタグ付きの対との等式になる。

  private
    rd : (E : S) (k : ℕ) (y z v : S)
       → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ → ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
       → Holds E z v × (y .fst ≡ pr (# k) (v .fst))
    rd E k y z v ha ht =

二つの妥当性の同値に沿って移送すると、充足の証人は Wit が要求する成分、すなわちグラフ所属 Holds E z v と、y をタグ k の付いた対と同一視する等しさになる。

        subst ⟨_⟩ (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ [])) ha
      , subst ⟨_⟩ (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ [])) ht

逆に、Holds E z v と底集合についての等しさ y = (k,v) から、妥当性に沿って逆向きに移送すると適用の原子式の充足が得られる。

    wr : (E : S) (k : ℕ) (y z v : S)
       → Holds E z v → y .fst ≡ pr (# k) (v .fst)
       → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ × ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
    wr E k y z v ha ht =
        subst ⟨_⟩ (sym (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ []))) ha

同じ逆向きの移送により、タグ付き対の等しさはタグ原子式の充足になる。二つの証明を合わせると、存在量化子のもとにある連言が再構成される。

      , subst ⟨_⟩ (sym (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ []))) ht

fo の充足証明は二つの選言肢に分けて読む。左からは z ∈ D₁ と 0 のタグが付いた切り詰められた E₁ の証人が得られ、右からは z ∉ D₁ と 1 のタグが付いた対応する E₂ の証人が得られる。各切り詰めの内側で rd を適用すると、Wit y z の切り詰められた要素が得られる。

  fo-out : (y z : S) → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩ → ∥ Wit y z ∥₁
  fo-out y z = map₁
    (λ { (inl (h , hv)) → inl (h , map₁ (λ { (v , (ha , ht)) → v , rd E₁  y z v ha ht }) hv)
       ; (inr (h , hv)) → inr ((λ z∈ → lower (h z∈))
           , map₁ (λ { (v , (ha , ht)) → v , rd E₂  y z v ha ht }) hv) })

グラフの内向きの読み出しは、ホスト側の証人を場合ごとに充足へ変える。左の場合は、所属と切り詰められた項目を、適用とタグの符号化の妥当性の等式に沿って運び、右の場合は、所属しないことの反駁を対象言語の否定へ持ち上げてから同じことをする。

  fo-in : (y z : S) → Wit y z → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩
  fo-in y z (inl (h , hv)) =
    ∣ inl (h , map₁ (λ { (v , (ha , ht)) → v , wr E₁  y z v ha ht }) hv) ∣₁
  fo-in y z (inr (h , hv)) =
    ∣ inr ((λ z∈ → lift (h z∈))

右の場合の残りが第二の選言肢を完成させる。E₂ の項目は、タグを 0 から 1 に替えるだけで左と同じように運ばれる。二つの選言肢は切り詰められた存在へ注入され、導入は終わりである。

        , map₁ (λ { (v , (ha , ht)) → v , wr E₂  y z v ha ht }) hv) ∣₁

符号化されたそれぞれの関係は一価である。第一成分を共有する項目は第二成分も共有する。これが注入の符号の最初の連言項で、適用の符号化の妥当性を通して読み出される。

private
  sv₁ : (x y y' : S) → Holds E₁ x y → Holds E₁ x y' → y .fst ≡ y' .fst
  sv₁ = svAt-out zero (E₁ ∷ D₁ ∷ []) (c₁ .fst)
  sv₂ : (x y y' : S) → Holds E₂ x y → Holds E₂ x y' → y .fst ≡ y' .fst
  sv₂ = svAt-out zero (E₂ ∷ D₂ ∷ []) (c₂ .fst)

符号化された関係はさらに単射でもある。第二成分を共有する項目は、第一成分の基礎の集合が等しくなる。範囲の条項はここからはじまり、関係のどの値も基数の中にあると述べる。

  ij₁ : (y x x' : S) → Holds E₁ x y → Holds E₁ x' y → x .fst ≡ x' .fst
  ij₁ = injAt-out zero (E₁ ∷ D₁ ∷ []) (((c₁ .snd) .snd) .fst)
  ij₂ : (y x x' : S) → Holds E₂ x y → Holds E₂ x' y → x .fst ≡ x' .fst
  ij₂ = injAt-out zero (E₂ ∷ D₂ ∷ []) (((c₂ .snd) .snd) .fst)
  ran₁ : (x y : S) → Holds E₁ x y → ⟨ y .fst ∈ κ .fst ⟩

二つ目の値域条件により、二つの単射符号から読み出すデータがそろう。各関係について一価性、単射性、そしてすべての値が κ に属することが得られ、タグ付き写像はこれらの性質から構成される。

  ran₁ = ((c₁ .snd) .snd) .snd
  ran₂ : (x y : S) → Holds E₂ x y → ⟨ y .fst ∈ κ .fst ⟩
  ran₂ = ((c₂ .snd) .snd) .snd

証人は要素についての二つの場合から構成する。z ∈ D₁ なら E₁ から取り出した関数の値を使い、そうでなければ、そこから得られる z ∈ D₂ に対して E₂ から取り出した関数の値を使う。どちらの場合も、取り出しによりグラフの項目と、タグ付きの対を選んだ値と同一視する等式の両方が得られる。

wit : (z : S) (m : Mem z) (c : Case z) → Wit (val z m c) z
wit z m (yes h) = inl (h , ∣ X₁.toFun (z , h)
  , (X₁.toFun-graph (z , h) , prʟ-fst (nn ) (X₁.toFun (z , h))) ∣₁)
wit z m (no nmem) = inr (nmem , ∣ X₂.toFun (z , off z m nmem)
  , (X₂.toFun-graph (z , off z m nmem) , prʟ-fst (nn ) (X₂.toFun (z , off z m nmem))) ∣₁)

左の場合の一意性は、三つの等式を合成する。項目の第二成分が、切り詰められた証人が名指す値に等しいこと。E₁ の一価性が二つの関数の値を同一視すること。そして対の第一射影の等式が、値がちょうどタグつきの項目であることを述べる。

only : (z : S) (m : Mem z) (c : Case z) (y : S) → Wit y z → y .fst ≡ (val z m c) .fst
only z m (yes h) y (inl (_ , hv)) = rec₁ (setIsSet _ _)
  (λ { (v , (hg , hy)) →
     hy ∙ cong (pr (# )) (sv₁ z v (X₁.toFun (z , h)) hg (X₁.toFun-graph (z , h)))
        ∙ sym (prʟ-fst (nn ) (X₁.toFun (z , h))) }) hv

交差する場合はそのまま反駁される。D₁ の中の要素が、D₁ の外で記録された証人をもつことはできず、逆もまた然りである。右と右の場合は、E₂ とタグ 1、そして外れた要素での関数の値を使って、左とまったく同じように処理される。

only z m (yes h) y (inr (nmem , _)) = ⊥₀-rec (nmem h)
only z m (no nmem) y (inl (h , _)) = ⊥₀-rec (nmem h)
only z m (no nmem) y (inr (_ , hv)) = rec₁ (setIsSet _ _)
  (λ { (v , (hg , hy)) →
     hy ∙ cong (pr (# )) (sv₂ z v (X₂.toFun (z , off z m nmem)) hg (X₂.toFun-graph (z , off z m nmem)))

最後の等式が、タグの同定と対の第一射影の等式を合成し、一意性が完成する。こうして、どちらの場合でも証人はその値を決定する。

        ∙ sym (prʟ-fst (nn ) (X₂.toFun (z , off z m nmem))) }) hv

値は内部の直積に落ちる。数項 0 か 1 と関数の値の対は、その第一射影の等式を通して提示され、二つの数項が κ の中にあり、範囲の条項によって関数の値も κ の中にあるので、prodL-in がそれを受け入れる。

into : (z : S) (m : Mem z) (c : Case z) → ⟨ (val z m c) .fst ∈ˢ (prodL κ) .fst ⟩
into z m (yes h) = subst (λ w → ⟨ w ∈ˢ (prodL κ) .fst ⟩) (sym (prʟ-fst (nn ) (X₁.toFun (z , h))))
  (prodL-in κ (nn ) (X₁.toFun (z , h)) 0∈κ (ran₁ z (X₁.toFun (z , h)) (X₁.toFun-graph (z , h))))
into z m (no nmem) = subst (λ w → ⟨ w ∈ˢ (prodL κ) .fst ⟩) (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m nmem))))
  (prodL-in κ (nn ) (X₂.toFun (z , off z m nmem)) 1∈κ

右の場合は E₂ と数項 1 から範囲の事実を供給し、タグつきの値がどちらも直積の中にあることが揃う。

    (ran₂ z (X₂.toFun (z , off z m nmem)) (X₂.toFun-graph (z , off z m nmem))))

これらの材料から、通常の和集合 D から内部直積 prodL κ への写像を定める。値は左側を優先する場合分けで選ばれ、into がそのタグ付きの値が直積に属することを証明する。

Dmap : DefinableMap
Dmap = record
  { dom = D ; cod = prodL κ ; fn = fn
  ; into = λ z m → into z m (decide z)
  ; graph = fo

定義の条項が証人をグラフの導入に渡し、一意性が、どのグラフの項目も、決められた場合の値へ、台の等しさに沿って変換する。これで定義可能な写像は完成である。

  ; defines = λ z m → fo-in (fn z m) z (wit z m (decide z))
  ; only = λ z m y h → S≡ (rec₁ (setIsSet _ _) (only z m (decide z) y) (fo-out y z h)) }

タグつきの写像の単射性は、二つの入力について決められた場合を比較することで証明する。場合分けには四つの組み合わせがあり、タグつきの対の構造がそれをきれいに分ける。

inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z') → (fn z m) .fst ≡ (fn z' m') .fst → z .fst ≡ z' .fst
inj z m z' m' = go (decide z) (decide z')
  where
  go : (c : Case z) (c' : Case z') → (val z m c) .fst ≡ (val z' m' c') .fst → z .fst ≡ z' .fst
  go (yes h) (yes h') q = ij₁ (X₁.toFun (z , h)) z z' (X₁.toFun-graph (z , h))

同じタグの場合は、対の等式を pr-inj で逆にたどる。タグが一致するので、値の等式が二つの関数の値を同一視し、これが単射性の条項が消費する議論そのものである。

    (subst (λ w → ⟨ pr (z' .fst) w ∈ E₁ .fst ⟩) (sym (p .snd)) (X₁.toFun-graph (z' , h')))
    where
    p : (#  ≡ # ) × ((X₁.toFun (z , h)) .fst ≡ (X₁.toFun (z' , h')) .fst)
    p = pr-inj (sym (prʟ-fst (nn ) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn ) (X₁.toFun (z' , h')))
  go (yes h) (no nmem') q = ⊥₀-rec (znots (#-inj   (

タグが異なる二つの場合はいずれも不可能である。二つの値が等しければ数項 0 と数項 1 が等しくなってしまい、二つの向きはそれぞれ znots と snotz に反する。両方の入力が右側の場合は、E₂ の単射性がそれらを同一視する。

    (pr-inj (sym (prʟ-fst (nn ) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn ) (X₂.toFun (z' , off z' m' nmem')))) .fst)))
  go (no nmem) (yes h') q = ⊥₀-rec (snotz (#-inj   (
    (pr-inj (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m nmem))) ∙ q ∙ prʟ-fst (nn ) (X₁.toFun (z' , h')))) .fst)))
  go (no nmem) (no nmem') q = ij₂ (X₂.toFun (z , off z m nmem)) z z' (X₂.toFun-graph (z , off z m nmem))
    (subst (λ w → ⟨ pr (z' .fst) w ∈ E₂ .fst ⟩) (sym (p .snd)) (X₂.toFun-graph (z' , off z' m' nmem')))

右と右の場合の対の等式は、タグの一致と関数の値の一致に分かれ、単射性が消費するのは後者である。

    where
    p : (#  ≡ # ) × ((X₂.toFun (z , off z m nmem)) .fst ≡ (X₂.toFun (z' , off z' m' nmem')) .fst)
    p = pr-inj (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m nmem))) ∙ q
                ∙ prʟ-fst (nn ) (X₂.toFun (z' , off z' m' nmem')))

得られたグラフは、通常の和集合 D₁ ∪ D₂ から prodL κ への符号化された単射である。写像は値のタグで二つの枝を区別し、両方に属する要素は第一の枝で扱う。

injL : InjL D (prodL κ)
injL = Inj.injL Dmap inj

定義域への所属は型として記録され、議論が要素とともにそれを運べるようにする。

Mem : S → Type (ℓ-suc ℓ)
Mem z = ⟨ z .fst ∈ D .fst ⟩

グラフの論理式は、定数 G の適用の条項である。対の上で成立することは、ちょうどその対が関係に属することを意味する。

private
  graphFo : Formula S 
  graphFo = appC G i0 i1

存在仮定を共通の段階へ移すが、前者を大域的に選ぶことはしない。切り詰めのもとで存在する各前者は P に属し、したがって Lset γ に属する。さらに妥当性の等式が、その関係への所属をグラフ論理式の充足へ変える。

  have-γ : (z : S) → Mem z
         → ∥ Σ[ p ∶ S ] (⟨ p .fst ∈ Lset γ ⟩ × ⟨ (p ∷ z ∷ []) ⊨ graphFo ⟩) ∥₁
  have-γ z m = map₁
    (λ { (p , h) → p , P⊆L p (inP p z h)
                     , subst ⟨_⟩ (sym (appC-adequate G i0 i1 (p ∷ z ∷ []))) h })

もとの切り詰められた存在が、輸送が消費する証人を供給する。

    (have z m)

段階順序による構成は、定義域の各要素に対して Lset γ にある最小の G 前者を選ぶ。また、定義可能なグラフと、各入力をその選ばれた値に対応させる所属の読み出しも与える。

  module Ls = Least γ oγ D graphFo have-γ using ( fn; fn-holds; Dmap; T; T-in; T-out )

選ばれた最小の前者が、この構成の値を与える関数である。

fn : (z : S) → Mem z → S
fn = Ls.fn

値はその入力で関係を満たす。内部の充足は、値と入力を対にした環境での適用の条項へと運び戻される。

fn-holds : (z : S) (m : Mem z) → Holds G (fn z m) z
fn-holds z m = subst ⟨_⟩ (appC-adequate G i0 i1 (fn z m ∷ z ∷ [])) (Ls.fn-holds z m)

定義可能な写像は、余域を P として記録される。値の所属は、既存の仮定の内向きの方向が保証する。

Dmap : DefinableMap
Dmap = record Ls.Dmap { cod = P ; into = λ z m → inP (fn z m) z (fn-holds z m) }

最小の前者の関数のグラフは L の要素であり、段階の機構がその所属の記述とともに返す。

T : S
T = Ls.T

内向きの読み出しは、入力と選ばれた値の対がグラフの項目であることを示す。

T-in : (z : S) (m : Mem z) → ⟨ pr (z .fst) ((fn z m) .fst) ∈ T .fst ⟩
T-in = Ls.T-in

外向きの読み出しは、すべての項目から、入力と、第二成分を選ばれた値と同一視する等式を復元する。のちの議論が候補を比較するときに使うのはこれである。

T-out : (z e : S) → ⟨ pr (z .fst) (e .fst) ∈ T .fst ⟩
      → Σ[ m ∶ Mem z ] (e .fst ≡ (fn z m) .fst)
T-out = Ls.T-out

関係が関数的であるという追加の仮定のもとで、最小の前者の関数は単射になる。モジュールが携えるのは、この一つの仮定だけである。

module Functional
  (funct : (p z z' : S) → Holds G p z → Holds G p z' → z .fst ≡ z' .fst) where

inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z')
    → (fn z m) .fst ≡ (fn z' m') .fst → z .fst ≡ z' .fst
inj z m z' m' q = funct (fn z m) z z' (fn-holds z m)
  (subst (λ w → ⟨ pr w (z' .fst) ∈ G .fst ⟩) (sym q) (fn-holds z' m'))

injL : InjL D P
injL = Inj.injL Dmap inj

Y を a から作られる構成可能な単集合とする。議論で使うのは、その所属の導入則と除去則だけである。

Y : S
Y = sglʟ a

要素 a はそれ自身の単集合に属する。一元集合の構成の導入の読み出しによるものである。

Y-in : ⟨ a .fst ∈ Y .fst ⟩
Y-in = sglʟ-in a (a .fst) refl

消去の読み出しは、単集合がそれ以外を含まないと言う。どの要素も、基礎の集合は a である。

Y-out : (z : S) → ⟨ z .fst ∈ Y .fst ⟩ → z .fst ≡ a .fst
Y-out z = sglʟ-out a (z .fst)

グラフは、二つの自由スロットをもつ原子論理式で記述される。この論理式は値のスロットを内部の空集合と等置し、その底の集合は数項 0 である。

fo : Formula S 
fo = var i0 ≐ con ∅ʟ

定義可能な写像は、ただ一つの入力を零番の数項へ送る。余域への所属は、既存の事実 0∈κ である。

Dmap : DefinableMap
Dmap = record
  { dom = Y ; cod = κ ; fn = λ _ _ → nn 
  ; into = λ _ _ → 0∈κ
  ; graph = fo

グラフは定義どおりに成立する。原子文が数項をそれ自身と等置するからである。一意性は、単集合の二つの要素が同じ基礎の集合を提示することから成立する。

  ; defines = λ z m → refl
  ; only = λ z m y h → S≡ h }

単射性は、二つの外向きの読み出しを合成する。どちらの入力も a と同じ基礎の集合を提示するので、台の要素として両者は等しいのである。

inj : (z : S) (m : ⟨ z .fst ∈ Y .fst ⟩) (z' : S) (m' : ⟨ z' .fst ∈ Y .fst ⟩)
    → (nn ) .fst ≡ (nn ) .fst → z .fst ≡ z' .fst
inj z m z' m' _ = Y-out z m ∙ sym (Y-out z' m')

単集合から基数への単射は、ほかの計数の部品と同じ形でまとめられる。

injL : InjL Y κ
injL = Inj.injL Dmap inj

計数の目標は、ω の外にある内部の基数 κ と、始点からそれへの符号化された単射である。課題は、同じ基数で包全体を数えることである。

この包は有限反復 hullStep n の和集合として表される。一回の閉包は Φ によって定まり、その非自明な枝は、論理式の鍵と現在の反復上の有限なパラメータ環境による最小証人を記録する。

module Cn = Condense′ lam ordλ succλ X X⊆L ∅∈λ elem sup X-isL
  using ( hullStep; hullL; hullStep⊆Hull )
module B = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ
  using ( A; Body
        ; LeastWitness; leastWitnessFo; leastWitness-in; leastWitness-out

最小証人に付随するデータから、自然数の長さ、現在の集合への有限な割り当て、その符号化された環境、そして論理式の鍵が Lset ω に属することが得られる。一意性は、鍵と環境を固定した後に成立する。

        ; LeastWitnessData; leastWitness-data; leastWitness-unique; witFo-leastWitness
        ; Φ; Φ-out; λ-isL; ω-num; pack )
module SM = SatGraph B.A using ( pairs; pairs-out; valOf )

有限反復には所属の導入則と除去則があり、各反復は包全体に含まれる。さらに包全体は Lset lam に含まれる。これらの包含により、計数構成で使う各集合は固定した周囲の段階内に保たれる。

module It = Telescope.HullIter.It lam ordλ succλ X X⊆L ∅∈λ X-isL B.pack
  using ( Num; iter; iter-in; iter-out; iterUnion-out; ω-num )
module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
open Cn using ( hullStep; hullL )

κ は順序数であり ω に属さないので、すべての有限数項を含む。この結論に内部基数性は使われず、内部基数性は別に平方法則で必要になる。

num∈κ : (k : ℕ) → ⟨ # k ∈ κ .fst ⟩
num∈κ k = ω⊆ (κ .fst) oκ κ∉ω (# k) (#∈ω k)

無限基数の平方に関する議論から、符号化された単射 pairκ : InjL (prodL κ) κ が得られる。ここでは κ の順序数性、内部基数性、ω に属さないことの三つをすべて使う。結論は単射であり、全単射ではない。

pairκ : InjL (prodL κ) κ
pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (κ .fst) (κ .snd) oκ cκ κ∉ω

段階 Lω = Lset ω は、単射の合成によって κ へ入る。極限段階の計数がまず Lω ↪ ωʟ を与え、κ の順序数性と非有限性から得られる ω ⊆ κ が ωʟ ↪ κ を与える。

Lω↪κ : InjL Lω κ
Lω↪κ = injl-trans Lω ωʟ κ limit-stage-counted
  (inclusion-coded ωʟ κ (λ z hz → ω⊆ (κ .fst) oκ κ∉ω z hz))

一回の閉包を数えるため、Lset lam に含まれる構成可能な集合 Z と、InjCode E Z κ を満たす実際のグラフ E を固定する。目標は、この選ばれた段階の単射から、符号化単射の単なる存在 InjL (Φ Z) κ を構成することである。

module OneStep (Z : S) (Z⊆ : (z : V ℓ) → ⟨ z ∈ˢ Z .fst ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
               (E : S) (cE : InjCode E Z κ) where

ΦZ : S
ΦZ = B.Φ Z

opaque
  D₂ : S
  D₂ = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .fst

  D₂-spec : (z : S) → (z .fst ∈ D₂ .fst)
          ≡ ((z .fst ∈ ΦZ .fst) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z)))
  D₂-spec z = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .snd z

opaque
  D₂-in : (z : S) → ⟨ z .fst ∈ ΦZ .fst ⟩ → (⟨ z .fst ∈ Z .fst ⟩ → ⊥₀) → ⟨ z .fst ∈ D₂ .fst ⟩
  D₂-in z h nmem = subst ⟨_⟩ (sym (D₂-spec z)) (h , λ z∈ → lift (nmem z∈))

  D₂-out : (z : S) → ⟨ z .fst ∈ D₂ .fst ⟩ → ⟨ z .fst ∈ ΦZ .fst ⟩ × (⟨ z .fst ∈ Z .fst ⟩ → ⊥₀)
  D₂-out z h = r .fst , λ z∈ → lower (r .snd z∈)
    where
    r : ⟨ z .fst ∈ ΦZ .fst ⟩
      × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z) ⟩

    r = subst ⟨_⟩ (D₂-spec z) h

opaque
  D∅ : S
  D∅ = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .fst

  D∅-spec : (z : S) → (z .fst ∈ D∅ .fst)
          ≡ ((z .fst ∈ D₂ .fst) ⊓ ((z ∷ []) ⊨ var i0 ≐ con ∅ʟ))
  D∅-spec z = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .snd z

opaque
  D∅-in : (z : S) → ⟨ z .fst ∈ D₂ .fst ⟩ → z .fst ≡ ∅ → ⟨ z .fst ∈ D∅ .fst ⟩
  D∅-in z h e = subst ⟨_⟩ (sym (D∅-spec z)) (h , e)