Satisfiability

📁 Source: Mathlib/ModelTheory/Satisfiability.lean

Statistics

Metric	Count
Definitions Categorical, IsComplete, IsFinitelySatisfiable, IsMaximal, IsSatisfiable, ModelsBoundedFormula, «term_⊨ᵇ_»	7
Theorems isComplete, empty_infinite_Theory_isComplete, empty_theory_categorical, eq_complete_theory, isComplete_iff_models_elementarily_equivalent, models_elementarily_equivalent, models_not_iff, realize_sentence_iff, isComplete, mem_iff_models, mem_of_models, mem_or_not_mem, isFinitelySatisfiable, mono, isSatisfiable, realize_boundedFormula, realize_formula, realize_sentence, exists_large_model_of_infinite_model, exists_model_card_eq, isSatisfiable_directed_union_iff, isSatisfiable_empty, isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset, isSatisfiable_iff_isFinitelySatisfiable, isSatisfiable_of_isSatisfiable_onTheory, isSatisfiable_onTheory_iff, isSatisfiable_union_distinctConstantsTheory_of_card_le, isSatisfiable_union_distinctConstantsTheory_of_infinite, models_formula_iff, models_formula_iff_onTheory_models_equivSentence, models_iff_finset_models, models_iff_not_satisfiable, models_of_models_theory, models_sentence_iff, models_sentence_of_mem, models_toFormula_iff, isComplete, isMaximal, isSatisfiable, mem_or_not_mem, exists_elementarilyEquivalent_card_eq, exists_elementaryEmbedding_card_eq, exists_elementaryEmbedding_card_eq_of_ge, exists_elementaryEmbedding_card_eq_of_le	44
Total	51

Cardinal

Definitions

Name	Category	Theorems
Categorical 📖	MathDef	3 math math: FirstOrder.Field.ACF_categorical, empty_theory_categorical, FirstOrder.Language.aleph0_categorical_dlo

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
empty_infinite_Theory_isComplete 📖	mathematical	—	FirstOrder.Language.Theory.IsComplete FirstOrder.Language.empty FirstOrder.Language.infiniteTheory	—	Categorical.isComplete empty_theory_categorical le_rfl FirstOrder.Language.card_empty lift_id canonicallyOrderedAdd FirstOrder.Language.model_infiniteTheory_iff instInfiniteNat FirstOrder.Language.Theory.ModelType.is_model
empty_theory_categorical 📖	mathematical	—	Categorical FirstOrder.Language.empty	—	FirstOrder.Language.empty.nonempty_equiv_iff

Cardinal.Categorical

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isComplete 📖	mathematical	Cardinal.Categorical Cardinal Cardinal.instLE Cardinal.aleph0 Cardinal.lift FirstOrder.Language.card Infinite FirstOrder.Language.Theory.ModelType.Carrier	FirstOrder.Language.Theory.IsComplete	—	FirstOrder.Language.Theory.exists_model_card_eq FirstOrder.Language.Theory.models_sentence_iff Mathlib.Tactic.Push.not_forall_eq FirstOrder.Language.exists_elementarilyEquivalent_card_eq FirstOrder.Language.ElementarilyEquivalent.realize_sentence FirstOrder.Language.StrongHomClass.realize_sentence FirstOrder.Language.Equiv.instStrongHomClass FirstOrder.Language.Sentence.realize_not

