Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.IsComplete.eq_complete_theory

∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsComplete → ∀ (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M], {φ | T ⊨ᵇ φ} = L.completeTheory M

A complete theory is the completeTheory Th(M) of one of its models.

Defined in

Mathlib.ModelTheory.Satisfiability

Cited by

2 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FirstOrder.Language.StructureFirstOrder.Language.Theory.ModelNonempty