---
title: "単集合と対を表す論理式"
module: L.Coding.PairFormulas
lang: ja
site: "Bedrock"
description: "単集合と対を表す論理式"
stage: "内部の符号化：式と定義域"
reading_order: 40
canonical: https://bedrock.institute/ja/L.Coding.PairFormulas.html
html: L.Coding.PairFormulas.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/PairFormulas.lagda.md
prerequisites: [Base.Prelude, FOL.Syntax, FOL.LevyHierarchy, FOL.Semantics, V.Hierarchy, V.Coding]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.PairFormulas.md, https://bedrock.institute/zh/L.Coding.PairFormulas.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 単集合と対を表す論理式

この章の目標は、対象言語に、割り当てられたある集合が他の二つの集合の Kuratowski 順序対であると認識させること、そして道すがら、Kuratowski 対を構成する単集合と非順序対も認識させることです。一階の論理式が語れるのは所属と等号だけなので、認識は外延的でなければなりません。`pr U W` を認識するとは、所属だけを通して、どの要素をちょうど持つのかを言うことです。本章では有界な論理式を三つ構成します。`sglAt` は「この集合はあれの単集合である」、`pairAt` は「これはあの二つの非順序対である」、`prAt` はこれらを組み合わせて「これはあの二つの Kuratowski 対である」と読み取る式です。

最後の妥当性定理は正確な同一視です。任意の割当てに対して、`prAt q u v` の充足は真理値のパスであり、その先にあるのは「`q` の位置の値が、`u` と `v` の位置の値に `pr` を施した結果と等しい」という命題です。一方向の含意のようなより弱い主張はここでは行いません。

各論理式の量化子は指定された集合で限られ、自由変数の位置は引数として与えられる de Bruijn 添字なので、同じ式を任意の入れ子の深さで使えます。すべての節が原子か有界量化子であるため、各読解式は Lévy 階層の Δ₀ です。

外側の目標は明確な所属の形を持ちます。`pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆` です。外側の集合は非順序対で、第 1 の要素は `U` の単集合、第 2 の要素は `U` と `W` の非順序対です。したがって順序対の認識は、指定された二要素がともに存在し、すべての要素がそのどちらかであるという三条件に帰着します。最後の条件は命題的に切り詰められており、非順序対の所属の分類と一致します。これは選択肢の存在を記録しますが、どちら側かは選びません。

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

open import Base.Prelude

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

open import FOL.Syntax
```

これらの記述を表す道具は、一階言語の有界フラグメントです。原子 `_∈̇_` と `_≐_`、結合子 `_∧̇_` と `_∨̇_` は、各位置に割り当てられた集合の間の所属と等号を述べます。量化子 `∀̇∈` と `∃̇∈` は常に割り当てられた集合で限られます。これらだけから作られる論理式は Lévy 階層の有界クラス `Δ₀` をなし、`checkΔ₀` が構文的に検査します。

認識の対象は Kuratowski 符号化 `pr` で、`pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆` と定義されます。順序対は、`U` の単集合と `U` と `W` の対という二つの集合の非順序対として提示されるのです。したがって認識の問題は、有界論理式で、ある集合が `U` の単集合である要素をひとつ、`U` と `W` の非順序対である要素をひとつ持ち、それ以外の要素を持たない、と言うことに帰着します。単集合と非順序対への所属にはそれぞれ分類があり、外延性が完全な所属の条件を集合の間の等号に変換します。

```agda
  using ( var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy using ( Δ₀; checkΔ₀ )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; extensionalV )
