名前の比較を表す論理式

宇宙レベル ℓ と、必要な一段高いレベルでの排中律を固定する。これは本章が引き継ぐ古典論理のインターフェースである。以下の論理式構成子は構文を組み立てるだけであるが、そこで用いる自然数対象、充足関係グラフ、極限段階の符号順序、正準名の理論は、いずれも同じ仮定のもとで構成されている。したがって、このモジュールはこれらの意味論的依存関係を記録するが、改めて選択を行うことはない。LeastNameAt は最小性を表し、最小名を選ぶ構成は引き続き CanonicalNames.leastName である。

module L.Choice.NameComparison {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

同じ定義可能な部分集合が複数の名前をもつことがある。メタ言語における名前は、アリティ k、suc k 個の変数位置をもつ無パラメータ論理式、そして台から取った k 個のパラメータのベクトルから成る。名前の指示対象は、この三つのデータから導かれる。余分な一つの変数が候補となる要素を表し、残りの変数がパラメータベクトルを受け取る。したがって、指示対象は名前の第四の成分ではない。

このデータを L の内部で表すために、本章はパラメータベクトルを有限な環境グラフで表し、論理式の評価を充足関係グラフで表す。正しい論理式キーにおいて、satGraphAt はそのキーを、論理式を満たす環境全体の集合に関係づける。その出力は、まさにこの充足環境の集合である。NameAt はアリティ、無パラメータ論理式の符号、パラメータ環境を、それらから導かれる指示対象に結び付ける。後で競合する名前を量化するとき、それらは同じ指示対象をもたなければならない。

名前は辞書式に比較される。まず極限段階の順序で論理式の符号を比較し、次にアリティを比較し、最後に台上の与えられた順序でパラメータベクトルを比較する。論理式 ≺At はこの三つの場合を表す。LeastNameAt は、同じ指示対象をもち、現在の名前より小さい名前がないことを述べるだけである。最小名を実際に選ぶのは、先に構成された CanonicalNames.leastName である。StepAt は二つの最小名を局所的に量化して比較する。本章で証明する妥当性は、ちょうど ≺At とメタ言語の関係 _≺ₙ_ との対応までである。NameAt、LeastNameAt、StepAt の完全な妥当性は後続の展開で証明される。

基礎となる言語は、宇宙レベル、有限添字、ベクトル、命題値の主張を与える。古典的推論は、明示された一つの仮定 LEM (ℓ-suc ℓ) を通して入る。そのレベルは、以下で使う充足関係の構成と整列順序を扱うのに十分である。この仮定を明示しておくことで、性質を述べるだけの記述と、証人を実際に選ぶ先行の構成とを区別できる。

対象言語は所属と等号を述べ、命題を組み合わせ、台全体または一つの集合の上で量化できる。その意味論は命題値の構造で読み取られる。定数の写像は、後で必要となる三つの表示を結び付ける。すなわち、本当にパラメータをもたない論理式、空のアルファベット上の論理式、構成可能な台上で解釈された同じ構文である。これらの写像は論理式の構造を保つので、無パラメータ骨格の符号を内部で認識できるようになる。

論理式の符号、順序対、数項は、それ自身が累積階層の集合である。構成可能部分構造は論理式を読む台を与え、推移性は構成可能な符号集合への所属から、その成分に必要な構成可能性を与える。対の符号化と数項の符号化の単射性によって、後に等しいキーからアリティと骨格符号を復元できる。各 Lset 段階は極限段階の符号順序の舞台となる。

アリティは内部の自然数集合に属する数項で表し、パラメータベクトルは有限環境のグラフで表す。対象言語の論理式は、順序対、適用、定義域を調べ、候補となる要素を環境に追加し、外延的に部分集合を定義できる。ある台上の論理式に対して、Sat はその論理式を満たす環境全体の集合である。後で充足関係グラフから復元する意味論的な値は、この集合である。

充足関係はすでに表として構成されており、各項目は部分式のキーと、再帰的に定まる充足環境の集合を対にしている。スロットの閉性と全性により、再帰で必要となるすべての正しいキーに項目が与えられ、充足関係の橋渡しが論理式の定数を選ばれた台の要素として同定する。したがって本章では、充足関係の再帰を再実行せずに、キーに保存された集合値を読み取れる。

各台について、AllCodes はその台上の正しい論理式キーをちょうど集め、その二方向の読みは所属と元の論理式を結び付ける。統一充足関係の橋渡しは、関係を表す論理式 satGraphAt B x y を支える。x がスロット B の台上の正しいキーであるとき、y は対応する充足環境の集合である。GraphWitAt と二つのグラフの読みは、この集合値の関係を新しい再帰なしに示す。

環境の塔とタグ付き再帰データは、充足関係グラフの読みが各構文要素について成り立つことを保証する。この内部の仕組みに対し、正準名の理論は名前比較の基準となるメタ言語の対象を与える。メタ言語の Name が保存するのは、アリティ、無パラメータ論理式、パラメータベクトルである。limitCode は論理式から第一の比較キーを導き、指示対象は充足関係から別に導かれる。後のスロット論理式も、この区別を保たなければならない。

名前の符号は極限段階の要素であり、limitOrder によって比較される。第三のキーは、台上に与えられた任意の狭義整列順序から来る。正準名の理論は、これらと自然数のアリティをすでに _≺ₙ_ にまとめ、その関係の整礎性を証明し、leastName で用いている。本章では二つの非数値的な順序を、表示法則を伴う関係スロットによって受け取る。したがって、どちらの順序も再構成せず、それらによる比較を記述する。

自然数の順序が第二の比較キーを与える。アリティが数項で表されるとき、一方の数項が他方に所属することは狭義の不等号を表す。有限添字は、パラメータベクトルの成分と、二つのベクトルが最初に異なる位置を指定する。後の妥当性の議論では、共通の長さに関する帰納法により、この最初の相違による記述が _≺ₙ_ で使われる再帰的なベクトル順序と一致することを証明する。

open import Cubical.Data.Nat.Order
  using ( _<_; zero-≤; suc-≤-suc; pred-≤-pred; ¬-<-zero; <-trans )
open import Cubical.Data.FinData.Properties using ( toℕ<n; fromℕ'; toFromId' )

証明データは辞書式順序の形に従う。依存対は位置とその証拠を運び、直和は符号、アリティ、パラメータの三つの場合を分ける。先行するキーの等しさにより、依存する論理式とベクトルを共通のアリティへ輸送してから、次のキーを比較できる。空の型は、定数をもたない論理式に必要な定数解釈を一意に与える。

存在式と選言式の充足意味論は命題的に切り詰められている。証人が存在することは保つが、どの証人が与えられたかは忘れる。そのため、論理式の符号や名前比較を外向きに読むと、結論にも切り詰められた存在が残り、消去先は命題に限られる。ここで使われるのは命題的切り詰めであり、命題のリサイズではない。累積階層は集合値の所属関係と、その読みの後で必要となる外延的な等しさの原理を与える。

open import Cubical.Foundations.Transport using ( constSubstCommSlice )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties

階層集合の小さな要素は周囲の階層へ埋め込まれ、その埋め込みの単射性によって、後に表現されたパラメータの等しさから台の中での等しさを復元できる。空集合は空のアルファベットとして働く。定数がないので、そこから出る写像は一意に定まり、無パラメータ論理式は必要な付け替えの下で同じ符号を保つ。フォン・ノイマン数項 # k、その後者、そして ω が、環境の定義域と名前比較に使う内部のアリティを与える。

