---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


```agda
{-# OPTIONS --cubical --safe --guardedness #-}
module FOL.Absoluteness where
```

# 絶対性

```agda
open import Base.Prelude
open import FOL.ZFStructure using ( ZFStructure; ZFStructureₕ; module hPropView; _↾_ )
open import FOL.Syntax using ( Term; con; var; Formula; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using
  ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-⊥; δ-∀∈; δ-∃∈
  ; Σ₁; σ-Δ₀; σ-∃; Π₁; π-Δ₀; π-∀ )
import FOL.Semantics
```

推移的部分構造で論理式を解釈した真理値が、周囲の構造で解釈した真理値と等しいとき、その論理式は絶対的である。ここで部分構造の台 `𝒮 ↾ M` の元は、周囲の元と、それがクラス `M` に属する証拠との対である。周囲での解釈には、それらの対を `fst` で射影したうえで同じ構文を使う。推移性が与える要点は、ある範囲が `M` に属すれば、その範囲の各要素も `M` に属するということである。

本章では、すべての Δ₀ 論理式について内側と外側の真理値が等しいことを帰納法で証明する。原子論理式は項の評価の一致に帰着し、結合子は帰納法の仮定を保つ。推移性が必要になるのは、有界量化子が周囲の元を部分構造の元に直す箇所だけである。最後にこの等式を一方向の法則へ拡張し、Σ₁ の真理は部分構造から周囲の構造へ上向きに、Π₁ の真理は周囲の構造から部分構造へ下向きに保存されることを示す。

ここでの構造は命題値である。`ZFStructureₕ` の台の等号と所属は `hProp ℓ` に値を取るので、充足の主張は基礎型をもつ命題になり、二つの充足の主張はパスとしての等しさで比較できる。数学的内容を担う概念がさらに二つある。第一は `Transitive` で、閉性の条件 `y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M`、すなわち `M` の要素の要素も `M` に属することを述べる。第二は `_↾_` で、構造をクラスへ制限し、「要素と、それがクラスに属する証拠」の対を新しい台とする。変わるのは何を要素とみなすかだけで、関係は第一射影に沿って引き継がれる。

構文の側では、論理式には定数 `con` と変数 `var`、そして項の値の要素を範囲とする二つの有界量化子 `∀̇∈` と `∃̇∈` が現れる。Lévy 階層は帰納的特徴づけを通して登場する。`Δ₀` は、原始的な所属と等号から出発し、命題結合子と有界量化子で作られる論理式の帰納的な類であり、その構成子には `δ-` 系の名前が付いている。`Σ₁` と `Π₁` はその上に築かれる。Δ₀ 論理式であるか、無制限の存在 (それぞれ全称) 量化子を持ち母式が再び Σ₁ (それぞれ Π₁) であるかで、`σ-∃` と `π-∀` が証拠となる。これらの証拠こそ、絶対性の証明が消費する帰納のデータである。

意味論は汎用的なので、本章では同じ構文の上で世界ごとに二回使うことになる。これからの証明のために三つの記法がある。`map` は環境全体に第一射影を適用し、`⇔toPath` は二つの含意を真理値のパスに合成する。切断の機構が `PT` として現れるのは、無制限の存在量化子の充足が単に inhabited な型だからである。したがって証拠の二世界間の移動は切断の下で行われる。

## 設定：一つの構文と二つの意味論

周囲の構造 `𝒮` と推移的クラス `M` を固定する。内側の世界は制限 `𝒮 ↾ M` であり、その台 `SM` は `M` の要素からなる。構文は `K := SM` を取る。論理式に現れる定数は `M` の要素でなければならず、パラメータについての規律が型で強制される。同じ論理式の族はこうして**二つの意味論**を受け取る。外側では `𝒮` の中で、定数を `fst` で解釈して評価し、内側では `𝒮 ↾ M` の中で、定数がそれ自身を表すものとして評価する。相対化は構文操作ではなく、一つの汎用的な意味論の二つの読み方なのである。充足を表す記号の上付き `ᵛ` と `ᵐ` は「どこで評価したか」を読み取る目印である。

