Theorems · Theorem · logic and foundations

FirstOrder.Language.Theory.IsComplete.models_elementarily_equivalent

∀ {L : FirstOrder.Language} {T : L.Theory},
  T.IsComplete →
    ∀ (M : Type u_1) (N : Type u_2) [inst : L.Structure M] [inst_1 : L.Structure N] [M ⊨ T] [N ⊨ T] [Nonempty M]
      [Nonempty N], L.ElementarilyEquivalent M N

If a theory is complete all its models are elementarily equivalent.

Defined in

Mathlib.ModelTheory.Satisfiability

Cited by

0 results in Mathlib

Foundations

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

Assumes

FirstOrder.Language.StructureFirstOrder.Language.StructureFirstOrder.Language.Theory.ModelFirstOrder.Language.Theory.ModelNonemptyNonempty