Satisfaction, internalized

The instance. For a formula of the meta-language and a set of L its environments range over, the satisfaction table is an element of L, defined there by an object-language formula.

funct is the two halves meeting. Existence hands the graph the objects the previous chapters built: the slot as the index set, the table over it, the carrier as the constant. Uniqueness takes an arbitrary table the graph accepts and pins its value against the one the meta-level recursion built. Neither half does anything here; both were finished before this chapter opened, and this is the page where they are applied.

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

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

module L.Coding.Satisfaction {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) 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.Model {ℓ} using ( prʟ-fst; domAt; domAt-intro; domAt-out )
open import L.Coding.Sat {ℓ} lem using ( Sat )
open import L.Coding.Table {ℓ} lem
  using ( keyʟ; slot; satTable; tree; ent; slot-ent; total; inSlot
        ; module Parts )
open import L.Coding.Slot {ℓ} lem using ( slotClosed )
open import L.Coding.Sound {ℓ} lem using ( soundness )
open import L.Coding.Unique {ℓ} lem using ( module Good )
open import L.Coding.Graph {ℓ} lem using ( satGraph; graph-in; graph-out )
open import L.Recursion {ℓ} lem using ( Recursion; mereFunct; module Of )

open import Cubical.Data.Sigma using ( Σ≡Prop )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open hPropStructure 𝒮ʟ

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

The instance

The domain is the slot; the graph is the one the previous chapter wrote; and

funct is filled through mereFunct, because a merely existing unique solution is a contractible one and contractibility is a proposition. That was the first finding of this whole goal, made before any of it was built, and this is where it is spent.

module _ (B : S) {n : ℕ} (φ : Formula S n) where
  private
    C T : S
    C = slot B φ
    T = satTable B φ

    Ci Ti : Fin 
    Ci = suc (suc zero)
    Ti = suc zero

    δ : (x y : S) → S ^ 
    δ x y = B ∷ T ∷ C ∷ y ∷ x ∷ []

    hdom : (x y : S) → ⟨ δ x y ⊨ domAt Ti Ci ⟩
    hdom x y = domAt-intro Ti Ci (δ x y)
      (λ z → (λ h → PT.rec (snd (fst z ∈ fst C))
                (λ { (w , hw) → inSlot B φ (fst z) (fst w) hw }) h)
           , (λ h → total B φ (fst z) h))

    entry : ∀ {m} (ψ : Formula S m) (x : S) → fst x ≡ fst (keyʟ ψ)
          → ((z : V ℓ) → ⟨ z ∈ fst (tree B (ent B) ψ) ⟩ → ⟨ z ∈ fst T ⟩)
          → ⟨ pr (fst x) (fst (Sat B ψ)) ∈ fst T ⟩
    entry ψ x q incl =
      subst (λ w → ⟨ pr w (fst (Sat B ψ)) ∈ fst T ⟩) (sym q)
        (incl (pr (fst (keyʟ ψ)) (fst (Sat B ψ)))
          (subst (λ w → ⟨ w ∈ fst (tree B (ent B) ψ) ⟩)
            (prʟ-fst (keyʟ ψ) (Sat B ψ)) (Parts.self B (ent B) ψ)))

  satRec : Recursion
  Recursion.dom satRec = C
  Recursion.graph satRec = satGraph B
  Recursion.funct satRec x x∈ = mereFunct (satGraph B) x (PT.map
    (λ { (m , ψ , (q , incl)) → Sat B ψ
       , ( graph-in B x (Sat B ψ)
             ∣ C , (T , (B , (refl
             , ( slotClosed B φ (Sat B ψ ∷ x ∷ [])
             , ( hdom x (Sat B ψ)
             , ( entry ψ x q incl
             , soundness B φ (Sat B ψ ∷ x ∷ []) )))))) ∣₁
         , (λ y' hy' → Σ≡Prop (λ v → snd (isL v))
             (PT.rec (setIsSet (fst y') (fst (Sat B ψ)))
               (λ { (C' , (T' , (b , (eb , (hc , (hd , (ha , h12))))))) →
                 Good.pinned (b ∷ T' ∷ C' ∷ y' ∷ x ∷ []) Ci Ti zero
                     hc hd h12 ψ x y' q
                     (domAt-out Ti Ci (b ∷ T' ∷ C' ∷ y' ∷ x ∷ []) hd x y' ha) ha
                 ∙ cong (λ w → fst (Sat w ψ))
                     (Σ≡Prop (λ v → snd (isL v)) eb) })
               (graph-out B x y' hy'))) ) })
    (slot-ent B φ (fst x) x∈))

  module Table = Of satRec