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} : T ⟹ Γ → ∃ φ ∈ Γ, (Semiformula.Evalfm M ε) φ

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} : T ⊢! φ → T ⊨[Struc L] φ

theorem LO.FirstOrder.sound₀ {L : Language} {T : Theory L} {φ : SyntacticFormula L} : 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 ≼ 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) : System.Consistent T