Commit 2022-04-13 10:56 50ff59ad

View on Github →

feat(model_theory/skolem, satisfiability): A weak Downward Loewenheim Skolem (#13141) Defines a language and structure with built-in Skolem functions for a particular language Proves a weak form of Downward Loewenheim Skolem: every structure has a small (in the universe sense) elementary substructure Shows that T having a model in any universe implies T.is_satisfiable.

Estimated changes

Modified src/model_theory/bundled.lean

Modified src/model_theory/language_map.lean

Modified src/model_theory/satisfiability.lean

modified theorem first_order.language.Theory.model.is_satisfiable

Modified src/model_theory/semantics.lean

Created src/model_theory/skolem.lean

added theorem first_order.language.exists_small_elementary_substructure

added def first_order.language.skolem₁

added theorem first_order.language.substructure.coe_sort_elementary_skolem₁_reduct

added theorem first_order.language.substructure.skolem₁_reduct_is_elementary