この章を読むか、対話型目次と依存グラフで別のルートを選べます。

対話型目次 · 依存グラフ

複合的な集合の値を一階の有界論理式で記述するには、固定された部分を定数で名指し、各証人を集合で限界づける。ここでのすべては、ひとつの固定されたレベル ℓ の上で行われる。周囲の階層は V ℓ であり、有界量化子がその要素を渡る模型は、その中に置かれた構成可能模型である。充足の判断は真理値を比較するものなので、これらの論理式が主張する事実は、hProp (ℓ-suc ℓ) の命題になる。

module L.Coding.Expressions {ℓ : Level} where

符号化された充足関係の再帰は、L の内部で「環境 γ は符号 c の論理式を充足するか」という形の問いを判定しなければならない。Kuratowski 対のような複合的な値を有界論理式で認識するには、証人自身が模型の要素でなければならない。成分 u と v をもつ対 q に対しては、s が q に属し、u と v が s に属する構成可能集合 s が要る。読みの論理式はこの三者を一度に束縛し、v, u, s に元の割り当てを続けた拡張割り当てのもとで二つの成分条件を評価する。元のスロットはずらしの下で保たれる。

本章はこれを一度だけ組み立てる。代入スロット、構成可能なリテラル、数項、Kuratowski 対からなる小さな式の言語上の構造的な読みを与え、その双方向の妥当性を証明する。外向きの方向は充足の判断から出発し、三つの命題的切り捨てを受けた存在を命題値のパスへ消去し、対の等式を帰納的な成分のパスと連結する。内向きの方向は二つの部分式の明示的な内部要素を選び、それらの共通の構成可能コンテナを取得する。截断から選択を取り出すことは一切ない。

同じ読みはいくつもの方向に特殊化される。式の値がある項の指示への所属は L の推移性を用いる。周囲の値が項の構成可能な解釈に属するという事実がその値の構成可能性を証明し、それによって値は模型の要素として働ける。これは実際の構成であって、截断の消去を正当化する命題値の対象という制限とは別物である。外延的な集合の記述は普通の全称含意の対であり、外側に截断はなく、候補となる集合を構成するのではなく特徴づける。アリティ付きタグの認識器は二層の入れ子の対、すなわちアリティと「タグとペイロードの対」を読む。最後に、後者と環境拡張の論理式は有界絶対性によって持ち上げられる。その転送は確立された推移的モデルの設定と、射影の下での参照の相容性に依拠する。環境拡張の論理式が本章を閉じる。

ひとつの区別の二つの側面が本章を貫く。階層の外では、構造 𝒮ᵥ が V ℓ の上で一階の言語を解釈し、そこの Kuratowski 対が演算 pr である。模型の内側では、同じ言語が構成可能集合の上で改めて解釈される。したがって複合的な値を認識する節は、両方の場所で同時に読めなければならず、以下の各妥当性の主張が述べるのはまさにそのことである。内部の論理式の模型での真理値が、経路として、pr と射影された割り当てについての対応する周囲の主張と同一視されるのである。

構成可能模型の要素とは、周囲の集合に「それが構成可能である」という証明を添えたものである。L の推移性が、有界な証人が両側の間を移れるようにする。isL-trans により、構成可能集合の要素はそれ自身構成可能であり、したがってそれ自体が模型の要素になれる。有界絶対性は論理式について対応する仕事をする。階層についての、すべての定数が構成可能集合を名指す Δ₀ 論理式は、L の内部でも意味を変えない。BoundedFo データが記録する定数の有界性は、この転送が要る前提そのものである。後者と環境拡張の論理式はすでに階層の側で証明されており、模型への持ち上げはこの転送を適用することにほかならない。

数項にはひとつの相容性の事実が必要である。内部の数項 numeralL k はフォン・ノイマンの自然数 k を模型の内部で実現し、numeralL-fst はその射影を周囲の # k と同一視する。数項の節の両方向はこれに依存する。いくつかの節は有限個のスロットについて同時に量化するので、環境はスロットの再索引付けに沿って移される。ひとつの論理的な形式が全章を貫く。妥当性の主張は命題の同値の二つの含意から得られる真理値の経路であり、対象言語の有界量化子は命題的切り捨てを受けた存在として読まれる。

周囲の階層 V ℓ は h-集合なので、その二つの集合の等しさは命題であり、真理値の中に置ける。これが後の梱包された等式を正当化するものである。自然数は集合として現れる。# k は階層におけるフォン・ノイマンの数項、sucV はその後者演算であり、宇宙レベルとも、符号が持つアリティの指標とも別の概念である。命題的切り捨ては単なる存在を与え、その消去が正当なのは命題値の対象に限られる。対の読みの外向きの証明はこの制限を明示的に守る。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; setIsSet; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

ここで使う真理値はレベル ℓ-suc ℓ の hProp の命題であり、それぞれ「それが命題である証明」とともに梱包され、結合子と量化子はこれらの命題に直接作用する。模型の台 S は、周囲の集合と構成可能性の証明の対からなる。絶対性の仕組みはこの状況に対して一度だけ設けられる。相対化される構造は階層 𝒮ᵥ、部分模型を選ぶクラスは isL、Δ₀ 論理式を絶対的に保つのが推移性である。充足は ⊨、項の解釈は ⟦_⟧ と書き、環境は模型の要素からなるベクトルである。

open hPropView 𝒮ʟ using ( S )

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

模型の辞書の中で、主な構成に決定的なのは対の形をした事実である。模型の対 prʟ は prʟ-fst によって周囲の対へ射影され、その有界な読みの論理式が prAtL である。レコード Container と container は、ある対に等しい値に対して、両方の成分を収める構成可能集合をひとつ作る。有界な論理式で対を読むには、まさにそのような中間集合が必要であり、lookup-fst と envOverAt は、のちに使われる同じ辞書の射影と環境の事実である。

