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

Equations

• LO.FirstOrder.Derivation.completeness_of_encodable h = LO.FirstOrder.Completeness.syntacticMainLemmaTop ⋯

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

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

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

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

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

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

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

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

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

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

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

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

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