---
title: "全コード上の一様な充足関係"
module: L.Coding.UniformSatisfaction
lang: ja
site: "Bedrock"
description: "全コード上の一様な充足関係"
stage: "内部の符号化：表と一様な充足関係"
reading_order: 68
canonical: https://bedrock.institute/ja/L.Coding.UniformSatisfaction.html
html: L.Coding.UniformSatisfaction.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/UniformSatisfaction.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Manipulation.Relabelling, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Definability, L.Coding.Model, L.Coding.Satisfaction, L.Coding.SatisfactionBridge, L.Coding.SatisfactionTable, L.Coding.SlotClosure, L.Coding.EnvironmentTower, L.Coding.Quantification, L.Coding.CodeDomain, L.Coding.PinnedRecursion, L.Coding.SatisfactionGraph, L.Coding.CodeSet, L.Recursion]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.UniformSatisfaction.md, https://bedrock.institute/zh/L.Coding.UniformSatisfaction.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 全コード上の一様な充足関係
`AllCodes A` 上の再帰により一つの充足関係の割当てを作り、各論理式の鍵での値がその論理式の明示的な充足関係表と一致することを示します。これにより論理式とアリティを越えて充足関係を一様に使えます。
英語原文
Consumers of internal satisfaction arrive holding a **code**, not the formula
from which it came. The internal definable powerset ranges over all arity-one
codes at a stage, while the well-order may compare codes that are not subcodes
of any common formula. The recursion therefore needs one table whose visible
domain is the whole stage code set. `AllCodes` supplies exactly those
keys, at every arity.
英語原文
The graph itself binds a table and a qualifying index set existentially. To show
that a member has a graph value, `funct` may use the member's own
subformula slot, whose closed, total, clause-satisfying table was certified by
the preceding coding chapters. Uniformity then says that these local witnesses
cohere into the value read from the whole code set.
英語原文
A second bridge is needed because the code set uses the **hierarchy's** coding
over a stage alphabet, whereas the recursive table uses the **model's** coding
over the model language. This chapter identifies the two presentations and
exports the uniform satisfaction table consumed by powerset and Choice.
```agda
{-# OPTIONS --cubical --safe --guardedness #-}
open import Base.Prelude
open import Base.Classical using ( LEM )
module L.Coding.UniformSatisfaction {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
open import FOL.Manipulation.ConstantMapping using ( mapFo; mapFo-comp )
open import FOL.Manipulation.Relabelling using ( ⊨-map )
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.Definability {ℓ} using ( module DefOf )
open import L.Coding.Model {ℓ} using ( domAt; domAt-intro; domAt-out )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )
open import L.Coding.SatisfactionBridge {ℓ} lem
using ( intoL; asConst; Sat-spec ) renaming ( graph to envGraph )
open import L.Coding.SatisfactionTable {ℓ} lem
using ( keyʟ; slot; satTable; total; inSlot; entry-in )
open import L.Coding.SlotClosure {ℓ} lem using ( slotClosed )
open import L.Coding.EnvironmentTower {ℓ} lem using ( towerAt; module Tower; module TowerHolds )
open import L.Coding.Quantification {ℓ} using ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9 )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SlotHolds ) renaming ( keyBridge to keyBridge' )
open import L.Coding.SatisfactionGraph {ℓ} lem using
( satGraph; graph-in; graph-out; Bi; Ti; Ci; Ei; NN; ev; numν; numTags )
open import L.Coding.CodeSet {ℓ} lem
using ( keyS; AllCodes; AllCodes-out; key∈AllCodes )
open import L.Recursion {ℓ} lem using ( Recursion; mereFunct; module Of )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Vec using ( _∷_; [] )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫ )
open hPropStructure 𝒮ʟ
module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```
## コード集合の要素を名づける
`AllCodes A` の仕様は任意の要素から、`A` の要素を定数とし、その要素を鍵にもつ論理式を得ます。`keyIn` は得られた鍵を再帰で使える `L` の要素として包装します。
英語原文
Three lines, and they are the only one-time decision in this chapter. A consumer that
wants the value at a particular formula has to name the member the value is taken
at, and the obvious name is the key itself; naming it that way does not
elaborate, because the key unfolds into a pair of a numeral with a code and that
construction then sits inside the recursion's domain and inside a satisfaction.
英語原文
So the name is made opaque where it is made. As an opaque definition, it is an
element of `L` that a type can mention without unfolding, and the two facts a
consumer needs come out with it: it lies in the domain, and it is the key of
the formula it was made from. Everything below is stated at a variable member and
reaches its key by an equation, so this opaque name is the only thing that
would need unfolding, and no step unfolds it.
```agda
module _ (A : S) where
opaque
keyIn : ∀ {n} → Formula ⟪ fst A ⟫ n → S
keyIn ψ = keyS A ψ
keyIn≡ : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) → fst (keyIn ψ) ≡ fst (keyS A ψ)
keyIn≡ ψ = refl
keyIn∈ : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n) → ⟨ keyIn ψ ∈ˢ AllCodes A ⟩
keyIn∈ ψ = key∈AllCodes A ψ
```
## 外側と内側の論理式の鍵を結ぶ
`keyBridge` は、`A` の要素を定数とする論理式を直接符号化した鍵と、定数を `L` へ移してからモデル内部で作った鍵の台が一致することを示します。続く枠組みはグラフ論理式に必要な数項タグ、塔、コード領域を固定します。
英語原文
A key in the hierarchy's coding is the arity numeral paired with the code of the
formula relabelled along the alphabet's embedding; a key in the model's coding is
the numeral of `L` paired with the code taken in `L`. `codeBridge` equates
the two codes, one clause per constructor. It was written in the model chapter
and has not been used since, because this is the statement it was written for.
英語原文
What it does not supply is the relabelling. The set's formulas are over the
alphabet `⟪ A ⟫` and the recursion's formulas are over `L`, so the two
sides pass through two different maps and their composite has to be recognized as
one map. That is functoriality of relabelling, which belongs where relabelling is
defined and is now there, so the whole bridge is four rewrites and no induction.
英語原文
The map into the model is not built here either. It is the bridge chapter's own
`asConst`, the alphabet's embedding followed by the class inclusion, and
taking that one rather than an equal one is what lets the last section quote the
adequacy without a translation step.
英語原文
The bridge takes the alphabet and nothing else. The set the environments range
over never appears in it, so it is stated one parameter short of the recursion
below, and a later chapter that needs the two codings to agree at a carrier held
in a slot can use it without supplying a second carrier it does not have.
```agda
module _ (A : S) where
keyBridge : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n)
→ fst (keyS A ψ) ≡ fst (keyʟ (mapFo (asConst A) ψ))
keyBridge = keyBridge' A
module _ (B : S) where
fr : ∀ {m n} (φ : Formula S m) (γ : S ^ n) → S ^ (14 + n)
fr φ γ = ev numν (Tower.tower B) (slot B φ) (satTable B φ) B γ
frTags : ∀ {m n} (φ : Formula S m) (γ : S ^ n) → Tags (fr φ γ) NN
frTags φ γ = numTags (Tower.tower B) (slot B φ) (satTable B φ) B γ
frTow : ∀ {m n} (φ : Formula S m) (γ : S ^ n) → ⟨ fr φ γ ⊨ towerAt Ei Bi (NN f0) ⟩
frTow φ γ = TowerHolds.holds Ei Bi (NN f0) (fr φ γ) B refl refl refl
frDom : ∀ {m n} (φ : Formula S m) (γ : S ^ n) → ⟨ fr φ γ ⊨ domAt Ti Ci ⟩
frDom φ γ = domAt-intro Ti Ci (fr φ γ)
(λ z → (λ h → PT.rec (snd (fst z ∈ fst (slot B φ)))
(λ { (w , hw) → inSlot B φ (fst z) (fst w) hw }) h)
, (λ h → total B φ (fst z) h))
module _ (A B : S) where
private
```
## 名づけられた論理式での存在と一意性
`AllCodes B` の要素が名づける論理式について、明示的な充足関係表は対応する鍵での出力を与えます。表の鍵による決定性定理はその鍵での任意の二出力が等しいことを示し、再帰に必要な存在と一意性を与えます。
英語原文
Both halves come from the previous chapters, applied at the formula the member
is the key of rather than at an ambient formula, and the change makes existence
*shorter*. The per-formula instance had to transport a subformula's entry along the
inclusion of its own subtree into the ambient table; here the recovered formula
**is** the formula whose table is being handed over, so `entry-in` applies
directly and the transport is gone.
英語原文
The change does not affect uniqueness at all, and the reason is structural.
`Pinned` speaks about the index set and the table the graph produced,
which are bound variables of the caller's environment, never about the
recursion's domain. The domain occurs nowhere in it, nor in the ten clauses,
so changing what the recursion is indexed by cannot reach uniqueness.
英語原文
Only the totality hypothesis is written out here, and its environment is written
out with it. Left to inference, the graph's three existentially bound slots
determine nothing and six metavariables survive; naming the environment costs one
line and is the difference between elaborating and not.
```agda
toB : ∀ {n} → Formula ⟪ fst B ⟫ n → Formula S n
toB = mapFo (asConst B)
exists : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) (x : S) → fst x ≡ fst (keyʟ (toB ψ))
→ ⟨ (Sat B (toB ψ) ∷ x ∷ []) ⊨ satGraph B ⟩
exists {n} ψ x k = graph-in B x (Sat B (toB ψ))
∣ numν
, (Tower.tower B
, (slot B (toB ψ)
, (satTable B (toB ψ)
, (B
, (refl
, (frTags B (toB ψ) δ2
, (frTow B (toB ψ) δ2
, (slotClosed B (toB ψ) (Tower.tower B ∷ numν f0 ∷ numν f1 ∷ numν f2 ∷ numν f3
∷ numν f4 ∷ numν f5 ∷ numν f6 ∷ numν f7 ∷ numν f8 ∷ numν f9 ∷ Sat B (toB ψ) ∷ x ∷ [])
, (frDom B (toB ψ) δ2
, (subst (λ w → ⟨ pr w (fst (Sat B (toB ψ))) ∈ fst (satTable B (toB ψ)) ⟩) (sym k)
(entry-in B (toB ψ))
, SlotHolds.holds B Ti Bi Ci Ei NN (fr B (toB ψ) δ2) refl
(frTags B (toB ψ) δ2) (frTow B (toB ψ) δ2) ψ refl refl)))))))))) ∣₁
where δ2 = Sat B (toB ψ) ∷ x ∷ []
unique : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) (x : S) → fst x ≡ fst (keyʟ (toB ψ))
→ (y : S) → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ → y ≡ Sat B (toB ψ)
unique {n} ψ x k y hy = Σ≡Prop (λ v → snd (isL v))
(PT.rec (setIsSet (fst y) (fst (Sat B (toB ψ))))
(λ { (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) →
SatSoundC.pinned Ti Bi Ci Ei NN (ev ν E C T b (y ∷ x ∷ [])) B eb tg hE hc h12
ψ (subst (λ u → ⟨ u ∈ fst C ⟩) (k ∙ sym (keyBridge' B ψ))
(domAt-out Ti Ci (ev ν E C T b (y ∷ x ∷ [])) hd x y ha)) y
(subst (λ u → ⟨ pr u (fst y) ∈ fst T ⟩) (k ∙ sym (keyBridge' B ψ)) ha) })
(graph-out B x y hy))
```
## 全コード集合上の再帰
`satRec` は `AllCodes B`、充足関係グラフ、部分式についての閉包性、前節の存在一意性の証明を用いて抽象的な再帰定理を具体化します。その値関数が以下で使う一様な充足関係の割当てです。
英語原文
The domain is the code set at the stage, the graph is the one two chapters back,
and `funct` is filled through `mereFunct`, because a merely existing
unique solution is a contractible one. A member arrives as a mere key of a
formula over the alphabet, the bridge turns its equation into one about the
model's key, and the two halves above are applied at that key.
英語原文
The two carriers are independent parameters and stay so. `A` is the alphabet the
codes' constants are drawn from; `B` is the set the environments range over;
nothing in the recursion relates them, and charging the recursion for a relation
it does not use would be stating a weaker theorem. They are pinned together in
the next section, and only there, because that is where satisfaction acquires a
meaning.
```agda
satRec : Recursion
Recursion.dom satRec = AllCodes B
Recursion.graph satRec = satGraph B
Recursion.funct satRec x x∈ = mereFunct (satGraph B) x
(PT.map
(λ { (n , ψ , q) → Sat B (toB ψ)
, ( exists ψ x (q ∙ keyBridge' B ψ)
, unique ψ x (q ∙ keyBridge' B ψ) ) })
(AllCodes-out B x x∈))
module Table = Of satRec
```
## 各再帰値を同定する
`val-at` は論理式の鍵での再帰値を、すでに各条件を満たすと分かっている明示的な `Sat` の値と同一視します。続く `val-sat` はその値への所属を、表された論理式が符号化環境の下で満たされることとして読みます。
英語原文
A recursion connected to nothing defines nothing, so the value is stated twice.
英語原文
Against the recursion's own construction first, and that is uniqueness spent in
the other direction: the value at a member that is the key of a formula is the
set the meta-level recursion built at that formula, because the existence half
exhibits that set as a solution and the recursion's value is the only solution.
This is the reading a consumer needs to get anything out of the table at all,
since the value function comes from a contractibility and computes to nothing on
its own.
英語原文
The member is a **variable** and its key is reached by an equation, and that is a
measurement, not a taste. Stated at the key itself, the value function's argument
is a concrete code construction, which puts that construction inside the graph
satisfaction the value is defined from; the statement that costs four seconds at
a variable ran past six minutes at the key and was abandoned, and so did the same
statement written as a corollary of the variable one, which shows the cost is in
the *statement* and not in the proof. The uniqueness chapter recorded this law at
its first case and it holds here unchanged.
英語原文
Nothing is lost, in either direction. A consumer holding a member holds it as a
member, with its key equation beside it; and a consumer that wants to *name* the
member gets the convenient form back through the sealed name, at no cost, because
what the type mentions there does not unfold.
```agda
val-at : ∀ {n} (ψ : Formula ⟪ fst B ⟫ n) (x : S) (x∈ : ⟨ x ∈ˢ AllCodes B ⟩)
→ fst x ≡ fst (keyS B ψ)
→ Table.val x x∈ ≡ Sat B (toB ψ)
val-at ψ x x∈ q =
Table.val-uniq x x∈ (Sat B (toB ψ)) (exists ψ x (q ∙ keyBridge' B ψ))
```
英語原文
And against satisfaction, which is the reason to have the goal. The bridge
chapter proved that a member of the meta-level value is an environment satisfying
the formula in the world `(B, ∈)`; composing it with the reading above says the
same of the table this recursion produces. At arity one it specializes to the
definable subset the definable powerset means, so **the table read at a member
that is the key of a formula is that formula's definable subset**, which is the
statement the internal hierarchy will read `Def` off.
英語原文
The two carriers meet here because this is where they have to. A formula whose
constants are members of the carrier is one the inner world can read; a formula
naming an arbitrary element of `L` is not, and the bridge chapter says so about
itself. So the two theorems below are stated at the one carrier, which is the
instantiation the consumer wants anyway: the codes at a stage, satisfied over
that same stage.
```agda
module _ (A : S) where
module DA = DefOf (fst A)
open DA using ( _⊨ᵐ_ )
val-sat : ∀ {n} (ψ : Formula ⟪ fst A ⟫ n)
(x : S) (x∈ : ⟨ x ∈ˢ AllCodes A ⟩) → fst x ≡ fst (keyS A ψ)
→ (δ : DA.SM ^ n) (z : S) → fst z ≡ envGraph A δ
→ (z ∈ˢ Table.val A A x x∈) ≡ (δ ⊨ᵐ ψ)
val-sat ψ x x∈ q δ z qz =
cong (z ∈ˢ_)
(val-at A A ψ x x∈ q ∙ cong (Sat A) (sym (mapFo-comp DA.ι (intoL A) ψ)))
∙ Sat-spec A (mapFo DA.ι ψ) δ z qz
∙ ⊨-map DA.𝒮M DA.ι id ψ δ
```
## まとめ
この構成により全論理式コード上の一つのグラフが得られ、`val-at` と `val-sat` により、その各値が単なる再帰方程式の解ではなく意図した充足集合であることが保証されます。
英語原文
`satRec` is satisfaction as an internalized recursion over **the codes at
a stage**, not over one formula's subformulas, and `Table` is the table it
yields. `val-at` reads a value out at a member given as a key, and
`val-sat` says that value **is** satisfaction over the carrier.
英語原文
Nothing below was re-indexed and nothing was weakened. The registered risk for
this goal was that the domain or its well-formedness predicate would need the
carrier as a *constant* somewhere it cannot be a slot, which would have re-indexed
the slot, the table, totality and membership at a pair of a carrier and a key, and
charged the two halves a transport for each of their ten cases. It did not
fire, and the direct evidence is that `slot`, `satTable`,
`total`, `inSlot`, `slotClosed`, `soundness` and
`Good.pinned` are all applied above at their existing types. The code
carrier never reaches the graph: it is bound and pinned inside the code set's own
predicate, and what comes out is an element of `L`, which is all a domain is.
英語原文
What made this cheap is the existential in the graph, and it is worth keeping as
a design fact rather than an accident. A graph that quantifies its table
existentially lets a value be justified by *any* admissible table, so an instance
may answer at each index with the smallest table that reaches it. Had the graph
named its table, the domain and the table would have had to grow together and
every earlier chapter would have moved.
英語原文
The one cost that was not predicted is in the statements, not in the proofs, and
it is the chapter's measurement. A value read at a key *written out* does not
elaborate, at any length of proof, because the key's construction lands inside a
satisfaction; the reading that costs four seconds at a variable member ran past
six minutes at the key, and so did the same statement written as a corollary of
the variable one. Two things fix it and they are the two recorded laws, one each:
every reading takes the member as a variable and reaches its key by an equation,
and the name a consumer would write instead is sealed where it is built. The
first is the uniqueness chapter's law, met again where nothing is being proved by
induction; the second is the law about a construction appearing in a goal, met at
a goal that is a plain equation.