Commit 2023-05-25 08:25 4a1f49bf

View on Github →

feat: port ModelTheory.Satisfiability (#3980)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Satisfiability.lean

added theorem Cardinal.Categorical.isComplete

added def Cardinal.Categorical

added theorem Cardinal.empty_infinite_Theory_isComplete

added theorem Cardinal.empty_theory_categorical

added theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_inf_not

added theorem FirstOrder.Language.BoundedFormula.IsQF.induction_on_sup_not

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.induction_on_all_ex

added theorem FirstOrder.Language.BoundedFormula.induction_on_exists_not

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.semanticallyEquivalent_toPrenex

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.IsComplete.models_not_iff

added theorem FirstOrder.Language.Theory.IsComplete.realize_sentence_iff

added def FirstOrder.Language.Theory.IsComplete

added def FirstOrder.Language.Theory.IsFinitelySatisfiable

added theorem FirstOrder.Language.Theory.IsMaximal.isComplete

added theorem FirstOrder.Language.Theory.IsMaximal.mem_iff_models

added theorem FirstOrder.Language.Theory.IsMaximal.mem_of_models

added theorem FirstOrder.Language.Theory.IsMaximal.mem_or_not_mem

added def FirstOrder.Language.Theory.IsMaximal

added theorem FirstOrder.Language.Theory.IsSatisfiable.isFinitelySatisfiable

added theorem FirstOrder.Language.Theory.IsSatisfiable.mono

added def FirstOrder.Language.Theory.IsSatisfiable

added theorem FirstOrder.Language.Theory.Model.isSatisfiable

added theorem FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence

added def FirstOrder.Language.Theory.ModelsBoundedFormula

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_bd_iff

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.realize_iff

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.refl

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.symm

added theorem FirstOrder.Language.Theory.SemanticallyEquivalent.trans

added def FirstOrder.Language.Theory.SemanticallyEquivalent

added theorem FirstOrder.Language.Theory.exists_large_model_of_infinite_model

added theorem FirstOrder.Language.Theory.exists_model_card_eq

added theorem FirstOrder.Language.Theory.isSatisfiable_directed_union_iff

added theorem FirstOrder.Language.Theory.isSatisfiable_empty

added theorem FirstOrder.Language.Theory.isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset

added theorem FirstOrder.Language.Theory.isSatisfiable_iff_isFinitelySatisfiable

added theorem FirstOrder.Language.Theory.isSatisfiable_of_isSatisfiable_onTheory

added theorem FirstOrder.Language.Theory.isSatisfiable_onTheory_iff

added theorem FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_card_le

added theorem FirstOrder.Language.Theory.isSatisfiable_union_distinctConstantsTheory_of_infinite

added theorem FirstOrder.Language.Theory.models_formula_iff

added theorem FirstOrder.Language.Theory.models_iff_not_satisfiable

added theorem FirstOrder.Language.Theory.models_sentence_iff

added theorem FirstOrder.Language.Theory.models_sentence_of_mem

added def FirstOrder.Language.Theory.semanticallyEquivalentSetoid

added theorem FirstOrder.Language.completeTheory.isComplete

added theorem FirstOrder.Language.completeTheory.isMaximal

added theorem FirstOrder.Language.completeTheory.isSatisfiable

added theorem FirstOrder.Language.completeTheory.mem_or_not_mem

added theorem FirstOrder.Language.exists_elementarilyEquivalent_card_eq

added theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq

added theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_ge

added theorem FirstOrder.Language.exists_elementaryEmbedding_card_eq_of_le