模型における有界量化子は S の要素を渡る。したがって論理式に認識させたい複合的な値は、それ自身が模型の要素である有界な証人によって一致させられねばならない。本節はその一般的な道具を組み立てる。代入スロット、構成可能なリテラル、数項、Kuratowski 対から値を組み立てる帰納的な言語 Expr と、表現を論理式へ変えるひとつの構造的な読み、そして論理式の意味を表現の指す値と同一視する両方向の妥当性定理である。本章の残りはすべて、この読みの特殊化である。

本節は小さな二つの準備から始まる。PairIs a p は「周囲の値 a が p に等しい」という主張を真理値として梱包する。階層は h-集合なので、その等式の型は命題であり、setIsSet との対によって hProp (ℓ-suc ℓ) の要素になる。以後の妥当性の主張は、充足の判断とこれらの梱包された等式をパスに沿って比較することになる。式の言語そのものは自然数 n を指標とし、利用できる自由変数スロットの数を確定する。ひとつのスロットが使われないままであっても構わない。

private
  PairIs : V ℓ → V ℓ → hProp (ℓ-suc ℓ)
  PairIs a p = (a ≡ p) , setIsSet a p

module PairExpression where

data Expr (n : ℕ) : Type (ℓ-suc ℓ) where

表現の言語は四つの構成子で確定し、それぞれが複合的な値が論理式に現れるひとつのしかたに対応する。slot i は周囲の割り当ての第 i 項を参照する、変数に相当するものである。literal a は模型の要素ひとつを、構成可能性の証明書ごとまとめて名指し、対象言語の定数のように振る舞う。numeral k はフォン・ノイマンの自然数 k を名指し、pair は二つの部分表現を Kuratowski 対へ合成する。表現は値の有限な記述であって、それ自身は集合ではないので、二つの独立した読み方が許され、目標はこの二つが一致することの証明である。

  slot : Fin n → Expr n
  literal : S → Expr n
  numeral : ℕ → Expr n
  pair : Expr n → Expr n → Expr n

value : ∀ {n} → Expr n → (Fin n → V ℓ) → V ℓ

第一の読みは周囲のものである。階層の集合を各スロットに割り当てると、value は表現の指す集合を計算する。スロットは参照され、リテラルは fst で証明書を射影して捨てられ、数項は # k になり、対は指された二つの集合の Kuratowski 対 pr である。妥当性定理が右辺として取り戻すのはこの読みである。有界な論理式の意義は、外で自然に記述される値を模型の内部から識別することにある。

value (slot i) γ = γ i
value (literal a) γ = a .fst
value (numeral k) γ = # k
value (pair a b) γ = pr (value a γ) (value b γ)

element : ∀ {n} → Expr n → (Fin n → S) → S

第二の読みは模型の内部にとどまる。S の要素を各スロットに割り当てると、element は S の要素をひとつ計算する。リテラルはもともと証明書を伴う模型の要素であり、数項は模型内部の数項 numeralL を使い、対は模型自身の対 prʟ で作られる。二つの読みは条項ごとに平行しており、この平行性こそ両者を結ぶ橋が証明できる理由である。比較はつねに対応する場合どうしの比較で済むからである。

element (slot i) γ = γ i
element (literal a) γ = a
element (numeral k) γ = numeralL k
element (pair a b) γ = prʟ (element a γ) (element b γ)

element-fst : ∀ {n} (e : Expr n) (γ : Fin n → S)

橋となるのが element-fst である。内部の要素を射影すると、その道はちょうど、射影された割り当てにおける周囲の値になる。スロットとリテラルでは二つの読みが文字どおり一致するので、証明は refl である。数項が最初の本格的な場合で、その内部の形は numeralL-fst によって周囲の形へ射影される。これは数項の章が供給する、内部の数項と周囲の数項の間の相容性の事実である。方向に注意してほしい。これは後章でも繰り返される。道は内部の値の射影から周囲の値へ向かう。

            → (element e γ) .fst ≡ value e (λ i → (γ i) .fst)
element-fst (slot i) γ = refl
element-fst (literal a) γ = refl
element-fst (numeral k) γ = numeralL-fst k
element-fst (pair a b) γ = prʟ-fst (element a γ) (element b γ)

対の場合は独立した二つの相容性を連結する。模型の対は prʟ-fst によって周囲の対へ射影され、各成分の射影の法則は帰納的な事実である。pr の下での合同性が二つの成分の道をひとつにまとめ、入れ子になった表現の射影の法則は帰納法で従う。構文の側では、lift3 が対の読み出しに要る再索引付けである。各スロットを三つ上げる、つまり lift3 ρ i = suc (suc (suc (ρ i))) とすることで、各スロットが指す旧来の項目を保ったまま、三つの新しい変数の分の空きができる。

  ∙ cong₂ pr (element-fst a γ) (element-fst b γ)

lift3 : ∀ {n m} → (Fin n → Fin m) → Fin n → Fin (3 + m)
lift3 ρ i = suc (suc (suc (ρ i)))

read : ∀ {n m} → Expr n → (Fin n → Fin m) → Fin m → Formula S m
read (slot i) ρ q = var q ≐ var (ρ i)

読み出し read は、スロット q の表現を有界な論理式へ変える。スロットは対応する再索引付けされた変数との等しさを、リテラルはその定数との等しさを、数項は内部の数項を名指す定数との等しさを要求する。数学的な内容を担うのは対の場合である。三つの有界存在によって、q の集合の中の集合 s と、s の中の要素 u、v を結び、s が q の項目の要素であり、u と v が s の要素になるようにする。そして模型の対の読みの論理式 prAtL を通して、q の項目が対 pr u v に等しいと主張する。成分の条件はその後、ずらしたスロットで帰納的に読まれ、これを lift3 が担う。こうして複合的な値は、模型の内部から、Kuratowski の二成分をともに収める構成可能な中間集合を経由して認識される。

read (literal a) ρ q = var q ≐ con a
read (numeral k) ρ q = var q ≐ con (numeralL k)
read (pair a b) ρ q = ∃̇∈ (var q) (∃̇∈ (var zero) (∃̇∈ (var (suc zero))
  (prAtL (suc (suc (suc q))) (suc zero) zero
    ∧̇ (read a (lift3 ρ) (suc zero) ∧̇ read b (lift3 ρ) zero))))