open import V.Coding {ℓ} using ( pr )
```

単集合と非順序対の所属には、階層での所属 `⟨ y ∈ b ⟩` と、それぞれの構成が用いる小さな所属の分類という同値な二つの形があります。`∈∈ₛ` が両者を結びます。単集合の分類はパス `y ≡ u` を与え、非順序対の分類は切り詰められた選択肢 `∥ (y ≡ u) ⊎ (y ≡ v) ∥₁` を与えます。各所属の記述を両方向に証明すれば、`⇔toPath` が所属命題の同値を外延性に必要なパスへ変えます。

```agda
open import Cubical.Data.Unit using ( tt )
import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
```

意味論は、レベル `ℓ-suc ℓ` の `hProp` を真理値として取ります。論理式は裸のブール値に評価されるのではなく、その値は命題であり、環境のもとでの論理式の充足それ自体が判定ではなく命題です。複合した論理式を読むとき、連言と選言はこれらの `hProp` 真理値に直接作用します。この命題的な設定が目標にとって重要です。有界論理式の充足を、集合とその符号化された対の等号のような外側の条件と、パスとして同一視できるからです。

```agda
open import Cubical.Functions.Logic using ( ⇔toPath )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
```

この意味論の中で、定数解釈は `V ℓ` 上の恒等写像に固定されます。言語の定数はただの集合であり、自分自身を表示するのです。したがって `⟦ var k ⟧ γ` は環境 `γ` が位置 `k` に割り当てる値であり、論理式は割り当てられた集合を直接語ることができます。

```agda
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s; SingletonPackage; module InfinitySet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)
open InfinitySet using ( #_ )
```

これが次の妥当性の主張を意味あるものにします。読解式 `prAt` の位置 `q`、`u`、`v` での充足が、真理値として、`⟦ var q ⟧ γ` と `pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ)` の等号と比較されるのです。

```agda
module Sem = FOL.Semantics 𝒮ᵥ
open Sem using ( _^_ )
open Sem.At (V ℓ) id using ( _⊨_; ⟦_⟧ )
```

## 単集合と非順序対を特徴付ける

唯一の要素が `u` である集合は `u` の単集合であり、要素がちょうど `u` と `v` である集合はそれらの非順序対です。これらは対象言語の読解式が表すことになる外側の意味なので、メタレベルでここに一度証明します。どちらの特徴付けも同じ手法に依ります。二つの集合が同じ要素を許すなら、外延性 `extensionalV` が点ごとの所属の同値を集合間のパスに変えるのです。

二つの方向は強さが異なります。`⁅ u ⁆s` の要素が `u` と等しいことは外側の切り詰めを伴わないパスですが、`⁅ u , v ⁆` の要素が `u` か `v` のどちらかであることは命題的に切り詰められた形でしか、つまり命題として丸められた選言でしか言えません。証明はこの区別を正確に保ちます。

単集合への所属は `SingletonPackage` の分類によって完全に記述されます。`y` が `⁅ u ⁆s` に属するのは、`y` が `u` と等しいとき、かつそのときに限ります。橋 `∈∈ₛ` が階層本来の所属とこの小さい所属の間を行き来するので、`∈sgl-elim` は橋の前半と分類をつなげ、単なる所属の証明から実際のパス `y ≡ u` を取り出します。`∈sgl-intro` は同じ二段階を逆向きに進めます。ここに丸めは一切ありません。等号のパスはそのまま使え、`V ℓ` が h-集合であるため命題のままです。

```agda
∈sgl-elim : {u y : V ℓ} → ⟨ y ∈ ⁅ u ⁆s ⟩ → y ≡ u
∈sgl-elim {u} {y} h =
    SetPackage.classification (SingletonPackage u) y .fst (∈∈ₛ {a = y} {b = ⁅ u ⁆s} .fst h)

