Commit 2024-09-11 03:54 cb6040d8

View on Github →

feat(ModelTheory/Satisfiability): Fix universe on ModelsBoundedFormula, derive consequences for models in all universes (#16676) Redefines ModelsBoundedFormula to require a formula to be true in all models of a higher universe Derives that ModelsBoundedFormula implies a formula is true in models in all universes from properties of satisfiability (ultimately derived from Löwenheim-Skolem)

Estimated changes

Modified Mathlib/ModelTheory/Satisfiability.lean

added theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_boundedFormula

added theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_formula

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.models_sentence_iff

modified theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff

modified theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_iff

added theorem FirstOrder.Language.Theory.models_formula_iff_onTheory_models_equivSentence

added theorem FirstOrder.Language.Theory.models_toFormula_iff