妥当性には二つの方向があり、out は健全性の証明が消費する方向である。充足の判断の要素から、「スロット q の項目を射影すると指された値に等しい」という道を作る。スロットとリテラルは定義どおりそのような道そのものであり、数項の場合は前提を numeralL-fst と合成する。方向は element-fst と同じである。本格的な仕事は対の場合にあり、次の二段がそれを扱う。

out : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : Vec S m)
     → ⟨ γ ⊨ read e ρ q ⟩ → (lookup q γ) .fst ≡ value e (λ i → (lookup (ρ i) γ) .fst)
out (slot i) ρ q γ h = h
out (literal a) ρ q γ h = h
out (numeral k) ρ q γ h = h ∙ numeralL-fst k

対の場合の前提は三層に重なった截断された有界存在なので、証明はそれを一度にひとつずつ消去し、各消去には命題値の対象が必要である。ここで setIsSet が登場する。結論は階層 (h-集合) における道であり、したがって対象は命題なので、消去は正当である。截断が何を与え、何を与えないかは率直に述べるべきである。証人 s、u、v は要素として現れるので数学はそれを使えるが、前提が主張するのはそれらの単なる存在にすぎない。一意性も、選ばれた代表もない。

out (pair a b) ρ q γ = rec₁ (setIsSet _ _) (λ { (s , s∈ , hs) →
  rec₁ (setIsSet _ _) (λ { (u , u∈ , hu) →
    rec₁ (setIsSet _ _) (λ { (v , v∈ , p , ha , hb) →
      subst ⟨_⟩ (prAtL-adequate (suc (suc (suc q))) (suc zero) zero (v ∷ u ∷ s ∷ γ)) p
      ∙ cong₂ pr (out a (lift3 ρ) (suc zero) (v ∷ u ∷ s ∷ γ) ha)

三つの証人が手に入れば、最も内側の論理式は対の読み出し自身の妥当性によって展開される。p を prAtL-adequate に沿って輸送すると、対の主張は等式 (lookup q γ) .fst ≡ pr (u .fst) (v .fst) になる。続く二つの帰納的な前提が、スロット 0 と 1 での成分の射影、すなわち u .fst ≡ value a と v .fst ≡ value b を与え、pr の下での合同が右辺を pr (value a) (value b) へ書き換える。これはまさにその対の表現の値である。内側の証明は、輸送ひとつと合同ひとつからなる。

                 (out b (lift3 ρ) zero (v ∷ u ∷ s ∷ γ) hb) }) hu }) hs })

into : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : Vec S m)
      → (lookup q γ) .fst ≡ value e (λ i → (lookup (ρ i) γ) .fst) → ⟨ γ ⊨ read e ρ q ⟩
into (slot i) ρ q γ h = h
into (literal a) ρ q γ h = h

逆方向の into は、裸の等式から充足の判断の要素を構成する。スロットとリテラルは直接であり、数項の場合は numeralL-fst の対称と合成して、先の相容性の向きを逆にする。対の場合には三つの截断の層すべてを一度に供給しなければならないが、ここでは截断から何かを取り出すのではなく、証人をその場で構成する。内部の要素 u と v は再索引付けされた割り当てでの element a と element b として選ばれ、Container と container が調整済みの道 e を用いて、両方を収める構成可能な集合 s を、すべての所属の証明書とともに作る。これは L の推移性の独立した使用であり、上で消去を正当化した命題値の確認とは別物である。あちらは截断を消費し、こちらは具体的な要素を作り出す。

into (numeral k) ρ q γ h = h ∙ sym (numeralL-fst k)
into {n} {m} (pair a b) ρ q γ h = ∣ s , c .snd .fst , ∣ u , c .snd .snd .fst ,
  ∣ v , c .snd .snd .snd ,
    subst ⟨_⟩ (sym (prAtL-adequate (suc (suc (suc q))) (suc zero) zero δ)) e
    , into a (lift3 ρ) (suc zero) δ (element-fst a η)

拡張された割り当て δ は v ∷ u ∷ s ∷ γ であり、その配置がこの構成のすべての簿記である。

スロット項目役割
0vb の内部要素
1ua の内部要素
2s中間集合、q の項目の要素
i + 3古いスロット i元の割り当て、そのまま
三つの新しいスロットが元の割り当てに先立ち、元のスロットは順に後ろへ移る

対の論理式は s ∈ q、u ∈ s、v ∈ s、そして q ≡ pr u v を主張する。u がスロット 1 に、v がスロット 0 にあるので、lift3 によって、スロット 1 での read a とスロット 0 での read b はちょうど古いスロットを参照する。各部分証明は into 自身がずらしたスロットで組み立て、読まれる成分の射影の経路 element-fst を与えられ、最後に三つの入れ子の截断された存在は、層ごとにひとつの明示的な ∣_∣₁ で閉じられる。

    , into b (lift3 ρ) zero δ (element-fst b η) ∣₁ ∣₁ ∣₁
  where
  η : Fin n → S
  η i = lookup (ρ i) γ
  u v : S

残りの局所的な定義は、この構成の算術を記録する。η は古い割り当てを再索引付けされたスロットに制限したものであり、u と v はそのもとでの二つの部分表現の明示的な内部的な要素である。これらは直接選ばれるのであって、截断から取り出されるのではない。経路 e は、スロット q の項目が周囲の対 pr (u .fst) (v .fst) に等しいと述べる。その方向が重要である。前提 h は項目が対全体の指す値に等しいと言い、成分の射影の合同 element-fst の対称と合成することで、コンテナの構成が期待する対象がちょうど得られる。

  u = element a η
  v = element b η
  e : (lookup q γ) .fst ≡ pr (u .fst) (v .fst)
  e = h ∙ sym (cong₂ pr (element-fst a η) (element-fst b η))
  c : Container (lookup q γ) u v

