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

Verification

Sorry-free, with every headline result depending on exactly the three standard axioms propext, Classical.choice, Quot.sound. See the latest release.

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, Lyndon and Malitz 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; and Malitz’s quantifier-class refinement, in which an entailment with universal consequent has a universal interpolant.
• 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.
• An honest coded-fragment interface — coded-family presentations, a fragment closed upward under exactly the families a presentation certifies and carrying no compactness data, and the HF fragment (the first-order image inside L_ω1ω) as its regression instance, with compactness derived from Mathlib rather than assumed. Barwise compactness and Nadel’s bound remain future results.

Documentation

• README — the results and their hypotheses, import bundles, and the directory layout
• Blueprint (web) · Blueprint (pdf) · Dependency graph
• API docs
• Releases · How to cite

Hypotheses and directory layout are maintained in the README, proof narratives in the blueprint, so neither can drift out of sync here.

_{Built from commit eec5b0e.}