The infiniteness axiom of L_ω₁ω

L_ω₁ω defines infiniteness, which first-order logic cannot: infiniteAxiom is the countable conjunction of Mathlib's finitary "there are at least n elements" sentences, embedded along Sentence.toLω, and realize_infiniteAxiom says a nonempty structure realizes it exactly when its carrier is infinite.

This is the standard device for restricting attention to infinite models — in particular for transferring a statement about coded countable structures (whose carrier is ℕ, hence infinite) to a statement about arbitrary models of a sentence, where a finite model would otherwise escape.

def FirstOrder.Language.infiniteAxiom (L : Language) : L.Sentenceω

The infiniteness axiom: the countable conjunction of the finitary sentences "there are at least n elements".

Equations

• L.infiniteAxiom = FirstOrder.Language.BoundedFormulaω.iInf fun (n : ℕ) => (FirstOrder.Language.Sentence.cardGe L n).toLω

@[simp]

theorem FirstOrder.Language.realize_infiniteAxiom {L : Language} {M : Type} [L.Structure M] [Nonempty M] : L.infiniteAxiom.Realize M ↔ Infinite M

A nonempty structure realizes the infiniteness axiom exactly when it is infinite.