---
title: "部分式についての閉包"
module: L.Coding.SubformulaClosure
lang: ja
site: "Bedrock"
description: "部分式についての閉包"
stage: "内部の符号化：式と定義域"
reading_order: 47
canonical: https://bedrock.institute/ja/L.Coding.SubformulaClosure.html
html: L.Coding.SubformulaClosure.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SubformulaClosure.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Closure, L.Coding.CodeConstructibility]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.SubformulaClosure.md, https://bedrock.institute/zh/L.Coding.SubformulaClosure.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 部分式についての閉包

論理式コード上の再帰には、各構成子が要求する直接の部分式の鍵を含む添字集合が必要です。本章では、まず `Peel` 性をもつ任意の集合について対象言語の七つの閉包条件を証明し、次に論理式の実際の部分式閉包へ適用します。

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

The proof is short because the two halves it needs were built to meet here. An
element of the closure is the key of a formula, and it brings a closure of its
own that sits inside; a key of a given constructor shape has known subkeys, and
which ones is computed from the shape's tag. So each of the seven clauses is the
same four moves: take the element apart, read its tag, ask what that tag demands,
and hand back what the formula's own closure already contains.

</details>

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

open import Base.Prelude

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( 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.Coding.Closure {ℓ} using ( closedAt; binShapeAt; unShapeAt; bothSameAt; oneSameAt; oneSuccAt; succSndAt; binSameClosed-in; unSameClosed-in; unSuccClosed-in; binSuccClosed-in )
open import L.Coding.CodeConstructibility {ℓ}
  using ( closure; closureL; closure-inv; byTag; Concl; key )

open import Cubical.Foundations.HLevels using ( isProp× )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

open hPropStructure 𝒮ʟ using ( S )

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

## モデルの要素としての閉包

`clo φ` は外側で構成した集合 `closure f h φ` とその構成可能性の証明を組み合わせ、`closedAt` を評価できる `L` の要素にします。

```agda
module _ {K : Type ℓ} (f : K → V ℓ) (h : (k : K) → ⟨ isL (f k) ⟩) where
  private
    Cl : ∀ {n} → Formula K n → V ℓ
    Cl = closure f h

  clo : ∀ {n} → Formula K n → S
  clo φ = closure f h φ , closureL f h φ
```

## 部分式の鍵を復元する

`Peel C` は、`C` の各要素がある論理式の鍵であり、その論理式自身の閉包が `C` に含まれることを表します。これは構成子のタグが要求する直接の部分式の鍵を復元するために必要な情報そのものです。

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

Stating it separately is not tidiness. A later chapter cuts a set of codes out of
a stage and has to prove the same closedness for it, and that set is not a
closure of anything; what it has instead is a characterization of its members as
keys, and `Peel` is what a characterization turns into. So the seven
clauses are proved once, for any set that peels, and the closure is the first of
the two instances rather than the subject.

</details>

```agda
  Peel : V ℓ → Type (ℓ-suc ℓ)
  Peel C = (x : V ℓ) → ⟨ x ∈ C ⟩
         → ∥ (Σ[ m ∈ ℕ ] Σ[ ψ ∈ Formula K m ]
               ((x ≡ key f h ψ) × ((z : V ℓ) → ⟨ z ∈ Cl ψ ⟩ → ⟨ z ∈ C ⟩))) ∥₁
```

## 七つの閉包節

補助構成 `same`、`one`、`up`、`sndUp` は、取り出した論理式の鍵を、二項、単項、アリティを増やす構成子、有界量化子が要求する部分鍵へ変換します。七つのタグへの適用が七つの閉包条件を証明します。

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

The truncation that peeling returns is eliminated straight away, which is allowed
because what is being produced is a membership, or a pair of them, and membership
is a proposition.

</details>

```agda
  module _ (D : S) (peel : Peel (fst D)) where
    private
      C : V ℓ
      C = fst D

      viaKey : (k : ℕ) (c : S) (ar p : V ℓ)
             → ⟨ fst c ∈ C ⟩ → fst c ≡ pr ar (pr (# k) p)
             → (T : Type (ℓ-suc ℓ)) → isProp T
             → (Concl f h C k ar p → T) → T
      viaKey k c ar p c∈ sh T pT g = PT.rec pT
        (λ { (m , ψ , q , incl) →
          g (byTag f h C ψ k ar p incl (sym q ∙ sh)) })
        (peel (fst c) c∈)

      same : ∀ {m} (γ : S ^ m) (k : ℕ)
           → ((ar a b : V ℓ) → Concl f h C k ar (pr a b)
              → ⟨ pr ar a ∈ C ⟩ × ⟨ pr ar b ∈ C ⟩)
           → ⟨ (D ∷ γ) ⊨ binShapeAt zero k (bothSameAt zero) ⟩
      same γ k use = binSameClosed-in zero k (D ∷ γ)
        (λ c ar a b c∈ sh →
          viaKey k c (fst ar) (pr (fst a) (fst b)) c∈ sh _
            (isProp× (snd (pr (fst ar) (fst a) ∈ C))
                     (snd (pr (fst ar) (fst b) ∈ C)))
            (use (fst ar) (fst a) (fst b)))

      one : ∀ {m} (γ : S ^ m) (k : ℕ)
          → ((ar a : V ℓ) → Concl f h C k ar a → ⟨ pr ar a ∈ C ⟩)
          → ⟨ (D ∷ γ) ⊨ unShapeAt zero k (oneSameAt zero) ⟩
      one γ k use = unSameClosed-in zero k (D ∷ γ)
        (λ c ar a c∈ sh →
          viaKey k c (fst ar) (fst a) c∈ sh _
            (snd (pr (fst ar) (fst a) ∈ C)) (use (fst ar) (fst a)))

      up : ∀ {m} (γ : S ^ m) (k : ℕ)
         → ((ar a : V ℓ) → Concl f h C k ar a → ⟨ pr (sucV ar) a ∈ C ⟩)
         → ⟨ (D ∷ γ) ⊨ unShapeAt zero k (oneSuccAt zero) ⟩
      up γ k use = unSuccClosed-in zero k (D ∷ γ)
        (λ c ar a c∈ sh →
          viaKey k c (fst ar) (fst a) c∈ sh _
            (snd (pr (sucV (fst ar)) (fst a) ∈ C)) (use (fst ar) (fst a)))

      sndUp : ∀ {m} (γ : S ^ m) (k : ℕ)
            → ((ar a b : V ℓ) → Concl f h C k ar (pr a b)
               → ⟨ pr (sucV ar) b ∈ C ⟩)
            → ⟨ (D ∷ γ) ⊨ binShapeAt zero k (succSndAt zero) ⟩
      sndUp γ k use = binSuccClosed-in zero k (D ∷ γ)
        (λ c ar a b c∈ sh →
          viaKey k c (fst ar) (pr (fst a) (fst b)) c∈ sh _
            (snd (pr (sucV (fst ar)) (fst b) ∈ C))
            (use (fst ar) (fst a) (fst b)))
```

## 七つの節の連言

`closedOf` は七つのタグの適用を、台となる集合が `Peel` を満たす任意のモデル要素についての連言 `closedAt` にまとめます。`closureClosed` は `closure-inv` を渡して `clo φ` に対する結果を得ます。

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

`closureClosed` is then the instance at a closure, and its peeling is
`closure-inv` unchanged: the two statements are the same type, because
`Peel` was read off that lemma's conclusion.

</details>

```agda
    closedOf : ∀ {m} (γ : S ^ m) → ⟨ (D ∷ γ) ⊨ closedAt zero ⟩
    closedOf γ =
        same γ 2 (λ _ a b r → r a b refl)
      , ( same γ 3 (λ _ a b r → r a b refl)
      , ( same γ 4 (λ _ a b r → r a b refl)
      , ( up γ 6 (λ _ _ r → r)
      , ( up γ 7 (λ _ _ r → r)
      , ( sndUp γ 8 (λ _ a b r → r a b refl)
      , sndUp γ 9 (λ _ a b r → r a b refl) )))))

  closureClosed : ∀ {n m} (φ : Formula K n) (γ : S ^ m)
                → ⟨ (clo φ ∷ γ) ⊨ closedAt zero ⟩
  closureClosed φ γ = closedOf (clo φ) (closure-inv f h φ) γ
```

## まとめ

任意の Peel 性を持つ集合について closedOf が部分式閉包条件を証明し、closureClosed がそれを論理式の実際の閉包に適用する。内容は満足関係の値ではなく、各コード形が要求する部分鍵の包含である。

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

What it cost is worth recording, because the same shape is what the satisfaction
instance will pay. Four readers, seven lines of instantiation, and one lemma per
reader; the content is in `byTag` one chapter earlier, where the ten
constructors were matched against the seven demands once and for all rather than
ten times seven. `byTag` was already written against an arbitrary target
set, which is why generality here is free: the closure was never the subject, only
the first thing handed in.

</details>