  using ( ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_ )
open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet using ( #_; ω; sucV )

以下の論理式は構成可能宇宙で解釈される。hPropView 𝒮ʟ を開くことで、その台 S が定まる。台の要素は、周囲の宇宙にある集合と、それが構成可能であるという証拠の組である。また、この構造の命題値をとる等号関係と所属関係もスコープに入る。したがって自由変数と定数は構成可能集合の中を動き、証明で等号や所属の証拠が必要なときには、⟨_⟩ がその命題の基礎型を取り出す。

open hPropView 𝒮ʟ

同じ構文には、互いに両立する二つの読み方がある。この絶対性の実例は、周囲の宇宙の構造 𝒮ᵥ から出発し、それを推移的クラス isL に制限する。外側の読みでは構成可能集合をその基礎にある周囲の集合として扱い、内側の読みでは定数がそれを名指す構成可能集合を表し、制限された構造が等号と所属を解釈する。本章では内側の充足関係を ⊨ と書く。したがって γ : Vec S n に対する判断 γ ⊨ F は、有限環境 γ のもとで F が L の内部に成り立つことを意味する。これは、L 自身が名前を識別して比較する論理式に必要な読み方である。

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

これらの論理式は、環境内の位置によって先に与えられたデータを参照する。新しい束縛子の下では、もとの位置は新たに束縛された値を越えなければならない。二つの束縛子の下では、位置 i は suc (suc i) になる。sh2 はこの移動を表す略記である。FreeAt が後続のアリティとその符号鍵を束縛してから骨格と空のアルファベットの符号集合を参照するとき、また表示の条件が候補要素と拡張環境を束縛してからもとのパラメータ環境を参照するときに使われる。

private
  sh2 : ∀ {n} → Fin n → Fin (suc (suc n))
  sh2 i = suc (suc i)

表示の条件の内部では、四つの値が環境に加わった後で初めて、骨格と台の符号集合を参照する。その四つは、候補要素 z、拡張環境 c、その定義域 k、そして考察中の鍵である。したがって、もとの位置を四回持ち上げる必要がある。sh4 はまさにこの移動を行い、その鍵が台の符号集合に属することと、k と骨格から作られる対に等しいことの両方を述べられるようにする。

  sh4 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc n))))
  sh4 i = suc (suc (suc (suc i)))

さらに一つの存在量化子が鍵に対応する値 v を束縛するため、satGraphAt を用いる時点では台が五つ先の位置にある。ここで v は符号化された論理式を充足する環境全体の集合であり、真理値ではない。続く所属原子は、拡張環境がその集合に属するかを問う。同じ移動は LexAt にも現れる。一つの添字、その位置で二つの環境から得られる値、より前の添字、そして両者の一致を証す共通の値を順に束縛すると、もとのパラメータ環境はやはり五つ先にある。sh5 は両方の論理式に共通する添字計算を記録する。

  sh5 : ∀ {n} → Fin n → Fin (suc (suc (suc (suc (suc n)))))
  sh5 i = suc (suc (suc (suc (suc i))))

空のアルファベットでも同じ符号

空のアルファベットは、空集合の要素の小さな表示 ⟪ ∅ ⟫ である。もし m がその記号の一つなら、埋め込み ⟪ ∅ ⟫↪ によって周囲の集合が得られ、表示の法則はそれが ∅ に属すると述べる。定理 ∅-empty はまさにそのような証拠を否定するので、noAlpha m が従う。したがって、このアルファベット上の論理式は定数の節を含めない。これは無パラメータ論理式の一つの構文的表示である。メタ言語の名前が用いる空の定数域 ⊥* と比較するには、この二つの空型を結び付ければ十分である。

private
  noAlpha : ⟪ ∅ {ℓ} ⟫ → ⊥₀
  noAlpha m = ∅-empty (⟪ ∅ ⟫↪ m) (∈ₛ⟪ ∅ ⟫↪ m)