FirstOrder.Language

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_elementarilyEquivalent_card_eq 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Cardinal.lift card	ElementarilyEquivalent CategoryTheory.Bundled.α Structure CategoryTheory.Bundled.structure	—	exists_elementaryEmbedding_card_eq ElementarilyEquivalent.symm ElementaryEmbedding.elementarilyEquivalent
exists_elementaryEmbedding_card_eq 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Cardinal.lift card	ElementaryEmbedding CategoryTheory.Bundled.α Structure CategoryTheory.Bundled.structure	—	le_or_gt exists_elementaryEmbedding_card_eq_of_le Nontrivial.to_nonempty Infinite.instNontrivial exists_elementaryEmbedding_card_eq_of_ge le_of_lt
exists_elementaryEmbedding_card_eq_of_ge 📖	mathematical	Cardinal Cardinal.instLE Cardinal.lift card	ElementaryEmbedding CategoryTheory.Bundled.α Structure CategoryTheory.Bundled.structure	—	Theory.exists_large_model_of_infinite_model model_completeTheory exists_elementaryEmbedding_card_eq_of_le Theory.ModelType.nonempty' Cardinal.aleph0_le_lift LE.le.trans Cardinal.lift_lift Cardinal.lift_le card_withConstants Cardinal.lift_add add_comm Cardinal.add_eq_max Cardinal.infinite_iff max_le_iff Cardinal.lift_umax Cardinal.lift_id le_refl LHom.isExpansionOn_reduct ElementaryEmbedding.theory_model_iff Theory.ModelType.is_model
exists_elementaryEmbedding_card_eq_of_le 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Cardinal.lift card	ElementaryEmbedding CategoryTheory.Bundled.α Structure CategoryTheory.Bundled.structure	—	exists_elementarySubstructure_card_eq Cardinal.mk_eq_zero Set.instIsEmptyElemEmptyCollection Cardinal.lift_zero Cardinal.canonicallyOrderedAdd Cardinal.small_iff_lift_mk_lt_univ Cardinal.lift_lift Cardinal.lift_lt_univ' trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv Cardinal.lift_mk_shrink'

FirstOrder.Language.Theory

Definitions

