Theorems · Definition · logic and foundations
FirstOrder.Language.Theory.IsComplete
{L : FirstOrder.Language} → L.Theory → PropA theory is complete when it is satisfiable and models each sentence or its negation.
- Defined in
- Mathlib.ModelTheory.Satisfiability
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Theorystatement and proof · cited by 154
- FirstOrder.Language.Sentenceproof · cited by 127
- FirstOrder.Language.Theory.ModelsBoundedFormulaproof · cited by 30
- FirstOrder.Language.Formula.notproof · cited by 27
- FirstOrder.Language.Theory.IsSatisfiableproof · cited by 25
Cited by11
Results whose statement or proof uses this declaration.
- FirstOrder.Field.ACF_isCompletestatement · cited by 3
- Cardinal.Categorical.isCompletestatement · cited by 3
- FirstOrder.Language.Theory.IsComplete.realize_sentence_iffstatement and proof · cited by 3
- FirstOrder.Language.Theory.IsMaximal.isCompletestatement · cited by 2
- FirstOrder.Language.Theory.IsComplete.eq_complete_theorystatement and proof · cited by 2
- FirstOrder.Language.Theory.IsComplete.models_not_iffstatement and proof · cited by 2
- Cardinal.empty_infinite_Theory_isCompletestatement · cited by 0
- FirstOrder.Language.Theory.IsComplete.isComplete_iff_models_elementarily_equivalentstatement and proof · cited by 0
- FirstOrder.Language.Theory.IsComplete.models_elementarily_equivalentstatement and proof · cited by 0
- FirstOrder.Language.dlo_isCompletestatement · cited by 0
- FirstOrder.Language.completeTheory.isCompletestatement · cited by 0