noncomputable def LO.FirstOrder.Derivation.completeness_of_encodable {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {Γ : LO.FirstOrder.Sequent L} (h : ∀ (M : Type u) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M], M ⊧ₘ* T → ∃ p ∈ Γ, M ⊧ₘ p) : T ⟹ Γ

Equations

• LO.FirstOrder.Derivation.completeness_of_encodable h = let_fun this := ⋯; LO.FirstOrder.Completeness.syntacticMainLemmaTop this

theorem LO.FirstOrder.completeness_of_encodable {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] {p : LO.FirstOrder.SyntacticFormula L} : T ⊨ p → T ⊢! p

instance LO.FirstOrder.instCompleteTheorySyntacticFormulaSetSmallStrucModels {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] : LO.Complete T (LO.Semantics.models (LO.FirstOrder.SmallStruc L) T)

Equations

• ⋯ = ⋯

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

theorem LO.FirstOrder.complete_iff {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {p : LO.FirstOrder.SyntacticFormula L} : T ⊨ p ↔ T ⊢! p

instance LO.FirstOrder.instCompleteTheorySyntacticFormulaSetSmallStrucModels_1 {L : LO.FirstOrder.Language} (T : LO.FirstOrder.Theory L) : LO.Complete T (LO.Semantics.models (LO.FirstOrder.SmallStruc L) T)

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.satisfiable_of_consistent' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} (h : LO.System.Consistent T) : LO.Semantics.Satisfiable (LO.FirstOrder.SmallStruc L) T

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

theorem LO.FirstOrder.satisfiable_iff_consistent' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T ↔ LO.System.Consistent T

theorem LO.FirstOrder.satisfiable_iff_consistent {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} : LO.FirstOrder.Satisfiable T ↔ LO.System.Consistent T

theorem LO.FirstOrder.satidfiable_iff_satisfiable {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} : LO.Semantics.Satisfiable (LO.FirstOrder.Struc L) T ↔ LO.FirstOrder.Satisfiable T

theorem LO.FirstOrder.consequence_iff_consequence {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {p : LO.FirstOrder.SyntacticFormula L} : T ⊨[LO.FirstOrder.Struc L] p ↔ T ⊨ p

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

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

Equations

• ⋯ = ⋯