Name	Category	Theorems
IsComplete 📖	MathDef	7 math math: FirstOrder.Language.dlo_isComplete, IsMaximal.isComplete, Cardinal.Categorical.isComplete, Cardinal.empty_infinite_Theory_isComplete, IsComplete.isComplete_iff_models_elementarily_equivalent, FirstOrder.Language.completeTheory.isComplete, FirstOrder.Field.ACF_isComplete
IsFinitelySatisfiable 📖	MathDef	2 math math: isSatisfiable_iff_isFinitelySatisfiable, IsSatisfiable.isFinitelySatisfiable
IsMaximal 📖	MathDef	3 math math: FirstOrder.Language.completeTheory.isMaximal, CompleteType.isMaximal', CompleteType.isMaximal
IsSatisfiable 📖	MathDef	17 math math: isSatisfiable_iff_isFinitelySatisfiable, isSatisfiable_directed_union_iff, CompleteType.nonempty_iff, simpleGraph_isSatisfiable, isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset, isSatisfiable_onTheory_iff, FirstOrder.Field.ACF_isSatisfiable, Model.isSatisfiable, IsSatisfiable.mono, isSatisfiable_empty, isSatisfiable_of_isSatisfiable_onTheory, CompleteType.setOf_subset_eq_empty_iff, isSatisfiable_union_distinctConstantsTheory_of_infinite, IsComplete.isComplete_iff_models_elementarily_equivalent, isSatisfiable_union_distinctConstantsTheory_of_card_le, FirstOrder.Language.completeTheory.isSatisfiable, models_iff_not_satisfiable
ModelsBoundedFormula 📖	MathDef	17 math math: FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime, models_iff_finset_models, FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize, FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero, models_formula_iff, IsComplete.models_not_iff, models_sentence_iff, models_formula_iff_onTheory_models_equivSentence, FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize, CompleteType.setOf_mem_eq_univ_iff, IsMaximal.mem_iff_models, IsComplete.realize_sentence_iff, models_sentence_of_mem, models_toFormula_iff, CompleteType.setOf_subset_eq_univ_iff, IsComplete.eq_complete_theory, models_iff_not_satisfiable
«term_⊨ᵇ_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_large_model_of_infinite_model 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.lift ModelType.Carrier	—	isSatisfiable_union_distinctConstantsTheory_of_infinite ModelType.nonempty' Model.mono ModelType.is_model Set.subset_union_left ModelType.reduct_Carrier coe_of trans instIsTransLe Cardinal.lift_le le_of_eq Cardinal.mk_out Cardinal.mk_univ LE.le.trans FirstOrder.Language.card_le_of_model_distinctConstantsTheory Set.subset_union_right Cardinal.lift_lift le_refl
exists_model_card_eq 📖	—	Infinite ModelType.Carrier Cardinal Cardinal.instLE Cardinal.aleph0 Cardinal.lift FirstOrder.Language.card	—	—	FirstOrder.Language.exists_elementarilyEquivalent_card_eq FirstOrder.Language.ElementarilyEquivalent.nonempty ModelType.nonempty' FirstOrder.Language.ElementarilyEquivalent.theory_model ModelType.is_model
isSatisfiable_directed_union_iff 📖	mathematical	Directed FirstOrder.Language.Theory Set.instHasSubset FirstOrder.Language.Sentence	IsSatisfiable Set.iUnion	—	IsSatisfiable.mono Set.subset_iUnion isSatisfiable_iff_isFinitelySatisfiable IsFinitelySatisfiable.eq_1 Directed.exists_mem_subset_of_finset_subset_biUnion
isSatisfiable_empty 📖	mathematical	—	IsSatisfiable FirstOrder.Language.Theory Set.instEmptyCollection FirstOrder.Language.Sentence	—	—
isSatisfiable_iUnion_iff_isSatisfiable_iUnion_finset 📖	mathematical	—	IsSatisfiable Set.iUnion FirstOrder.Language.Sentence Finset Finset.instMembership	—	IsSatisfiable.mono Set.iUnion_mono Set.iUnion_subset_iff refl Set.instReflSubset isSatisfiable_iff_isFinitelySatisfiable Directed.exists_mem_subset_of_finset_subset_biUnion Monotone.directed_le Finset.isDirected_le Set.iUnion_mono' Set.iUnion_eq_iUnion_finset
isSatisfiable_iff_isFinitelySatisfiable 📖	mathematical	—	IsSatisfiable IsFinitelySatisfiable	—	IsSatisfiable.isFinitelySatisfiable Finset.map_subtype_subset Filter.atTop_neBot Finset.isDirected_le FirstOrder.Language.Ultraproduct.sentence_realize ModelType.nonempty' Filter.Eventually.filter_mono Ultrafilter.of_le Filter.eventually_atTop realize_sentence_of_mem ModelType.is_model Finset.coe_map Set.image_congr Finset.mem_singleton_self FirstOrder.Language.Ultraproduct.Product.instNonempty
isSatisfiable_of_isSatisfiable_onTheory 📖	mathematical	—	IsSatisfiable	—	Model.isSatisfiable ModelType.nonempty' ModelType.is_model
isSatisfiable_onTheory_iff 📖	mathematical	FirstOrder.Language.LHom.Injective	IsSatisfiable FirstOrder.Language.LHom.onTheory	—	isSatisfiable_of_isSatisfiable_onTheory Model.isSatisfiable ModelType.nonempty' ModelType.is_model
isSatisfiable_union_distinctConstantsTheory_of_card_le 📖	mathematical	—	IsSatisfiable FirstOrder.Language.withConstants FirstOrder.Language.Theory Set.instUnion FirstOrder.Language.Sentence FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants FirstOrder.Language.distinctConstantsTheory	—	Cardinal.lift_mk_le' Model.union FirstOrder.Language.LHom.onTheory_model FirstOrder.Language.withConstants_expansion FirstOrder.Language.model_distinctConstantsTheory Function.Embedding.injective Function.Injective.extend_apply Subtype.coe_injective Model.isSatisfiable
isSatisfiable_union_distinctConstantsTheory_of_infinite 📖	mathematical	—	IsSatisfiable FirstOrder.Language.withConstants FirstOrder.Language.Theory Set.instUnion FirstOrder.Language.Sentence FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants FirstOrder.Language.distinctConstantsTheory	—	FirstOrder.Language.distinctConstantsTheory_eq_iUnion Set.union_iUnion isSatisfiable_directed_union_iff Monotone.directed_le Finset.isDirected_le Monotone.union monotone_const Monotone.comp FirstOrder.Language.monotone_distinctConstantsTheory Finset.coe_map Set.image_congr Set.monotone_image Finset.coe_subset isSatisfiable_union_distinctConstantsTheory_of_card_le Nontrivial.to_nonempty Infinite.instNontrivial LE.le.trans Cardinal.lift_le_aleph0 LT.lt.le Cardinal.finset_card_lt_aleph0 Cardinal.aleph0_le_lift
models_formula_iff 📖	mathematical	—	ModelsBoundedFormula FirstOrder.Language.Formula.Realize ModelType.Carrier ModelType.struc	—	Unique.forall_iff Fin.isEmpty'
models_formula_iff_onTheory_models_equivSentence 📖	mathematical	—	ModelsBoundedFormula FirstOrder.Language.withConstants FirstOrder.Language.LHom.onTheory FirstOrder.Language.lhomWithConstants DFunLike.coe Equiv FirstOrder.Language.Formula FirstOrder.Language.Sentence EquivLike.toFunLike Equiv.instEquivLike FirstOrder.Language.Formula.equivSentence	—	models_sentence_iff FirstOrder.Language.LHom.isExpansionOn_reduct FirstOrder.Language.Formula.realize_equivSentence FirstOrder.Language.LHom.onTheory_model ModelType.is_model ModelType.nonempty' Fin.isEmpty' models_formula_iff FirstOrder.Language.withConstants_expansion ModelsBoundedFormula.realize_sentence
models_iff_finset_models 📖	mathematical	—	ModelsBoundedFormula Set FirstOrder.Language.Sentence Set.instHasSubset SetLike.coe Finset Finset.instSetLike	—	isSatisfiable_iff_isFinitelySatisfiable IsFinitelySatisfiable.eq_1 Mathlib.Tactic.Contrapose.contrapose_iff₂ Mathlib.Tactic.Push.not_and_eq Set.union_singleton Finset.union_singleton Finset.coe_insert Finset.coe_union Finset.coe_singleton Set.union_subset_union Set.Subset.refl IsSatisfiable.mono Finset.coe_erase Set.insert_diff_singleton
models_iff_not_satisfiable 📖	mathematical	—	ModelsBoundedFormula IsSatisfiable FirstOrder.Language.Theory Set.instUnion FirstOrder.Language.Sentence FirstOrder.Language.Formula Set.instSingletonSet FirstOrder.Language.Formula.not	—	models_sentence_iff IsSatisfiable.eq_1 Set.subset_union_left FirstOrder.Language.Sentence.realize_not realize_sentence_of_mem ModelType.subtheoryModel_models Set.subset_union_right Set.mem_singleton Mathlib.Tactic.Contrapose.contrapose₂ ModelType.is_model Set.mem_singleton_iff ModelType.nonempty'
models_of_models_theory 📖	—	ModelsBoundedFormula	—	—	model_iff ModelsBoundedFormula.realize_sentence ModelType.is_model ModelType.nonempty'
models_sentence_iff 📖	mathematical	—	ModelsBoundedFormula FirstOrder.Language.Sentence.Realize ModelType.Carrier ModelType.struc	—	models_formula_iff Unique.forall_iff Empty.instIsEmpty
models_sentence_of_mem 📖	mathematical	FirstOrder.Language.Sentence FirstOrder.Language.Theory Set.instMembership	ModelsBoundedFormula	—	models_sentence_iff realize_sentence_of_mem ModelType.is_model
models_toFormula_iff 📖	mathematical	—	ModelsBoundedFormula FirstOrder.Language.BoundedFormula.toFormula	—	ModelsBoundedFormula.realize_formula ModelType.is_model ModelType.nonempty'

