Mathlib Map

Theorems · Definition · logic and foundations

FirstOrder.Language.Theory.IsMaximal

{L : FirstOrder.Language} → L.Theory → Prop

A theory is maximal when it is satisfiable and contains each sentence or its negation. Maximal theories are complete.

Defined in
Mathlib.ModelTheory.Satisfiability
Cited by
10 results in Mathlib
Foundations
Depth 9 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FirstOrder.Language.Theory.CompleteType.isMaximal · cited by 8CompleteType.isMaximalFirstOrder.Language.Theory.IsMaximal.mem_iff_models · cited by 3IsMaximal.mem_iff_modelsFirstOrder.Language.Theory.IsMaximal.isComplete · cited by 2IsMaximal.isCompleteFirstOrder.Language.Theory.IsMaximal.mem_of_models · cited by 2IsMaximal.mem_of_modelsFirstOrder.Language.Theory.IsMaximal.mem_or_not_mem · cited by 2IsMaximal.mem_or_not_memFirstOrder.Language.completeTheory.isMaximal · cited by 2completeTheory.isMaximalFirstOrder.Language.Theory.CompleteType.isMaximal' · cited by 1CompleteType.isMaximal'FirstOrder.Language.Theory.CompleteType.mk.inj · cited by 1mk.injFirstOrder.Language.Theory.CompleteType.mk.noConfusion · cited by 1mk.noConfusionFirstOrder.Language.Theory.CompleteType.noConfusion · cited by 0CompleteType.noConfusionFirstOrder.Language.Theory.CompleteType.noConfusionType · cited by 0CompleteType.noConfusionT…FirstOrder.Language.Theory.CompleteType.recOn · cited by 0CompleteType.recOnFirstOrder.Language.Theory.CompleteType.mk.injEq · cited by 0mk.injEqFirstOrder.Language.Theory.CompleteType.mk.sizeOf_spec · cited by 0mk.sizeOf_specFirstOrder.Language.Theory.CompleteType.casesOn · cited by 0CompleteType.casesOnFirstOrder.Language · cited by 1084FirstOrder.LanguageFirstOrder.Language.Theory · cited by 154Language.TheoryFirstOrder.Language.Sentence · cited by 127Language.SentenceFirstOrder.Language.Formula.not · cited by 27Formula.notFirstOrder.Language.Theory.IsSatisfiable · cited by 25Theory.IsSatisfiableTheory.IsMaximalCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by15

Results whose statement or proof uses this declaration.