∈sgl-intro : {u y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u ⁆s ⟩
∈sgl-intro {u} {y} e = ∈∈ₛ {a = y} {b = ⁅ u ⁆s} .snd
```

非順序対については、分類 `pairing-ax` が所属を選言で記述します。要素は `u` と等しいか、`v` と等しいかです。ここに丸めが現れます。`∈pair-elim` は所属の証明を、命題的に切り詰められた形でしか成り立たない選言 `∥ (y ≡ u) ⊎ (y ≡ v) ∥₁` に変えます。下の分類が側の選択を命題として丸めて返すためで、それを丸めなしの直和型へ消去することはできません。逆に `∈pair-introL` と `∈pair-introR` はそれぞれ片側の明示的なパスを受け取り、それを「どちらか一方が成り立つという切り詰められた形」として封入して所属を得ます。

```agda
    (SetPackage.classification (SingletonPackage u) y .snd e)

∈pair-elim : {u v y : V ℓ} → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁
∈pair-elim {u} {v} {y} h = pairing-ax u v y .fst (∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .fst h)

∈pair-introL : {u v y : V ℓ} → y ≡ u → ⟨ y ∈ ⁅ u , v ⁆ ⟩
∈pair-introL {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd
```

二つ目の導入は一つ目と対称です。両方の構成への出入りの所属が揃ったので、外側の特徴付けを述べられます。`sgl-char` はこう言います。`u` が `x` に属し、`x` のすべての要素が `u` と等しいなら、`x` は `u` の単集合である、と。`pair-char` は二つの成分について同様のことを言い、「すべての要素」の節が命題的に切り詰められた選言になるだけです。どちらの結論も集合間のパスであり、後でどちらも読解式 `prAt` が表す節をちょうど供給します。

```agda
    (pairing-ax u v y .snd ∣ inl e ∣₁)

∈pair-introR : {u v y : V ℓ} → y ≡ v → ⟨ y ∈ ⁅ u , v ⁆ ⟩
∈pair-introR {u} {v} {y} e = ∈∈ₛ {a = y} {b = ⁅ u , v ⁆} .snd
    (pairing-ax u v y .snd ∣ inr e ∣₁)

sgl-char : (x u : V ℓ) → ⟨ u ∈ x ⟩ → ((y : V ℓ) → ⟨ y ∈ x ⟩ → y ≡ u) → x ≡ ⁅ u ⁆s
```

二つの所属の仮定から `x ≡ ⁅ u ⁆s` を証明するには、外延性を点ごとに適用します。各 `y` について、命題 `⟨ y ∈ x ⟩` を `⟨ y ∈ ⁅ u ⁆s ⟩` と結ぶパスが必要であり、`⇔toPath` は同値からまさにそのようなパスを作ります。順方向は「`x` のすべての要素は `u` に等しい」という仮定を使い、その後で単集合への所属を再導入します。これが `sub₁` です。

```agda
sgl-char x u hu hall = extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))
  where
  sub₁ : (y : V ℓ) → ⟨ y ∈ x ⟩ → ⟨ y ∈ ⁅ u ⁆s ⟩
  sub₁ y hy = ∈sgl-intro (hall y hy)
  sub₂ : (y : V ℓ) → ⟨ y ∈ ⁅ u ⁆s ⟩ → ⟨ y ∈ x ⟩
```

逆向きの `sub₂` は単集合への所属から出発し、`x` への所属を作らねばなりません。消去がパス `y ≡ u` を与え、その逆方向に所属が輸送されます。`u` が `x` に属し、`y` が `u` とパス一本分しか違わないなら、`y` も `x` に属する、というわけです。この「パスに沿った輸送」の型は、構成を直接比較する代わりの標準的な手段であり、本章の残りのすべての証明で繰り返し現れます。両方向が揃えば、`⇔toPath` が点ごとの同値を組み立て、`extensionalV` がパス `x ≡ ⁅ u ⁆s` を返します。

```agda
  sub₂ y hy = subst (λ z → ⟨ z ∈ x ⟩) (sym (∈sgl-elim hy)) hu

pair-char : (x u v : V ℓ) → ⟨ u ∈ x ⟩ → ⟨ v ∈ x ⟩
          → ((y : V ℓ) → ⟨ y ∈ x ⟩ → ∥ (y ≡ u) ⊎ (y ≡ v) ∥₁)
          → x ≡ ⁅ u , v ⁆
