BedrockSatisfaction, one formula at a time
The value the table will record. For a formula of the meta-language and a set of L the environments range over, this is the set of those environments that satisfy it, built by recursion on the formula.
Nothing here is internal. The recursion is on a formula Agda can see, so each step may name the sets the previous steps produced as constants, and the object language never has to quantify over a code. That is what makes every step a single separation off the ambient set, and what makes the twelve clauses of the internal recursion, when they come, into identities rather than definitions.
The atoms are shorter here than in the internal clauses for the same reason. A term of the meta-language is a variable or a constant and the recursion knows which, so the reader for its value is one case rather than two.
{-# OPTIONS --cubical --safe --guardedness #-} open import Base.Prelude open import Base.Truth open import Base.Classical using ( LEM ) module L.Coding.Sat {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where open import FOL.ZFStructure using ( module hPropStructure ) open import FOL.Syntax using ( Term; con; var; 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.Axioms.Full {ℓ} lem using ( hasSeparationL ) open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; consAtL; numL ) open import L.Coding.EnvSet {ℓ} lem using ( envSet ) open import Cubical.Data.FinData using ( toℕ ) import Cubical.HITs.PropositionalTruncation as PT open PT using ( ∣_∣₁; ∥_∥₁; squash₁ ) open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ ) open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet ) open InfinitySet using ( #_ ) open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ)) open hPropStructure 𝒮ʟ module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
Reading a term the recursion can see
Two clauses, and which one applies is decided in the meta-language rather than by the object language matching a tag. A variable's value is what the environment records at its index; a constant's value is itself.
private nn : ℕ → S nn k = # k , numL k tmIs : ∀ {n m} → Term S n → Fin m → Fin m → Formula S m tmIs (var i) v e = ∃̇ ((var zero ≐ con (nn (toℕ i))) ∧̇ appAt (suc e) zero (suc v)) tmIs (con c) v e = var v ≐ con c tmIs-var-in : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m) → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩ → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩ tmIs-var-in i γ v e h = ∣ nn (toℕ i) , ( refl , subst ⟨_⟩ (sym (appAt-adequate (suc e) zero (suc v) (nn (toℕ i) ∷ γ))) h ) ∣₁ tmIs-var-out : ∀ {n m} (i : Fin n) (γ : S ^ m) (v e : Fin m) → ⟨ γ ⊨ tmIs {n} (var i) v e ⟩ → ⟨ pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩ tmIs-var-out i γ v e = PT.rec (snd (pr (# (toℕ i)) (fst (lookup v γ)) ∈ fst (lookup e γ))) (λ { (x , (qx , m)) → subst (λ w → ⟨ pr w (fst (lookup v γ)) ∈ fst (lookup e γ) ⟩) qx (subst ⟨_⟩ (appAt-adequate (suc e) zero (suc v) (x ∷ γ)) m) })
The value
Twelve clauses, each one separation off the ambient set. The propositional ones name the values below them and combine them with the object language's own connective, which is why the clause for implication is the Heyting arrow rather than a complement of a union: the chapter that wrote the internal clauses made the same choice for the same reason, and the two have to agree.
The quantifiers cons a member of the carrier onto the environment and ask whether the result is in the value below, which is one arity up. The two bounded ones do the same, and the member is drawn from the carrier and guarded by the bounding term's value, not from that value alone. Drawing it from the value alone is wrong for the same reason it was wrong in the internal clauses, where an audit caught it: a member of the bound need not be a member of the carrier, so the environment it would be consed onto would not be an environment, and the two sides would not agree.
private opaque sep : (a : S) → Formula S 1 → S sep a φ = hasSeparationL a φ .fst .fst sep-mem : (a : S) (φ : Formula S 1) (x : S) → (x ∈ˢ sep a φ) ≡ ((x ∈ˢ a) ⊓ ((x ∷ []) ⊨ φ)) sep-mem a φ = hasSeparationL a φ .fst .snd module _ (B : S) where cond : ∀ {n} → Formula S n → Formula S 1 Sat : ∀ {n} → Formula S n → S Sat {n} φ = sep (envSet B n) (cond φ) Sat-mem : ∀ {n} (φ : Formula S n) (x : S) → (x ∈ˢ Sat φ) ≡ ((x ∈ˢ envSet B n) ⊓ ((x ∷ []) ⊨ cond φ)) Sat-mem {n} φ = sep-mem (envSet B n) (cond φ) cond (t ∈̇ u) = (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero)) ∧̇ ( tmIs u zero (suc (suc zero)) ∧̇ (var (suc zero) ∈̇ var zero) )))) cond (t ≐ u) = (∃̇ (∃̇ ( tmIs t (suc zero) (suc (suc zero)) ∧̇ ( tmIs u zero (suc (suc zero)) ∧̇ (var (suc zero) ≐ var zero) )))) cond (a ∧̇ b) = ((var zero ∈̇ con (Sat a)) ∧̇ (var zero ∈̇ con (Sat b))) cond (a ∨̇ b) = ((var zero ∈̇ con (Sat a)) ∨̇ (var zero ∈̇ con (Sat b))) cond (a ⇒̇ b) = ((var zero ∈̇ con (Sat a)) ⇒̇ (var zero ∈̇ con (Sat b))) cond (¬̇ a) = ¬̇ (var zero ∈̇ con (Sat a)) cond ⊤̇ = ⊤̇ cond ⊥̇ = ⊥̇ cond (∃̇ a) = (∃̇∈ (con B) (∃̇ ( consAtL zero (suc zero) (suc (suc zero)) ∧̇ (var zero ∈̇ con (Sat a)) ))) cond (∀̇ a) = (∀̇∈ (con B) (∀̇ ( consAtL zero (suc zero) (suc (suc zero)) ⇒̇ (var zero ∈̇ con (Sat a)) ))) cond (∀̇∈ t a) = (∀̇ ( tmIs t zero (suc zero) ⇒̇ ∀̇∈ (con B) ( (var zero ∈̇ var (suc zero)) ⇒̇ ∀̇ ( consAtL zero (suc zero) (suc (suc (suc zero))) ⇒̇ (var zero ∈̇ con (Sat a)) ) ) )) cond (∃̇∈ t a) = (∃̇ ( tmIs t zero (suc zero) ∧̇ ∃̇∈ (con B) ( (var zero ∈̇ var (suc zero)) ∧̇ ∃̇ ( consAtL zero (suc zero) (suc (suc (suc zero))) ∧̇ (var zero ∈̇ con (Sat a)) ) ) ))
What each clause says
The membership equations, one per constructor, and the only thing this chapter exports besides the value itself. They are what the internal clauses will be checked against: an internal clause says the recorded value stands in some relation to the recorded subvalues, and these say the same of the values built here, so verifying a clause is transporting one along the other.
Each is the separation's own specification with the constructor's condition already substituted, which is why they are one line apiece.
CondAtom : ∀ {n} → Term S n → Term S n → (S → S → Type (ℓ-suc ℓ)) → S → Type (ℓ-suc ℓ) CondAtom t u R z = Σ[ v ∈ S ] (Σ[ w ∈ S ] (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs t (suc zero) (suc (suc zero)) ⟩ × (⟨ (w ∷ v ∷ z ∷ []) ⊨ tmIs u zero (suc (suc zero)) ⟩ × R v w))) cond∈-in : ∀ {n} (t u : Term S n) (z : S) → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁ → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩ cond∈-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ }) cond∈-out : ∀ {n} (t u : Term S n) (z : S) → ⟨ (z ∷ []) ⊨ cond (t ∈̇ u) ⟩ → ∥ CondAtom t u (λ v w → ⟨ fst v ∈ fst w ⟩) z ∥₁ cond∈-out t u z = PT.rec squash₁ (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv }) cond≐-in : ∀ {n} (t u : Term S n) (z : S) → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁ → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩ cond≐-in t u z = PT.map (λ { (v , (w , r)) → v , ∣ w , r ∣₁ }) cond≐-out : ∀ {n} (t u : Term S n) (z : S) → ⟨ (z ∷ []) ⊨ cond (t ≐ u) ⟩ → ∥ CondAtom t u (λ v w → fst v ≡ fst w) z ∥₁ cond≐-out t u z = PT.rec squash₁ (λ { (v , hv) → PT.map (λ { (w , r) → v , (w , r) }) hv }) CondQuant : ∀ {n} → Formula S (suc n) → S → Type (ℓ-suc ℓ) CondQuant a z = Σ[ x ∈ S ] (⟨ fst x ∈ fst B ⟩ × (Σ[ e' ∈ S ] (⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩ × ⟨ fst e' ∈ fst (Sat a) ⟩))) cond∃-in : ∀ {n} (a : Formula S (suc n)) (z : S) → ∥ CondQuant a z ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ cond∃-in a z = PT.map (λ { (x , (x∈ , (e' , r))) → x , (x∈ , ∣ e' , r ∣₁) }) cond∃-out : ∀ {n} (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∃̇ a) ⟩ → ∥ CondQuant a z ∥₁ cond∃-out a z = PT.rec squash₁ (λ { (x , (x∈ , hv)) → PT.map (λ { (e' , r) → x , (x∈ , (e' , r)) }) hv }) cond∀-in : ∀ {n} (a : Formula S (suc n)) (z : S) → ((x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩ cond∀-in a z k x x∈ e' hc = k x e' x∈ hc cond∀-out : ∀ {n} (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∀̇ a) ⟩ → ((x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ (e' ∷ x ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc zero)) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) cond∀-out a z h x e' x∈ hc = h x x∈ e' hc CondBnd : ∀ {n} → Formula S (suc n) → S → S → Type (ℓ-suc ℓ) CondBnd a z w = Σ[ x ∈ S ] ((⟨ fst x ∈ fst B ⟩ × ⟨ fst x ∈ fst w ⟩) × (Σ[ e' ∈ S ] (⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ × ⟨ fst e' ∈ fst (Sat a) ⟩))) cond∃∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ × ∥ CondBnd a z w ∥₁)) ∥₁ → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩ cond∃∈-in t a z = PT.map (λ { (w , (hw , hx)) → w , (hw , PT.map (λ { (x , ((x∈B , x∈w) , (e' , r))) → x , (x∈B , (x∈w , ∣ e' , r ∣₁)) }) hx) }) cond∃∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∃̇∈ t a) ⟩ → ∥ (Σ[ w ∈ S ] (⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ × ∥ CondBnd a z w ∥₁)) ∥₁ cond∃∈-out t a z = PT.map (λ { (w , (hw , hx)) → w , (hw , PT.rec squash₁ (λ { (x , (x∈B , (x∈w , hv))) → PT.map (λ { (e' , r) → x , ((x∈B , x∈w) , (e' , r)) }) hv }) hx) }) cond∀∈-in : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ → (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩ → ⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩ cond∀∈-in t a z k w hw x x∈B x∈w e' hc = k w hw x e' x∈B x∈w hc cond∀∈-out : ∀ {n} (t : Term S n) (a : Formula S (suc n)) (z : S) → ⟨ (z ∷ []) ⊨ cond (∀̇∈ t a) ⟩ → ((w : S) → ⟨ (w ∷ z ∷ []) ⊨ tmIs t zero (suc zero) ⟩ → (x e' : S) → ⟨ fst x ∈ fst B ⟩ → ⟨ fst x ∈ fst w ⟩ → ⟨ (e' ∷ x ∷ w ∷ z ∷ []) ⊨ consAtL zero (suc zero) (suc (suc (suc zero))) ⟩ → ⟨ fst e' ∈ fst (Sat a) ⟩) cond∀∈-out t a z h w hw x e' x∈B x∈w hc = h w hw x x∈B x∈w e' hc