Fo∅ n は、n 個の変数位置を使える空のアルファベット上の論理式の族 Formula ⟪ ∅ ⟫ n を表す略記である。定数を含まないことは、論理式に別の述語を課すのではなく、定数記号の型そのものから従う。メタ言語の名前は、これに対応する族 Formula ⊥* n を使う。より正確には、Name が格納するのはアリティ、この族に属して変数位置を一つ余分にもつ無パラメータ論理式、そしてそのアリティのパラメータ列である。表示はこの三つから導かれるものであり、別の格納成分ではない。

  Fo∅ : ℕ → Type ℓ
  Fo∅ = Formula ⟪ ∅ {ℓ} ⟫

写像 ε は、空のアルファベット ⟪ ∅ ⟫ から空の定数域 ⊥* への移行を与える。仮に始域の記号 m が与えられれば、noAlpha m が矛盾を導き、空型の消去によって必要な終域の値が得られる。したがって mapFo ε は ⟪ ∅ ⟫ 上の論理式を ⊥* 上の論理式へ改名する。逆向きには、embed を ⊥* から ⟪ ∅ ⟫ への改名として特殊化できる。もともと定数の出現がないので、どちらの操作も定数の出現を変えない。そこで改名の合成則から、空のアルファベットによる特徴付けに必要な論理式の符号の等式が得られる。

  ε : ⟪ ∅ {ℓ} ⟫ → ⊥* {ℓ}
  ε m = ⊥₀-rec (noAlpha m)

モデルの内部で無パラメータ論理式のコードを認識するには、まず「定数を持たない」ことの二つの表し方を結び付ける必要がある。⟪ ∅ ⟫ 上の論理式ψ では、定数域は空集合の要素の型である。一方、mapFo ε ψ は同じ構文を空型⊥* の上で表す。空集合の要素を仮定すれば矛盾が得られるため、写像 εを定義できる。したがって、ψ を直接宇宙へ読む経路と、ε に沿って改名してから宇宙へ埋め込む経路の違いは、空型から出る写像の違いだけである。関数外延性がそれらの写像を同一視し、mapFo-comp が改名の合成を同一視する。このように sameCode は、まず得られる宇宙上の論理式そのものの等式を証明する。後でこの等式にコード化写像を適用すれば、対応するコードの等式が得られる。

  sameCode : ∀ {n} (ψ : Fo∅ n) → mapFo ⟪ ∅ ⟫↪ ψ ≡ embed (mapFo ε ψ)
  sameCode ψ = cong (λ f → mapFo f ψ) (funExt (λ m → ⊥₀-rec (noAlpha m)))
             ∙ sym (mapFo-comp ε ⊥*-rec ψ)

逆向きの比較は、無パラメータ論理式 χ : Formula ⊥* n から始まる。まず χ を ⟪ ∅ ⟫ 上の論理式へ埋め込み、そのアルファベットから宇宙への包含写像に沿って改名することも、初めから宇宙上の論理式へ埋め込むこともできる。mapFo-comp によれば、前者は ⊥* からの一回の改名である。⊥*からの任意の二つの関数は等しいので、この改名は直接の埋め込みで使われるものと一致する。sameCode' の等式は、AllCodes ∅ʟ が埋め込まれた論理式に与えるキーを、χ の通常の宇宙上の論理式コードからなるキーへ移すのに必要な向きを持っている。

  sameCode' : ∀ {n} (χ : Formula (⊥* {ℓ}) n)
            → mapFo ⟪ ∅ {ℓ} ⟫↪ (embed χ) ≡ embed χ
  sameCode' χ = mapFo-comp ⊥*-rec ⟪ ∅ ⟫↪ χ
              ∙ cong (λ f → mapFo f χ) (funExt (λ b → ⊥*-rec b))

もう一つ、依存型に由来する問題がある。アリティは論理式の型の一部なので、等式 e : i ≡ j は ψ : Fo∅ i を subst Fo∅ e ψ : Fo∅ j へ移す。しかし、この移動の後もキーに入る論理式コードは同じでなければならない。論理式を読み、コード化する関数の終域は固定された宇宙 V ℓ であり、アリティの添字には依存しない。したがって、一般の置換計算 constSubstCommSlice により、論理式を輸送してもコードは変わらない。codeShift はこの等式を、輸送後の論理式のコードから元のコードへ向かう形で記録し、復号の議論で行うアリティの調整に備える。

  codeShift : {i j : ℕ} (e : i ≡ j) (ψ : Fo∅ i)
            → VCode.⌜ mapFo ⟪ ∅ ⟫↪ (subst Fo∅ e ψ) ⌝
            ≡ VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝
  codeShift e ψ = sym (constSubstCommSlice
    Fo∅ (V ℓ) (λ _ u → VCode.⌜ mapFo ⟪ ∅ ⟫↪ u ⌝) e ψ)

これで、コード集合との橋の直接な向きを証明できる。無パラメータな k 項論理式 χ を ⟪ ∅ ⟫ 上へ埋め込むと、その論理式のキーはkey∈AllCodes により AllCodes ∅ʟ に属する。このキーは、数項 # k と、埋め込まれた論理式を空のアルファベットを通して読んだコードとの対である。sameCode' はその論理式を χ の宇宙への直接の埋め込みと同一視し、後者のコードはちょうど (limitCode χ) .fst である。この等式に沿って所属の証明を輸送すると freeCode-in が得られる。すなわち、コード集合はすべての無パラメータ論理式について、アリティとコードからなるキーを含む。

