Documentation

TauCeti.ModelTheory.Infinitary.Infinite

An infinitary sentence for infinite structures #

The sentence FirstOrder.Language.infiniteSentence is the countable conjunction of Mathlib's FirstOrder.Language.Sentence.cardGe sentences. It holds exactly in infinite structures, so conjoining it with a sentence restricts that sentence to its infinite models, without changing its models on an infinite carrier.

The cardinality assertions reuse Mathlib's FirstOrder.Language.Sentence.cardGe and FirstOrder.Language.Sentence.realize_cardGe; their characterization of infinite structures uses Cardinal.aleph0_le and Cardinal.infinite_iff.

source
def FirstOrder.Language.infiniteSentence (L : Language) :
L.Sentenceω

The countable conjunction asserting that the structure has at least n elements for every natural number n.

Instances For
    source
    theorem FirstOrder.Language.infiniteSentence_def (L : Language) :
    L.infiniteSentence = BoundedFormulaInf.iInf fun (n : ℕ) => BoundedFormula.toInf (Sentence.cardGe L n)

    The infinitude sentence is the conjunction of the finitary cardinality sentences.

    source
    @[simp]
    theorem FirstOrder.Language.realize_infiniteSentence_iff (L : Language) {M : Type w} [L.Structure M] :
    SentenceInf.Realize L.infiniteSentence M ↔ Infinite M

    A structure satisfies the infinitude sentence exactly when its carrier is infinite. This also applies to empty structures and to languages with function symbols.