BedrockSatisfaction, one formula at a time
表将要记录的那个取值。给定元语言的一条公式，以及诸环境所落之上的 L 的一个集合，这就是满足它的那些环境构成的集合，沿公式递归造出。
此处没有任何内部的东西。递归沿一条 Agda 看得见的公式进行，故每一步都可以把前几步产出的集合以常元点名，而对象语言从不必对码作量化。正是这一点使每一步只是「在周遭集合上作一次分离」，也正是这一点使内部递归那十二条子句到来时成为等式而非定义。
出于同样理由，此处的原子比内部子句短。元语言的一个词项要么是变元、要么是常元，而递归知道是哪个，故读它取值的读式只有一种情形，不是两种。
{-# 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 _⊨_ )
读一个递归看得见的词项
两条子句，而适用哪一条由元语言决定，不由对象语言去匹配标签。变元的取值是环境在它序号处记录的东西；常元的取值就是它自己。
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) })
那个取值
十二条子句，每条都是在周遭集合上作一次分离。命题的那几条把它们下面的诸取值点名，再用对象语言自己的联结词把它们合起来；蕴含那一条因此是 Heyting 箭头，而非「并的补」：写内部诸子句的那一章出于同样理由作了同样的选择，而两者必须一致。
两个量词把载体的一个成员接到环境头上，再问结果是否落在下面那个取值之中，而后者高一个元数。两个有界量词做同样的事，而那个成员取自载体、由界项的取值设防，不是单取自那个取值。单取自那个取值是错的，理由与它在内部诸子句里曾经错的理由相同 (那次由一次审计抓出)：界的成员未必是载体的成员，于是被接上去的环境根本不是环境，两侧也就对不上。
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)) ) ) ))
每条子句说了什么
诸成员等式，每个构造子一条，也是本章除那个取值本身之外唯一导出的东西。它们是内部诸子句将被对照的对象：一条内部子句说「被记录的取值与被记录的诸子取值处于某种关系」，而这些说的是同一件事、只不过对象是此处造出的诸取值；故验证一条子句就是沿其中之一把另一条搬过去。
每一条都是那次分离自己的规格，且构造子的条件已代入，这就是它们一条一行的原因。
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