def Quotient.liftOnVec {α : Type u_1} {n : ℕ} {β : Sort u_2} {s : Setoid α} (v : Vec (Quotient s) n) (f : Vec α n → β) (h : ∀ (v₁ v₂ : Vec α n), (∀ (i : Fin n), v₁ i ≈ v₂ i) → f v₁ = f v₂) : β

Equations

• Quotient.liftOnVec v f h = (Quotient.finChoice v).liftOn f h

theorem Quotient.liftOnVec_mk {α : Type u_1} {n : ℕ} {β : Sort u_2} {v : Vec α n} {s : Setoid α} {f : Vec α n → β} {h : ∀ (v₁ v₂ : Vec α n), (∀ (i : Fin n), v₁ i ≈ v₂ i) → f v₁ = f v₂} : liftOnVec (fun (i : Fin n) => ⟦v i⟧) f h = f v

def FirstOrder.Language.FormulaSet.TermSetoid {L : Language} {n : ℕ} (Γ : L.FormulaSet n) : Setoid (L.Term n)

Equations

• Γ.TermSetoid = { r := fun (t₁ t₂ : L.Term n) => Γ ⊢ t₁ ≐ t₂, iseqv := ⋯ }

def FirstOrder.Language.FormulaSet.TermModel {L : Language} {n : ℕ} (Γ : L.FormulaSet n) : Type

Equations

• Γ.TermModel = Quotient Γ.TermSetoid

instance FirstOrder.Language.FormulaSet.instHasStructureTermModel {n : ℕ} {L : Language} {Γ : L.FormulaSet n} : L.HasStructure Γ.TermModel

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem FirstOrder.Language.FormulaSet.interpFunc_def {n : ℕ} {L : Language} {Γ : L.FormulaSet n} {m✝ : ℕ} (f : L.Func m✝) (v : Vec Γ.TermModel m✝) : HasStructure.interpFunc f v = Quotient.liftOnVec v (fun (x : Vec (L.Term n) m✝) => ⟦f ⬝ᶠ x⟧) ⋯

@[simp]

theorem FirstOrder.Language.FormulaSet.interpRel_def {n : ℕ} {L : Language} {Γ : L.FormulaSet n} {m✝ : ℕ} (r : L.Rel m✝) (v : Vec Γ.TermModel m✝) : HasStructure.interpRel r v = Quotient.liftOnVec v (fun (x : Vec (L.Term n) m✝) => Γ ⊢ r ⬝ʳ x) ⋯

theorem FirstOrder.Language.FormulaSet.TermModel.interp_term {n m : ℕ} {L : Language} {Γ : L.FormulaSet n} {σ : L.Subst m n} {t : L.Term m} : (⟦t⟧ₜ Γ.TermModel, fun (x : Fin m) => ⟦σ x⟧) = ⟦t[σ]ₜ⟧

theorem FirstOrder.Language.FormulaSet.TermModel.interp_formula {n m : ℕ} {L : Language} {Γ : L.FormulaSet n} {σ : L.Subst m n} (h₁ : Consistent Γ) (h₂ : Complete Γ) (h₃ : Henkin Γ) {p : L.Formula m} : Γ.TermModel ⊨[fun (x : Fin m) => ⟦σ x⟧] p ↔ Γ ⊢ p[σ]ₚ

theorem FirstOrder.Language.FormulaSet.TermModel.satisfiable {n : ℕ} {L : Language} {Γ : L.FormulaSet n} (h₁ : Consistent Γ) (h₂ : Complete Γ) (h₃ : Henkin Γ) : Satisfiable.{u_1} Γ