A Lean 4 formalization of infinitary logic (L_∞ω and L_ω1ω) and its model theory, building on Mathlib.

Status

Sorry-free, with every headline result depending on exactly the three standard axioms propext, Classical.choice, Quot.sound. Latest release: v1.7.0.

Headline results

• Scott analysis and Karp’s theorem — every countable structure has a Scott sentence characterizing it up to isomorphism; Scott rank is a countable ordinal; back-and-forth equivalence at all ordinals characterizes L_∞ω-equivalence.
• Model existence and Löwenheim–Skolem — consistency properties, the Henkin construction, omitting types, Karp completeness, and downward Löwenheim–Skolem in both the sentence and fragment-elementary forms.
• Hanf numbers — ℶ_ω1 is a Hanf bound for every L_ω1ω-sentence over an arbitrary language, with no side hypotheses, and it is sharp: Hanf(L_ω1ω) = ℶ_ω1.
• Small models, complete sentences, categoricity — models of every infinite size realizing countably many types; small models lie in complete subclasses; κ-categorical sentences have κ-categorical complete completions.
• Craig and Lyndon interpolation — sharp shared-vocabulary interpolants over arbitrary languages, with the PC-separation form; and their polarity refinement, in which the interpolant’s positively (negatively) occurring relation symbols are bounded by the roots’ positive (negative) occurrences, equality being logical and unconstrained.
• Well-ordering — a uniform countable bound on the order types of well-ordered models (Marker 4.27); no sentence defines the class of well-orders; and the coded well-order class is not Borel.
• Descriptive set theory — the standard Borel structure space, Silver’s theorem and the Silver–Burgess dichotomy (via Miller’s category route, formalized here), and Morley counting.
• The López–Escobar theorem — a class of coded countable structures is Borel and isomorphism-invariant iff it is the model class of a single L_ω1ω-sentence; equivalently, the invariant Borel classes are exactly the range of ModelsOf.

Documentation

• README — precise statements, proof routes, import bundles, and the directory layout
• Blueprint (web) · Blueprint (pdf) · Dependency graph
• API docs
• Releases · How to cite

Scope, component-by-component contents, and proof-route narratives are maintained in the README only, so they cannot drift out of sync here.