FirstOrder.Language.Theory.IsComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_complete_theory 📖	mathematical	FirstOrder.Language.Theory.IsComplete	setOf FirstOrder.Language.BoundedFormula FirstOrder.Language.Theory.ModelsBoundedFormula FirstOrder.Language.completeTheory	—	Set.ext FirstOrder.Language.mem_completeTheory FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence FirstOrder.Language.Sentence.realize_not
isComplete_iff_models_elementarily_equivalent 📖	mathematical	—	FirstOrder.Language.Theory.IsComplete FirstOrder.Language.Theory.IsSatisfiable FirstOrder.Language.ElementarilyEquivalent FirstOrder.Language.Theory.ModelType.Carrier FirstOrder.Language.Theory.ModelType.struc	—	FirstOrder.Language.ElementarilyEquivalent.eq_1 eq_complete_theory FirstOrder.Language.Theory.ModelType.is_model FirstOrder.Language.Theory.ModelType.nonempty' FirstOrder.Language.Theory.models_sentence_iff FirstOrder.Language.elementarilyEquivalent_iff FirstOrder.Language.Sentence.realize_not
models_elementarily_equivalent 📖	mathematical	FirstOrder.Language.Theory.IsComplete	FirstOrder.Language.ElementarilyEquivalent	—	FirstOrder.Language.ElementarilyEquivalent.eq_1 eq_complete_theory
models_not_iff 📖	mathematical	FirstOrder.Language.Theory.IsComplete	FirstOrder.Language.Theory.ModelsBoundedFormula FirstOrder.Language.Formula.not	—	FirstOrder.Language.Theory.models_sentence_iff
realize_sentence_iff 📖	mathematical	FirstOrder.Language.Theory.IsComplete	FirstOrder.Language.Sentence.Realize FirstOrder.Language.Theory.ModelsBoundedFormula	—	FirstOrder.Language.Theory.ModelsBoundedFormula.realize_sentence FirstOrder.Language.Sentence.realize_not models_not_iff

