絶対性

module Single {ℓ} (𝒮 : ZFStructureₕ ℓ)
              (M : ZFStructure.S 𝒮 → hProp ℓ)
              (trans : hPropView.Transitive 𝒮 M) where

open ZFStructure 𝒮

内側の世界の台は Σ 型 SM である。S の要素に、それが M に属する証拠を対にしたものである。𝒮 ↾ M の関係は第一射影の上で解釈されるので、𝒮 の目には、内側の要素とその fst による像は S の同じ inhabitant を指す。汎用の意味論はこの台の上で二回使われる。一度は外側の構造 𝒮 で評価し、一度は制限 𝒮M で評価する。両者の読み方が構文を共有するのは、定数域をともに SM とするからで、違いは構造と定数解釈にだけある。

SM : Type ℓ
SM = Σ[ x ∶ S ] (x ∈ᶜ M)

𝒮M : ZFStructureₕ ℓ
𝒮M = 𝒮 ↾ M

module SemV = FOL.Semantics 𝒮

外側の読み方は定数解釈 ι := (λ p → p .fst) を用いる。M の要素を名指す定数は、𝒮 の中ではその要素そのものを指す。記号は固定される。𝒮 での充足は _⊨ᵛ_、項の値は ⟦_⟧ᵛ と書く。

module SemM = FOL.Semantics 𝒮M

open module V = SemV.At SM (λ p → p .fst) public
  renaming ( _⊨_ to _⊨ᵛ_ ; ⟦_⟧ to ⟦_⟧ᵛ )
open module Mse = SemM.At SM id public

内側の読み方は ι := id を用いる。𝒮 ↾ M の中では定数はそれが名指す対そのものであり、制限の関係はその対の第一射影を読み取る。したがって、内側の原子的な主張 xm ∈ˢ ym は、𝒮 ではちょうど xm .fst ∈ˢ ym .fst を意味する。これが二つの充足関係を比較できる理由である。記号は _⊨ᵐ_ と ⟦_⟧ᵐ となり、各論理式は内側の δ ⊨ᵐ φ としても外側の (map (λ p → p .fst) δ) ⊨ᵛ φ としても読める。

  renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )

二つの世界の違いは環境の読み方にだけある。内側の環境 δ : Vec SM n は fst を通して外側の値を名指すので、map (λ p → p .fst) δ が対応する外側の環境である。二つの補題が両側の項の評価を結ぶ。定数はどちらの側でも自分の第一射影を値とし、変数はどちらの世界でも一回の参照にすぎない。したがって辞書の問題は原子の段階で解決される。

最初の補題は、参照と射影を項ごとに交換する。射影後の環境の第 i 項を読むことは、第 i 項を射影することと同じである。証明は添字で場合分けし、先頭では refl、尾では再帰する。lookup と map がどちらも項ごとに計算されるからである。

private
  lookup-fst : ∀ {n} (i : Fin n) (δ : Vec SM n)
             → lookup i (map (λ p → p .fst) δ) ≡ (lookup i δ) .fst
  lookup-fst zero    (m ∷ δ) = refl
  lookup-fst (suc i) (m ∷ δ) = lookup-fst i δ

二つ目の補題はこれを項へ持ち上げる。内側で項を評価してから射影したものは、射影後の環境での外側の値に等しい。定数の場合は、それぞれの解釈 id と fst により両辺とも m .fst に計算され、refl で足りる。変数の場合は、外側の値が map (λ p → p .fst) δ への参照であり、最初の補題がそれを内側の参照の射影へ書き換える。sym は等式を必要な向きに置くためのものである。すべての項はこの二つの場合から作られるので、辞書はこれで完結である。

  ⟦⟧-fst : ∀ {n} (t : Term SM n) (δ : Vec SM n)
         → (⟦ t ⟧ᵐ δ) .fst ≡ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ)
  ⟦⟧-fst (con m) δ = refl
  ⟦⟧-fst (var i) δ = sym (lookup-fst i δ)

Δ₀ 絶対性定理

Δ₀ の絶対性は、Δ₀ の証拠についての構造的帰納法で証明する。原子と結合子の場合は帳簿づけにすぎない。原子の場合は前節の項の補題を使い、各結合子は部分の真理値から全体の真理値を計算するので、部分の等しさが全体の等しさに伝わる。数学が起きるのは有界全称の場合である。外向きには、界の外側の要素 x を M の要素として内側の意味論に引き渡すための束ね直しが必要である。界の値が M に属するので、x ∈ ⟦ t ⟧ と ⟦ t ⟧ ∈ᶜ M から推移性によってちょうど x ∈ᶜ M が得られる。逆向きは射影だけで済む。有界存在はその双対で、命題の切断のもとで行われる。推移性が使われるのは、外側の裸の要素を内側の要素に直す必要があるときである。有界全称では内側から外側への方向、有界存在では外側から内側への方向に当たる。

