An internal graph of uniform satisfaction

Let W be a constructible set, used both as the alphabet from which formula constants are drawn and as the range of values allowed in environments. The uniform satisfaction construction assigns to every code in AllCodes W the set of environments satisfying the coded formula. This chapter proves that the assignment itself has a graph inside L: a set whose members are precisely the ordered pairs of a formula code and its satisfaction set. The mathematical step is an instance of replacement. The uniform graph formula has a unique value over every code, so its image over the set AllCodes W can be collected as a set.

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

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

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

Fix such a constructible set W and excluded middle at the proposition level required by the coding construction. Ordered pairs are formed in the ambient hierarchy, while the domain, the values and the graph all belong to the constructible carrier S.

open import FOL.ZFStructure using ( module hPropStructure )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )

The domain AllCodes W is the constructible set of well-formed formula codes over the alphabet at W. Formula syntax supplies the type of the graph formula; dependent-pair extensionality will later prove uniqueness of a solution together with its satisfaction certificate.

open import L.Coding.CodeSet {ℓ} lem using ( AllCodes )

open import FOL.Syntax using ( Formula )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Data.Vec using ( _∷_; [] )

Membership in the cumulative hierarchy is truncated existence, so the final description of an arbitrary graph member is truncated as well. The carrier S is that of the constructible structure 𝒮ʟ; each of its elements consists of an ambient set together with a certificate of constructibility.

import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )

open hPropStructure 𝒮ʟ using ( S )

The satisfaction relation used here is the inner semantics of the restricted structure 𝒮ᵥ ↾ isL, which is the constructible structure 𝒮ʟ. Constants are interpreted by the identity map on its carrier. Thus _⊨_ says directly that a formula is satisfied in L; no comparison with the ambient semantics is used in this chapter.

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

For the fixed W, both parameters of the uniform construction are instantiated by this same set, so the code alphabet and the range of environment values are both W. Table.graph W W is one binary formula describing the value relation uniformly over all members of AllCodes W, and Table.val W W x mx is its unique value at the particular code x.

open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table )
open import L.Recursion {ℓ} lem using ( Recursion )
open import L.Recursion.Graph {ℓ} lem using () renaming ( module Graph to MapGraph )

module SatGraph (W : S) where

For a code x with membership certificate mx, write this unique value as valOf x mx. The equation valOf≡ identifies it definitionally with Table.val W W x mx. The notation isolates the mathematical function whose graph is to be collected: a domain member is sent to its satisfaction set.

  opaque
    valOf : (x : S) → ⟨ fst x ∈ fst (AllCodes W) ⟩ → S
    valOf x mx = Table.val W W x mx

    valOf≡ : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → valOf x mx ≡ Table.val W W x mx
    valOf≡ x mx = refl

Let gr be the single binary formula Table.graph W W. Its first free position receives a proposed satisfaction set and its second receives a formula code. The relation it defines is therefore the candidate graph relation between codes and values.

  private
    opaque
      unfolding valOf
      gr : Formula S 
      gr = Table.graph W W

Two facts make gr functional. Existence says that gr holds of the table value and its code; this is the witness extracted from Table.funct. Uniqueness says that any other y satisfying the same graph formula equals valOf x mx; it is the symmetry of the table's uniqueness theorem.

      defines' : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → ⟨ (valOf x mx ∷ x ∷ []) ⊨ gr ⟩
      defines' x mx = Table.funct W W x mx .fst .snd

      only' : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) (y : S) → ⟨ (y ∷ x ∷ []) ⊨ gr ⟩ → y ≡ valOf x mx
      only' x mx y h = sym (Table.val-uniq W W x mx y h)

For each code, the type of solutions to gr is contractible. Its centre is the pair consisting of valOf x mx and the proof defines' that this value satisfies gr. Given another solution (y , h), only' identifies the values. The remaining components are proofs of a proposition, so Σ≡Prop lifts equality of values to equality of the complete dependent pairs. This contractibility is exactly the functional premise needed for replacement.

    M : Recursion
    M = record
      { dom = AllCodes W ; graph = gr
      ; funct = λ x mx → (valOf x mx , defines' x mx)
          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ gr)) (sym (only' x mx y h)) } }

Replacement now applies to the functional relation gr over the constructible set AllCodes W. It collects the ordered pairs pr (fst x) (fst (valOf x mx)) into a constructible set, denoted pairs. Thus the graph is internal to L: both its domain and every value are constructible, and replacement forms their pair relation as one set.

    module G = MapGraph M using ( F; F-in; pair-out )

  opaque
    pairs : S
    pairs = G.F

Every code in AllCodes W contributes its graph pair. Concretely, pairs-in proves that the ordered pair of the underlying code and the underlying satisfaction set belongs to pairs.

    pairs-in : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → ⟨ pr (fst x) (fst (valOf x mx)) ∈ fst pairs ⟩
    pairs-in = G.F-in

Conversely, suppose an ordered pair pr (fst x) (fst y) belongs to pairs. The fibre of the replacement image is proposition-valued, so its truncated witness may be eliminated into the dependent pair stating that x is in AllCodes W and that y equals the unique value there. This is the untruncated conclusion of pairs-out.

    pairs-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst pairs ⟩
              → Σ[ mx ∈ ⟨ fst x ∈ fst (AllCodes W) ⟩ ] (fst y ≡ fst (valOf x mx))
    pairs-out = G.pair-out

An arbitrary member of pairs need not arrive already displayed as an ordered pair. The general image theorem therefore yields only a truncated description: merely, there are a code x, a membership certificate mx, and an equality exhibiting the member as the pair of x and its value. This is precisely pairs-shape; the truncation is inherited from membership in the replacement image.

    pairs-shape : (e : S) → ⟨ fst e ∈ fst pairs ⟩
                → ∥ Σ[ x ∈ S ] Σ[ mx ∈ ⟨ fst x ∈ fst (AllCodes W) ⟩ ] (fst e ≡ pr (fst x) (fst (valOf x mx))) ∥₁
    pairs-shape e h = MapGraph.F-out M (fst e) h

The set pairs is therefore the internal graph of uniform satisfaction for formulas whose constants and environments range over W. Existence and uniqueness of the uniform value make the relation functional; replacement turns that relation into a set of L; and the three membership theorems characterize the set both for displayed pairs and for arbitrary members.