---
title: "An internal graph of uniform satisfaction"
module: L.Coding.SatisfactionGraphSet
lang: en
site: "Bedrock"
description: "An internal graph of uniform satisfaction"
stage: "Proving GCH"
reading_order: 98
canonical: https://bedrock.institute/en/L.Coding.SatisfactionGraphSet.html
html: L.Coding.SatisfactionGraphSet.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionGraphSet.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.CodeSet, FOL.Syntax, L.Coding.UniformSatisfaction, L.Recursion, L.Recursion.Graph]
routes: [gch-descriptions]
translations: [https://bedrock.institute/zh/L.Coding.SatisfactionGraphSet.md, https://bedrock.institute/ja/L.Coding.SatisfactionGraphSet.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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`.

```agda
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.

```agda
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.

```agda
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.

```agda
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`.

```agda
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.

```agda
  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.

```agda
  private
    opaque
      unfolding valOf
      gr : Formula S 2
      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.

```agda
      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.

```agda
    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.

```agda
    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`.

```agda
    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`.

```agda
    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.

```agda
    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.