---
title: "从码恢复公式"
module: L.Coding.FormulaRecovery
lang: zh
site: "Bedrock"
description: "从码恢复公式"
stage: "内部编码：表与统一满足关系"
reading_order: 55
canonical: https://bedrock.institute/zh/L.Coding.FormulaRecovery.html
html: L.Coding.FormulaRecovery.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/FormulaRecovery.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Syntax, FOL.Manipulation.ConstantMapping, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Rank, L.Axioms.Numerals, L.Coding.Model, L.Coding.Closure, L.Coding.Descent, L.Coding.CodeShape]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/en/L.Coding.FormulaRecovery.md, https://bedrock.institute/ja/L.Coding.FormulaRecovery.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 从码恢复公式

形状正确且对子码封闭的键集合应当包含真正的公式码。给定一个元数为指定自然数的键，本章证明它编码了一条常元取自指定载体的公式。证明对码的秩作归纳，所得结论是所恢复公式的仅仅存在性。

那条公式落在哪个字母表上，是整章的要害，而它在此处定案，而不在末尾。模型之上的公式会由同样六个框架还原出来，而对消费方毫无用处，因为它的索引类型是单个载体之上的诸公式。故目标在一个字母表上陈述，字母表是一个参数，而关于它的、形状谓词供不出的那一件事，即载体的诸成员就是字母表的像，作为一条假设摆在旁边。

目标采用字母表自身的编码，这使各框架更短。在模型上，每个框架都必须先对应模型编码与层级编码，才能比较一个码和一个载荷；在字母表上，码本来就是层级的元素，因此不需要这层对应。

此处**没有**证明的是「每个成员都是这样一个键」，而欠这笔账的是那个集合。形状把元数分量存在量化、且对它不加任何条件，故一个持有「第一分量不是数码的对」的集合同样满足两半，而本定理对它什么也没说。下一章所造的那个集合从外面把元数钉住，即在一个固定元数上被索引的族之内作分离，这正是不去要求那条谓词的原因。

递归跑在**码的秩**上，不跑在码上、也不跑在键上。不跑在码上，是因为成员关系不下降进 Kuratowski 的对；不跑在键上，是因为键在码旁边还带着元数，而「对的秩的算术」是一条没人证过的事实。把元数作为一个自然数在旁边带着、只对码下降，两者都不需要。

一步是 `peel`，一次下降是上一章，而十个情形收拢为六个，因为十个标签之间只有六种形状，而一种形状之内变动的只是一个标签与一个构造子。

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

open import Base.Prelude

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Term; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.Manipulation.ConstantMapping using ( mapTm; mapFo )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-induction )
open import V.Coding {ℓ} using ( pr; pr-inj; module VCode )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Rank {ℓ} using ( rank )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Coding.Model {ℓ} using ( prʟ; prʟ-fst )
open import L.Coding.Closure {ℓ} using ( closedAt )
open import L.Coding.Descent {ℓ} using ( payload≺; leftPart; rightPart )
open import L.Coding.CodeShape {ℓ}
  using ( shapedAt; isTmAt-decode; Onto; BinWit; UnWit; bothTm; zeroPay
        ; module Peel )

