Bedrock論理式上の再帰による充足関係
この章を読むか、読書案内と依存マップで別のルートを選べます。
読書案内 · 依存マップL の集合 B と論理式を与え、その論理式を充足する B 上の環境の集合を構成します。構成は論理式の上の再帰として進みます。複合の論理式の集合は直接の部分式の集合によって定まり、原子と偽はそれぞれ直接に扱われます。いずれの場合も、集合は分出によって得られます。すなわち、「B 上の長さ n のすべての環境」という集合から、記述の条件を満たすものを残すのです。得られる集合の所属の等式は十の論理式構成子を記述します。
再帰がメタ言語の論理式の上にあることが、すべての段階の形を決めます。Agda は論理式を検査できるので、各段階は部分式で作られた集合を記述の条件の定数として名指せます。対象言語が符号を量化する必要は一度も生じません。したがって各段階は一度の分出であり、原子の場合が短いのも同じ理由からです。メタ言語の項は変数か定数かが目に見えているため、値の読み取りは場合を一つしか持ちません。符号化された節が区別しなければならない二場合と比べてのことです。
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Classical using ( LEM ) module L.Coding.Satisfaction {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
構成は、モデルのレベルの後続での排中律を仮定します。扱うのは集合論の言語の論理式で、相等、所属、三つの二項結合子、偽、有界および非有界の量化子を含みます。
open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; con; var; Formula ; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ ) import FOL.Absoluteness
充足は、累積階層の構成可能部分構造で読み取ります。論理式の絶対性がその制限された読み方を与え、順序対が環境として用いるグラフを符号化します。
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ ) open import V.Coding {ℓ} using ( pr ) open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans ) open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
各論理式について、分出によって符号化環境の集合から充足集合を切り出します。appAt と consAtL は、環境グラフでの参照と一つの値による拡張を記述し、envSet は必要な長さのすべての環境を与えます。
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate ) open import L.Coding.Expressions {ℓ} using ( consAtL; numL ) open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
存在の節は、命題的に切り詰められた証人を与えます。有限添字は自然数へ変換され、階層内部のフォン・ノイマン数項で表されます。
open import Cubical.Data.FinData using ( toℕ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
階層の数項構成は、それらの添字を集合として名指します。構成可能な真理値構造を開くことで、本章を通じた所属と充足の意味が定まります。
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_ )
以下の _⊨_ は、有限環境ベクトルのもとで評価される、制限された構成可能構造の充足関係です。
open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
変数と定数の評価
変数の値はその添字に対応する環境の成分であり、定数は自らの値を指定しています。この二つの事実は対象言語の内部で言われなければなりません。記述の条件そのものが論理式だからです。項の読み tmIs は、値のスロットと環境のスロットについて、環境がその項を値のスロットの値に対応させることを述べます。定数なら、それは値のスロットと定数の間の等式そのものです。変数の場合は存在の主張になります。台のある要素が添字の数項に等しく、適用の節は、その添字と記録された値の対が、環境のスロットに記録された環境のグラフに属することを言います。充足の判断はすべて L の中で読まれます。
private nn : ℕ → S nn k = # k , numL k
内部の数項は、周囲のフォン・ノイマン数項にその構成可能性の証明を対にしたもので、添字は必要な場所でいつでも L の内部で名指せます。
tmIs : ∀ {n m} → Term S n → Fin m → Fin m → Formula S m
読みは、項と、その項の値を収めるスロットと、項を読む環境を収めるスロットを受け取り、その長さの環境の上の論理式を返します。
tmIs (var i) v e = ∃̇ ((var zero ≐ con (nn (toℕ i))) ∧̇ appAt (suc e) zero (suc v))
変数の場合、この節は次のように述べます。台のある要素 x が添字の数項に等しく、その添字と値のスロットの値の対が、環境のスロットに記録された環境のグラフに属する、と。等式は添字の証人を釘付けにするだけで、内容を運ぶのは適用の節です。
tmIs (con c) v e = var v ≐ con c
定数の場合、環境を調べる必要はありません。値のスロットはその定数と同一視されるだけです。
tmIs-var-in : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m) → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩ → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩
妥当性の二つの補題が、論理式とそれが符号化する周囲の所属とを結びます。内向きには、スロット e の環境が、数項 i とスロット v の値の対を含むなら、γ はこの読みを満たします。
tmIs-var-in i γ v e h = ∣ nn (toℕ i) , ( refl , subst ⟨_⟩ (sym (appAt-adequate (suc e) zero (suc v) (nn (toℕ i) ∷ γ))) h ) ∣₁
証人は数項そのものであり、その定義の等式は定義的です。所属は妥当性のパスに沿って逆向きに輸送され、周囲の主張から拡張された環境の上の内部の節へ変わります。
tmIs-var-out : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m) → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩ → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩
外向きには、読みの充足から周囲の所属が得られます。ここで本章の一般原則が初めて現れます。目標が命題か切り詰めである限り、切り詰められた証人は消費できます。以下のどこでもこの原則は破られません。
tmIs-var-out i γ v e = PT.rec (snd (pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ)))
切り詰められた証人は、項目 x と、x が添字の数項であること、そして拡張された環境の上で節が成り立つことの証明の組です。
(λ { (x , (qx , m)) → subst (λ w → ⟨ pr w (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩) qx (subst ⟨_⟩ (appAt-adequate (suc e) zero (suc v) (x ∷ γ)) m) })
妥当性のパスは、この節を x と値の対の所属と同一視します。x をその等式に沿って数項へ書き戻せば、外向きの方向が負う所属がちょうど残ります。
論理式を充足する環境の集合
各構成子について、分出で残す環境を論理式が指定し、どの記述の条件も、その論理式自身のアリティの環境の上の一変数の論理式です。結合子は部分式のためにすでに作られた集合を定数として名指して参照します。非有界の量化子は、台の要素を環境の先頭に加え、その拡張が一つアリティの大きい集合に属するかを調べます。有界の量化子はさらに、新しい項目が界の項の値に属するという守りを加えます。こうして構成の各段階はすべて一度の分出です。
private opaque sep : (a : S) → Formula S 1 → S sep a φ = hasSeparationL a φ .fst .fst
分出は不透明な包装の中に一度記録されます。集合と一変数の論理式から部分集合を作ります。
sep-mem : (a : S) (φ : Formula S 1) (x : S)
→ (x ∈ˢ sep a φ) ≡ ((x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ))
sep-mem a φ = hasSeparationL a φ .fst .snd
所属の仕様が分出の内容のすべてです。部分集合への所属は、周囲の集合への所属と条件の充足を合わせたものです。
module _ (B : S) where cond : ∀ {n} → Formula S n → Formula S 1
基礎集合 B を固定します。各論理式は、B 上の符号化された環境について一項の条件を定めます。その条件を満たす環境を分出すると、その論理式の充足集合が得られます。
Sat : ∀ {n} → Formula S n → S Sat {n} φ = sep (envSet B n) (cond φ)
論理式を充足する環境の集合は、その論理式のアリティの環境の集合全体から、条件を満たす環境を分出したものです。
Sat-mem : ∀ {n} (φ : Formula S n) (x : S) → (x ∈ˢ Sat φ) ≡ ((x ∈ˢ envSet B n) ⊓ ((x ∷ []) ⊨ cond φ)) Sat-mem {n} φ = sep-mem (envSet B n) (cond φ)
その所属の等式が記録するのは二つの要件です。環境が正しいアリティと値をもち、かつその論理式固有の条件を満たすことです。
cond (t ∈̇ u) = (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero)) ∧̇ ( tmIs u zero (suc (suc zero)) ∧̇ (var (suc zero) ∈̇ var zero) ))))
所属の原子式は二つの項目を束縛し、対象言語の所属を主張します。スロット suc zero で読まれる t の値が、スロット zero で読まれる u の値に属するというものです。どちらの値も環境のスロットに対して読まれます。
cond (t ≐ u) = (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero)) ∧̇ ( tmIs u zero (suc (suc zero)) ∧̇ (var (suc zero) ≐ var zero) ))))
相等の原子式は同じ形をし、所属の代わりに相等が置かれます。
cond (a ∧̇ b) = ((var zero ∈̇ con (Sat a)) ∧̇ (var zero ∈̇ con (Sat b)))
連言の条件は、その環境が二つの部分式の集合のどちらにも属すことを求めます。どちらの集合も定数として名指されます。
cond (a ∨̇ b) = ((var zero ∈̇ con (Sat a)) ∨̇ (var zero ∈̇ con (Sat b)))
選言の条件は、二つのうち少なくとも一方への所属を求めます。
cond (a ⇒̇ b) = ((var zero ∈̇ con (Sat a)) ⇒̇ (var zero ∈̇ con (Sat b)))
含意の条件は、前件の集合への所属が後件の集合への所属を導くと言います。
cond ⊥̇ = ⊥̇
偽の条件は偽そのものです。これを満たす環境はありません。
cond (∃̇ a) = (∃̇∈ (con B) (∃̇ ( consAtL zero (suc zero) (suc (suc zero)) ∧̇ (var zero ∈̇ con (Sat a)) )))
非有界の存在量化子は台の上を動きます。B のある要素 x が環境を拡張し、拡張の節が新しい列が環境であることを証明し、拡張された環境が部分式の集合に属します。
cond (∀̇ a) = (∀̇∈ (con B) (∀̇ ( consAtL zero (suc zero) (suc (suc zero)) ⇒̇ (var zero ∈̇ con (Sat a)) )))
非有界の全称はその双対です。台の各要素は、加えられさえすれば、拡張された環境を部分式の集合の中へ落とし入れます。
cond (∀̇∈ t a) = (∀̇ ( tmIs t zero (suc zero) ⇒̇ ∀̇∈ (con B) ( (var zero ∈̇ var (suc zero)) ⇒̇ ∀̇ ( consAtL zero (suc zero) (suc (suc (suc zero))) ⇒̇ (var zero ∈̇ con (Sat a)) ) ) ))
有界の全称は三層にわたって量化します。最も外側で、界の項の値 w をみずからのスロットから読み、そのような各 w の上で、台の要素 x が x ∈ B と x ∈ w の二つの守りつきで量化され、さらに各 x について、x で環境を拡張した e' が拡張の節の証明のもとで部分式の集合に属すことが要求されます。ここで w は境界の補助のスロットにすぎず、部分式 a の環境は e' であり、環境にちょうど一つの項目を加えたものです。
cond (∃̇∈ t a) = (∃̇ ( tmIs t zero (suc zero) ∧̇ ∃̇∈ (con B) ( (var zero ∈̇ var (suc zero)) ∧̇ ∃̇ ( consAtL zero (suc zero) (suc (suc (suc zero))) ∧̇ (var zero ∈̇ con (Sat a)) ) ) ))
有界の存在量化は、同じ三層を存在の主張として組み合わせます。まず界の項の値が読まれ、証人は台のうちその値に属する要素であり、その拡張された環境が部分式の集合に属することまで要求されます。基礎と境界の二つの守りがともに保たれます。
条件の読み取り
一般の等式 Sat-mem は、環境集合への所属と条件の充足を分けます。連言、選言、含意、偽は cond の定義によって直接簡約され、補助的な同値は要りません。以下の補題が扱うのは残りの場合です。二つの原子の存在式と存在量化子に隠れた証人を展開し、あるいは全称量化子が与える関数を読み取ります。これらは cond φ の充足だけを扱い、環境集合の連言は Sat-mem に残ります。
CondAtom : ∀ {n} → Term S n → Term S n → (S → S → Type (ℓ-suc ℓ)) → S → Type (ℓ-suc ℓ) CondAtom t u R z = Σ[ v ∈ S ] (Σ[ w ∈ S ] (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs t (suc zero) (suc (suc zero)) ⟩ × (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs u zero (suc (suc zero)) ⟩ × R v w)))
二つの原子式では、条件は存在の主張であり、その展開された形が Σ 型の CondAtom です。t の値 v と u の値 w が、それぞれ項の読みを通して z の環境に対して読まれ、さらに二つの基底集合の間の関係 R が伴います。この型そのものは切り詰めを帯びず、切り詰められた形は後の補題に現れます。
cond∈-in : ∀ {n} (t u : Term S n) (z : S) → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁ → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩ cond∈-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })
所属の内向きの写しは、切り詰められた三つ組を、二つの量化子が期待する入れ子の証人の形に組み直します。消去が正当なのは、目標である外側の切り詰めそれ自体が命題だからで、内側の関係の性質のためではありません。
cond∈-out : ∀ {n} (t u : Term S n) (z : S) → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩ → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁ cond∈-out t u z = PT.rec squash₁ (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv })
外向きの写しは、入れ子の証人を三つ組へと平らに戻します。議論の全体が切り詰めの内側にとどまります。
cond≐-in : ∀ {n} (t u : Term S n) (z : S) → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁ → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩ cond≐-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ })
相等の原子式が運ぶ関係は fst v ≡ fst w、すなわち基底集合の相等であり、その内向きの写しは所属の場合と一言一句変わりません。
cond≐-out : ∀ {n} (t u : Term S n) (z : S) → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩ → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁ cond≐-out t u z = PT.rec squash₁ (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv })
その外向きの写しも所属の場合と同じで、関係を取り替えただけです。
CondQuant : ∀ {n} → Formula S (suc n) → S → Type (ℓ-suc ℓ) CondQuant a z = Σ[ x ∈ S ] (⟨ fst x ∈ fst B ⟩ × (Σ[ e' ∈ S ] (⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩ × ⟨ fst e' ∈ fst (Sat a) ⟩)))
非有界の存在量化子では、展開された条件は Σ 型の CondQuant です。基礎の要素 x、拡張の節によって環境 z に x を加えた拡張であると証明される項目 e'、そして e' の部分式の集合への所属です。ここでも型は切り詰めを帯びず、切り詰めは補題で加えられます。
cond∃-in : ∀ {n} (a : Formula S (suc n)) (z : S) → ∥ CondQuant a z ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ cond∃-in a z = PT.map (λ { (x , (x∈ , (e' , r))) → x , (x∈ , ∣ e' , r ∣₁) })
内向きの写しは、拡張のデータを、存在量化子自身が与える一つの切り詰められた証人へ折りたたみます。
cond∃-out : ∀ {n} (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ → ∥ CondQuant a z ∥₁ cond∃-out a z = PT.rec squash₁ (λ { (x , (x∈ , hv)) → PT.map (λ { (e' , r) → x , (x∈ , (e' , r)) }) hv })
外向きには、入れ子になった二つの切り詰められた証人を順に展開します。どちらの目標も切り詰め、したがって命題なので、展開は正当です。
cond∀-in : ∀ {n} (a : Formula S (suc n)) (z : S) → ((x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩
許された各値と証明された拡張について、前提はその拡張が部分式の充足集合に属すことを与えます。
→ ⟨ fst e' ∈ fst (Sat a) ⟩) → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩ cond∀-in a z k x x∈ e' hc = k x e' x∈ hc
非有界の全称では、展開された条件は関数です。基礎の各要素とその拡張に対して、その拡張での部分式の真理値を割り当てます。内向きと外向きは、量化子の二つの向きで読んだ同じ関数です。
cond∀-out : ∀ {n} (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩ → ((x e' : S) → ⟨ fst x ∈ fst B ⟩
条件を外向きに読むとき、B から取った値と、それを付け加えて得た環境を保ちます。
→ ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) cond∀-out a z h x e' x∈ hc = h x x∈ e' hc
ここに切り詰めは現れません。全称の充足は検証者を与えることで確かめられ、二つの方向はともにまさにそれを行うからです。
CondBnd : ∀ {n} → Formula S (suc n) → S → S → Type (ℓ-suc ℓ) CondBnd a z w = Σ[ x ∈ S ] ((⟨ fst x ∈ fst B ⟩ × ⟨ fst x ∈ fst w ⟩) × (Σ[ e' ∈ S ] (⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ × ⟨ fst e' ∈ fst (Sat a) ⟩)))
有界の量化子は一層加わります。条件が順に量化するのは、界の項の値 w、w の内側にある基礎の要素 x、そして環境 z に x を加えた拡張 e' です。e' は拡張の節が証明し、部分式の集合に属することが要求されます。w の役割は補助です。境界の値を運ぶのは w であり、部分式の環境は e'、すなわち環境 z に要素 x をちょうど一つ加えたものです。
cond∃∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ × ∥ CondBnd a z w ∥₁)) ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩
有界の存在量化は証人を重ねます。外側の切り詰めは界の項の値 w の上にあり、その内側に CondBnd a z w の内側の切り詰め、すなわち台の要素とその拡張が収まります。
cond∃∈-in t a z = PT.map (λ { (w , (hw , hx)) → w , (hw , PT.map (λ { (x , ((x∈B , x∈w) , (e' , r))) → x , (x∈B , (x∈w , ∣ e' , r ∣₁)) }) hx) })
最初の PT.map が w の上の外側の切り詰めを消去し、入れ子の PT.map が CondBnd の内側の切り詰めを消去して、要素と拡張を存在量化子自身の量化の中へ折りたたみます。どちらの目標も切り詰め、したがって命題なので、二つの消去が正当な理由は同じです。
cond∃∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩ → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ × ∥ CondBnd a z w ∥₁)) ∥₁
外向きの主張は、同じ二層の形をそのまま見せます。外側に境界の値、その内側に切り詰められた、台の要素とその拡張の記録です。
cond∃∈-out t a z = PT.map (λ { (w , (hw , hx)) → w , (hw , PT.rec squash₁ (λ { (x , (x∈B , (x∈w , hv))) → PT.map (λ { (e' , r) → x , ((x∈B , x∈w) , (e' , r)) }) hv }) hx) })
その証明はこの二層を順に展開します。行程のすべてが切り詰めの内側にとどまります。
cond∀∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ → (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩
二つの条件は、x が基礎集合 B と境界項の値 w の両方に属すことを要求します。
→ ⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩ cond∀∈-in t a z k w hw x x∈B x∈w e' hc = k w hw x e' x∈B x∈w hc
有界の全称の条件は、三層に量化された関数です。界の項の値 w のそれぞれに対して、w の内側の基礎の各要素 x と、環境 z に x を加えた拡張であると証明された各 e' について、e' での部分式の真理値を割り当てます。内向きの写しは、その関数を適用した姿です。
cond∀∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩ → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩
結論は、同じ境界の値、基礎集合の要素、証明された一項の拡張にわたって量化します。
→ (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩ → ⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) cond∀∈-out t a z h w hw x e' x∈B x∈w hc = h w hw x x∈B x∈w e' hc
外向きの写しは同じ関数を、三つの量化子を通して逆向きに読んだものです。どちらの方向にも切り詰めは現れません。全称の検証は検証者を与えることで完了し、ここでは値に対して、要素に対して、そして拡張に対して、層ごとに検証者が与えられるのです。