---
title: "すべての論理式の符号からなる集合"
module: L.Coding.CodeSet
lang: ja
site: "Bedrock"
description: "すべての論理式の符号からなる集合"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 61
canonical: https://bedrock.institute/ja/L.Coding.CodeSet.html
html: L.Coding.CodeSet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/CodeSet.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, FOL.ZFModel, V.Hierarchy, V.Coding, L.Constructible, L.Recursion, L.Axioms.Full, L.Axioms.Numerals, L.Axioms.Infinity, L.Coding.Model, L.Coding.Expressions, L.Coding.Closure, L.Coding.CodeConstructibility, L.Coding.SubformulaClosure, L.Coding.CodeShape, L.Coding.FormulaRecovery]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.CodeSet.md, https://bedrock.institute/zh/L.Coding.CodeSet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# すべての論理式の符号からなる集合

閉じた符号の定義域を用いて、必要な形と閉性の証人を持つすべてのアリティの論理式の符号をちょうど含む、一つの構成可能集合を分出します。所属定理は、符号、アリティの数項、復号された論理式を相互に結びます。

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Coding.CodeSet {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; ∃̇_ )
open import FOL.Manipulation.ConstantMapping using ( mapFo )
import FOL.Absoluteness
import FOL.ZFModel
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( smallDom )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ; ω-specL )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate )
open import L.Coding.Expressions {ℓ} using ( tagAtL; tagAtL-adequate )
open import L.Coding.Closure {ℓ} using ( closedAt )
open import L.Coding.CodeConstructibility {ℓ} using ( key; keyL; codeL; key∈closure )
open import L.Coding.SubformulaClosure {ℓ} using ( clo; closureClosed )
open import L.Coding.CodeShape {ℓ} using ( shapedAt; closureShaped )
open import L.Coding.FormulaRecovery {ℓ} using ( keyOf-fst; module Decode )

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ; ∈ₛ⟪_⟫↪_; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( SetOf )

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

## 指定したアリティのキー

`keyArityAtL` は、与えられた集合が指定したアリティの論理式の構成子キーであることを表します。タグ読取式の妥当性を存在量化子の内側で使うことで、導入則と除去則が対象言語の充足関係と外部のキー証人を正確に対応させます。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The equation is discharged with the index, the numeral and the environment all
still variables; keeping them as variables is what avoids the extra
conversion-checking overhead that later instantiation would otherwise incur.

</details>

```agda
keyArityAtL : ∀ {n} → Fin n → ℕ → Formula S n
keyArityAtL c k = ∃̇ (tagAtL (suc c) k zero)

keyArityAtL-out : ∀ {n} (c : Fin n) (k : ℕ) (γ : S ^ n)
                → ⟨ γ ⊨ keyArityAtL c k ⟩
                → ∥ (Σ[ z ∈ S ] (fst (lookup c γ) ≡ pr (# k) (fst z))) ∥₁
keyArityAtL-out c k γ = PT.map
  (λ { (z , hz) →
    z , subst ⟨_⟩ (tagAtL-adequate (suc c) k zero (z ∷ γ)) hz })

keyArityAtL-in : ∀ {n} (c : Fin n) (k : ℕ) (γ : S ^ n) (z : S)
               → fst (lookup c γ) ≡ pr (# k) (fst z)
               → ⟨ γ ⊨ keyArityAtL c k ⟩
keyArityAtL-in c k γ z e =
  ∣ z , subst ⟨_⟩ (sym (tagAtL-adequate (suc c) k zero (z ∷ γ))) e ∣₁
```

## あるアリティのキー

アリティを指定せずに、ある自然数のアリティでキーとなることを存在量化します。`arityNumAtL` はそのアリティを有限数項として読み書きします。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Stating it takes one constant. `ωʟ` is an element of `L` whose members are
exactly the numerals, so "the arity component lies in `ωʟ`" *is* the
condition, written with the same unbounded membership the second conjunct already
uses. The whole formula has two existentials, one for the arity and one for the
payload, the pair reader between them, and the membership on the arity.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Reading it in the other direction is where the choice takes effect.
`ω-specL` is an equation between propositions, not an implication, so a
member of `ωʟ` *is* a truncated natural number, and one composition with the
chain's projection equation turns it into the metalevel `# m` that
`recover` takes as its arity argument. Neither direction needs induction;
the numeral chapter already did that work.

</details>