コンテナは経路 e から作られ、その最初の成分がまさに求める構成可能な集合 s である。これは二つの Kuratowski 成分のどちらにも到達する共通の中間体であり、s はスロット q の項目の要素であり、u と v は s の要素である。v、u、s の順に γ の先頭へ付け加えると、元よりアリティが三だけ大きい拡張された割り当て δ が得られる。以後、内向きの構成に要る材料はどれも、遊離した要素ではなく δ の項目になる。

  c = container (lookup q γ) u v e
  s : S
  s = c .fst
  δ : Vec S (suc (suc (suc m)))
  δ = v ∷ u ∷ s ∷ γ

二つの方向が、述べられた形に組み上がる。adequate は、γ での充足の判断が、真理値として、「スロット q の項目の射影」と「周囲の指示値」との、梱包された等式に等しいと述べる。⇔toPath が out と into の組の含意をこの経路に変える。最初の応用として、member e C は表現 e の値が項 C の指示に属すると述べる。C の解釈の要素について有界に量化し、その要素で拡張した割り当てのもとで、表現を先頭スロットへずらした読み出しを要求する。

adequate : ∀ {n m} (e : Expr n) (ρ : Fin n → Fin m) (q : Fin m) (γ : Vec S m)
          → (γ ⊨ read e ρ q) ≡ PairIs ((lookup q γ) .fst) (value e (λ i → (lookup (ρ i) γ) .fst))
adequate e ρ q γ = ⇔toPath (out e ρ q γ) (into e ρ q γ)

member : ∀ {n} → Expr n → Term S n → Formula S n
member e C = ∃̇∈ C (read e suc zero)

member の外向きの読みは、截断された有界存在を消去し、要素 x、その所属の証明 h、そして x で拡張した割り当てが表現の読みを満たす証明 p を受け取る。妥当性を外向きに p に適用すると等式 x .fst ≡ value e ... が得られ、その等式に沿って h を輸送すれば、x .fst の所属が表現の値の所属へ移る。対象は所属命題 value e ... ∈ (⟦ C ⟧ γ) .fst であり、その第二成分が rec₁ に必要な命題性の証明を与える。

member-out : ∀ {n} (e : Expr n) (C : Term S n) (γ : Vec S n)
            → ⟨ γ ⊨ member e C ⟩ → ⟨ value e (λ i → (lookup i γ) .fst) ∈ (⟦ C ⟧ γ) .fst ⟩
member-out e C γ = rec₁ ((value e (λ i → (lookup i γ) .fst) ∈ (⟦ C ⟧ γ) .fst) .snd)
  (λ { (x , h , p) → subst (λ v → ⟨ v ∈ (⟦ C ⟧ γ) .fst ⟩) (out e suc zero (x ∷ γ) p) h })

member-in : ∀ {n} (e : Expr n) (C : Term S n) (γ : Vec S n)

内向きの読みはその要素を示さねばならないが、表現 e の値そのものを模型の要素にすれば証人になる。前提によりそれは (⟦ C ⟧ γ) .fst の要素であり、項の解釈は構成可能なので、L の推移性がその値の構成可能性の証明書を与える。ここで isL-trans がしているのはまさにそれである。截断の消去は行われない。証明書と周囲の値を組にした明示的な模型要素 x が、有界存在の証人になる。拡張された割り当ての先頭は定義によりその値へ射影されるので、帰納的な into は経路 refl を受け取る。

           → ⟨ value e (λ i → (lookup i γ) .fst) ∈ (⟦ C ⟧ γ) .fst ⟩ → ⟨ γ ⊨ member e C ⟩
member-in e C γ h = ∣ x , h , into e suc zero (x ∷ γ) refl ∣₁
  where
  x : S
  x = value e (λ i → (lookup i γ) .fst) , isL-trans h ((⟦ C ⟧ γ) .snd)

最初の特殊化は、一般的な読み出しをタグの認識器に変える。tagAtL s k x は、スロット s で「数項 k とスロット x の対」という表現を読むもので、したがって、スロット s の項目が # k とスロット x の項目の順序対であると主張する有界論理式である。再帰に現れる符号は、ペイロードと対になった数値のタグを帯びており、まさにこの形をしている。

tagAtL : ∀ {n} → Fin n → ℕ → Fin n → Formula S n
tagAtL s k x = PairExpression.read
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s

tagAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (x : Fin n) (γ : Vec S n)
  → (γ ⊨ tagAtL s k x)

