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

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

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

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

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

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

Equations

• ⋯ = ⋯

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

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