```agda
arityNumAtL : ∀ {n} → Fin n → Formula S n
arityNumAtL c = ∃̇ (∃̇ (prAtL (suc (suc c)) (suc zero) zero
                     ∧̇ (var (suc zero) ∈̇ con ωʟ)))

arityNumAtL-out : ∀ {n} (c : Fin n) (γ : S ^ n)
                → ⟨ γ ⊨ arityNumAtL c ⟩
                → ∥ (Σ[ m ∈ ℕ ] Σ[ z ∈ S ]
                      (fst (lookup c γ) ≡ pr (# m) (fst z))) ∥₁
arityNumAtL-out c γ = PT.rec squash₁ (λ { (ar , h) →
  PT.rec squash₁ (λ { (z , (hp , hω)) → PT.map
    (λ { (m , qm) → lower m , z
       , ( subst ⟨_⟩
             (prAtL-adequate (suc (suc c)) (suc zero) zero (z ∷ ar ∷ γ)) hp
         ∙ cong (λ w → pr w (fst z)) (qm ∙ numeralL-fst (lower m)) ) })
    (subst ⟨_⟩ (ω-specL ar) hω) }) h })

arityNumAtL-in : ∀ {n} (c : Fin n) (γ : S ^ n) (m : ℕ) (z : S)
               → fst (lookup c γ) ≡ pr (# m) (fst z)
               → ⟨ γ ⊨ arityNumAtL c ⟩
arityNumAtL-in c γ m z e = ∣ numeralL m , ∣ z
  , ( subst ⟨_⟩ (sym (prAtL-adequate (suc (suc c)) (suc zero) zero
        (z ∷ numeralL m ∷ γ)))
        (e ∙ cong (λ w → pr w (fst z)) (sym (numeralL-fst m)))
    , subst ⟨_⟩ (sym (ω-specL (numeralL m))) ∣ lift m , refl ∣₁ ) ∣₁ ∣₁
```

## 符号を選ぶ述語

全体の符号集合を定める述語は、候補があるアリティのキーであり、閉じた符号領域に対応する形と復号証人を持つことを要求します。これにより異なるアリティの符号を一つの式で扱えます。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Nothing in the second conjunct is bounded, and nothing has to be. The witness is
produced from a formula's own subformula closure in the introduction, and
consumed as a set of `L` in the elimination, and the class model is where both
readings happen.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The second conjunct is written twice: once at two slots, the carrier and the
argument, and once with the carrier pinned to a constant. The general one is a
single existential, for the set; the pinned one wraps it in the binder that names
`A`, and that binder is the entire difference between them.

</details>

```agda
hasWitnessAt : ∀ {n} → Fin n → Fin n → Formula S n
hasWitnessAt A x = ∃̇ ((var (suc x) ∈̇ var zero)
                      ∧̇ (closedAt zero ∧̇ shapedAt zero (suc A)))

hasWitness : S → Formula S 1
hasWitness A = ∃̇ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero))

isCodeAny : S → Formula S 1
isCodeAny A = arityNumAtL zero ∧̇ hasWitness A
```

## 上位集合と分出された集合

まずすべての候補と証人を含む構成可能な上位集合を作り、その中で符号述語による分出を行います。結果として、すべてのアリティの論理式符号を含む一つの集合が得られます。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Then the superset. `smallDom` asks for a small family of elements of `L`
and returns a stage containing all of it; the family is indexed by the pairs of
an arity and a formula at it. The type is of the right size because syntax is an
inductive type at the alphabet's own level, and the arity is a natural number,
which costs no level at all. What comes back contains every key and much else,
and separation removes the else.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The set is sealed where it is built. Unsealed, every later type mentioning it
would carry the separation instrument's unfolding into conversion, and the facts
exported here are all any consumer needs. Only the ones that read a separation
are inside a seal; the directions back and the equations they compose into are
outside, since none of them needs to know what the set was cut out of.

</details>

```agda
module _ (A : S) where
  private
    ι : ⟪ fst A ⟫ → V ℓ
    ι = ⟪ fst A ⟫↪

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

    ιL : (m : ⟪ fst A ⟫) → ⟨ isL (ι m) ⟩
    ιL m = isL-trans {x = fst A} {y = ι m} (ι∈ m) (A .snd)

  codeS : ∀ {n} → Formula ⟪ fst A ⟫ n → S
  codeS φ = VCode.⌜ mapFo ι φ ⌝ , codeL ι ιL φ

  keyS : ∀ {n} → Formula ⟪ fst A ⟫ n → S
  keyS φ = key ι ιL φ , keyL ι ιL φ

  private
    smallAny : Σ[ d ∈ S ] ((p : Σ[ n ∈ ℕ ] Formula ⟪ fst A ⟫ n)
                          → ⟨ keyS (snd p) ∈ˢ d ⟩)
    smallAny = smallDom (Σ[ n ∈ ℕ ] Formula ⟪ fst A ⟫ n) (λ p → keyS (snd p))

    sepAny : isContr
      (SetOf (λ x → (x ∈ˢ smallAny .fst) ⊓ ((x ∷ []) ⊨ isCodeAny A)))
    sepAny = hasSeparationL (smallAny .fst) (isCodeAny A)
```