定理の主張は、単なる含意ではなく真理値のパスである。φ が Δ₀ であることを証明する証拠 d と SM への環境 δ のそれぞれに対して、内側の充足 δ ⊨ᵐ φ は、型として、射影後の環境での外側の充足と等しくなる。原子の場合、項の補題が両辺を評価する。∈ は構造のフィールド _∈ˢ_ を読み、≐ は _≈ˢ_ を読み、cong₂ が二つの項の値の等しさを関係に沿って運ぶ。結合子 ∧、∨、⇒ の意味論は ⊓、⊔、⇒ なので、二つの部分証拠に abs₀ を適用して cong₂ に渡すことが場合全体になる。これらの演算は関数であり、等しさを保つからである。

abs₀ : ∀ {n} {φ : Formula SM n} → Δ₀ φ → (δ : Vec SM n)
     → (δ ⊨ᵐ φ) ≡ ((map (λ p → p .fst) δ) ⊨ᵛ φ)
abs₀ (δ-∈ {t = t} {u}) δ = cong₂ _∈ˢ_ (⟦⟧-fst t δ) (⟦⟧-fst u δ)
abs₀ (δ-≐ {t = t} {u}) δ = cong₂ _≈ˢ_ (⟦⟧-fst t δ) (⟦⟧-fst u δ)
abs₀ (δ-∧ d e) δ = cong₂ _⊓_ (abs₀ d δ) (abs₀ e δ)

矛盾には仕事がない。δ-⊥ では両辺とも ⊥ であり、必要なパスは refl である。残るのは二つの有界量化子である。その範囲 ⟦ t ⟧ は外側の世界に住み、一方、内側の量化は「値と、その M への所属の証拠」の対を走査する。次のブロックで一方向ずつ展開する。

abs₀ (δ-∨ d e) δ = cong₂ _⊔_ (abs₀ d δ) (abs₀ e δ)
abs₀ (δ-⇒ d e) δ = cong₂ _⇒_ (abs₀ d δ) (abs₀ e δ)
abs₀ δ-⊥ δ = refl
abs₀ (δ-∀∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd
  where

∀̇∈ では、両方向が ⇔toPath によって一つのパスにまとめられる。まず二つの略記を用意する。tm は範囲を定める項の内側での値で、p は項の補題 tm .fst ≡ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ) をそれに特化したものであり、内側の範囲 (対) と外側の範囲 (その第一射影) を結ぶ橋である。

  tm : SM
  tm = ⟦ t ⟧ᵐ δ
  p : tm .fst ≡ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ)
  p = ⟦⟧-fst t δ
  fwd : ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩ → ⟨ (map (λ p → p .fst) δ) ⊨ᵛ (∀̇∈ t φ) ⟩

順方向は内側の検証者 h を受け取り、x ∈ˢ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ) を満たす各外側の x に対して母式の外側の真理値を与えなければならない。ここで x は M の要素ではなく素の要素なので、まず束ね直しが必要である。sym p に沿った輸送が所属の証拠を内側の範囲 tm .fst へ移し、次いで推移性が働く。x ∈ tm .fst と tm .fst ∈ᶜ M から x ∈ᶜ M が得られ、したがって xm := x , trans hx' (tm .snd) は正当な内側の要素である。xm で h を実行すると母式の内側の真理値が得られ、帰納仮定 abs₀ d (xm ∷ δ) がそれを外側へ運ぶ。帰納全体を通して前提 trans を消費するのは、この一段階だけである。

  fwd h x hx =
    let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx
        xm  = x , trans hx' (tm .snd)
    in subst ⟨_⟩ (abs₀ d (xm ∷ δ)) (h xm hx')
  bwd : ⟨ (map (λ p → p .fst) δ) ⊨ᵛ (∀̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩

逆方向は逆向きに進む。外側の検証者 g は素の要素を走査し、内側の節は所属の証拠を伴う対 xm を期待する。射影 xm .fst が外側の要素であり、項の補題がその所属を tm .fst から ⟦ t ⟧ᵛ (map (λ p → p .fst) δ) へ運ぶ。これはちょうど g が期待する形である。g を呼び出せば外側の真理値が得られ、abs₀ d (xm ∷ δ) を sym に沿って運ぶことで内側へ戻す。この方向に推移性は不要である。対 xm は証拠を伴って届くからである。

  bwd g xm hxm =
    subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ)))
          (g (xm .fst) (subst (λ s → ⟨ xm .fst ∈ˢ s ⟩) p hxm))
abs₀ (δ-∃∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd
  where

存在の場合 ∃̇∈ は全称の場合を写し取るが、構造上の違いが一つある。存在量化子の充足は台の上の上限、すなわち要素ごとの寄与すべてを覆う最小の真理値として定義され、切断された命題の上限は命題的切り詰めの下に住むため、両方向とも map₁ を通して動く。略記 tm と p は同じくスコープにあり、範囲を通して証拠を束ね直す数学は全称の場合と同一である。

  tm : SM
  tm = ⟦ t ⟧ᵐ δ
  p : tm .fst ≡ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ)
  p = ⟦⟧-fst t δ
  fwd : ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩ → ⟨ (map (λ p → p .fst) δ) ⊨ᵛ (∃̇∈ t φ) ⟩

