Commit 2024-09-17 09:07 0bdd5fad

View on Github →

chore(ModelTheory/Equivalence): Cleanup of FirstOrder.Language.Theory.SemanticallyEquivalent (#16799) Moves the definition and API of FirstOrder.Language.Theory.SemanticallyEquivalent to a new file, Mathlib/ModelTheory/Equivalence.lean, anticipating further development Cleans up the use of the namespace FirstOrder.Language.Theory.SemanticallyEquivalent Defines the notation φ ⇔[T] ψ for T.SemanticallyEquivalent φ ψ Other moving files, moving variables, introducing notation, and editing documentation, no changes were made.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/ModelTheory/Complexity.lean

Created Mathlib/ModelTheory/Equivalence.lean

added theorem FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not

added theorem FirstOrder.Language.BoundedFormula.ex_semanticallyEquivalent_not_all_not

added theorem FirstOrder.Language.BoundedFormula.imp_semanticallyEquivalent_not_sup

added theorem FirstOrder.Language.BoundedFormula.inf_semanticallyEquivalent_not_sup_not

added theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_all_liftAt

added theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_not_not

added theorem FirstOrder.Language.BoundedFormula.sup_semanticallyEquivalent_not_inf_not

added theorem FirstOrder.Language.Formula.imp_semanticallyEquivalent_not_sup

added theorem FirstOrder.Language.Formula.inf_semanticallyEquivalent_not_sup_not

added theorem FirstOrder.Language.Formula.semanticallyEquivalent_not_not

added theorem FirstOrder.Language.Formula.sup_semanticallyEquivalent_not_inf_not

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.models_sentence_iff

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_iff

added def FirstOrder.Language.Theory.SemanticallyEquivalent

added def FirstOrder.Language.Theory.semanticallyEquivalentSetoid

Modified Mathlib/ModelTheory/Satisfiability.lean

deleted theorem FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not

deleted theorem FirstOrder.Language.BoundedFormula.ex_semanticallyEquivalent_not_all_not

deleted theorem FirstOrder.Language.BoundedFormula.imp_semanticallyEquivalent_not_sup

deleted theorem FirstOrder.Language.BoundedFormula.inf_semanticallyEquivalent_not_sup_not

deleted theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_all_liftAt

deleted theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_not_not

deleted theorem FirstOrder.Language.BoundedFormula.sup_semanticallyEquivalent_not_inf_not

deleted theorem FirstOrder.Language.Formula.imp_semanticallyEquivalent_not_sup

deleted theorem FirstOrder.Language.Formula.inf_semanticallyEquivalent_not_sup_not

deleted theorem FirstOrder.Language.Formula.semanticallyEquivalent_not_not

deleted theorem FirstOrder.Language.Formula.sup_semanticallyEquivalent_not_inf_not

deleted theorem FirstOrder.Language.Theory.SemanticallyEquivalent.models_sentence_iff

deleted theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff

deleted theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_iff

deleted theorem FirstOrder.Language.Theory.SemanticallyEquivalent.refl

deleted theorem FirstOrder.Language.Theory.SemanticallyEquivalent.symm

deleted theorem FirstOrder.Language.Theory.SemanticallyEquivalent.trans

deleted def FirstOrder.Language.Theory.SemanticallyEquivalent

deleted def FirstOrder.Language.Theory.semanticallyEquivalentSetoid