部分式上の充足関係表

この章を読むか、読書案内と依存マップで別のルートを選べます。

論理式 φ に対して、本章は satTable φ を構成します。その各項目は部分式の鍵と再帰的に定義された充足関係の値を対にし、さらに鍵が隣に記録された値を一意に定めることを示します。

英語原文

The recursion's answer, assembled. For a formula of the meta-language, the finite set of pairs of a key with the value at it, one pair for the formula and one for each subformula, built exactly as the subformula closure was and for the same reason: the meta level can name what it has already built.

英語原文

Everything here is an element of the model by construction. The key is a pair of a numeral with a code, and the code is taken in the model's own coding, so no constructibility certificate is carried and none has to be proved. That is what the coding chapter's second instantiation bought, and this is the chapter that spends it.

英語原文

What the recursion actually needs from the table is the other direction: any value recorded against a key is the value at that key. That is where the code equation has to be injective, and where a table that merely happened to record two things at one key would not be a function at all.

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

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

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

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula )
open import V.Coding {ℓ} using ( pr; pr-inj; #-inj′ )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL )
open import L.Axioms.Numerals {ℓ} using ( numeralL; numeralL-fst )
open import L.Coding.Model {ℓ} using ( module LCode; prʟ; prʟ-fst )
open import L.Coding.CodeConstructibility {ℓ}
  using ( tree; Of; tree-inv )
  renaming ( module Parts to TreeParts )
open import L.Coding.Satisfaction {ℓ} lem using ( Sat )

open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.Prelude using ( J )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet using ( #_ )

open hPropStructure 𝒮ʟ using ( S )

鍵・項目・スロット

keyʟ φ は φ のアリティとそのコードを対にし、ent φ はその鍵を Sat B φ と対にします。同じ部分式の木の構成を項目と鍵に適用して、satTable φ とその添字となる slot φ を得ます。

英語原文

A key is the arity paired with the code, which is the shape every clause of the internal recursion reads. An entry is a key paired with the value.

英語原文

The shape both live in is the same, so it is written once and written elsewhere. tree is the closure chapter's recursion: it gathers one thing per subformula, and what that thing is is its parameter. With the entry it gives the table, with the key it gives the slot the table is indexed by. The recursion needs both and needs them to agree constructor for constructor, which is why they come from one recursion rather than two.

keyʟ : ∀ {n} → Formula S n → S
keyʟ {n} φ = prʟ (numeralL n) LCode.⌜ φ ⌝

module _ (B : S) where
  ent : ∀ {n} → Formula S n → S
  ent φ = prʟ (keyʟ φ) (Sat B φ)

  satTable : ∀ {n} → Formula S n → S
  satTable = tree ent

  slot : ∀ {n} → Formula S n → S
  slot = tree keyʟ

充足関係表とスロットを反転する

四つの反転補題は tree-inv の実例です。充足関係表またはスロットへの所属から、その要素を供給した部分式を特定し、slot-ent と ent-slot は項目とその鍵の間を移ります。

英語原文

Every member is one of the things gathered. That is the inversion the closure chapter proves, stated there against two collections at once, so the four readings below are four instantiations of it and no induction runs here.

  module Parts (f : ∀ {m} → Formula S m → S) where
    open TreeParts f public

  satTable-inv : ∀ {n} (φ : Formula S n) (x : V ℓ)
               → ⟨ x ∈ fst (satTable φ) ⟩ → Of ent ent φ x
  satTable-inv = tree-inv ent ent

  slot-inv : ∀ {n} (φ : Formula S n) (x : V ℓ)
           → ⟨ x ∈ fst (slot φ) ⟩ → Of keyʟ keyʟ φ x
  slot-inv = tree-inv keyʟ keyʟ

  slot-ent : ∀ {n} (φ : Formula S n) (x : V ℓ)
           → ⟨ x ∈ fst (slot φ) ⟩ → Of keyʟ ent φ x
  slot-ent = tree-inv keyʟ ent

  ent-slot : ∀ {n} (φ : Formula S n) (x : V ℓ)
           → ⟨ x ∈ fst (satTable φ) ⟩ → Of ent keyʟ φ x
  ent-slot = tree-inv ent keyʟ

鍵における値の一意性

二つの充足関係表の項目が同じアリティ・論理式コードの鍵をもつなら、対と論理式の符号化の単射性により二つの論理式が同一になります。したがって key-determines は両項目が同じ充足関係の値をもつことを示します。

英語原文

Two formulas with the same key have the same value, and that is where the code equation's injectivity is used. The arities come out equal from the numeral half of the key, and the code equation from the other half; the first is then eliminated by path induction so that the second can be used at a single arity, which is the only arity at which it is true.

  private
    same : ∀ {n} (ψ χ : Formula S n)
         → fst LCode.⌜ ψ ⌝ ≡ fst LCode.⌜ χ ⌝ → Sat B ψ ≡ Sat B χ
    same ψ χ e =
      cong (Sat B) (LCode.⌜⌝-inj ψ χ (Σ≡Prop (λ v → snd (isL v)) e))

    cross : ∀ {n m} (ψ : Formula S n) (χ : Formula S m) → n ≡ m
          → fst LCode.⌜ ψ ⌝ ≡ fst LCode.⌜ χ ⌝ → Sat B ψ ≡ Sat B χ
    cross {n} ψ χ p = J
      (λ m' p' → (χ' : Formula S m')
               → fst LCode.⌜ ψ ⌝ ≡ fst LCode.⌜ χ' ⌝ → Sat B ψ ≡ Sat B χ')
      (same ψ) p χ

  total : ∀ {n} (φ : Formula S n) (x : V ℓ) → ⟨ x ∈ fst (slot φ) ⟩
        → ∥ (Σ[ y ∈ S ] ⟨ pr x (fst y) ∈ fst (satTable φ) ⟩) ∥₁
  total φ x h = PT.map
    (λ { (m , χ , (q , incl)) → Sat B χ
       , subst (λ w → ⟨ pr w (fst (Sat B χ)) ∈ fst (satTable φ) ⟩) (sym q)
           (incl (pr (fst (keyʟ χ)) (fst (Sat B χ)))
             (subst (λ w → ⟨ w ∈ fst (tree ent χ) ⟩)
               (prʟ-fst (keyʟ χ) (Sat B χ)) (Parts.self ent χ))) })
    (slot-ent φ x h)

  inSlot : ∀ {n} (φ : Formula S n) (x y : V ℓ)
         → ⟨ pr x y ∈ fst (satTable φ) ⟩ → ⟨ x ∈ fst (slot φ) ⟩
  inSlot φ x y h = PT.rec (snd (x ∈ fst (slot φ)))
    (λ { (m , χ , (q , incl)) →
      subst (λ w → ⟨ w ∈ fst (slot φ) ⟩)
        (sym (pr-inj (q ∙ prʟ-fst (keyʟ χ) (Sat B χ)) .fst))
        (incl (fst (keyʟ χ)) (Parts.self keyʟ χ)) })
    (ent-slot φ (pr x y) h)

  key-determines : ∀ {n m} (ψ : Formula S n) (χ : Formula S m)
                 → fst (keyʟ ψ) ≡ fst (keyʟ χ) → Sat B ψ ≡ Sat B χ
  key-determines {n} {m} ψ χ e = cross ψ χ
    (#-inj′ (sym (numeralL-fst n) ∙ pr-inj q .fst ∙ numeralL-fst m))
    (pr-inj q .snd)
    where
    q : pr (fst (numeralL n)) (fst LCode.⌜ ψ ⌝)
      ≡ pr (fst (numeralL m)) (fst LCode.⌜ χ ⌝)
    q = sym (prʟ-fst (numeralL n) LCode.⌜ ψ ⌝)
      ∙ e ∙ prʟ-fst (numeralL m) LCode.⌜ χ ⌝

  entry-out : ∀ {n m} (φ : Formula S n) (ψ : Formula S m) (y : V ℓ)
            → ⟨ pr (fst (keyʟ ψ)) y ∈ fst (satTable φ) ⟩
            → y ≡ fst (Sat B ψ)
  entry-out φ ψ y h = PT.rec (setIsSet y (fst (Sat B ψ)))
    (λ { (m , χ , (q , _)) →
      let r = pr-inj (q ∙ prʟ-fst (keyʟ χ) (Sat B χ)) in
      r .snd ∙ cong fst (sym (key-determines ψ χ (r .fst))) })
    (satTable-inv φ (pr (fst (keyʟ ψ)) y) h)

  entry-in : ∀ {n} (φ : Formula S n)
           → ⟨ pr (fst (keyʟ φ)) (fst (Sat B φ)) ∈ fst (satTable φ) ⟩
  entry-in φ = subst (λ w → ⟨ w ∈ fst (satTable φ) ⟩)
    (prʟ-fst (keyʟ φ) (Sat B φ)) (Parts.self ent φ)

構成子タグが定める部分鍵

論理式コードが指定された構成子タグをもつ鍵について、最後の場合分けはそのスロットにある直接の部分式の鍵を特定します。二項、単項、量化子の各構成子は、再帰条件が要求するようにアリティを調整した鍵を返します。

英語原文

The dispatch a clause performs, and the last piece before the ten verifications. A clause is stated at a tag and receives a key of that shape; the formula the key names is recovered by the inversion above, and then its constructor has to be matched against the tag. That match is the coding chapter's own device, exported rather than rebuilt: the constructor is recoverable from the tag, so the shape of a formula of a given tag is computed from the tag, and the tag equation carries the formula's own case to it.

英語原文

So one lemma serves all ten clauses, and it returns three things: what the formula's constructor is, that the arity read is the formula's, and that the payload read is the formula's.

keyʟ-shape : ∀ {m} (ψ : Formula S m) (k : ℕ) (ar p : V ℓ)
           → fst (keyʟ ψ) ≡ pr ar (pr (# k) p)
           → LCode.Match k ψ
           × ((# m ≡ ar) × (fst (LCode.payOf ψ) ≡ p))
keyʟ-shape {m} ψ k ar p e =
    subst (λ j → LCode.Match j ψ) tag≡ (LCode.matches ψ)
  , ( sym (numeralL-fst m) ∙ pr-inj e' .fst
    , pr-inj inner .snd )
  where
  e' : pr (fst (numeralL m)) (fst LCode.⌜ ψ ⌝) ≡ pr ar (pr (# k) p)
  e' = sym (prʟ-fst (numeralL m) LCode.⌜ ψ ⌝) ∙ e

  inner : pr (fst (numeralL (LCode.tagOf ψ))) (fst (LCode.payOf ψ))
        ≡ pr (# k) p
  inner = sym (prʟ-fst (numeralL (LCode.tagOf ψ)) (LCode.payOf ψ))
        ∙ sym (cong fst (LCode.shape ψ))
        ∙ pr-inj e' .snd

  tag≡ : LCode.tagOf ψ ≡ k
  tag≡ = #-inj′ (sym (numeralL-fst (LCode.tagOf ψ)) ∙ pr-inj inner .fst)