その妥当性の補題は新しい証明を要らない。この表現について恒等リラベルで一般的な妥当性を実体化すると、その計算結果はすでに、充足の判断が、射影された項目と pr (# k) されたペイロードの PairIs と同一視されるというものである。これが本節全体の型である。表現を選び、PairExpression.adequate を引用すれば、節の意味が読み取れる。

  ≡ PairIs ((lookup s γ) .fst) (pr (# k) ((lookup x γ) .fst))
tagAtL-adequate s k x γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot x)) id s γ

tagPairAtL : ∀ {n} → Fin n → ℕ → Fin n → Fin n → Formula S n
tagPairAtL s k a b = PairExpression.read

第二の特殊化は、それ自身が対であるようなペイロードを扱い、二層の対は表現の中に入れ子になっている。tagPairAtL s k a b は「数項 k と、スロット a と b の対との対」という表現を読むので、pr (# k) (pr (entry a) (entry b)) の形の項目を認識する。タグが二成分のペイロードの上に載ったものである。

  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s

tagPairAtL-adequate : ∀ {n} (s : Fin n) (k : ℕ) (a b : Fin n) (γ : Vec S n)
  → (γ ⊨ tagPairAtL s k a b)
  ≡ PairIs ((lookup s γ) .fst)

妥当性の補題はここでも一般的なものから直接計算され、三つの成分すべてを、タグの数項と、射影後の二つのペイロードの項目とを取り戻す。入れ子は完全に表現の読み出しの内部で処理される。この層の節から見えるのは、表現の形だけである。

      (pr (# k) (pr ((lookup a γ) .fst) ((lookup b γ) .fst)))
tagPairAtL-adequate s k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.numeral k)
    (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b))) id s γ

外延によって集合を定める

前節の構造的な読みは Kuratowski 対の層を通して値を認識したが、多くの再帰の節が語りたいのは、ある集合の要素が何であるかということである。両者は同じ種類の主張、すなわち模型の中の一階の論理式が、周囲の階層へ読み戻されたときにスロットの値をちょうど指し示す、という形をしている。本節ではその外延的な形を作る。

extAt y φ は、スロット y の集合について、その要素が一変数の条件 φ を満たす対象とちょうど一致することを述べる。外側の構造は、普通の連言で結ばれた二つの非有界な全称量化である。一方は集合への所属から φ への含意、もう一方は逆向きの含意である。extAt 自体は新たな命題の切り捨てを導入しないが、パラメータ φ は任意の論理式であり、その内部に量化子や切り捨てられた存在を含むことはある。外側の証拠が素の連言であるため、二つの読みは連言の射影そのもの、導入もそれらの順序対そのものになる。これは記述としてちょうどよい強さである。この論理式は候補となる集合を特徴づけるだけで、そのような集合が存在するかどうかには何も言わない。存在は、後で値を供給する構成の仕事である。

この定義は候補のための新しい変数を一つ束縛し、全体として二つの非有界な全称量化の連言である。すなわち、スロット y の集合のすべての要素が φ を満たすこと、そして φ を満たすすべてのものが要素であること。外側の結合子は普通の連言であり、extAt はどちらの含意も切り捨てで包まないが、条件 φ はそのまま渡され、量化子や切り捨てられた存在を内部に含む任意の論理式であって構わない。extAt 自体が確定するのは外側の形だけである。量化子の下にある二つの含意の対であり、各側は模型の要素とその充足の証明の上の関数である。これこそ、この論理式が記述として機能する理由である。値を束縛するだけで、値の存在を主張することはないのである。

extAt : ∀ {n} → Fin n → Formula S (suc n) → Formula S n
extAt y φ = ∀̇ ((var zero ∈̇ var (suc y)) ⇒̇ φ)
         ∧̇ ∀̇ (φ ⇒̇ (var zero ∈̇ var (suc y)))

module _ {n : ℕ} (y : Fin n) (φ : Formula S (suc n)) (γ : Vec S n) where

extAt-out : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)

二つの読みは、外側の連言の二つの射影である。extAt y φ の要素から出発して、extAt-out は第一の成分を取る。これはすべての模型の要素 z に対して、z .fst がスロット y の集合に属することから、拡張された環境での φ の充足への含意を割り当てる。extAt-in は第二の成分を取り、同じ含意を逆向きに与える。どちらの読みも切り捨ての除去も証人の選択も経路に沿う輸送も行わない。φ の内部に何があっても、この外側の層では証拠は順序対であり、各読みは文字どおりその射影である。

          → ⟨ z .fst ∈ (lookup y γ) .fst ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩
extAt-out h = h .fst

extAt-in : ⟨ γ ⊨ extAt y φ ⟩ → (z : S)
         → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ z .fst ∈ (lookup y γ) .fst ⟩
extAt-in h = h .snd

導入は射影を逆向きに走らせるもので、二つの含意をそれぞれ関数として与えたときの順序対である。そこで extAt-in-both が成り立つ。条件の両方向をともに確立できる節は、二つの関数を対にするだけでこの論理式を充足し、外側の層ではそれ以上の仕事は要らない。量化子や切り捨てに伴う仕事はすべて φ の内部で起き、そこで片づけられる。この主張はそのまま読む価値がある。二つの関数から充足の判断の要素を作るのであって、φ を満たす要素をもつ集合の存在については何も主張しない。そのような集合が実際に供給されるかどうかは、値が構成される側で決まる事柄であり、ここではない。

extAt-in-both : ((z : S) → ⟨ z .fst ∈ (lookup y γ) .fst ⟩ → ⟨ (z ∷ γ) ⊨ φ ⟩)
              → ((z : S) → ⟨ (z ∷ γ) ⊨ φ ⟩ → ⟨ z .fst ∈ (lookup y γ) .fst ⟩)
              → ⟨ γ ⊨ extAt y φ ⟩
extAt-in-both f g = f , g

二層の鍵を読む

充足関係の再帰における鍵は、二層の入れ子になった対から組み上げられた集合である。アリティと符号との対であり、符号そのものはタグの数項とペイロードとの対である。したがって有界な論理式で鍵を認識するとは、この二層の対を検査することであるが、構造的な読みは任意の入れ子の式をすでに扱えるので、その任に十分に応える。そこで以下の各論理式は適切な式に読みを適用したものであり、各妥当性補題は PairExpression.adequate の対応する特殊化である。アリティが数項に固定されず変数スロットとして残されているのは意図的なことである。異なるアリティの部分論理式を生む構成子の節は、アリティの値そのものについて語る必要があるからである。

arityTagPairAtL c ar k a b は、スロット c の集合が順序対であることを述べる。第一成分はスロット ar の集合であり、第二成分はさらに、# k という数項とスロット a、b の集合の対との対である。定義式は pair (slot ar) (pair (numeral k) (pair (slot a) (slot b))) という形で、恒等リラベルの下で c において読まれる。これはペイロードが二スロットの符号である鍵の形状である。

arityTagPairAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Fin n → Formula S n
arityTagPairAtL c ar k a b = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c

妥当性の主張は、この論理式の真理値を命題 PairIs ((lookup c γ) .fst) (...)、すなわち周囲の階層におけるパスと同一視する。これは c の集合が各スロットの射影から組み上げられた入れ子の Kuratowski 対に等しいと述べるものである。各成分は右辺から読み取れる。タグの数項 # k は固定されており、ar、a、b はそれぞれ参照された値を寄与する。この主張は一方向の含意ではなく真理値の間のパスなので、後の証明ではどちらの方向にも書き換えに使える。

arityTagPairAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a b : Fin n) (γ : Vec S n)
  → (γ ⊨ arityTagPairAtL c ar k a b)
  ≡ PairIs ((lookup c γ) .fst)
      (pr ((lookup ar γ) .fst)
        (pr (# k) (pr ((lookup a γ) .fst) ((lookup b γ) .fst))))

証明は PairExpression.adequate を同じ式、同じリラベル、同じスロットに適用する一行の特殊化である。有界な証人、截断された存在の除去と導入、prAtL の妥当性に沿う輸送はすべて構造定理で一度に片づけられているため、ここに新しい意味論的議論は現れない。対ペイロードの場合が整うと、一つのペイロードを持つ変種 arityTagAtL c ar k a が同じ仕方で定義される。違いは最も内側の式が二つのスロットの対ではなく単一のスロット a である点だけである。

arityTagPairAtL-adequate c ar k a b γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k)
      (PairExpression.pair (PairExpression.slot a) (PairExpression.slot b)))) id c γ

arityTagAtL : ∀ {n} → Fin n → Fin n → ℕ → Fin n → Formula S n

本体は恒等リラベルの下で c において構造的な読みを適用するものであり、妥当性の主張もやはり PairIs のパスの形をとる。すなわち c の集合は、アリティの値と「# k と a の値の対」との対に等しいということである。符号のペイロードが二つではなく単一のスロットである場合、たとえば変数の番号一つや部分論理式のスロット一つである場合に、必要なのはまさにこの形である。

arityTagAtL c ar k a = PairExpression.read
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c

arityTagAtL-adequate : ∀ {n} (c ar : Fin n) (k : ℕ) (a : Fin n) (γ : Vec S n)
  → (γ ⊨ arityTagAtL c ar k a)