順方向では、切断された内側の証拠は三つ組である。範囲内の内側の要素 xm、その所属の証拠、そして母式の内側の真理値である。map はこれを xm .fst に送り、p に沿って所属を外側へ運んで ⟨ xm .fst ∈ˢ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ) ⟩ の形にし、さらに帰納仮定 abs₀ d (xm ∷ δ) を通して母式の真理値を外側へ運ぶ。証拠そのものが取り出されることはなく、切断の内側でだけ使われる。

  fwd = map₁ λ { (xm , hxm , hφ) →
          xm .fst
        , subst (λ s → ⟨ xm .fst ∈ˢ s ⟩) p hxm
        , subst ⟨_⟩ (abs₀ d (xm ∷ δ)) hφ }
  bwd : ⟨ (map (λ p → p .fst) δ) ⊨ᵛ (∃̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩

逆方向では、外側の証拠は三つ組である。素の要素 x、外側の範囲での所属、そして母式の外側の真理値である。sym p に沿う輸送が所属を内側の範囲へ引き戻し、推移性が続いて x ∈ᶜ M を証明するので xm は内側の要素となり、母式の真理値は sym (abs₀ d (xm ∷ δ)) を通して内側へ運ばれる。切断された出力はやはり map₁ で組み立てられるため、どこでも選択公理は使われない。二つの有界量化子の場合は、両側とも単に inhabited な証拠で成立する。

  bwd = map₁ λ { (x , hx , hφ) →
          let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx
              xm  = x , trans hx' (tm .snd)
          in xm , hx' , subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ))) hφ }

Σ₁ は上向き、Π₁ は下向き

Δ₀ の外に出ると、絶対性は一方向になるが、その二方向は双対である。内側で真な Σ₁ 論理式は外側でも真であり、外側で真な Π₁ 論理式は内側でも真である。この非対称は量化子の変異から来る。Σ₁ の証拠は Δ₀ の核の上に、任意の有限個の無制限存在量化子の連なりで作られ得て、内側の存在の証拠は fst を通して外側へ渡る。Π₁ の証拠も同様に無制限の全称量化子で作られ得て、外側の検証者は各段階で内側の要素の fst に特殊化される。これらの無制限の段階で推移性がさらに使われることはない。ただし、それぞれの帰納の Δ₀ の基底は絶対性定理に、ひいては推移性の仮定に依存する。

Δ₀ の基底の場合、abs₀ d δ は内側と外側の真理値を結ぶパスであり、subst は内側の真理値の証明をそのパスに沿って外側へ輸送する。この基底の場合そのものは命題的切り詰めを導入しない。Σ₁ の場合 σ-∃ は台の上の無制限の存在量化であり、その充足は命題的切り詰めのもとでの上限なので、map₁ が切断された対に作用する。内側の証拠 xm と母式の内側の真理値 h の対は、外側の要素 xm .fst に送られ、再帰呼び出し σ₁-up s (xm ∷ δ) h は対全体で環境を拡張して、基底の場合が包みを捨てるまで証拠を内側に保つ。

σ₁-up : ∀ {n} {φ : Formula SM n} → Σ₁ φ → (δ : Vec SM n)
      → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ (map (λ p → p .fst) δ) ⊨ᵛ φ ⟩
σ₁-up (σ-Δ₀ d) δ = subst ⟨_⟩ (abs₀ d δ)
σ₁-up (σ-∃ s)  δ = map₁ λ { (xm , h) → xm .fst , σ₁-up s (xm ∷ δ) h }

π₁-down : ∀ {n} {φ : Formula SM n} → Π₁ φ → (δ : Vec SM n)

下向きの法則はその鏡像である。Δ₀ の場合は sym (abs₀ d δ) に沿って輸送し、Π₁ の場合 π-∀ は無制限の全称量化である。外側の検証者 h が与えられると、各内側の要素 xm に対して xm .fst でインスタンス化し、再帰呼び出しが拡張された環境で母式を証明する。ここに切断は現れない。全称の充足は下限、すなわち要素ごとの寄与すべての下にある最大の真理値であり、検証者を直接与えることで明示的に検証できるからである。そして無制限の段階に推移性は使われない。無制限の量化子は台全体を走査し、そこでは対の構成と射影がはじめから使えるからである。

        → ⟨ (map (λ p → p .fst) δ) ⊨ᵛ φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩
π₁-down (π-Δ₀ d) δ = subst ⟨_⟩ (sym (abs₀ d δ))
π₁-down (π-∀ s)  δ h xm = π₁-down s (xm ∷ δ) (h (xm .fst))