Documentation

Foundation.FirstOrder.Completeness.Completeness

source
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 → ∃ φ ∈ Γ, M ⊧ₘ φ) :
T ⟹ Γ
Equations
Instances For
    source
    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)] {φ : LO.FirstOrder.SyntacticFormula L} :
    T ⊨ φ → T ⊢! φ
    source
    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
    • ⋯ = ⋯
    source
    theorem LO.FirstOrder.complete {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} :
    T ⊨ φ → T ⊢! φ
    source
    theorem LO.FirstOrder.complete_iff {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} :
    T ⊨ φ ↔ T ⊢! φ
    source
    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
    • ⋯ = ⋯
    source
    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
    source
    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
    source
    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
    source
    theorem LO.FirstOrder.satisfiable_iff_consistent {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} :
    LO.FirstOrder.Satisfiable T ↔ LO.System.Consistent T
    source
    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
    source
    theorem LO.FirstOrder.consequence_iff_consequence {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} :
    T ⊨[LO.FirstOrder.Struc L] φ ↔ T ⊨ φ
    source
    theorem LO.FirstOrder.complete' {L : LO.FirstOrder.Language} {T : LO.FirstOrder.Theory L} {φ : LO.FirstOrder.SyntacticFormula L} :
    T ⊨[LO.FirstOrder.Struc L] φ → T ⊢! φ
    source
    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
    • ⋯ = ⋯