pair-char x u v hu hv hall = extensionalV (λ y → ⇔toPath (sub₁ y) (sub₂ y))
```

`pair-char` の証明は同じ計画に従いますが、新しい特徴が一つあります。「すべての要素」の仮定は丸められているので、順方向の `sub₁` は `y` がどちらの側かでパターンマッチできません。代わりに、`PT.rec` で丸めを、実際に命題値である所属の命題 `⟨ y ∈ ⁅ u , v ⁆ ⟩` へ消去し、直和の二つの側で場合分けします。`u` に等しい要素は対に左から、`v` に等しい要素は右から入ります。これが命題的に切り詰められた選言の事実を用いる正しいやり方です。

```agda
  where
  sub₁ : (y : V ℓ) → ⟨ y ∈ x ⟩ → ⟨ y ∈ ⁅ u , v ⁆ ⟩
  sub₁ y hy = PT.rec ((y ∈ ⁅ u , v ⁆) .snd)
    (Sum.rec (∈pair-introL {u = u} {v = v}) (∈pair-introR {u = u} {v = v})) (hall y hy)
  sub₂ : (y : V ℓ) → ⟨ y ∈ ⁅ u , v ⁆ ⟩ → ⟨ y ∈ x ⟩
```

逆向きの `sub₂` はこれを鏡写しにします。`⁅ u , v ⁆` への所属から `∈pair-elim` で丸められた選言を得て、それを所属の命題 `⟨ y ∈ x ⟩` へ消去し、各分岐で取り戻したパスに沿って対応する仮定 `hu` か `hv` を逆方向へ輸送します。こうして `sub₁` と `sub₂` は、対の構成の分類だけを材料に `x` への所属を作り出し、`extensionalV` が点ごとの結果を `x ≡ ⁅ u , v ⁆` へ引き上げます。

```agda
  sub₂ y hy = PT.rec ((y ∈ x) .snd)
    (Sum.rec (λ e → subst (λ z → ⟨ z ∈ x ⟩) (sym e) hu)
             (λ e → subst (λ z → ⟨ z ∈ x ⟩) (sym e) hv)) (∈pair-elim hy)
```

## メタレベルの Kuratowski 対

読解式 `prAt` は、集合 `Q` について、`U` の単集合である要素をひとつ持ち、`U` と `W` の非順序対である要素をひとつ持ち、しかもすべての要素がこのどちらかである、と言います。この節は、まさにこの三つの条件が `Q` を Kuratowski 対 `pr U W = ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆` と等しくすること、およびその逆を証明します。下の二つの補助述語は条件を節ごとに記録し、その形は有界論理式の充足が展開されていく形とちょうど同じです。そのため、妥当性の節の意味論的補題は、仮定をここで証明したメタレベルの補題にそのまま渡すことができ、同じことを二度証明する必要がありません。

最初の述語 `SglOf U w` は、`w` が `U` の単集合であることを所属の言葉だけで述べます。`U` が `w` に属し、`w` に属する任意の `z` は打ち切りなしに `U` と等しい、ということです。二つ目の `PairOf U W w` は、`w` が非順序対であることを述べます。`U` と `W` がともに `w` に属し、すべての要素が命題的に切り詰められた形でこのどちらかである、つまり命題として丸められた選言です。両方がレベル `ℓ-suc ℓ` に住むのは、`V ℓ` のすべての集合を量化するのに一レベル必要で、それが意味論が真理値を取るレベルと同じだからです。

```agda
private
  SglOf : V ℓ → V ℓ → Type (ℓ-suc ℓ)
  SglOf U w = ⟨ U ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → z ≡ U)

  PairOf : V ℓ → V ℓ → V ℓ → Type (ℓ-suc ℓ)
  PairOf U W w =