freeCode-in : (k : ℕ) (χ : Formula (⊥* {ℓ}) k)
            → ⟨ pr (# k) ((limitCode χ) .fst) ∈ (AllCodes ∅ʟ) .fst ⟩
freeCode-in k χ =
  subst (λ u → ⟨ pr (# k) VCode.⌜ u ⌝ ∈ (AllCodes ∅ʟ) .fst ⟩) (sameCode' χ)
    (key∈AllCodes ∅ʟ (embed χ))

逆向きでは、pr (# k) c が AllCodes ∅ʟ に属すると仮定する。除去定理AllCodes-out は、要素を命題的切り詰めの下でのみ復号し、入力には S の要素、すなわち集合とその構成可能性の証明を要求する。必要な入力の台集合はすでに pr (# k) c なので、残るのはその構成可能性の証明である。それが得られれば、map₁ read は切り詰められた各復号データを、求める k 項の無パラメータなデータへ変換する。この操作が命題的切り詰めを取り除くことはない。

freeCode-out : (k : ℕ) (c : V ℓ) → ⟨ pr (# k) c ∈ (AllCodes ∅ʟ) .fst ⟩
             → ∥ Σ[ χ ∶ Formula (⊥* {ℓ}) k ] (c ≡ (limitCode χ) .fst) ∥₁
freeCode-out k c h = map₁ read (AllCodes-out ∅ʟ (pr (# k) c , cL) h)
  where
  cL : ⟨ isL (pr (# k) c) ⟩

不足していた証明書は、構成可能性の推移性から得られる。AllCodes ∅ʟ .snd はコード集合が構成可能であることを述べ、h はキーがその集合に属することを述べる。したがってisL-trans h (AllCodes ∅ʟ .snd) により、キー自身の構成可能性が証明される。この証明書を pr (# k) c と組にすれば、AllCodes-out が要求する S の要素が得られる。ここでは新たな復号も選択も行われない。

  cL = isL-trans h (AllCodes ∅ʟ .snd)

命題的切り詰めの内部で、AllCodes-out はアリティ n、論理式ψ : Fo∅ n、そして与えられたキーが ψ のキーであることを示す等式を与える。局所関数 read は、そのような各データを、要求されたアリティk の無パラメータ論理式と、c がそのコードに等しいことの証明へ変換する。まず ψ を ψ' : Fo∅ k へ輸送し、次に、現れ得ない定数を ε に沿って改名する。したがって構成される証人は mapFo ε ψ' である。対の等式は、輸送に必要なアリティの等式と、返される依存対に必要なコードの等式をともに与える。

  read : Σ[ n ∶ ℕ ] Σ[ ψ ∶ Fo∅ n ] (pr (# k) c ≡ (keyS ∅ʟ ψ) .fst)
       → Σ[ χ ∶ Formula (⊥* {ℓ}) k ] (c ≡ (limitCode χ) .fst)
  read (n , (ψ , q)) = mapFo ε ψ' , (pr-inj q .snd ∙ step)
    where
    e : n ≡ k

キーの等式の二つの成分が構成を完成させる。第一成分の型は # k ≡ # nである。数項の単射性と対称性から e : n ≡ k が得られ、ψ はそれに沿ってψ' へ輸送される。第二成分は、c が元の ψ から得られる宇宙上の論理式コードに等しいことを述べる。codeShift により、そのコードは輸送後の ψ' のコードと一致する。さらに sameCode により、後者はembed (mapFo ε ψ') のコードと一致する。これらの等式を合成すると、証人と組にすべき証明がちょうど得られる。read は map₁ を通してのみ使われるため、freeCode-out の結論は、そのような無パラメータ論理式が命題的切り詰めの下で存在するということだけである。コード集合から論理式を選び出してはいない。

    e = sym (#-inj′ (pr-inj q .fst))
    ψ' : Fo∅ k
    ψ' = subst Fo∅ e ψ
    step : VCode.⌜ mapFo ⟪ ∅ ⟫↪ ψ ⌝ ≡ VCode.⌜ embed (mapFo ε ψ') ⌝
    step = sym (codeShift e ψ) ∙ cong VCode.⌜_⌝ (sameCode ψ')

無パラメータ性を一つの原子で述べる

符号集合では、論理式はアリティと骨格からなるキーのもとに格納される。このことを一つの所属原子で表すため、FreeAt はまずアリティ位置の値の後続を束縛し、次にその後続と骨格との対を束縛して、最後にその対が符号集合位置に属するかを問う。したがってメタ言語の記法では ∃[ z ] ∃[ y ] という形をもち、z が後続アリティ、y がキーである。各シフトは、一つまたは二つの束縛子の下から元のどの位置を参照するかを正確に記録する。この段階で論理式が述べるのは C₀ に置かれた集合への所属だけである。その位置を空のアルファベットの符号集合と同定して初めて、無パラメータ性という意味が得られる。

FreeAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
FreeAt C₀ s a =
  ∃̇ ( sucAtL (suc a) zero
    ∧̇ ∃̇ ( prAtL zero (suc zero) (sh2 s)
         ∧̇ (var zero ∈̇ var (sh2 C₀)) ) )

最初の一対の読みは、任意の環境 γ に対して成り立つ。外側から与えられる等式 qa は、アリティ位置の値を数項 # k と同定する。これは意味論的な読みの仮定であり、FreeAt の内部にある別の節ではない。骨格位置と符号集合位置はまだ任意なので、これらの補題は特定の符号集合を選ぶ前に、二つの束縛子の論理的内容だけを取り出している。

module _ {n : ℕ} (C₀ s a : Fin n) (γ : Vec S n) (k : ℕ)
         (qa : (lookup a γ) .fst ≡ # k) where

FreeAt-in : ⟨ pr (# (suc k)) ((lookup s γ) .fst) ∈ (lookup C₀ γ) .fst ⟩
          → ⟨ γ ⊨ FreeAt C₀ s a ⟩
FreeAt-in h = ∣ numAt , ( hsuc , ∣ keyAt , ( hpr , h ) ∣₁ ) ∣₁
  where
  numAt : S

  numAt = # (suc k) , numL (suc k)
  keyAt : S
  keyAt = pr (# (suc k)) ((lookup s γ) .fst) , isL-trans h (lookup C₀ γ .snd)
  hsuc : ⟨ (numAt ∷ γ) ⊨ sucAtL (suc a) zero ⟩
  hsuc = subst ⟨_⟩ (sym (sucAtL-adequate (suc a) zero (numAt ∷ γ)))

    (cong sucV (sym qa))
  hpr : ⟨ (keyAt ∷ numAt ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
  hpr = subst ⟨_⟩
    (sym (prAtL-adequate zero (suc zero) (sh2 s) (keyAt ∷ numAt ∷ γ))) refl

FreeAt-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
           → ⟨ pr (# (suc k)) ((lookup s γ) .fst) ∈ (lookup C₀ γ) .fst ⟩
FreeAt-out = rec₁ ((pr (# (suc k)) ((lookup s γ) .fst)
                          ∈ (lookup C₀ γ) .fst) .snd) atNum
  where

  Target : Type (ℓ-suc ℓ)
  Target = ⟨ pr (# (suc k)) ((lookup s γ) .fst) ∈ (lookup C₀ γ) .fst ⟩

  atKey : (z : S) → z .fst ≡ sucV ((lookup a γ) .fst)
        → Σ[ y ∶ S ] ( ⟨ (y ∷ z ∷ γ) ⊨ prAtL zero (suc zero) (sh2 s) ⟩
                     × ⟨ y .fst ∈ (lookup C₀ γ) .fst ⟩ )
        → Target
  atKey z qz (y , (hp , hy)) =

    subst (λ u → ⟨ u ∈ (lookup C₀ γ) .fst ⟩)
      (subst ⟨_⟩ (prAtL-adequate zero (suc zero) (sh2 s) (y ∷ z ∷ γ)) hp
       ∙ cong (λ u → pr u ((lookup s γ) .fst)) (qz ∙ cong sucV qa)) hy

  atNum : Σ[ z ∶ S ] ( ⟨ (z ∷ γ) ⊨ sucAtL (suc a) zero ⟩
                     × ⟨ (z ∷ γ) ⊨ ∃̇ ( prAtL zero (suc zero) (sh2 s)
                                     ∧̇ (var zero ∈̇ var (sh2 C₀)) ) ⟩ )
        → Target
  atNum (z , (hs , hk)) = rec₁ ((pr (# (suc k)) ((lookup s γ) .fst)

                                       ∈ (lookup C₀ γ) .fst) .snd)
    (atKey z (subst ⟨_⟩ (sucAtL-adequate (suc a) zero (z ∷ γ)) hs)) hk

続く二つの読みでは、それまで任意だった二つの位置を具体化する。等式 q₀ は C₀ 位置の集合を AllCodes ∅ʟ と同定する。その要素は空のアルファベット上の論理式のキーである。また qa は、アリティ値を再び # k と同定する。これらの仮定のもとで、FreeAt-in と FreeAt-out が特徴付けた所属を、アリティ suc k の無パラメータ論理式についての具体的な主張へ変換できる。

module _ {n : ℕ} (C₀ s a : Fin n) (γ : Vec S n) (k : ℕ)
         (q₀ : (lookup C₀ γ) .fst ≡ (AllCodes ∅ʟ) .fst)
         (qa : (lookup a γ) .fst ≡ # k) where

codeFree-out : ⟨ γ ⊨ FreeAt C₀ s a ⟩
             → ∥ Σ[ χ ∶ Formula (⊥* {ℓ}) (suc k) ]
                   ((lookup s γ) .fst ≡ (limitCode χ) .fst) ∥₁
codeFree-out h = freeCode-out (suc k) ((lookup s γ) .fst)
  (subst (λ u → ⟨ pr (# (suc k)) ((lookup s γ) .fst) ∈ u ⟩) q₀

    (FreeAt-out C₀ s a γ k qa h))

codeFree-in : (χ : Formula (⊥* {ℓ}) (suc k))
            → (lookup s γ) .fst ≡ (limitCode χ) .fst → ⟨ γ ⊨ FreeAt C₀ s a ⟩
codeFree-in χ q = FreeAt-in C₀ s a γ k qa
  (subst (λ u → ⟨ pr (# (suc k)) ((lookup s γ) .fst) ∈ u ⟩) (sym q₀)
    (subst (λ u → ⟨ pr (# (suc k)) u ∈ (AllCodes ∅ʟ) .fst ⟩) (sym q)

      (freeCode-in (suc k) χ)))

列の長さを読む

まず、集合として符号化されたグラフへの任意の所属を特徴づける。g が Fin k で添字づけられ、pr x y が env g に属するなら、x ≡ # (toℕ i) かつ y ≡ g i となる添字 i が単に存在する。階層の集合への所属が記録するのは、生成元となる項目の単なる存在だけなので、結果は命題的切り詰めのもとに留まる。したがって memberOf は可能な添字を明らかにするが、その一つを選び出しはしない。

private
  memberOf : (k : ℕ) (g : Fin k → V ℓ) (x y : V ℓ) → ⟨ pr x y ∈ env g ⟩
           → ∥ Σ[ i ∶ Fin k ] ((x ≡ # (toℕ i)) × (y ≡ g i)) ∥₁
  memberOf k g x y = map₁
    (λ { (li , e) → lower li

所属の証人は、グラフに格納された項目と問い合わせた順序対との等式を含む。順序対の構成子の単射性により、この一つの等式は二つの成分の等式に分かれる。証人では格納された項目が先に書かれているため、両方の成分のパスを逆向きにして、memberOf が必要とする向きにする。すなわち、x と y から、それぞれ数項の鍵と g の与える値へ向かう等式である。

       , (sym (pr-inj e .fst) , sym (pr-inj e .snd)) })

逆に、指定された各添字は一つの項目を与える。i : Fin k に対して、順序対 pr (# (toℕ i)) (g i) は env g に属する。持ち上げられた添字が所属の証人となり、項目の等式は反射性である。こうして memberOf と entryOfは、この有限グラフの第一成分を認識するために必要な二つの向きを与える。

  entryOf : (k : ℕ) (g : Fin k → V ℓ) (i : Fin k)
          → ⟨ pr (# (toℕ i)) (g i) ∈ env g ⟩
  entryOf k g i = ∣ lift i , refl ∣₁

定義域の順向きの包含は、pr x (y .fst) がグラフに入るようなモデルの元y が単に存在することから始まる。目標は所属命題 x ∈ # k なので、外側の命題的切り詰めをこの目標へ消去できる。代表 y を一つ固定した後は、グラフへの所属から添字を復元し、その数項が # k に属することを示せば十分である。

  dom-into : (k : ℕ) (g : Fin k → V ℓ) (x : V ℓ)
           → ⟨ ∃[ y ∶ S ] pr x (y .fst) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
  dom-into k g x = rec₁ ((x ∈ # k) .snd) atEntry
    where
    atIndex : (u : V ℓ) → Σ[ i ∶ Fin k ] ((x ≡ # (toℕ i)) × (u ≡ g i))

具体的な添字 i に対して、定義域が必要とするのは第一成分の等式だけである。toℕ i < k なので、数項に関する補題 #mono は # (toℕ i) を # k に入れる。さらに x ≡ # (toℕ i) に沿って輸送すれば、x もそこに属する。第二成分の等式はグラフの値を同定するが、この包含には不要である。補助関数atEntry は値 y を固定してから、残る切り詰められた添字の情報を消去する。

            → ⟨ x ∈ # k ⟩
    atIndex u (i , (qx , _)) = subst (λ v → ⟨ v ∈ # k ⟩) (sym qx)
      (#mono (toℕ i) k (toℕ<n i))
    atEntry : Σ[ y ∶ S ] ⟨ pr x (y .fst) ∈ env g ⟩ → ⟨ x ∈ # k ⟩
    atEntry (y , p) = rec₁ ((x ∈ # k) .snd) (atIndex (y .fst))

グラフへの所属に memberOf を適用すると、必要な添字の情報がちょうど得られるが、それはまだ命題的切り詰めのもとにある。x ∈ # k は命題なので、rec₁ は各代表を atIndex に渡せる。これで添字を通常のデータとして取り出すことなく、順向きの包含が閉じる。

      (memberOf k g x (y .fst) p)

逆向きの包含では x ∈ # k と仮定する。von Neumann 数項の消去により、ある自然数 m < k について x ≡ # m であることが、命題的切り詰めのもとで得られる。そのような m は Fin k の添字を定める。結論もグラフの値の存在を命題的に切り詰めたものなので、map₁ はいずれかを選ぶことなく、各数項の証人を変換できる。仮定 cg は、その値をモデルの元として提示するために必要な構成可能性の証明を供給する。

  dom-from : (k : ℕ) (g : Fin k → V ℓ) → ((i : Fin k) → ⟨ isL (g i) ⟩)
           → (x : V ℓ) → ⟨ x ∈ # k ⟩ → ⟨ ∃[ y ∶ S ] pr x (y .fst) ∈ env g ⟩
  dom-from k g cg x h = map₁ atNumeral (∈#-elim k x h)
    where
    atNumeral : Σ[ m ∶ ℕ ] ((m < k) × (x ≡ # m))

代表 m < k に対し、i を対応する有限添字とする。存在量化の証人はモデルの元 (g i , cg i)、すなわちその添字での値と構成可能性の証明である。グラフについての事実は entryOf から得られる。標準的な第一成分# (toℕ i) をもつ対が一つの項目だからである。この第一成分を x へ輸送すれば、pr x (g i) がグラフに属するという必要な所属が得られる。

              → Σ[ y ∶ S ] ⟨ pr x (y .fst) ∈ env g ⟩
    atNumeral (m , (p , qx)) = (g i , cg i)
      , subst (λ u → ⟨ pr u (g i) ∈ env g ⟩) (sym qi) (entryOf k g i)
      where
      i : Fin k

変換 fromℕ' k m p は境界の証明 p : m < k から添字 i を作る。その往復則 toFromId' は toℕ i ≡ m を証明する。x ≡ # m と、往復の等式を逆向きにして数項へ写したパスとを合成すると、qi : x ≡ # (toℕ i) が得られる。これは標準的な項目を問い合わせた第一成分へ移すためのパスそのものである。これで定義域の逆向きの包含も完成する。

      i = fromℕ' k m p
      qi : x ≡ # (toℕ i)
      qi = qx ∙ cong #_ (sym (toFromId' k m p))

これで、二つの集合レベルの包含を対象言語の定義域の論理式と対応させられる。環境 γ、族 g : Fin k → V ℓ、そしてスロット e の台集合を env g と同定する等式 qe を固定し、スロット d は定義域の候補として残す。各 cg i は g i が構成可能モデルの元であることを証明する。これは逆向きの包含が存在の証人を作るときに、まさに必要となる条件である。この文脈で、次の二つの補題が domAt e d を読み出し、また充填する。

module _ {n : ℕ} (e d : Fin n) (γ : Vec S n)
         (k : ℕ) (g : Fin k → V ℓ) (cg : (i : Fin k) → ⟨ isL (g i) ⟩)
         (qe : (lookup e γ) .fst ≡ env g) where

domAt-numeral : ⟨ γ ⊨ domAt e d ⟩ → (lookup d γ) .fst ≡ # k
domAt-numeral h = cong (λ p → p .fst) (extensionalL {a = lookup d γ} {b = # k , numL k} pt)
  where
  fwd : (x : S) → ⟨ x .fst ∈ (lookup d γ) .fst ⟩ → ⟨ x .fst ∈ # k ⟩
  fwd x hx = dom-into k g (x .fst)

    (subst (λ u → ⟨ ∃[ y ∶ S ] pr (x .fst) (y .fst) ∈ u ⟩) qe
      (domAt-in e d γ h x hx))
  bwd : (x : S) → ⟨ x .fst ∈ # k ⟩ → ⟨ x .fst ∈ (lookup d γ) .fst ⟩
  bwd x hx = rec₁ ((x .fst ∈ (lookup d γ) .fst) .snd) put (dom-from k g cg (x .fst) hx)
    where

    put : Σ[ y ∶ S ] ⟨ pr (x .fst) (y .fst) ∈ env g ⟩ → ⟨ x .fst ∈ (lookup d γ) .fst ⟩
    put (y , p) = domAt-out e d γ h x y
      (subst (λ u → ⟨ pr (x .fst) (y .fst) ∈ u ⟩) (sym qe) p)
  pt : (x : S) → (x .fst ∈ (lookup d γ) .fst) ≡ (x .fst ∈ # k)
  pt x = ⇔toPath (fwd x) (bwd x)

domAt-fill : (lookup d γ) .fst ≡ # k → ⟨ γ ⊨ domAt e d ⟩
domAt-fill qd = domAt-intro e d γ step
  where
  step : (x : S)
       → (⟨ ∃[ y ∶ S ] pr (x .fst) (y .fst) ∈ (lookup e γ) .fst ⟩

          → ⟨ x .fst ∈ (lookup d γ) .fst ⟩)
       × (⟨ x .fst ∈ (lookup d γ) .fst ⟩
          → ⟨ ∃[ y ∶ S ] pr (x .fst) (y .fst) ∈ (lookup e γ) .fst ⟩)
  step x =
      (λ hy → subst (λ u → ⟨ x .fst ∈ u ⟩) (sym qd) (dom-into k g (x .fst)

        (subst (λ u → ⟨ ∃[ y ∶ S ] pr (x .fst) (y .fst) ∈ u ⟩) qe hy)))
    , (λ hx → subst (λ u → ⟨ ∃[ y ∶ S ] pr (x .fst) (y .fst) ∈ u ⟩) (sym qe)
        (dom-from k g cg (x .fst) (subst (λ u → ⟨ x .fst ∈ u ⟩) qd hx)))

充足関係グラフが割り当てる値

次に、充足関係グラフが実際の論理式の鍵で何を割り当てるかを調べる。周囲の環境 γ を固定し、スロット B から台を、x と y から鍵と値の候補を受け取る。略記 Bs = lookup B γ により、以下の証明はこの三つのスロットについて一様に述べられる。ここで扱う論理式の定数は、台集合 Bs .fst の要素によって添字づけられる。

module _ {n : ℕ} (B x y : Fin n) (γ : Vec S n) where

private
  Bs : S
  Bs = lookup B γ

  fr : ∀ {m} (φ : Formula S m) → Vec S ( + n)
  fr φ = ev numν (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ

  tgs : ∀ {m} (φ : Formula S m) → Tags (fr φ) NN
  tgs φ = numTags (Tower.tower Bs) (slot Bs φ) (satTable Bs φ) Bs γ

  htow : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ towerAt Ei Bi (NN f0) ⟩
  htow φ = TowerHolds.holds Ei Bi (NN f0) (fr φ) Bs refl refl refl

  hdom : ∀ {m} (φ : Formula S m) → ⟨ fr φ ⊨ domAt Ti Ci ⟩
  hdom φ = domAt-intro Ti Ci (fr φ)
    (λ z → (λ h → rec₁ ((z .fst ∈ (slot Bs φ) .fst) .snd)
               (λ { (w , hw) → inSlot Bs φ (z .fst) (w .fst) hw }) h)
         , (λ h → total Bs φ (z .fst) h))

graphAt-value : ∀ {m} (ψ : Formula ⟪ Bs .fst ⟫ m)
              → (lookup x γ) .fst ≡ (keyS Bs ψ) .fst
              → (lookup y γ) .fst ≡ (Sat Bs (mapFo (asConst Bs) ψ)) .fst
              → ⟨ γ ⊨ satGraphAt B x y ⟩
graphAt-value {m} ψ qx qy = graphAt-in B x y γ

  ∣ numν
  , (Tower.tower Bs
  , (slot Bs φ
  , (satTable Bs φ
  , (Bs

  , (refl
  , (tgs φ
  , (htow φ
  , (slotClosed Bs φ (Tower.tower Bs ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
       ∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ γ)

  , (hdom φ
  , (subst2 (λ u v → ⟨ pr u v ∈ (satTable Bs φ) .fst ⟩)
       (sym (qx ∙ keyBridge Bs ψ)) (sym qy) (entry-in Bs φ)
  , SlotHolds.holds Bs Ti Bi Ci Ei NN (fr φ) refl (tgs φ) (htow φ) ψ refl refl)))))))))) ∣₁
  where

  φ : Formula S m
  φ = mapFo (asConst Bs) ψ

graphAt-only : ∀ {m} (ψ : Formula ⟪ Bs .fst ⟫ m)
             → (lookup x γ) .fst ≡ (keyS Bs ψ) .fst
             → ⟨ γ ⊨ satGraphAt B x y ⟩
             → (lookup y γ) .fst ≡ (Sat Bs (mapFo (asConst Bs) ψ)) .fst
graphAt-only {m} ψ qx h = rec₁ (setIsSet _ _) read (graphAt-out B x y γ h)

  where
  read : GraphWitAt B x y γ → (lookup y γ) .fst ≡ (Sat Bs (mapFo (asConst Bs) ψ)) .fst
  read (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) =
    SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b γ) Bs eb tg hE hc h12
      ψ (subst (λ u → ⟨ u ∈ C .fst ⟩) qx

           (domAt-out Ti Ci (ev ν E C T b γ) hd (lookup x γ) (lookup y γ) ha))
      (lookup y γ)
      (subst (λ u → ⟨ pr u ((lookup y γ) .fst) ∈ T .fst ⟩) qx ha)

名前をスロット上で記述する

表示を定める本体は、候補 z を一つずつ調べる。最初の連言 z ∈ B は、記述される集合を台の内部に制限する。次に環境 c を束縛し、c がパラメータ環境 e の先頭に z を加えて得られる符号化環境であることを要求する。この時点では c と z が周囲の割り当ての前に置かれているので、e への参照は二つの束縛子を越えて移される。

DenoteBody : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Formula S (suc n)
DenoteBody B C s e =
  (var zero ∈̇ var (suc B))
  ∧̇ ∃̇ ( consAtL zero (suc zero) (sh2 e)
       ∧̇ ∃̇ ( domAt (suc zero) zero

残る三つの証人は、骨格をどのように解釈するかを定める。まず k が拡張環境 c の定義域であることを要求する。次に key はスロット C の符号集合に属し、k と骨格の符号 s の対に等しくなければならない。最後に v は、台 B の充足関係グラフがその鍵で許す値であり、末尾の所属は c ∈ v を述べる。C に台の実際の符号集合が入ると、これらの条件は、任意の鍵でグラフを参照するだけではなく、拡張環境が骨格を充足することを表す。

            ∧̇ ∃̇ ( (var zero ∈̇ var (sh4 C))
                 ∧̇ ( prAtL zero (suc zero) (sh4 s)
                   ∧̇ ∃̇ ( satGraphAt (sh5 B) (suc zero) zero
                        ∧̇ (var (suc (suc (suc zero))) ∈̇ var zero) ) ) ) ) )

メタ言語の名前は、アリティ、無パラメータ論理式、パラメータベクトルからなる。NameAt はそれらをアリティのスロット a、骨格の符号のスロット s、環境のスロット e で表し、表示のスロット d にはそのデータから導かれる集合を記録する。最初の連言は、a の後続と s から作った対が空のアルファベットの符号集合に属することを確かめる。この後続は欠かせない。a 個のパラメータをもつ名前には、候補となる要素を置く変数がもう一つ必要だからである。次の連言は、a がモデルの自然数の集合に属することを要求する。

NameAt : ∀ {n} → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n → Fin n
       → Formula S n
NameAt B C C₀ s a e d =
  FreeAt C₀ s a
  ∧̇ ( (var a ∈̇ con ωʟ)

第三の連言は、e が定義域をちょうど a とし、B に値をとる環境であることを要求する。これにより、パラメータベクトルが一つ前のスロットに記録されたアリティと結び付く。最後の連言は d を外延的に特徴づける。各候補について、d への所属は DenoteBody の充足と同値であり、その本体の最初の連言がすでに候補を B の中に制限している。したがって d は名前の三つのデータから導かれるもので、メタ言語の名前に追加で保存される成分ではない。

    ∧̇ ( envOverAt e a B ∧̇ extAt d (DenoteBody B C s e) ) )

DenoteOf z は、DenoteBody の四層の存在量化に対応するメタ言語の中身である。拡張環境 c、その定義域の候補 k、論理式の鍵、グラフの値 v と、それらを結ぶすべての条件を記録する。これらを一つの依存対にまとめることで、対象言語の論理式を組み立てるのに必要な証人を明示しながら、後の条件が先に選んだ値に依存することも保たれる。

module _ {n : ℕ} (B C s e : Fin n) (γ : Vec S n) where

DenoteOf : (z : S) → Type (ℓ-suc ℓ)
DenoteOf z = Σ[ c ∶ S ] Σ[ k ∶ S ] Σ[ key ∶ S ] Σ[ v ∶ S ]
  ( ⟨ (c ∷ z ∷ γ) ⊨ consAtL zero (suc zero) (sh2 e) ⟩
  × ( ⟨ (k ∷ c ∷ z ∷ γ) ⊨ domAt (suc zero) zero ⟩

    × ( ⟨ key .fst ∈ (lookup C γ) .fst ⟩
      × ( (key .fst ≡ pr (k .fst) ((lookup s γ) .fst))
        × ( ⟨ (v ∷ key ∷ k ∷ c ∷ z ∷ γ) ⊨ satGraphAt (sh5 B) (suc zero) zero ⟩
          × ⟨ c .fst ∈ v .fst ⟩ ) ) ) ) )

DenoteBody-in : (z : S) → ⟨ z .fst ∈ (lookup B γ) .fst ⟩ → DenoteOf z
              → ⟨ (z ∷ γ) ⊨ DenoteBody B C s e ⟩
DenoteBody-in z hz (c , (k , (key , (v , (hc , (hk , (hi , (hp , (hg , hm)))))))))
  = hz , ∣ c , (hc , ∣ k , (hk , ∣ key , (hi
  , ( subst ⟨_⟩ (sym (prAtL-adequate zero (suc zero) (sh4 s) (key ∷ k ∷ c ∷ z ∷ γ))) hp