--- title: "絶対性" module: FOL.Absoluteness lang: ja site: "Bedrock" description: "絶対性" stage: "一階論理" reading_order: 10 canonical: https://bedrock.institute/ja/FOL.Absoluteness.html html: FOL.Absoluteness.html agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/Absoluteness.lagda.md prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics] routes: [common-foundations] translations: [https://bedrock.institute/en/FOL.Absoluteness.md, https://bedrock.institute/zh/FOL.Absoluteness.md] agent_guide: /llms.txt license: CC-BY-NC-SA-4.0 --- # 絶対性 推移的部分構造で論理式を解釈した真理値が、周囲の構造で解釈した真理値と等しいとき、その論理式は絶対的です。ここで部分構造の台 `𝒮 ↾ M` の元は、周囲の元と、それがクラス `M` に属する証拠との対です。周囲での解釈には、それらの対を `fst` で射影したうえで同じ構文を使います。推移性が与える要点は、ある範囲が `M` に属すれば、その範囲の各要素も `M` に属するということです。 本章では、すべての Δ₀ 論理式について内側と外側の真理値が等しいことを帰納法で証明します。原子論理式は項の評価の一致に帰着し、結合子は帰納法の仮定を保ちます。推移性が必要になるのは、有界量化子が周囲の元を部分構造の元に直す箇所だけです。最後にこの等式を一方向の法則へ拡張し、Σ₁ の真理は部分構造から周囲の構造へ上向きに、Π₁ の真理は周囲の構造から部分構造へ下向きに保存されることを示します。 ここでの構造は命題値です。`ZFStructure` の台の等号と所属は `hProp ℓ` に値を取るので、充足の主張は基礎型をもつ命題になり、二つの充足の主張はパスとしての等しさで比較できます。数学的内容を担う概念がさらに二つあります。第一は `Transitive` で、閉性の条件 `y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M`、すなわち `M` の要素の要素も `M` に属することを述べます。第二は `_↾_` で、構造をクラスへ制限し、「要素と、それがクラスに属する証拠」の対を新しい台とします。変わるのは何を要素とみなすかだけで、関係は第一射影に沿って引き継がれます。 ```agda {-# OPTIONS --cubical --safe --guardedness #-} module FOL.Absoluteness where open import Base.Prelude open import FOL.ZFStructure using ( ZFStructure; Transitive; _↾_ ) ``` 構文の側では、論理式には定数 `con` と変数 `var`、そして項の値の要素を範囲とする二つの有界量化子 `∀̇∈` と `∃̇∈` が現れます。Lévy 階層は帰納的特徴づけを通して登場します。`Δ₀` は、原始的な所属と等号から出発し、命題結合子と有界量化子で作られる論理式の帰納的な類であり、その構成子には `δ-` 系の名前が付いています。`Σ₁` と `Π₁` はその上に築かれます。Δ₀ 論理式であるか、無制限の存在 (それぞれ全称) 量化子を持ち母式が再び Σ₁ (それぞれ Π₁) であるかで、`σ-∃` と `π-∀` が証拠となります。これらの証拠こそ、絶対性の証明が消費する帰納のデータです。 ```agda open import FOL.Syntax using ( Term; con; var; Formula; ∀̇∈; ∃̇∈ ) open import FOL.LevyHierarchy using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈ ; Σ₁; σ-Δ₀; σ-∃; Π₁; π-Δ₀; π-∀ ) import FOL.Semantics ``` 意味論は汎用的なので、本章では同じ構文の上で世界ごとに二回使うことになります。これからの証明のために三つの記法があります。`map` は環境全体に第一射影を適用し、`⇔toPath` は二つの含意を真理値のパスに合成します。切断の機構が `PT` として現れるのは、無制限の存在量化子の充足が単に inhabited な型だからです。したがって証拠の二世界間の移動は切断の下で行われます。 ```agda open import Cubical.Data.Vec using ( map ) open import Cubical.Functions.Logic using ( ⇔toPath ) import Cubical.HITs.PropositionalTruncation as PT ``` ## 設定：一つの構文と二つの意味論 周囲の構造 `𝒮` と推移的クラス `M` を固定します。内側の世界は制限 `𝒮 ↾ M` であり、その台 `SM` は `M` の要素からなります。構文は `K := SM` を取ります。論理式に現れる定数は `M` の要素でなければならず、パラメータについての規律が型で強制されます。同じ論理式の族はこうして**二つの意味論**を受け取ります。外側では `𝒮` の中で、定数を `fst` で解釈して評価し、内側では `𝒮 ↾ M` の中で、定数がそれ自身を表すものとして評価します。相対化は構文操作ではなく、一つの汎用的な意味論の二つの読み方なのです。充足を表す記号の上付き `ᵛ` と `ᵐ` は「どこで評価したか」を読み取る目印です。 この節は三つの固定パラメータのもとで進みます。構造 `𝒮`、その台上で `hProp ℓ` に値を取るクラス `M`、そして推移性の証明 `trans` です。台 `S` と真理値の関係 `_∈ˢ_`、`_≈ˢ_` は `𝒮` に属し、`hProp` 上の直接の演算 `⊓`、`⊔`、`⇒` が結合子を解釈します。現時点で `M` について使うのはそれがクラスであることだけです。推移性が現れるのは定理の証明であり、それを述べる定義ではありません。 ```agda module Single {ℓ} (𝒮 : ZFStructure ℓ) (M : ZFStructure.S 𝒮 → hProp ℓ) (trans : Transitive 𝒮 M) where open ZFStructure 𝒮 ``` 内側の世界の台は Σ 型 `SM` です。`S` の要素に、それが `M` に属する証拠を対にしたものです。`𝒮 ↾ M` の関係は第一射影の上で解釈されるので、`𝒮` の目には、内側の要素とその `fst` による像は `S` の同じ inhabitant を指します。汎用の意味論はこの台の上で二回使われます。一度は外側の構造 `𝒮` で評価し、一度は制限 `𝒮M` で評価します。両者の読み方が構文を共有するのは、定数域をともに `SM` とするからで、違いは構造と定数解釈にだけあります。 ```agda SM : Type ℓ SM = Σ[ x ∈ S ] (x ∈ᶜ M) 𝒮M : ZFStructure ℓ 𝒮M = 𝒮 ↾ M module SemV = FOL.Semantics 𝒮 ``` 外側の読み方は定数解釈 `ι := fst` を用います。`M` の要素を名指す定数は、`𝒮` の中ではその要素そのものを指します。記号は固定されます。`𝒮` での充足は `_⊨ᵛ_`、項の値は `⟦_⟧ᵛ` と書き、環境の記法 `_^_` は章全体で使えます。 ```agda module SemM = FOL.Semantics 𝒮M open SemV using ( _^_ ) public open module V = SemV.At SM fst public renaming ( _⊨_ to _⊨ᵛ_ ; ⟦_⟧ to ⟦_⟧ᵛ ) open module Mse = SemM.At SM id public ``` 内側の読み方は `ι := id` を用います。`𝒮 ↾ M` の中では定数はそれが名指す対そのものであり、制限の関係はその対の第一射影を読み取ります。したがって、内側の原子的な主張 `xm ∈ˢ ym` は、`𝒮` ではちょうど `fst xm ∈ˢ fst ym` を意味します。これが二つの充足関係を比較できる理由です。記号は `_⊨ᵐ_` と `⟦_⟧ᵐ` となり、各論理式は内側の `δ ⊨ᵐ φ` としても外側の `(map fst δ) ⊨ᵛ φ` としても読めます。 ```agda renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ ) ``` 二つの世界の違いは環境の読み方にだけあります。内側の環境 `δ : SM ^ n` は `fst` を通して外側の値を名指すので、`map fst δ` が対応する外側の環境です。二つの補題が両側の項の評価を結びます。定数はどちらの側でも自分の第一射影を値とし、変数はどちらの世界でも一回の参照にすぎません。したがって辞書の問題は原子の段階で解決されます。 最初の補題は、参照と射影を項ごとに交換します。射影後の環境の第 `i` 項を読むことは、第 `i` 項を射影することと同じです。証明は添字で場合分けし、先頭では `refl`、尾では再帰します。`lookup` と `map` がどちらも項ごとに計算されるからです。 ```agda private lookup-fst : ∀ {n} (i : Fin n) (δ : SM ^ n) → lookup i (map fst δ) ≡ fst (lookup i δ) lookup-fst zero (m ∷ δ) = refl lookup-fst (suc i) (m ∷ δ) = lookup-fst i δ ``` 二つ目の補題はこれを項へ持ち上げます。内側で項を評価してから射影したものは、射影後の環境での外側の値に等しい。定数の場合は、それぞれの解釈 `id` と `fst` により両辺とも `fst m` に計算され、`refl` で足ります。変数の場合は、外側の値が `map fst δ` への参照であり、最初の補題がそれを内側の参照の射影へ書き換えます。`sym` は等式を必要な向きに置くためのものです。すべての項はこの二つの場合から作られるので、辞書はこれで完結です。 ```agda ⟦⟧-fst : ∀ {n} (t : Term SM n) (δ : SM ^ n) → fst (⟦ t ⟧ᵐ δ) ≡ ⟦ t ⟧ᵛ (map 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₂` に渡すことが場合全体になります。これらの演算は関数であり、等しさを保つからです。 ```agda abs₀ : ∀ {n} {φ : Formula SM n} → Δ₀ φ → (δ : SM ^ n) → (δ ⊨ᵐ φ) ≡ ((map 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` への所属の証拠」の対を走査します。次のブロックで一方向ずつ展開します。 ```agda 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` は項の補題 `fst tm ≡ ⟦ t ⟧ᵛ (map fst δ)` をそれに特化したものであり、内側の範囲 (対) と外側の範囲 (その第一射影) を結ぶ橋です。 ```agda tm : SM tm = ⟦ t ⟧ᵐ δ p : fst tm ≡ ⟦ t ⟧ᵛ (map fst δ) p = ⟦⟧-fst t δ fwd : ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩ → ⟨ (map fst δ) ⊨ᵛ (∀̇∈ t φ) ⟩ ``` 順方向は内側の検証者 `h` を受け取り、`x ∈ˢ ⟦ t ⟧ᵛ (map fst δ)` を満たす各外側の `x` に対して母式の外側の真理値を与えなければなりません。ここで `x` は `M` の要素ではなく素の要素なので、まず束ね直しが必要です。`sym p` に沿った輸送が所属の証拠を内側の範囲 `fst tm` へ移し、次いで推移性が働きます。`x ∈ fst tm` と `fst tm ∈ᶜ M` から `x ∈ᶜ M` が得られ、したがって `xm := x , trans hx' (snd tm)` は正当な内側の要素です。`xm` で `h` を実行すると母式の内側の真理値が得られ、帰納仮定 `abs₀ d (xm ∷ δ)` がそれを外側へ運びます。帰納全体を通して前提 `trans` を消費するのは、この一段階だけです。 ```agda fwd h x hx = let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx xm = x , trans hx' (snd tm) in subst ⟨_⟩ (abs₀ d (xm ∷ δ)) (h xm hx') bwd : ⟨ (map fst δ) ⊨ᵛ (∀̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩ ``` 逆方向は逆向きに進みます。外側の検証者 `g` は素の要素を走査し、内側の節は所属の証拠を伴う対 `xm` を期待します。射影 `fst xm` が外側の要素であり、項の補題がその所属を `fst tm` から `⟦ t ⟧ᵛ (map fst δ)` へ運びます。これはちょうど `g` が期待する形です。`g` を呼び出せば外側の真理値が得られ、`abs₀ d (xm ∷ δ)` を `sym` に沿って運ぶことで内側へ戻します。この方向に推移性は不要です。対 `xm` は証拠を伴って届くからです。 ```agda bwd g xm hxm = subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ))) (g (fst xm) (subst (λ s → ⟨ fst xm ∈ˢ s ⟩) p hxm)) abs₀ (δ-∃∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd where ``` 存在の場合 `∃̇∈` は全称の場合を写し取りますが、構造上の違いが一つあります。存在量化子の充足は台の上の上限、すなわち要素ごとの寄与すべてを覆う最小の真理値として定義され、切断された命題の上限は命題的切り詰めの下に住むため、両方向とも `PT.map` を通して動きます。略記 `tm` と `p` は同じくスコープにあり、範囲を通して証拠を束ね直す数学は全称の場合と同一です。 ```agda tm : SM tm = ⟦ t ⟧ᵐ δ p : fst tm ≡ ⟦ t ⟧ᵛ (map fst δ) p = ⟦⟧-fst t δ fwd : ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩ → ⟨ (map fst δ) ⊨ᵛ (∃̇∈ t φ) ⟩ ``` 順方向では、切断された内側の証拠は三つ組です。範囲内の内側の要素 `xm`、その所属の証拠、そして母式の内側の真理値です。map はこれを `fst xm` に送り、`p` に沿って所属を外側へ運んで `⟨ fst xm ∈ˢ ⟦ t ⟧ᵛ (map fst δ) ⟩` の形にし、さらに帰納仮定 `abs₀ d (xm ∷ δ)` を通して母式の真理値を外側へ運びます。証拠そのものが取り出されることはなく、切断の内側でだけ使われます。 ```agda fwd = PT.map λ { (xm , hxm , hφ) → fst xm , subst (λ s → ⟨ fst xm ∈ˢ s ⟩) p hxm , subst ⟨_⟩ (abs₀ d (xm ∷ δ)) hφ } bwd : ⟨ (map fst δ) ⊨ᵛ (∃̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩ ``` 逆方向では、外側の証拠は三つ組です。素の要素 `x`、外側の範囲での所属、そして母式の外側の真理値です。`sym p` に沿う輸送が所属を内側の範囲へ引き戻し、推移性が続いて `x ∈ᶜ M` を証明するので `xm` は内側の要素となり、母式の真理値は `sym (abs₀ d (xm ∷ δ))` を通して内側へ運ばれます。切断された出力はやはり `PT.map` で組み立てられるため、どこでも選択公理は使われません。二つの有界量化子の場合は、両側とも単に inhabited な証拠で成立します。 ```agda bwd = PT.map λ { (x , hx , hφ) → let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx xm = x , trans hx' (snd tm) in xm , hx' , subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ))) hφ } ``` ## Σ₁ は上向き、Π₁ は下向き Δ₀ の外に出ると、絶対性は一方向になりますが、その二方向は双対です。内側で真な Σ₁ 論理式は外側でも真であり、外側で真な Π₁ 論理式は内側でも真です。この非対称は量化子の変異から来ます。Σ₁ の証拠は Δ₀ の核の上に、任意の有限個の無制限存在量化子の連なりで作られ得て、内側の存在の証拠は `fst` を通して外側へ渡ります。Π₁ の証拠も同様に無制限の全称量化子で作られ得て、外側の検証者は各段階で内側の要素の `fst` に特殊化されます。これらの無制限の段階で推移性がさらに使われることはありません。ただし、それぞれの帰納の Δ₀ の基底は絶対性定理に、ひいては推移性の仮定に依存します。 Δ₀ の基底の場合、`abs₀ d δ` は内側と外側の真理値を結ぶパスであり、`subst` は内側の真理値の証明をそのパスに沿って外側へ輸送します。この基底の場合そのものは命題的切り詰めを導入しません。Σ₁ の場合 `σ-∃` は台の上の無制限の存在量化であり、その充足は命題的切り詰めのもとでの上限なので、`PT.map` が切断された対に作用します。内側の証拠 `xm` と母式の内側の真理値 `h` の対は、外側の要素 `fst xm` に送られ、再帰呼び出し `σ₁-up s (xm ∷ δ) h` は対全体で環境を拡張して、基底の場合が包みを捨てるまで証拠を内側に保ちます。 ```agda σ₁-up : ∀ {n} {φ : Formula SM n} → Σ₁ φ → (δ : SM ^ n) → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ (map fst δ) ⊨ᵛ φ ⟩ σ₁-up (σ-Δ₀ d) δ = subst ⟨_⟩ (abs₀ d δ) σ₁-up (σ-∃ s) δ = PT.map λ { (xm , h) → fst xm , σ₁-up s (xm ∷ δ) h } π₁-down : ∀ {n} {φ : Formula SM n} → Π₁ φ → (δ : SM ^ n) ``` 下向きの法則はその鏡像です。Δ₀ の場合は `sym (abs₀ d δ)` に沿って輸送し、Π₁ の場合 `π-∀` は無制限の全称量化です。外側の検証者 `h` が与えられると、各内側の要素 `xm` に対して `fst xm` でインスタンス化し、再帰呼び出しが拡張された環境で母式を証明します。ここに切断は現れません。全称の充足は下限、すなわち要素ごとの寄与すべての下にある最大の真理値であり、検証者を直接与えることで明示的に検証できるからです。そして無制限の段階に推移性は使われません。無制限の量化子は台全体を走査し、そこでは対の構成と射影がはじめから使えるからです。 ```agda → ⟨ (map fst δ) ⊨ᵛ φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩ π₁-down (π-Δ₀ d) δ = subst ⟨_⟩ (sym (abs₀ d δ)) π₁-down (π-∀ s) δ h xm = π₁-down s (xm ∷ δ) (h (fst xm)) ``` ## まとめ 境界は明確です。推移性のもとで、Δ₀ の真理値は `𝒮 ↾ M` と `𝒮` の間で一致し、`abs₀` は各 Δ₀ の証拠に真理値のパスを与えます。有界全称では、内側の検証者を界の任意の外側の要素へ適用するときに推移性を使います。有界存在では、外側の証人を内側の台へ入れるときに使います。この基底から、`σ₁-up` は Σ₁ の真理を上向きに、`π₁-down` は Π₁ の真理を下向きに保存します。逆方向は一般には得られません。任意の外側の存在証人が `M` に属するとは限らず、内側の全称検証者は `M` の外側の要素について何も述べないからです。