Theorems · Definition · logic and foundations
FirstOrder.Language.completeTheory
(L : FirstOrder.Language) → (M : Type w) → [L.Structure M] → L.Theory
The complete theory of a structure M is the set of all sentences M satisfies.
- Defined in
- Mathlib.ModelTheory.Semantics
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses Quot.sound
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.
- Set.ofPredproof · cited by 6,101
- FirstOrder.Languagestatement and proof · cited by 1,084
- FirstOrder.Language.Structurestatement and proof · cited by 775
- FirstOrder.Language.Theorystatement · cited by 154
- FirstOrder.Language.Sentenceproof · cited by 127
- FirstOrder.Language.Sentence.Realizeproof · cited by 62
Cited by17
Results whose statement or proof uses this declaration.
- FirstOrder.Language.ElementarilyEquivalentproof · cited by 19
- FirstOrder.Language.mem_completeTheorystatement · cited by 3
- FirstOrder.Language.ElementarilyEquivalent.theory_model_iffproof · cited by 3
- FirstOrder.Language.Theory.typeOfproof · cited by 3
- FirstOrder.Language.Theory.CompleteType.setOfPred_subset_eq_empty_iffproof · cited by 3
- FirstOrder.Language.Theory.IsComplete.eq_complete_theorystatement · cited by 2
- FirstOrder.Language.Theory.model_iff_subset_completeTheorystatement · cited by 2
- FirstOrder.Language.elementaryDiagramproof · cited by 2
- FirstOrder.Language.completeTheory.isMaximalstatement · cited by 2
- FirstOrder.Language.ElementarilyEquivalent.completeTheory_eqstatement · cited by 1
- FirstOrder.Language.completeTheory.mem_or_not_memstatement · cited by 1
- FirstOrder.Language.Theory.completeTheory.subsetstatement · cited by 1