## 証人の導入と除去

符号集合への所属から、アリティ、論理式、形、閉性の証人を取り出せます。逆にこれらのデータから所属を構成できるため、内部集合は外部の符号概念を正確に表します。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Introduction is the half that adds nothing beyond what is given. The witness is the subformula
closure, whose three obligations are `key∈closure`, `closureClosed`
and `closureShaped`, one chapter each and all already discharged. The last
of them asks for one thing more, that every constant is a member of the carrier,
and at this alphabet that is the fact the alphabet was defined by, carried across
the slot's equation.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

Elimination is the other half, and it starts from the member already in key form
at a stated arity, which is what `recover` demands and what nothing in the
second conjunct would supply. The carrier slot's equation turns a membership in
whatever that slot holds into a membership in `A`, which is what makes the
decode's hypothesis dischargeable: `A`'s members are exactly the image of
`⟪ A ⟫`, by the presentation of a set by its own members. Read the existential
and a closed, shaped set arrives with it. Then the decode runs, and its answer is
a formula over the carrier, at the arity it was handed.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The pinned pair is these two at the environment the naming binder makes, and
that is the whole of what pinning costs: introduction supplies `A` for the binder
and `refl` for its equation, elimination reads the binder off and hands
what it holds to the general form. **Reading it off is where the payload has to
be named.** Left to inference, the truncation's payload at a pinned carrier is a
metavariable standing for the satisfaction of a formula the elaborator has not
committed to, and the same two lines that check in two seconds with the type
written out ran past 140 seconds without it and were killed there. This is the
law the recursion's totality hypothesis recorded, met again in a different place:
it is not about the graph, it is about `PT.rec` at a concrete environment.

</details>

```agda
  witnessAt-in : ∀ {n k} (b c : Fin n) (γ : S ^ n) (φ : Formula ⟪ fst A ⟫ k)
               → fst (lookup b γ) ≡ fst A
               → fst (lookup c γ) ≡ fst (keyS φ)
               → ⟨ γ ⊨ hasWitnessAt b c ⟩
  witnessAt-in b c γ φ qb qc = ∣ clo ι ιL φ
    , ( subst (λ w → ⟨ w ∈ fst (clo ι ιL φ) ⟩) (sym qc) (key∈closure ι ιL φ)
      , ( closureClosed ι ιL φ γ
        , closureShaped ι ιL φ b γ
            (λ m → subst (λ w → ⟨ ι m ∈ w ⟩) (sym qb) (ι∈ m)) ) ) ∣₁

  witnessAt-out : ∀ {n} (b c : Fin n) (γ : S ^ n)
                → fst (lookup b γ) ≡ fst A
                → ⟨ γ ⊨ hasWitnessAt b c ⟩
                → (k : ℕ) (z : S) → fst (lookup c γ) ≡ pr (# k) (fst z)
                → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ]
                      (fst (lookup c γ) ≡ fst (keyS ψ))) ∥₁
  witnessAt-out b c γ qb hw k z qz = PT.rec squash₁ viaSlot hw
    where
    Target : Type (ℓ-suc ℓ)
    Target = ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ]
                 (fst (lookup c γ) ≡ fst (keyS ψ))) ∥₁

    onto : (y : V ℓ) → ⟨ y ∈ fst (lookup b γ) ⟩
         → ∥ Σ[ m ∈ ⟪ fst A ⟫ ] (ι m ≡ y) ∥₁
    onto y y∈ = ∣ ∈-asFiber {a = y} {b = fst A}
      (subst (λ w → ⟨ y ∈ w ⟩) qb y∈) ∣₁

    viaSlot : Σ[ C ∈ S ] ⟨ (C ∷ γ) ⊨ ((var (suc c) ∈̇ var zero)
                ∧̇ (closedAt zero ∧̇ shapedAt zero (suc b))) ⟩
            → Target
    viaSlot (C , (x∈C , (hcl , hsh))) = PT.map
      (λ { (ψ , qψ) → ψ , (qz ∙ cong (pr (# k)) (sym qψ)) })
      (Decode.recover ι zero (suc b) (C ∷ γ) onto hcl hsh k z
        (subst (λ w → ⟨ w ∈ fst C ⟩) (qz ∙ sym (keyOf-fst k z)) x∈C))

  private
    witness-in : ∀ {n} (φ : Formula ⟪ fst A ⟫ n)
               → ⟨ (keyS φ ∷ []) ⊨ hasWitness A ⟩
    witness-in φ = ∣ A , ( refl
      , witnessAt-in zero (suc zero) (A ∷ keyS φ ∷ []) φ refl refl ) ∣₁

    witness-out : (x : S) → ⟨ (x ∷ []) ⊨ hasWitness A ⟩
                → (k : ℕ) (z : S) → fst x ≡ pr (# k) (fst z)
                → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst x ≡ fst (keyS ψ))) ∥₁
    witness-out x hw k z qz = PT.rec squash₁ viaCarrier hw
      where
      viaCarrier : Σ[ B ∈ S ] ⟨ (B ∷ x ∷ [])
                     ⊨ ((var zero ≐ con A) ∧̇ hasWitnessAt zero (suc zero)) ⟩
                 → ∥ (Σ[ ψ ∈ Formula ⟪ fst A ⟫ k ] (fst x ≡ fst (keyS ψ))) ∥₁
      viaCarrier (B , (qB , hB)) =
        witnessAt-out zero (suc zero) (B ∷ x ∷ []) qB hB k z qz
```

