Soundness of first-order logic

This file formalizes the soundness theorem of first-order logic.

theorem FirstOrder.Language.Entails.ax {L : Language} {n : ℕ} {Γ : L.FormulaSet n} {p : L.Formula n} : p ∈ L.Axiom → Γ ⊨ p

theorem FirstOrder.Language.Entails.mp {L : Language} {n : ℕ} {Γ : L.FormulaSet n} {p q : L.Formula n} : Γ ⊨ p ⇒ q → Γ ⊨ p → Γ ⊨ q

theorem FirstOrder.Language.soundness {L : Language} {n : ℕ} {Γ : L.FormulaSet n} {p : L.Formula n} : Γ ⊢ p → Γ ⊨ p

Soundness theorem.

theorem FirstOrder.Language.Consistent.of_satisfiable {L : Language} {n : ℕ} {Γ : L.FormulaSet n} : Satisfiable.{u_1} Γ → Consistent Γ

theorem FirstOrder.Language.Consistent.empty {L : Language} {n : ℕ} : Consistent ∅

theorem FirstOrder.Language.Theory.soundness {L : Language} {M : Type u} [L.HasStructure M] {T : L.Theory} [T.IsModel M] {p : L.Sentence} : T ⊢ p → M ⊨ₛ p

theorem FirstOrder.Language.Theory.IsModel.of_subtheory {L : Language} {M : Type u} [L.HasStructure M] {T₁ : L.Theory} (T₂ : L.Theory) [T₁ ⊆ᵀ T₂] [T₂.IsModel M] : T₁.IsModel M

instance FirstOrder.Language.Theory.subtheory_theory {L : Language} {M : Type u} [L.HasStructure M] {T : L.Theory} [T.IsModel M] : T ⊆ᵀ L.theory M

theorem FirstOrder.Language.Complete.provable_iff_satisfied {L : Language} (M : Type u) [L.HasStructure M] {T : L.Theory} [T.IsModel M] {p : L.Sentence} (h : Complete T) : T ⊢ p ↔ M ⊨ₛ p

theorem FirstOrder.Language.Complete.theorems_eq_theory {L : Language} (M : Type u) [L.HasStructure M] {T : L.Theory} [T.IsModel M] (h : Complete T) : T.theorems = L.theory M

theorem FirstOrder.Language.theory_consistent (L : Language) (M : Type u) [L.HasStructure M] : Consistent (L.theory M)

theorem FirstOrder.Language.theory_complete (L : Language) (M : Type u) [L.HasStructure M] : Complete (L.theory M)

theorem FirstOrder.Language.theorems_theory_eq_theory (L : Language) (M : Type u) [L.HasStructure M] : (L.theory M).theorems = L.theory M