Commit 2024-10-02 18:00 74620cae

View on Github →

feat(ModelTheory/Equivalence): Implication of formulas modulo a theory (#16800) Defines FirstOrder.Language.Theory.Implies: φ ⟹[T] ψ indicates that φ implies ψ in models of T. Relates Theory.Implies to Theory.SemanticallyEquivalent. Proves lemmas that will set up a BooleanAlgebra instance on formulas modulo a theory

Estimated changes

Modified Mathlib/ModelTheory/Complexity.lean

added theorem FirstOrder.Language.BoundedFormula.iff_toPrenex

deleted theorem FirstOrder.Language.BoundedFormula.semanticallyEquivalent_toPrenex

Modified Mathlib/ModelTheory/Equivalence.lean

added theorem FirstOrder.Language.BoundedFormula.all_iff_not_ex_not

deleted theorem FirstOrder.Language.BoundedFormula.all_semanticallyEquivalent_not_ex_not

added theorem FirstOrder.Language.BoundedFormula.ex_iff_not_all_not

deleted theorem FirstOrder.Language.BoundedFormula.ex_semanticallyEquivalent_not_all_not

added theorem FirstOrder.Language.BoundedFormula.iff_all_liftAt

added theorem FirstOrder.Language.BoundedFormula.iff_not_not

added theorem FirstOrder.Language.BoundedFormula.imp_iff_not_sup

deleted theorem FirstOrder.Language.BoundedFormula.imp_semanticallyEquivalent_not_sup

added theorem FirstOrder.Language.BoundedFormula.inf_iff_not_sup_not

added theorem FirstOrder.Language.BoundedFormula.inf_not_iff_bot

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

added theorem FirstOrder.Language.BoundedFormula.sup_iff_not_inf_not

added theorem FirstOrder.Language.BoundedFormula.sup_not_iff_top

deleted theorem FirstOrder.Language.BoundedFormula.sup_semanticallyEquivalent_not_inf_not

added theorem FirstOrder.Language.Formula.iff_not_not

added theorem FirstOrder.Language.Formula.imp_iff_not_sup

deleted theorem FirstOrder.Language.Formula.imp_semanticallyEquivalent_not_sup

added theorem FirstOrder.Language.Formula.inf_iff_not_sup_not

deleted theorem FirstOrder.Language.Formula.inf_semanticallyEquivalent_not_sup_not

deleted theorem FirstOrder.Language.Formula.semanticallyEquivalent_not_not

added theorem FirstOrder.Language.Formula.sup_iff_not_inf_not

deleted theorem FirstOrder.Language.Formula.sup_semanticallyEquivalent_not_inf_not

added theorem FirstOrder.Language.Theory.Iff.models_sentence_iff

added theorem FirstOrder.Language.Theory.Iff.realize_bd_iff

added theorem FirstOrder.Language.Theory.Iff.realize_iff

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 def FirstOrder.Language.Theory.SemanticallyEquivalent

added theorem FirstOrder.Language.Theory.bot_imp

added def FirstOrder.Language.Theory.iffSetoid

added theorem FirstOrder.Language.Theory.iff_iff_imp_and_imp

added theorem FirstOrder.Language.Theory.imp_antisymm

added theorem FirstOrder.Language.Theory.imp_inf

added theorem FirstOrder.Language.Theory.imp_inf_iff

added theorem FirstOrder.Language.Theory.imp_sup_left

added theorem FirstOrder.Language.Theory.imp_sup_right

added theorem FirstOrder.Language.Theory.imp_top

added theorem FirstOrder.Language.Theory.inf_imp_left

added theorem FirstOrder.Language.Theory.inf_imp_right

deleted def FirstOrder.Language.Theory.semanticallyEquivalentSetoid

added theorem FirstOrder.Language.Theory.sup_imp

added theorem FirstOrder.Language.Theory.sup_imp_iff