この節は三つの固定パラメータのもとで進む。構造 `𝒮`、その台上で `hProp ℓ` に値を取るクラス `M`、そして推移性の証明 `trans` である。台 `S` と真理値の関係 `_∈ˢ_`、`_≈ˢ_` は `𝒮` に属し、`hProp` 上の直接の演算 `⊓`、`⊔`、`⇒` が結合子を解釈する。現時点で `M` について使うのはそれがクラスであることだけである。推移性が現れるのは定理の証明であり、それを述べる定義ではない。

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
module Single {ℓ} (𝒮 : ZFStructureₕ ℓ)
              (M : ZFStructure.S 𝒮 → hProp ℓ)
              (trans : hPropView.Transitive 𝒮 M) where
```

</summary>
<div class="submodule-fold-content">

```agda
  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 𝒮
```

外側の読み方は定数解釈 `ι := (λ p → p .fst)` を用いる。`M` の要素を名指す定数は、`𝒮` の中ではその要素そのものを指す。記号は固定される。`𝒮` での充足は `_⊨ᵛ_`、項の値は `⟦_⟧ᵛ` と書く。

```agda
  module SemM = FOL.Semantics 𝒮M

  open module V = SemV.At SM (λ p → p .fst) public
    renaming ( _⊨_ to _⊨ᵛ_ ; ⟦_⟧ to ⟦_⟧ᵛ )
  open module Mse = SemM.At SM id public
```

内側の読み方は `ι := id` を用いる。`𝒮 ↾ M` の中では定数はそれが名指す対そのものであり、制限の関係はその対の第一射影を読み取る。したがって、内側の原子的な主張 `xm ∈ˢ ym` は、`𝒮` ではちょうど `xm .fst ∈ˢ ym .fst` を意味する。これが二つの充足関係を比較できる理由である。記号は `_⊨ᵐ_` と `⟦_⟧ᵐ` となり、各論理式は内側の `δ ⊨ᵐ φ` としても外側の `(map (λ p → p .fst) δ) ⊨ᵛ φ` としても読める。

```agda
    renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ )
```

二つの世界の違いは環境の読み方にだけある。内側の環境 `δ : Vec SM n` は `fst` を通して外側の値を名指すので、`map (λ p → p .fst) δ` が対応する外側の環境である。二つの補題が両側の項の評価を結ぶ。定数はどちらの側でも自分の第一射影を値とし、変数はどちらの世界でも一回の参照にすぎない。したがって辞書の問題は原子の段階で解決される。

最初の補題は、参照と射影を項ごとに交換する。射影後の環境の第 `i` 項を読むことは、第 `i` 項を射影することと同じである。証明は添字で場合分けし、先頭では `refl`、尾では再帰する。`lookup` と `map` がどちらも項ごとに計算されるからである。

```agda
  private
    lookup-fst : ∀ {n} (i : Fin n) (δ : Vec SM n)
               → lookup i (map (λ p → p .fst) δ) ≡ (lookup i δ) .fst
    lookup-fst zero    (m ∷ δ) = refl
    lookup-fst (suc i) (m ∷ δ) = lookup-fst i δ