```

パッケージは、前節の特徴付けを通して等号と結び付きます。`w` が `SglOf U` を持てば、その二つの成分はちょうど `sgl-char` の仮定であり、`sgl-char` はパス `w ≡ ⁅ U ⁆s` を返します。同様に `pair-char` は `PairOf` のパッケージを `w ≡ ⁅ U , W ⁆` に変えます。つまりパッケージは対応する構成との等号の証明書であり、`w` がどう作られたかを検査することなしに得られます。

```agda
    ⟨ U ∈ w ⟩ × (⟨ W ∈ w ⟩ × ((z : V ℓ) → ⟨ z ∈ w ⟩ → ∥ (z ≡ U) ⊎ (z ≡ W) ∥₁))

  sglOf→≡ : {U w : V ℓ} → SglOf U w → w ≡ ⁅ U ⁆s
  sglOf→≡ {U} {w} (hu , hall) = sgl-char w U hu hall

  pairOf→≡ : {U W w : V ℓ} → PairOf U W w → w ≡ ⁅ U , W ⁆
  pairOf→≡ {U} {W} {w} (hu , hv , hall) = pair-char w U W hu hv hall
```

逆向きのデータも存在します。構成そのものが自分のパッケージを持つのです。`⁅ U ⁆s` については、`U` の所属は反射パスでの `∈sgl-intro` から、すべての要素が `U` と等しいことは `∈sgl-elim` から従います。非順序対も、二つの導入と `∈pair-elim` を使って同様にパッケージされます。最後に、パッケージは集合 `w` についての命題値の型なので、集合間のパスに沿って輸送できます。`w ≡ ⁅ U ⁆s` からは、`⁅ U ⁆s` のパッケージをパスに沿って逆方向へ輸送して `SglOf U w` が得られます。

```agda
  sglOf⁅⁆ : (U : V ℓ) → SglOf U ⁅ U ⁆s
  sglOf⁅⁆ U = ∈sgl-intro refl , (λ z z∈ → ∈sgl-elim z∈)

  pairOf⁅⁆ : (U W : V ℓ) → PairOf U W ⁅ U , W ⁆
  pairOf⁅⁆ U W = ∈pair-introL refl , ∈pair-introR refl , (λ z z∈ → ∈pair-elim z∈)

  sglOf-subst : {U w : V ℓ} → w ≡ ⁅ U ⁆s → SglOf U w
```

パッケージが揃ったので、メタレベルの特徴付けを述べられます。`prChar-fwd` は三つの仮定を受け取り、パス `Q ≡ pr U W` という結論を出します。最初の二つは丸められた存在の主張です。`Q` のある要素 `w` が `SglOf U` を持つこと、`Q` のある要素 `w` が `PairOf U W` を持つことが、いずれも命題的に切り詰められた形で主張されます。三つ目は全称の節です。`Q` のすべての要素 `y` は、`U` の単集合か、`U` と `W` の対かのどちらかに命題的に切り詰められたります。`pr U W` の外側の集合は、順序づけられた成分を符号化する二つの要素を持つ非順序対であり、`Q` がその外側の対と等しいことを `pair-char` で示すことに注意してください。

```agda
  sglOf-subst {U} e = subst (SglOf U) (sym e) (sglOf⁅⁆ U)

  pairOf-subst : {U W w : V ℓ} → w ≡ ⁅ U , W ⁆ → PairOf U W w
  pairOf-subst {U} {W} e = subst (PairOf U W) (sym e) (pairOf⁅⁆ U W)

prChar-fwd : (Q U W : V ℓ)
  → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁
```

最初の二つの仮定は、それぞれ命題的に切り詰められた形で、`Q` の要素と、その要素が対応する構成と等しいことを証明するパッケージを与えます。丸めは、命題値である所属の命題 `⟨ ⁅ U ⁆s ∈ Q ⟩` か `⟨ ⁅ U , W ⁆ ∈ Q ⟩` へ消去されるので、witness の選び方を揃える必要はありません。各分岐の中で、パッケージはパス `w ≡ ⁅ U ⁆s` か `w ≡ ⁅ U , W ⁆` に変えられ、`w` の所属がそれに沿って輸送され、その構成の `Q` への所属が得られます。これは、`u` と `v` の場所に `⁅ U ⁆s` と `⁅ U , W ⁆` を置いた `pair-char` が要求する最初の二つの引数にちょうど相当します。

```agda
  → ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁
  → ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁)
  → Q ≡ pr U W