妥当性の証明はここでも、同じ式とスロットに対して PairExpression.adequate を引用するもので、対の場合と同じ作法である。したがって二つのアリティ付きタグ論理式と二つの妥当性補題は、唯一の構造定理の上に立つ。読みを汎用的に作ったことの見返りがこれである。復元されたアリティの値をその後どう扱うかは、充足関係の再帰の節に属する事柄であり、それらの節は L.Coding.SatisfactionClauses で述べられる。本章が供給するのは、それらの節が読む形状である。

  ≡ PairIs ((lookup c γ) .fst)
      (pr ((lookup ar γ) .fst) (pr (# k) ((lookup a γ) .fst)))
arityTagAtL-adequate c ar k a γ = PairExpression.adequate
  (PairExpression.pair (PairExpression.slot ar)
    (PairExpression.pair (PairExpression.numeral k) (PairExpression.slot a))) id c γ

表から部分符号を引く

充足関係表のエントリは、アリティと符号からなる鍵に対して、その論理式を充足する環境の集合を記録する。したがって部分論理式の値を読むとは、その鍵を対象言語の内部で作ること、すなわちアリティと部分符号の対を作り、候補となる集合との等しさを主張することを意味する。部分論理式自身のアリティでは表の項目を全称量化し、鍵の等式を含意の前件として一致する項目を選ぶ。部分論理式が変数を束縛するときには、同じ参照が次のアリティで行われ、そのアリティは次節の後者の論理式が内部で証人となる。

節の共通形

再帰の一つの節は、符号、そのアリティ、ペイロードの成分、そして符号の位置に記録された値を束縛し、符号のタグ付きの形を述べ、記録された値の間で構成子ごとの条件を一つ述べる。節を読み戻すことは、本章で確立した妥当性の補題に沿った書き換えの連鎖であり、節を組み立てることは、その書き換えを逆向きに走らせることである。

正の結合子

論理積と論理和にとって、構成子ごとの条件は小さなものである。符号の位置の値は二つの部分値の逐点連言、それぞれ逐点選言であり、いずれも同じアリティの表から読み出される。この条件のほかに節が要るものは、上の参照の仕組みだけである。

周囲の環境集合

envSetAt は、外延による特徴づけによって、あるスロットにあるアリティの、別のスロットの台の上での環境の集合を記述する。これは集合を特徴づけるのであって、構成するのではない。

この定義は、外延による特徴づけをスロット E に適用し、条件として環境の述語 envOverAt をとる。この述語は定義域と値域に対して一つの候補環境を分類するものなので、extAt が新たに束縛する変数 (拡張された環境の位置 0) が候補の役割を果たす。定義域と値域の引数が suc ar と suc B と現れるのは、条件が拡張された環境で評価されるからであり、論理式自身が束縛するスロットより一つアリティが上である。射影 extAt-out と extAt-in により、envSetAt E ar B の証明はちょうど二つの含意を与えるもの、すなわち E の集合が、ar に記録されたアリティの上で B の台が受け入れる候補環境をちょうど含む、と言うものになる。この論理式は集合を記述するだけで、その構成は充足関係表が作られる場所で行われる。

envSetAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
envSetAt E ar B = extAt E (envOverAt zero (suc ar) (suc B))

含意と偽

論理の節のうち、含意と偽は、その値の形において正の結合子と一線を画する。偽には部分符号がなく、共通の外延の枠組みの中で条件が偽なので、その値は空である。ただし枠組みが束縛する周囲の環境集合は使う。含意は、符号のアリティにおけるすべての環境の集合の上で解釈されるため、その節はその周囲の集合を名指し、外延的に制約しなければならない。前節の環境の集合が存在するのはまさにこのためである。含意は「補集合と後件の結び」ではなく含意として述べられるとき、hProp 上の関数空間の含意と一致する。含意を直接用いれば、排中律を呼び出さずに構成的な意味論と一致する。

次のアリティ

sucAtL は、スロット j の集合がスロット i の集合の sucV であることを述べる内部論理式である。その妥当性補題は任意の集合に適用でき、数項や順序数であることを仮定しない。

部分論理式が一つ高いアリティにある節は、現在のアリティの後続であると制約されたアリティで表を参照する。階層側の論理式 sucAt はこの集合の等式を表し、定数を含まない。持ち上げには liftFo が要求する BoundedFo InL の引数が必要である。これとは別の定理 Δ₀-sucAt は、後で transferFo に渡され、有界絶対性を正当化する。

定義は sucAtL i j = liftFo (sucAt i j) _ である。sucAt は定数を含まないため、その BoundedFo InL の引数には非自明な定数の構成可能性の証人はない。妥当性の証明では、transferFo はこの引数と、階層側の Δ₀ 証明書である Δ₀-sucAt i j とを別々に受け取る。得られるパスは充足を PairIs ((lookup j γ) .fst) (sucV ((lookup i γ) .fst))、すなわちスロット j の集合がスロット i の集合の後続集合であるという命題と同一視する。

sucAtL : ∀ {n} → Fin n → Fin n → Formula S n
sucAtL i j = liftFo (sucAt i j) _

sucAtL-adequate : ∀ {n} (i j : Fin n) (γ : Vec S n)
  → (γ ⊨ sucAtL i j) ≡ PairIs ((lookup j γ) .fst) (sucV ((lookup i γ) .fst))
sucAtL-adequate i j γ =

証明は三つのパスを連結する。まず転送の補題が有界性の証明書を使い、持ち上げられた論理式の L での充足を、射影された割り当て map (λ p → p .fst) γ での sucAt i j の周囲の充足と等しいとする。転送は確立された推移的モデルの設定に依拠する。次に階層側の妥当性定理 sucAt-adequate が、その充足を解釈された値の間の等式へ書き換える。最後に lookup-fst が射影された割り当てでの二度の参照を γ での参照の射影へ移し、合同が sucV を内側へ移し、cong₂ が等式を PairIs の下で組み立て直す。得られるのは述べられた同一視である。

    transferFo (sucAt i j) _ (Δ₀-sucAt i j) γ
  ∙ sucAt-adequate i j (map (λ p → p .fst) γ)
  ∙ cong₂ PairIs (lookup-fst j γ) (cong sucV (lookup-fst i γ))

環境を拡張する

consAtL は新しい先頭値による環境の拡張を記述し、その妥当性補題が得られる符号化環境を正確に同一視する。

量化された本体は、現在の環境の先頭に値を一つ加えた環境で評価される。階層側の論理式 consAt はこの操作をすでに特徴づけており、consAtL は同じ特徴づけを構成可能模型の内部で表す。持ち上げには、符号化された拡張を組み立てる単集合、対、タグ、鍵の移動の各関係について有界性の証明が必要である。これらの関係は定数の数項を導入しない。指定されたタグは空集合であり、新しい先頭値はスロット m から読まれる。直後にここで定義される独立の補題 numL は、数項を実際に名指す別の有界論理式のために、周囲の数項の構成可能性を記録する。

numL k はここで定義され、周囲の数項 # k が構成可能であることを示す。内部数項 numeralL k はその射影の構成可能性をすでに備え、numeralL-fst k がその射影を # k と同一視する。このパスに沿って証明を輸送すると ⟨ isL (# k) ⟩ が得られる。続く非公開の定義は、空のタグを認識する論理式について BoundedFo InL のデータを与える。これは有界な形と、現れる定数の構成可能性の証人を組み合わせたものである。特に sgl0At k はスロット k の集合を {∅} と特徴づける。空の要素をもち、すべての要素が空であるという条件である。bddSgl0 はこの組み合わせたデータを与えるもので、独立な Δ₀ 定理ではない。

numL : (k : ℕ) → InL (# k)
numL k = subst (λ w → ⟨ isL w ⟩) (numeralL-fst k) (numeralL k .snd)

private
  bddSgl0 : ∀ {n} (k : Fin n) → BoundedFo InL (sgl0At k)
  bddSgl0 k = (_ , (_ , _)) , (_ , (_ , _))

pair0At k j は、スロット k の集合を非順序対 {∅, W} と特徴づける。ここで W は元の割り当てのスロット j の値であり、内側の量化子に入ると同じ値を suc j が指す。二つのスロットの値からなる Kuratowski 対ではない。tag0At s x は sgl0At と pair0At を組み合わせる。指定された二要素が {∅} と {∅, W} なので、スロット s の集合は Kuratowski 対 pr ∅ W である。bddPair0 と bddTag0 は、これらの記述の BoundedFo InL データを与え、必要な定数の構成可能性の証人も含む。

  bddPair0 : ∀ {n} (k j : Fin n) → BoundedFo InL (pair0At k j)
  bddPair0 k j = (_ , (_ , _)) , ((_ , _) , (_ , ((_ , _) , (_ , _))))

  bddTag0 : ∀ {n} (s x : Fin n) → BoundedFo InL (tag0At s x)
  bddTag0 {n} s x =
      (_ , bddSgl0 {suc n} zero)

bddTag0 の残りの部分は、空集合タグ自体に使う単集合の証明書と、外側と内側の対の層のための証明書とを対にする。その後の bddShift は shiftPairAt p' p を証明する。すなわち p' の項目は、p の項目の数項の鍵をその後者に置き換え、対になった値はそのままにして得られるものとして認識される。ここで証明書を単一のプレースホルダとして書けるのは、論理式の有界な部分論理式が、すでに扱った葉と有界量化子と同じだからである。

    , ( (_ , bddPair0 {suc n} zero (suc x))
      , (_ , (bddSgl0 {suc n} zero , bddPair0 {suc n} zero (suc x))) )

  bddShift : ∀ {n} (p' p : Fin n) → BoundedFo InL (shiftPairAt p' p)
  bddShift p' p = _

  bddCons : ∀ {n} (e' m e : Fin n) → BoundedFo InL (consAt e' m e)

bddCons は拡張の論理式が必要とするすべてを組み立てる。三つの連言を読むと、拡張されたグラフは m の値の上に載った空集合タグである項目、すなわち新しい先頭の項目を保持し、ずらしたスロットでの bddTag0 が証明する。旧グラフの各項目は鍵を後者へずらして現れ、二つアリティが上の bddShift が証明する。残りの連言は、拡張の外へ読み出す所属の方向について同じ二つの証明書を繰り返す。各連言の証明書はその量化子が作る深さに置かれるため、注釈のアリティが suc (suc n) まで増えるのである。

  bddCons {n} e' m e =
      (_ , bddTag0 {suc n} zero (suc m))
    , ( (_ , (_ , bddShift {suc (suc n)} zero (suc zero)))
      , (_ , ( bddTag0 {suc n} zero (suc m)
             , (_ , bddShift {suc (suc n)} (suc zero) zero) )) )

有界性の証明書がそろうと、consAtL e' m e は階層側の論理式 consAt e' m e を liftFo で持ち上げたものであり、その証明書として bddCons が与えられる。この妥当性の主張には、後者の場合にはなかった条件が付く。族 g : Fin k → V ℓ と、スロット e に置かれた集合が符号化環境 env g であるという証明 hE を仮定するのである。その仮定の下で、consAtL e' m e の充足は、真理値として PairIs ((lookup e' γ) .fst) (env (cons ((lookup m γ) .fst) g)) と同一視される。すなわち e' の集合は、m の値を g の先頭に付け加えて得られる符号化環境にほかならない。この論理式は、すでに符号化された環境に対して候補を分類するものであって、環境を構成するものではない。旧環境についての仮定こそ、この分類を意味の定まったものにする前提である。

consAtL : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
consAtL e' m e = liftFo (consAt e' m e) (bddCons e' m e)

consAtL-adequate : ∀ {n} (e' m e : Fin n) (γ : Vec S n)
  {k : ℕ} (g : Fin k → V ℓ)
  → (lookup e γ) .fst ≡ env g

証明は転送の補題から始まり、その入力は一度にすべて与えられる。論理式 consAt e' m e、その有界性の証明書 bddCons、そして階層側で記録された Δ₀ の証明書 Δ₀-consAt である。このステップは有界絶対性の実際の働きであり、確立された推移的モデルの設定に依存する。L が推移的であり、論理式が名指す定数がすべて構成可能であることから、持ち上げられた論理式の台での充足は、射影された割り当て map (λ p → p .fst) γ での元の論理式の充足へと移る。そこでは周囲の事実を直接述べることができる。

  → (γ ⊨ consAtL e' m e)
  ≡ PairIs ((lookup e' γ) .fst) (env (cons ((lookup m γ) .fst) g))
consAtL-adequate e' m e γ g hE =
    transferFo (consAt e' m e) (bddCons e' m e) (Δ₀-consAt e' m e) γ
  ∙ consAt-adequate e' m e (map (λ p → p .fst) γ) g

階層側の妥当性定理 consAt-adequate は次に、周囲の充足を、新しいスロットと拡張された符号化環境との同一視へ書き換える。仮定は射影された形で必要なので、入り口で lookup-fst e γ が hE と連結される。すなわち e の項目の射影は env g に等しいのである。続いて合同が残る二度の参照を移す。e' の値は lookup-fst で、m の値は関数 λ w → env (cons w g) の下で cong で処理される。経路の連鎖は約束された PairIs の同一視でちょうど終わる。これで本章固有の数学は閉じる。構文の形、アリティ、環境、そしてその拡張を認識するのに必要な内部論理式は、すべてここに揃った。

      (lookup-fst e γ ∙ hE)
  ∙ cong₂ PairIs (lookup-fst e' γ)
      (cong (λ w → env (cons w g)) (lookup-fst m γ))

非有界量化子

二つの非有界量化子の節は、共通の有界な枠 extB を使う。この枠は周囲の環境集合 F と拡張のデータを束縛してから、量化子固有の本体を適用する。quBody q では、引数 q は台の集合 w を走る外側の量化子であり、存在の場合は有界存在、全称の場合は有界全称である。拡張された環境が本体に記録された値に現れることを述べる内側の論理式 ∃̇∈ ya (consAtL ...) は、どちらの場合にも変わらない。したがって全称の場合に変わるのは外側の量化子だけで、最も内側の連言を含意へ置き換えるのではない。

項の評価と二つの原子論理式

項は変数か定数である。したがって符号化された項を評価する節には二つの場合がある。変数の値は環境がその鍵に記録するものであり、定数の値はその定数そのものであり、どの環境でも同じである。二つの原子論理式はその後、両方の項の符号を評価して、得られた値を模型の中で比較する。一方は所属を、他方は等式を主張する。そのペイロードは項の符号の対であり、充足関係表にはそこにエントリがないため、この節は枠組みに任せずに自分で参照を作るのである。

有界量化子

有界量化子のペイロードは、項の符号と論理式の符号の対である。境界は二つの場合をもつ評価の読みによって環境の中で評価され、本体の値はひとつアリティ上で読まれ、付け加えられる値は台と評価された境界の両方の要素に限られる。台と境界の両方を渡ることは冗長ではない。参照意味論は台の上で量化し、境界への所属で防ぐ。境界は台の外に要素をもつことも十分にあり得るので、境界だけを渡る量化は、表がもたないエントリを要求することになる。

まとめ

本章は、符号化された充足関係の節が L の内部で複合的な値を認識するための一階論理式を組み立てた。それを支えるのは三種類の主張である。表現の読みの構造的な妥当性は、スロット、リテラル、数項、Kuratowski 対についての論理式の充足を、両方向で、射影された項目と指示された周囲の値の等しさと同一視する。対の場合は構成可能な中間集合を通って行われる。外延的な特徴づけ extAt は二つの全称含意の普通の連言であり、その読みと導入は射影と対である。そして内部の後者の論理式と環境拡張の論理式は、推移的モデルの上の有界絶対性によって持ち上げられ、その妥当性の経路は転送された充足、階層側の定理、射影の下での参照の相容性から連結される。符号化充足関係の再帰を成す節の形状は、この上に立つ。