```

二つ目の補題はこれを項へ持ち上げる。内側で項を評価してから射影したものは、射影後の環境での外側の値に等しい。定数の場合は、それぞれの解釈 `id` と `fst` により両辺とも `m .fst` に計算され、`refl` で足りる。変数の場合は、外側の値が `map (λ p → p .fst) δ` への参照であり、最初の補題がそれを内側の参照の射影へ書き換える。`sym` は等式を必要な向きに置くためのものである。すべての項はこの二つの場合から作られるので、辞書はこれで完結である。

```agda
    ⟦⟧-fst : ∀ {n} (t : Term SM n) (δ : Vec SM n)
           → (⟦ t ⟧ᵐ δ) .fst ≡ ⟦ t ⟧ᵛ (map (λ p → p .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} → Δ₀ φ → (δ : Vec SM n)
       → (δ ⊨ᵐ φ) ≡ ((map (λ p → p .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` は項の補題 `tm .fst ≡ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ)` をそれに特化したものであり、内側の範囲 (対) と外側の範囲 (その第一射影) を結ぶ橋である。

```agda
    tm : SM
    tm = ⟦ t ⟧ᵐ δ
    p : tm .fst ≡ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ)
    p = ⟦⟧-fst t δ
    fwd : ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩ → ⟨ (map (λ p → p .fst) δ) ⊨ᵛ (∀̇∈ t φ) ⟩
```

順方向は内側の検証者 `h` を受け取り、`x ∈ˢ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ)` を満たす各外側の `x` に対して母式の外側の真理値を与えなければならない。ここで `x` は `M` の要素ではなく素の要素なので、まず束ね直しが必要である。`sym p` に沿った輸送が所属の証拠を内側の範囲 `tm .fst` へ移し、次いで推移性が働く。`x ∈ tm .fst` と `tm .fst ∈ᶜ M` から `x ∈ᶜ M` が得られ、したがって `xm := x , trans hx' (tm .snd)` は正当な内側の要素である。`xm` で `h` を実行すると母式の内側の真理値が得られ、帰納仮定 `abs₀ d (xm ∷ δ)` がそれを外側へ運ぶ。帰納全体を通して前提 `trans` を消費するのは、この一段階だけである。

```agda
    fwd h x hx =
      let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx
          xm  = x , trans hx' (tm .snd)
      in subst ⟨_⟩ (abs₀ d (xm ∷ δ)) (h xm hx')
    bwd : ⟨ (map (λ p → p .fst) δ) ⊨ᵛ (∀̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∀̇∈ t φ) ⟩
```

逆方向は逆向きに進む。外側の検証者 `g` は素の要素を走査し、内側の節は所属の証拠を伴う対 `xm` を期待する。射影 `xm .fst` が外側の要素であり、項の補題がその所属を `tm .fst` から `⟦ t ⟧ᵛ (map (λ p → p .fst) δ)` へ運ぶ。これはちょうど `g` が期待する形である。`g` を呼び出せば外側の真理値が得られ、`abs₀ d (xm ∷ δ)` を `sym` に沿って運ぶことで内側へ戻す。この方向に推移性は不要である。対 `xm` は証拠を伴って届くからである。

```agda
    bwd g xm hxm =
      subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ)))
            (g (xm .fst) (subst (λ s → ⟨ xm .fst ∈ˢ s ⟩) p hxm))
  abs₀ (δ-∃∈ {t = t} {φ = φ} d) δ = ⇔toPath fwd bwd
    where
```

存在の場合 `∃̇∈` は全称の場合を写し取るが、構造上の違いが一つある。存在量化子の充足は台の上の上限、すなわち要素ごとの寄与すべてを覆う最小の真理値として定義され、切断された命題の上限は命題的切り詰めの下に住むため、両方向とも `map₁` を通して動く。略記 `tm` と `p` は同じくスコープにあり、範囲を通して証拠を束ね直す数学は全称の場合と同一である。

```agda
    tm : SM
    tm = ⟦ t ⟧ᵐ δ
    p : tm .fst ≡ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ)
    p = ⟦⟧-fst t δ
    fwd : ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩ → ⟨ (map (λ p → p .fst) δ) ⊨ᵛ (∃̇∈ t φ) ⟩
```

順方向では、切断された内側の証拠は三つ組である。範囲内の内側の要素 `xm`、その所属の証拠、そして母式の内側の真理値である。map はこれを `xm .fst` に送り、`p` に沿って所属を外側へ運んで `⟨ xm .fst ∈ˢ ⟦ t ⟧ᵛ (map (λ p → p .fst) δ) ⟩` の形にし、さらに帰納仮定 `abs₀ d (xm ∷ δ)` を通して母式の真理値を外側へ運ぶ。証拠そのものが取り出されることはなく、切断の内側でだけ使われる。

```agda
    fwd = map₁ λ { (xm , hxm , hφ) →
            xm .fst
          , subst (λ s → ⟨ xm .fst ∈ˢ s ⟩) p hxm
          , subst ⟨_⟩ (abs₀ d (xm ∷ δ)) hφ }
    bwd : ⟨ (map (λ p → p .fst) δ) ⊨ᵛ (∃̇∈ t φ) ⟩ → ⟨ δ ⊨ᵐ (∃̇∈ t φ) ⟩
```

逆方向では、外側の証拠は三つ組である。素の要素 `x`、外側の範囲での所属、そして母式の外側の真理値である。`sym p` に沿う輸送が所属を内側の範囲へ引き戻し、推移性が続いて `x ∈ᶜ M` を証明するので `xm` は内側の要素となり、母式の真理値は `sym (abs₀ d (xm ∷ δ))` を通して内側へ運ばれる。切断された出力はやはり `map₁` で組み立てられるため、どこでも選択公理は使われない。二つの有界量化子の場合は、両側とも単に inhabited な証拠で成立する。

```agda
    bwd = map₁ λ { (x , hx , hφ) →
            let hx' = subst (λ s → ⟨ x ∈ˢ s ⟩) (sym p) hx
                xm  = x , trans hx' (tm .snd)
            in xm , hx' , subst ⟨_⟩ (sym (abs₀ d (xm ∷ δ))) hφ }
```

## Σ₁ は上向き、Π₁ は下向き

Δ₀ の外に出ると、絶対性は一方向になるが、その二方向は双対である。内側で真な Σ₁ 論理式は外側でも真であり、外側で真な Π₁ 論理式は内側でも真である。この非対称は量化子の変異から来る。Σ₁ の証拠は Δ₀ の核の上に、任意の有限個の無制限存在量化子の連なりで作られ得て、内側の存在の証拠は `fst` を通して外側へ渡る。Π₁ の証拠も同様に無制限の全称量化子で作られ得て、外側の検証者は各段階で内側の要素の `fst` に特殊化される。これらの無制限の段階で推移性がさらに使われることはない。ただし、それぞれの帰納の Δ₀ の基底は絶対性定理に、ひいては推移性の仮定に依存する。

Δ₀ の基底の場合、`abs₀ d δ` は内側と外側の真理値を結ぶパスであり、`subst` は内側の真理値の証明をそのパスに沿って外側へ輸送する。この基底の場合そのものは命題的切り詰めを導入しない。Σ₁ の場合 `σ-∃` は台の上の無制限の存在量化であり、その充足は命題的切り詰めのもとでの上限なので、`map₁` が切断された対に作用する。内側の証拠 `xm` と母式の内側の真理値 `h` の対は、外側の要素 `xm .fst` に送られ、再帰呼び出し `σ₁-up s (xm ∷ δ) h` は対全体で環境を拡張して、基底の場合が包みを捨てるまで証拠を内側に保つ。

```agda
  σ₁-up : ∀ {n} {φ : Formula SM n} → Σ₁ φ → (δ : Vec SM n)
        → ⟨ δ ⊨ᵐ φ ⟩ → ⟨ (map (λ p → p .fst) δ) ⊨ᵛ φ ⟩
  σ₁-up (σ-Δ₀ d) δ = subst ⟨_⟩ (abs₀ d δ)
  σ₁-up (σ-∃ s)  δ = map₁ λ { (xm , h) → xm .fst , σ₁-up s (xm ∷ δ) h }

  π₁-down : ∀ {n} {φ : Formula SM n} → Π₁ φ → (δ : Vec SM n)
```

下向きの法則はその鏡像である。Δ₀ の場合は `sym (abs₀ d δ)` に沿って輸送し、Π₁ の場合 `π-∀` は無制限の全称量化である。外側の検証者 `h` が与えられると、各内側の要素 `xm` に対して `xm .fst` でインスタンス化し、再帰呼び出しが拡張された環境で母式を証明する。ここに切断は現れない。全称の充足は下限、すなわち要素ごとの寄与すべての下にある最大の真理値であり、検証者を直接与えることで明示的に検証できるからである。そして無制限の段階に推移性は使われない。無制限の量化子は台全体を走査し、そこでは対の構成と射影がはじめから使えるからである。

```agda
          → ⟨ (map (λ p → p .fst) δ) ⊨ᵛ φ ⟩ → ⟨ δ ⊨ᵐ φ ⟩
  π₁-down (π-Δ₀ d) δ = subst ⟨_⟩ (sym (abs₀ d δ))
  π₁-down (π-∀ s)  δ h xm = π₁-down s (xm ∷ δ) (h (xm .fst))
```

</div>
</details>

## まとめ

境界は明確である。推移性のもとで、Δ₀ の真理値は `𝒮 ↾ M` と `𝒮` の間で一致し、`abs₀` は各 Δ₀ の証拠に真理値のパスを与える。有界全称では、内側の検証者を界の任意の外側の要素へ適用するときに推移性を使う。有界存在では、外側の証人を内側の台へ入れるときに使う。この基底から、`σ₁-up` は Σ₁ の真理を上向きに、`π₁-down` は Π₁ の真理を下向きに保存する。逆方向は一般には得られない。任意の外側の存在証人が `M` に属するとは限らず、内側の全称検証者は `M` の外側の要素について何も述べないからである。