prChar-fwd Q U W h₁ h₂ h₃ = pair-char Q ⁅ U ⁆s ⁅ U , W ⁆
  (PT.rec ((⁅ U ⁆s ∈ Q) .snd)
```

全称の節には消去はまったく要りません。`Q` の各要素 `y` について、パッケージの丸められた選言を変換 `sglOf→≡` と `pairOf→≡` を通して写せば、`y` が命題的に切り詰められた形で `⁅ U ⁆s` か `⁅ U , W ⁆` に等しいという丸められた主張が得られます。これが `pair-char` の三つ目の引数です。その結論は `Q ≡ ⁅ ⁅ U ⁆s , ⁅ U , W ⁆ ⁆` であり、これは定義により `Q ≡ pr U W` です。逆向きの `prChar-bwd` は、Kuratowski 対そのものについて三つの仮定を提示するだけの作業です。

```agda
    (λ { (w , hw , h) → subst (λ z → ⟨ z ∈ Q ⟩) (sglOf→≡ h) hw }) h₁)
  (PT.rec ((⁅ U , W ⁆ ∈ Q) .snd)
    (λ { (w , hw , h) → subst (λ z → ⟨ z ∈ Q ⟩) (pairOf→≡ h) hw }) h₂)
  (λ y hy → PT.map (Sum.map sglOf→≡ pairOf→≡) (h₃ y hy))

prChar-bwd : (Q U W : V ℓ) → Q ≡ pr U W
```

パス `Q ≡ pr U W` が与えられれば、三つの仮定が順に作られます。補助の `inQ` は、パスの逆方向に沿って輸送することで、`pr U W` への所属を `Q` への所属に移し、三つの成分すべてがこれを使います。

```agda
  → (∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁)
  × ((∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁)
  × ((y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁))
prChar-bwd Q U W e = h₁ , h₂ , h₃
  where
```

一つ目の存在の主張は、`⁅ U ⁆s` そのものが証人になります。外側の対が第一成分を含むこと、つまり反射パスでの `∈pair-introL` の実例によって、それは `pr U W` に属し、`inQ` を通した輸送の後、この所属は `Q` の中で成り立ちます。`SglOf U` を持つことはパッケージ `sglOf⁅⁆` によります。二つ目は、`⁅ U , W ⁆`、`∈pair-introR`、`pairOf⁅⁆` に置き換えた同じ議論です。どちらも型が求めるとおり丸めで封入されます。対象が単なる存在の主張である以上、選んだ証人で十分です。

```agda
  inQ : {z : V ℓ} → ⟨ z ∈ pr U W ⟩ → ⟨ z ∈ Q ⟩
  inQ {z} h = subst (λ w → ⟨ z ∈ w ⟩) (sym e) h
  h₁ : ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × SglOf U w) ∥₁
  h₁ = ∣ ⁅ U ⁆s , (inQ (∈pair-introL refl) , sglOf⁅⁆ U) ∣₁
  h₂ : ∥ Σ[ w ∈ V ℓ ] (⟨ w ∈ Q ⟩ × PairOf U W w) ∥₁
