Theorems · Theorem · logic and foundations
Cardinal.Categorical.isComplete
∀ {L : FirstOrder.Language} (κ : Cardinal.{w}) (T : L.Theory),
κ.Categorical T →
Cardinal.aleph0 ≤ κ →
Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
T.IsSatisfiable → (∀ (M : T.ModelType), Infinite ↑M) → T.IsCompleteThe Łoś–Vaught Test : a criterion for categorical theories to be complete.
- Defined in
- Mathlib.ModelTheory.Satisfiability
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites30
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Cardinalstatement and proof · cited by 2,598
- FirstOrder.Languagestatement and proof · cited by 1,084
- Cardinal.mkproof · cited by 942
- FirstOrder.Language.Structureproof · cited by 775
- CategoryTheory.Bundled.αproof · cited by 736
- Cardinal.liftstatement and proof · cited by 583
- Cardinal.aleph0statement and proof · cited by 521
- Infinitestatement and proof · cited by 352
- Nonempty.someproof · cited by 340
- FirstOrder.Language.Theorystatement and proof · cited by 154
- FirstOrder.Language.Sentenceproof · cited by 127
- FirstOrder.Language.Equivproof · cited by 83
Cited by3
Results whose statement or proof uses this declaration.
- FirstOrder.Field.ACF_isCompleteproof · cited by 3
- FirstOrder.Language.dlo_isCompleteproof · cited by 0
- Cardinal.empty_infinite_Theory_isCompleteproof · cited by 0