import Cubical.Data.Sum as Sum
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
open InfinitySet using ( #_; sucV )

open hPropStructure 𝒮ʟ

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

## 键与解码命题

一个键由元数与码配对而成。解码要求存在字母表 K 上具有该元数的公式，将其常元映入层级后，所得编码正是给定的码。命题截断记录这样一条公式的存在，而不选定具体代表。

码是对该公式在层级中的像取的，那正是 `mapFo` 在那里做的事。它不是构造的一步：常元改名按定义与每个构造子交换，故字母表之上的一条公式连同它的像，其编码与模型之上的公式完全一样。

```agda
keyOf : ℕ → S → S
keyOf n x = prʟ (numeralL n) x

keyOf-fst : (n : ℕ) (x : S) → fst (keyOf n x) ≡ pr (# n) (fst x)
keyOf-fst n x = prʟ-fst (numeralL n) x ∙ cong₂ pr (numeralL-fst n) refl

Coded : {K : Type ℓ} (f : K → V ℓ) → ℕ → S → Type (ℓ-suc ℓ)
Coded {K} f n x = ∥ Σ[ φ ∈ Formula K n ] (VCode.⌜ mapFo f φ ⌝ ≡ fst x) ∥₁
```

## 对码的秩作归纳

封闭性提供直接子公式的键，而它们的秩严格更小。因此，秩归纳允许先解码子公式，再重建整条公式。归纳命题允许元数变化，从而也能处理量词。

字母表的两个参数出于同样的理由骑在归纳之外。六个框架里只有两个去看它们，即载荷里放着词项的那两个，而它们看的方式，是把那条假设径直递给词项解码。

```agda
module Decode {K : Type ℓ} (f : K → V ℓ)
              {m : ℕ} (C A : Fin m) (γ : S ^ m) (onto : Onto f A γ)
              (hcl : ⟨ γ ⊨ closedAt C ⟩) (hsh : ⟨ γ ⊨ shapedAt C A ⟩) where
  open Peel C A γ hcl hsh

  Wf : ℕ → S → Type (ℓ-suc ℓ)
  Wf n x = ⟨ keyOf n x ∈ˢ lookup C γ ⟩

  recover : (n : ℕ) (x : S) → Wf n x → Coded f n x
  recover n x = ∈-induction go (rank (fst x)) n x refl
    where
    P : V ℓ → Type (ℓ-suc ℓ)
    P r = (j : ℕ) (z : S) → rank (fst z) ≡ r → Wf j z → Coded f j z

    go : (r : V ℓ) → ((y : V ℓ) → ⟨ y ∈ r ⟩ → P y) → P r
    go r IH j z qr wz = PT.rec squash₁ fill (peel (keyOf j z) wz)
      where
      D = fst (lookup C γ)

      rec : (i : ℕ) (u : S) → ⟨ rank (fst u) ∈ rank (fst z) ⟩
          → Wf i u → Coded f i u
      rec i u lt wu = IH (rank (fst u))
        (subst (λ w → ⟨ rank (fst u) ∈ w ⟩) qr lt) i u refl wu
```

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

The arity numeral and the payload, read out of the key's shape.

</details>

```agda
      split : (N : S) (p : V ℓ) → fst (keyOf j z) ≡ pr (fst N) p
            → (# j ≡ fst N) × (fst z ≡ p)
      split N p e = pr-inj (sym (keyOf-fst j z) ∙ e)

      inD : (i : ℕ) (N u : S) → # i ≡ fst N → ⟨ pr (fst N) (fst u) ∈ D ⟩
          → Wf i u
      inD i N u qN h = subst (λ w → ⟨ w ∈ D ⟩)
        (cong₂ pr (sym qN) refl ∙ sym (keyOf-fst i u)) h

      inD⁺ : (i : ℕ) (N u : S) → # i ≡ fst N
           → ⟨ pr (sucV (fst N)) (fst u) ∈ D ⟩ → Wf (suc i) u
      inD⁺ i N u qN h = subst (λ w → ⟨ w ∈ D ⟩)
        (cong₂ pr (cong sucV (sym qN)) refl ∙ sym (keyOf-fst (suc i) u)) h
```

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

The six frames. Each takes the constructor's coding equation rather than
leaving the elaborator to find it: with the constructor a variable, nothing
reduces, and the unification is the whole cost. Over the alphabet the equation
is still `refl` at every call site, because relabelling commutes with every
constructor definitionally.

</details>

```agda
      atom : (k : ℕ) (op : ∀ {i} → Term K i → Term K i → Formula K i)
           → (∀ {i} (t u : Term K i)
              → VCode.⌜ mapFo f (op t u) ⌝
                ≡ VCode.mkTag k (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapTm f u ⌝ᵗ))
           → BinWit k (bothTm A) γ (keyOf j z) → Coded f j z
      atom k op qop (N , (a , (b , (e , (ha , hb))))) =
        PT.rec squash₁
          (λ { (t , qt) → PT.map
            (λ { (u , qu) → op t u
               , ( qop t u
                 ∙ cong (VCode.mkTag k) (cong₂ pr qt qu)
                 ∙ sym qx ) })
            (isTmAt-decode f zero (suc (suc zero)) (suc (suc (suc (suc A))))
              (b ∷ a ∷ N ∷ keyOf j z ∷ γ) j (sym qN) onto hb) })
          (isTmAt-decode f (suc zero) (suc (suc zero)) (suc (suc (suc (suc A))))
            (b ∷ a ∷ N ∷ keyOf j z ∷ γ) j (sym qN) onto ha)
        where
        sp = split N (pr (# k) (pr (fst a) (fst b))) e
        qN = sp .fst
        qx = sp .snd

      binSame : (k : ℕ) (op : ∀ {i} → Formula K i → Formula K i → Formula K i)
              → (∀ {i} (φ ψ : Formula K i)
                 → VCode.⌜ mapFo f (op φ ψ) ⌝
                   ≡ VCode.mkTag k (pr VCode.⌜ mapFo f φ ⌝ VCode.⌜ mapFo f ψ ⌝))
              → BinSame k (keyOf j z) → Coded f j z
      binSame k op qop (N , (a , (b , (e , (ha , hb))))) =
        PT.rec squash₁
          (λ { (φ , qφ) → PT.map
            (λ { (ψ , qψ) → op φ ψ
               , ( qop φ ψ
                 ∙ cong (VCode.mkTag k) (cong₂ pr qφ qψ)
                 ∙ sym qx ) })
            (rec j b (subst (λ w → ⟨ rank (fst b) ∈ rank w ⟩) (sym qx)
                       (rightPart (# k) (fst a) (fst b)))
                     (inD j N b qN hb)) })
          (rec j a (subst (λ w → ⟨ rank (fst a) ∈ rank w ⟩) (sym qx)
                     (leftPart (# k) (fst a) (fst b)))
                   (inD j N a qN ha))
        where
        sp = split N (pr (# k) (pr (fst a) (fst b))) e
        qN = sp .fst
        qx = sp .snd

      unSame : (k : ℕ) (op : ∀ {i} → Formula K i → Formula K i)
             → (∀ {i} (φ : Formula K i)
                → VCode.⌜ mapFo f (op φ) ⌝ ≡ VCode.mkTag k VCode.⌜ mapFo f φ ⌝)
             → UnSame k (keyOf j z) → Coded f j z
      unSame k op qop (N , (a , (e , ha))) = PT.map
        (λ { (φ , qφ) → op φ
           , ( qop φ ∙ cong (VCode.mkTag k) qφ ∙ sym qx ) })
        (rec j a (subst (λ w → ⟨ rank (fst a) ∈ rank w ⟩) (sym qx)
                   (payload≺ (# k) (fst a)))
                 (inD j N a qN ha))
        where
        sp = split N (pr (# k) (fst a)) e
        qN = sp .fst
        qx = sp .snd

      konst : (k : ℕ) (op : ∀ {i} → Formula K i)
            → (∀ i → VCode.⌜ mapFo f (op {i}) ⌝ ≡ VCode.mkTag k (# 0))
            → UnWit k zeroPay γ (keyOf j z) → Coded f j z
      konst k op qop (N , (a , (e , ha))) = ∣ op
        , ( qop j ∙ cong (VCode.mkTag k) (sym (ha ∙ numeralL-fst 0))
          ∙ sym qx ) ∣₁
        where
        qx = split N (pr (# k) (fst a)) e .snd

      unSucc : (k : ℕ) (op : ∀ {i} → Formula K (suc i) → Formula K i)
             → (∀ {i} (φ : Formula K (suc i))
                → VCode.⌜ mapFo f (op φ) ⌝ ≡ VCode.mkTag k VCode.⌜ mapFo f φ ⌝)
             → UnSucc k (keyOf j z) → Coded f j z
      unSucc k op qop (N , (a , (e , ha))) = PT.map
        (λ { (φ , qφ) → op φ
           , ( qop φ ∙ cong (VCode.mkTag k) qφ ∙ sym qx ) })
        (rec (suc j) a
          (subst (λ w → ⟨ rank (fst a) ∈ rank w ⟩) (sym qx)
            (payload≺ (# k) (fst a)))
          (inD⁺ j N a qN ha))
        where
        sp = split N (pr (# k) (fst a)) e
        qN = sp .fst
        qx = sp .snd

      bnd : (k : ℕ) (op : ∀ {i} → Term K i → Formula K (suc i) → Formula K i)
          → (∀ {i} (t : Term K i) (φ : Formula K (suc i))
             → VCode.⌜ mapFo f (op t φ) ⌝
               ≡ VCode.mkTag k (pr VCode.⌜ mapTm f t ⌝ᵗ VCode.⌜ mapFo f φ ⌝))
          → BinSucc k (keyOf j z) → Coded f j z
      bnd k op qop (N , (a , (b , (e , (ha , hb))))) =
        PT.rec squash₁
          (λ { (t , qt) → PT.map
            (λ { (φ , qφ) → op t φ
               , ( qop t φ
                 ∙ cong (VCode.mkTag k) (cong₂ pr qt qφ)
                 ∙ sym qx ) })
            (rec (suc j) b (subst (λ w → ⟨ rank (fst b) ∈ rank w ⟩) (sym qx)
                             (rightPart (# k) (fst a) (fst b)))
                           (inD⁺ j N b qN hb)) })
          (isTmAt-decode f zero (suc zero) (suc (suc (suc A)))
            (a ∷ N ∷ keyOf j z ∷ γ) j (sym qN) onto ha)
        where
        sp = split N (pr (# k) (pr (fst a) (fst b))) e
        qN = sp .fst
        qx = sp .snd

      fill : PeelWit (keyOf j z) → Coded f j z
      fill =
        Sum.rec (atom 0 _∈̇_ (λ _ _ → refl))
        (Sum.rec (atom 1 _≐_ (λ _ _ → refl))
        (Sum.rec (binSame 2 _∧̇_ (λ _ _ → refl))
        (Sum.rec (binSame 3 _∨̇_ (λ _ _ → refl))
        (Sum.rec (binSame 4 _⇒̇_ (λ _ _ → refl))
        (Sum.rec (konst 5 ⊥̇ (λ _ → refl))
        (Sum.rec (unSucc 6 ∃̇_ (λ _ → refl))
        (Sum.rec (unSucc 7 ∀̇_ (λ _ → refl))
        (Sum.rec (bnd 8 ∀̇∈ (λ _ _ → refl))
        (bnd 9 ∃̇∈ (λ _ _ → refl))))))))))
```