```

全称の節は、対の構成の分類に帰着します。`Q` の要素 `y` について、パスに沿った輸送により `y` の `pr U W` への所属が得られ、`∈pair-elim` がそれを丸められた選言 `y ≡ ⁅ U ⁆s` か `y ≡ ⁅ U , W ⁆` に変えます。各側は輸送の補題 `sglOf-subst` と `pairOf-subst` によって対応するパッケージに引き上げられ、この対応はパスの選言をパッケージの選言へ写します。どちらの構成も展開されることは一度もありません。

```agda
  h₂ = ∣ ⁅ U , W ⁆ , (inQ (∈pair-introR refl) , pairOf⁅⁆ U W) ∣₁
  h₃ : (y : V ℓ) → ⟨ y ∈ Q ⟩ → ∥ SglOf U y ⊎ PairOf U W y ∥₁
  h₃ y y∈Q = PT.map (Sum.rec (λ q → inl (sglOf-subst q)) (λ q → inr (pairOf-subst q)))
    (∈pair-elim (subst (λ w → ⟨ y ∈ w ⟩) e y∈Q))
```

## 対象言語の読解式

外側の特徴付けを、対象言語の論理式にします。各読解式は、それが語る de Bruijn 位置を引数として取るので、同じ定義を任意の入れ子の深さで使えます。有界量化の簿記は標準的なものです。有界量化子は位置ゼロに新しい変数を束縛し、既存の位置を一つ外へずらします。束縛の下で言及される位置はその後者として現れるわけです。すべての節が原子、連言か選言、あるいは環境の変数で限られた量化子であるため、各読解式は Δ₀ であり、その界定集合は形から直接読めます。

単集合の読解式 `sglAt k i` は、位置 `k` と `i` に割り当てられた集合について、`i` のものが `k` のものの単集合であると言います。第一の連言支は原子 `var i ∈̇ var k` です。第二の支は `var k` の要素の上で有界に量化し、その内側で、位置ゼロに新しく束縛された変数を `var (suc i)` と比較します。後者は、束縛の下で一段ずらされた後の位置 `i` です。ある集合がこの読解を充足するのは、`k` の値と等しい要素をひとつ持ち、ほかに要素を持たないとき、かつそのときに限ります。これが `SglOf` の内容です。

```agda
sglAt : ∀ {n} → Fin n → Fin n → Formula (V ℓ) n
sglAt k i = (var i ∈̇ var k) ∧̇ (∀̇∈ (var k) (var zero ≐ var (suc i)))
```

非順序対の読解式 `pairAt k i j` は第二の成分を加え、全称の節を選言に弱めます。有界量化子の下では、位置ゼロの新しい変数が、ずらされた二つの引数位置 `var (suc i)` と `var (suc j)` のどちらとも比較されます。外側から読めば、`i` と `j` の値がともに属し、すべての要素が命題的に切り詰められた形でそのどちらかと等しいときに充足されます。これはパッケージ `PairOf` そのものです。`_∧̇_` と `_∨̇_` の結合の宣言はこれらの式の構文解析だけを制御するもので、結合子の結合律を主張するものではないことに注意してください。

```agda
pairAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n
pairAt k i j = (var i ∈̇ var k) ∧̇ ((var j ∈̇ var k)
            ∧̇ (∀̇∈ (var k) ((var zero ≐ var (suc i)) ∨̇ (var zero ≐ var (suc j)))))
```

組み立てられた対の読解式は、二つの小さな読解式を、メタレベルの特徴付けの三つの節とともにまとめます。ある要素が単集合であること、ある要素が対であること、そしてすべての要素がそのどちらかであることです。各有界量化子は `q` の値の要素の上で限られ、二つの引数位置は束縛の下で一つずつずれるので、内側の読解式はやはり新しい変数を位置ゼロとして参照します。

第一の節は、`var q` の要素の上に存在量化を限り、その本体を `sglAt zero (suc u)` とします。位置ゼロの新しい変数が候補の要素であり、`suc u` は一段ずれた後の `u` の位置です。第二の節は `pairAt` で同じことを行い、今度はずれた後の `u` と `v` 両方の位置に言及します。第三の節は全称量化子を限り、その本体が二つの読解式の選言です。`q` の値のすべての要素は、命題的に切り詰められた形で単集合か対のどちらかです。存在の証人も「どちらか一方」という分類も、`SglOf` と `PairOf` とまったく同じく命題として丸められたままです。対象言語は要素を選ばず、ひとつ命題的に切り詰められた形で存在することしか言いません。

```agda
prAt : ∀ {n} → Fin n → Fin n → Fin n → Formula (V ℓ) n
prAt q u v = (∃̇∈ (var q) (sglAt zero (suc u)))
          ∧̇ ((∃̇∈ (var q) (pairAt zero (suc u) (suc v)))
          ∧̇ (∀̇∈ (var q) (sglAt zero (suc u) ∨̇ pairAt zero (suc u) (suc v))))

