Commit 2022-06-29 20:38 6879dd0c

View on Github →

feat(model_theory/satisfiability): The Łoś–Vaught Test (#14758) Provides more API for elementary equivalence Shows that a κ-categorical theory with only infinite models is complete.

Estimated changes

Modified docs/overview.yaml

Modified src/model_theory/bundled.lean

added def equiv.bundled_induced

added def equiv.bundled_induced_equiv

added def first_order.language.elementarily_equivalent.to_Model

Modified src/model_theory/satisfiability.lean

added theorem cardinal.categorical.is_complete

added theorem cardinal.empty_infinite_Theory_is_complete

deleted theorem first_order.language.Theory.exists_elementary_embedding_card_eq

added theorem first_order.language.Theory.exists_model_card_eq

added theorem first_order.language.exists_elementarily_equivalent_card_eq

added theorem first_order.language.exists_elementary_embedding_card_eq

added theorem first_order.language.exists_elementary_embedding_card_eq_of_ge

added theorem first_order.language.exists_elementary_embedding_card_eq_of_le

Modified src/model_theory/semantics.lean

added theorem first_order.language.elementarily_equivalent.Theory_model

added theorem first_order.language.elementarily_equivalent.Theory_model_iff

added theorem first_order.language.elementarily_equivalent.complete_theory_eq

added theorem first_order.language.elementarily_equivalent.infinite

added theorem first_order.language.elementarily_equivalent.infinite_iff

added theorem first_order.language.elementarily_equivalent.nonempty

added theorem first_order.language.elementarily_equivalent.nonempty_iff

added theorem first_order.language.elementarily_equivalent.realize_sentence

added theorem first_order.language.elementarily_equivalent.symm

added theorem first_order.language.elementarily_equivalent.trans

added theorem first_order.language.equiv.elementarily_equivalent

Modified src/set_theory/cardinal/basic.lean

added theorem cardinal.lift_mk_shrink''

added theorem cardinal.lift_mk_shrink'

added theorem cardinal.lift_mk_shrink