FirstOrder.Language.Theory.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isComplete 📖	mathematical	FirstOrder.Language.Theory.IsMaximal	FirstOrder.Language.Theory.IsComplete	—	FirstOrder.Language.Theory.models_sentence_of_mem
mem_iff_models 📖	mathematical	FirstOrder.Language.Theory.IsMaximal	FirstOrder.Language.Sentence FirstOrder.Language.Theory Set.instMembership FirstOrder.Language.Theory.ModelsBoundedFormula	—	FirstOrder.Language.Theory.models_sentence_of_mem mem_of_models
mem_of_models 📖	mathematical	FirstOrder.Language.Theory.IsMaximal FirstOrder.Language.Theory.ModelsBoundedFormula	FirstOrder.Language.Sentence FirstOrder.Language.Theory Set.instMembership	—	mem_or_not_mem Set.insert_eq_of_mem Set.union_singleton FirstOrder.Language.Theory.models_iff_not_satisfiable
mem_or_not_mem 📖	mathematical	FirstOrder.Language.Theory.IsMaximal	FirstOrder.Language.Sentence FirstOrder.Language.Theory Set.instMembership FirstOrder.Language.Formula FirstOrder.Language.Formula.not	—	—

FirstOrder.Language.Theory.IsSatisfiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFinitelySatisfiable 📖	mathematical	—	FirstOrder.Language.Theory.IsFinitelySatisfiable	—	mono
mono 📖	mathematical	FirstOrder.Language.Theory Set.instHasSubset FirstOrder.Language.Sentence	FirstOrder.Language.Theory.IsSatisfiable	—	FirstOrder.Language.Theory.ModelType.nonempty' FirstOrder.Language.Theory.Model.mono FirstOrder.Language.Theory.ModelType.is_model

FirstOrder.Language.Theory.Model

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSatisfiable 📖	mathematical	—	FirstOrder.Language.Theory.IsSatisfiable	—	FirstOrder.Language.Theory.ModelType.nonempty' FirstOrder.Language.ElementarySubstructure.toModel.instSmall FirstOrder.Language.Substructure.elementarySkolem₁Reduct.instSmall

FirstOrder.Language.Theory.ModelsBoundedFormula

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realize_boundedFormula 📖	mathematical	FirstOrder.Language.Theory.ModelsBoundedFormula	FirstOrder.Language.BoundedFormula.Realize	—	realize_formula FirstOrder.Language.Theory.models_toFormula_iff
realize_formula 📖	mathematical	FirstOrder.Language.Theory.ModelsBoundedFormula	FirstOrder.Language.Formula.Realize	—	FirstOrder.Language.LHom.onTheory_model FirstOrder.Language.withConstants_expansion FirstOrder.Language.Formula.realize_equivSentence realize_sentence FirstOrder.Language.Theory.models_formula_iff_onTheory_models_equivSentence
realize_sentence 📖	mathematical	FirstOrder.Language.Theory.ModelsBoundedFormula	FirstOrder.Language.Sentence.Realize	—	Mathlib.Tactic.Contrapose.contrapose₂ Set.union_singleton FirstOrder.Language.Theory.model_iff FirstOrder.Language.Theory.Model.isSatisfiable FirstOrder.Language.Theory.models_iff_not_satisfiable

FirstOrder.Language.completeTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isComplete 📖	mathematical	—	FirstOrder.Language.Theory.IsComplete FirstOrder.Language.completeTheory	—	FirstOrder.Language.Theory.IsMaximal.isComplete isMaximal
isMaximal 📖	mathematical	—	FirstOrder.Language.Theory.IsMaximal FirstOrder.Language.completeTheory	—	isSatisfiable mem_or_not_mem
isSatisfiable 📖	mathematical	—	FirstOrder.Language.Theory.IsSatisfiable FirstOrder.Language.completeTheory	—	FirstOrder.Language.Theory.Model.isSatisfiable FirstOrder.Language.model_completeTheory
mem_or_not_mem 📖	mathematical	—	FirstOrder.Language.Sentence FirstOrder.Language.Theory Set.instMembership FirstOrder.Language.completeTheory FirstOrder.Language.Formula FirstOrder.Language.Formula.not	—	Empty.instIsEmpty

---

← Back to Index