Δ₀-prAt : ∀ {n} (q u v : Fin n) → Δ₀ (prAt q u v)
```

有界性は構文的に証明書を与えられます。検査器 `checkΔ₀` が組み立てられた論理式をたどり、すべての節点が原子、結合子、あるいは変数で限られた量化子であるため、自明な証明書 `tt` とともに受理され、`Δ₀-prAt` が得られます。これでこの読解式は有界なクラスに属し、その充足は推移的モデルの間で絶対的です。後の絶対性に関する章が依拠するのはこの事実です。

```agda
Δ₀-prAt q u v = checkΔ₀ (prAt q u v) tt
```

## 妥当性

最後の定理が、対象言語の読解式とその外側の意味を結び付けます。充足は `hProp` に値を持つので、この主張そのものが真理値の間のパスです。命題 `γ ⊨ prAt q u v` は、「`q` の値が `u` と `v` の値の Kuratowski 対と等しい」という命題と同一視されます。等号の型が命題であることの証明は、`V ℓ` が h-集合であることから付きます。三つの結合子と有界量化子の充足を展開すると、左辺はちょうど `prChar-fwd` と `prChar-bwd` が受け取る三つの仮定になります。したがって妥当性の証明は、既にある二つの議論を組み合わせるだけで、新しいことを証明するのではありません。

示されたパスの両辺はともに真理値です。右辺では、等号の型 `⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ)` に `setIsSet _ _` が組にされます。後者は、h-集合の二つの要素の等号が命題であることの証明です。この組がまさに `hProp` の作り方です。証明はその後、根底にある同値の二方向を与え、`⇔toPath` がそれらを命題の間のパスへ引き上げます。

```agda
prAt-adequate : ∀ {n} (q u v : Fin n) (γ : (V ℓ) ^ n)
              → (γ ⊨ prAt q u v) ≡ ((⟦ var q ⟧ γ ≡ pr (⟦ var u ⟧ γ) (⟦ var v ⟧ γ))
                                   , setIsSet _ _)
prAt-adequate q u v γ = ⇔toPath
  (λ { (h₁ , h₂ , h₃) → prChar-fwd _ _ _ h₁ h₂ h₃ })
```

順方向は `prAt q u v` の充足を受け取ります。`_∧̇_` と有界な `∃̇∈`、`∀̇∈` の意味論により、それは三つ組です。単集合の読解を満たす要素の丸められた存在、対の読解を満たす要素の丸められた存在、そして全称の節です。これらはちょうど `prChar-fwd` の三つの引数であり、`pr U W` へのパスを返します。逆向きは等号のパスを受け取り、`prChar-bwd` に渡します。後者はそれを、意味論が充足へと組み立て直す三つの節にパッケージします。どちらの方向でも、集合がどう構成されたかを検査することは一切ありません。

```agda
  (λ e → prChar-bwd _ _ _ e)
```

## まとめ

`prAt` は対象言語の内部から Kuratowski 対を読み取ります。それは Δ₀ であり、かつ妥当です。その充足は、割り当てられた値の `pr` との等号へのパスになっています。コードを分解するために証明書が必要とする情報は、いまやすべて有界な形で利用でき、再帰もコード値の比較も使いません。続く章は、これらの読解式の上に証明書を構築していきます。