Soundness

theorem LO.FirstOrder.Derivation.sound {L : Language} {T : Theory L} (M : Type u_1) [s : Structure L M] [Nonempty M] [M ⊧ₘ* T] (ε : ℕ → M) {Γ : Sequent L} : ∀ (a : T ⟹ Γ), ∃ φ ∈ Γ, (Semiformula.Evalfm M ε) φ

theorem LO.FirstOrder.sound {L : Language} {T : Theory L} {φ : SyntacticFormula L} : ∀ (a : T ⊢ φ), T ⊨[Struc L] φ

theorem LO.FirstOrder.sound! {L : Language} {T : Theory L} {φ : SyntacticFormula L} : T ⊢! φ → T ⊨[Struc L] φ

theorem LO.FirstOrder.sound₀ {L : Language} {T : Theory L} {φ : SyntacticFormula L} : ∀ (a : T ⊢ φ), T ⊨ φ

theorem LO.FirstOrder.sound₀! {L : Language} {T : Theory L} {φ : SyntacticFormula L} : T ⊢! φ → T ⊨ φ

instance LO.FirstOrder.instSoundTheorySyntacticFormulaSetStrucModels {L : Language} (T : Theory L) : Sound T (Semantics.models (Struc L) T)

theorem LO.FirstOrder.models_of_subtheory {L : Language} {T U : Theory L} [U wkn T] {M : Type u_1} [Structure L M] [Nonempty M] (hM : M ⊧ₘ* T) : M ⊧ₘ* U

theorem LO.FirstOrder.consistent_of_satidfiable {L : Language} {T : Theory L} (h : Semantics.Satisfiable (Struc L) T) : Entailment.Consistent T

theorem LO.FirstOrder.unprovable_of_countermodel {L : Language} {T : Theory L} {M : Type u_1} [s : Structure L M] [Nonempty M] [hM : M ⊧ₘ* T] (f : ℕ → M) (φ : SyntacticFormula L) (c : ¬(Semiformula.Evalfm M f) φ) : T ⊬ φ