## 各アリティでの符号集合

アリティ `n` を固定すると、`n` 変数のすべての論理式の符号が全体の符号集合に属します。また所属する `n`-項のキーから対応する論理式を復号できます。

```agda
  IsKeyOverAny : S → hProp (ℓ-suc ℓ)
  IsKeyOverAny x =
    ∥ (Σ[ n ∈ ℕ ] Σ[ ψ ∈ Formula ⟪ fst A ⟫ n ] (fst x ≡ fst (keyS ψ))) ∥₁
    , squash₁

  opaque
    AllCodes : S
    AllCodes = sepAny .fst .fst

    key∈AllCodes : ∀ {n} (φ : Formula ⟪ fst A ⟫ n) → ⟨ keyS φ ∈ˢ AllCodes ⟩
    key∈AllCodes {n} φ = subst ⟨_⟩ (sym (sepAny .fst .snd (keyS φ)))
      ( smallAny .snd (n , φ)
      , ( arityNumAtL-in zero (keyS φ ∷ []) n (codeS φ) refl
        , witness-in φ ) )

    AllCodes-out : (x : S) → ⟨ x ∈ˢ AllCodes ⟩ → ⟨ IsKeyOverAny x ⟩
    AllCodes-out x x∈ = PT.rec squash₁
      (λ { (k , z , qz) → PT.map (λ { (ψ , q) → k , ψ , q })
        (witness-out x (sat .snd) k z qz) })
      (arityNumAtL-out zero (x ∷ []) (sat .fst))
      where
      sat : ⟨ (x ∷ []) ⊨ isCodeAny A ⟩
      sat = subst ⟨_⟩ (sepAny .fst .snd x) x∈ .snd

  AllCodes-in : (x : S) → ⟨ IsKeyOverAny x ⟩ → ⟨ x ∈ˢ AllCodes ⟩
  AllCodes-in x = PT.rec (snd (x ∈ˢ AllCodes))
    (λ { (n , ψ , q) →
      subst (λ w → ⟨ w ∈ fst AllCodes ⟩) (sym q) (key∈AllCodes ψ) })
```

## まとめ

一つの構成可能集合が、すべてのアリティの整形式な論理式符号を集めます。所属の導入・除去定理により、符号、有限数項としてのアリティ、復号された論理式を相互に移せます。

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The whole content is in two conjuncts, and both are of the same kind. Closedness
and shapedness together recognize the *shape* of a code and say nothing about the
arity a key carries or the alphabet its constants come from, so a decode written
against them has to be handed both, and a set built from them has to state both.
`smallDom` and general-formula separation do the rest, and neither needed
anything the earlier chapters had not already established.

</details>

<details class="localized-fallback" lang="en">
<summary lang="ja">英語原文</summary>

The set exists for the *class* it characterizes, not for a theorem about it. A
recursion over codes has to answer at a code's subcodes, a quantifier's
subformula lives one arity up, and the arity-one class does not contain it, so
the domain has to be the keys at every arity.

</details>