論理式符号のアルファベット

この章を読むか、読書案内と依存マップで別のルートを選べます。

構成可能集合 W についての主張は、しばしば W の要素に言及します。たとえば W に属するある x が性質を満たすと言うには、論理式は x をパラメータとして伴わなければなりません。集合論の内部では、このようなパラメータは一階言語の定数記号として現れます。しかし周囲の構文符号化は、定数が任意の集合の要素への抽象的な参照ではなく、階層 V ℓ の集合であることを要求します。そこで橋渡しが必要になります。アルファベットが W の要素を索引づけ、各インデックスに集合としての指示対象を与える埋め込みをそろえた言語です。

この章では、固定された W に対しその橋を構築します。アルファベットは W の台集合の要素へのインデックスの型であり、埋め込みは各インデックスをそれが指す集合へ送り、その集合が W に属することの証拠を添えます。埋め込みに沿って各定数を書き換えれば、アルファベット上のすべての項と論理式は集合を定数とする構文になり、既存の V 値の符号化が適用できて、項の符号 ct と論理式の符号 cd が得られます。符号化はアリティを調べないので、アリティの相等の経路に沿って論理式を輸送しても符号は変わらず、これが cd-subst の記録する事実です。

この章のすべては、ただ一度だけ固定され章全体を通じて用いられる単一の型論的宇宙レベル ℓ の上で行われます。このレベルの集合の階層 V ℓ が最終的な符号化の目標であり、一階言語はパラメータが置かれる舞台です。方針は一様です。構成可能集合 W が与えられれば、その要素を定数記号として読み、抽象的なインデックスで名前を付け、各名前を V ℓ の中でそれが指す集合へ輸送します。この方針はどの W を選ぶかに依存しないので、任意の W に対して通用します。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude

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

open import FOL.ZFStructure using ( module hPropStructure )

対象言語の構文はアルファベットに対して汎用です。定数の型 K とアリティ n に対する論理式の型 Formula K n は、定数が何であるかを決して調べず、それらを論理構造へ配置するだけです。したがって、アルファベット上の任意の関数は構文の書き換えへ拡張されます。各定数をその関数を通して写せば、すべての出現が書き換えられ、論理結合子・量化子・変数はそのまま保たれます。ここで使う関数は要素のインデックスを V ℓ へ埋め込む写像であり、書き換え後の論理式は集合を定数とするので、階層上の集合値の構文符号化が要求する入力の形式にちょうど合います。残るのは、これらの定数が実際に W の要素になるようにアルファベットと埋め込みを選ぶことです。

open import FOL.Syntax using ( Formula; Term )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapTm )
open import V.Coding {ℓ} using ( module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ )

open import Cubical.Foundations.Prelude using ( J; substRefl )

二つの区別が構成を組織します。第一に、階層の集合の要素は ⟪ a ⟫ の抽象的なインデックス q によって提示され、埋め込み ⟪ a ⟫↪ はそのインデックスを指された集合へ送ります。インデックスは名前であり、値 ⟪ a ⟫↪ q は V ℓ における指示対象であり、この二つの役割は終始区別されます。第二に、W は任意の集合ではなく、構成可能な構造の台 S の要素なので、階層における台集合 fst W と構成可能性の証拠を伴います。まさにこのおかげで、その要素を構成可能集合についての言語のパラメータとして読むことができます。アルファベットは ⟪ fst W ⟫ そのものにとられ、次の節でこれらの部品が符号 ct と cd へと組み上げられます。

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties using
  ( ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_ )

open hPropStructure 𝒮ʟ using ( S )

定数を埋め込んで構文を符号化する

この節では、構成可能集合 W を台 S の要素として取り、W 上の構文をどのように集合へ符号化するかを考えます。構成は三段階の合成です。まず利用可能な定数記号の型 Ab を取り出し、次に各記号を階層 V ℓ へ埋め込み、それが実際に W に属することの証拠を添え、最後に書き換え後の項と論理式に集合値の符号化を施します。最後の補題は、論理式がアリティで索引づけられることに由来する簿記上の問題を片づけます。

要素 W : S は、階層のある集合を構造のデータとともに束ねたものです。fst W がその台集合になります。したがって Ab は ⟪ fst W ⟫、つまりその集合の要素へのインデックスの型であり、ι は埋め込み ⟪ fst W ⟫↪ で、各インデックスを V ℓ 内の指された要素へ送ります。つまり Ab の要素こそが利用可能な定数記号であり、ι は集合としてのその指示対象を計算します。

module Alphabet (W : S) where
  Ab : Type ℓ
  Ab = ⟪ fst W ⟫

  ι : Ab → V ℓ
  ι = ⟪ fst W ⟫↪

所属の証拠 ι∈ は、各定数記号 q に対して集合 ι q が実際に fst W の要素であることを述べます。これは、所属関係と分類つきの所属関係 ∈ₛ との間のライブラリの同値からそのまま読み取れます。アルファベットが整うと、cd と ct はほとんど自動的に決まります。mapFo ι と mapTm ι が各定数 con q を con (ι q) に置き換えて論理式や項を書き換え、階層符号化の括弧 ⌜_⌝ と ⌜_⌝ᵗ がその結果を集合としてまとめるのです。書き換えの後も論理式の論理的な骨格はそのまま保たれるので、既存の符号化をそのまま再利用できます。

  ι∈ : (q : Ab) → ⟨ ι q ∈ fst W ⟩
  ι∈ q = ∈∈ₛ {a = ι q} {b = fst W} .snd (∈ₛ⟪ fst W ⟫↪ q)

  cd : ∀ {n} → Formula Ab n → V ℓ
  cd ψ = VCode.⌜ mapFo ι ψ ⌝

  ct : ∀ {n} → Term Ab n → V ℓ

型 Formula Ab n の論理式はアリティ n を伴い、依存型理論ではこのインデックスが型の一部です。後の証明で n と n' の相等が必要になると、経路 e : n ≡ n' に沿って論理式を輸送します。輸送された論理式は、元の論理式が同じでも、構文の上では別の要素です。補題 cd-subst は、これが符号化には何の影響も与えないことを示します。輸送後の論理式に適用した cd は、元の論理式に適用した cd と等しいのです。証明は e に対する J によるもので、反射的な場合は refl に沿った輸送が恒等写像であり、substRefl がこの簡約を明示するため成立し、残りは cong cd で二つの適用を結びます。

  ct t = VCode.⌜ mapTm ι t ⌝ᵗ

  cd-subst : ∀ {n n'} (e : n ≡ n') (ψ : Formula Ab n) → cd (subst (Formula Ab) e ψ) ≡ cd ψ
  cd-subst {n} e ψ = J (λ n' e' → cd (subst (Formula Ab) e' ψ) ≡ cd ψ)
    (cong cd (substRefl {B = Formula Ab} ψ)) e

まとめ

Alphabet W は構成可能集合 W の要素を一階言語の定数記号とみなし、それぞれを証拠 ι∈ とともに周囲の階層へ埋め込み、ct と cd によって項と論理式の集合としての符号を与えます。符号化がアリティを決して調べないため、cd-subst は、アリティの相等の経路に沿って論理式を輸送してもその符号が変わらないことを保証します。