A Lean 4 formalization of infinitary logic (L_∞ω and L_ω1ω), Scott sentences, and classical results in infinitary model theory, building on Mathlib.

Main Results

• Scott sentences — Every countable structure in a countable relational language has a Scott sentence characterizing it up to isomorphism among countable structures.
• Scott rank < ω₁ — The Scott rank of any countable structure is a countable ordinal.
• Karp’s theorem — Back-and-forth equivalence at all ordinals characterizes L_∞ω elementary equivalence.
• Model existence — Every countable consistent set of L_ω1ω sentences in a countable language has a countable model (Henkin-style construction, omitting types, Karp completeness).

Scope

The formalization currently covers:

• L_∞ω infrastructure — syntax (BoundedFormulaInf with arbitrary index types for conjunctions/disjunctions), semantics, quantifier rank, and conversions between L_∞ω and L_ω1ω.
• Scott analysis — atomic diagrams, back-and-forth equivalence indexed by ordinals, Scott formulas/sentences, Scott height and rank, and the countable refinement hypothesis.
• Karp’s theorem — potential isomorphisms, the main equivalence (karp_theorem_w), and corollaries for countable structures.
• Model existence — consistency properties, Henkin construction, truth lemma, model existence theorem, Karp completeness, and omitting types.
• Further model theory — downward Löwenheim–Skolem for L_ω1ω, Hanf numbers, conditional Morley–Hanf bound (conditional on MorleyHanfTransfer), and counting models (Morley counting theorem: ≤ ℵ₁ or 2^ℵ₀ iso classes).
• Silver–Burgess dichotomy — splitting lemma, Cantor scheme, Silver’s theorem for closed equivalence relations on Polish spaces, and silverBurgessDichotomy (1 sorry: borel_to_closed_reduction in GandyHarrington.lean, Gandy–Harrington topology).
• Admissible fragments — Barwise compactness, Barwise completeness II, and the Nadel bound.

Some results carry explicit hypotheses that package external mathematical content not yet formalized (e.g., MorleyHanfTransfer for Erdős–Rado / Ehrenfeucht–Mostowski machinery, SilverBurgessDichotomy for the Silver–Burgess dichotomy).

Components

Directory	Contents
InfinitaryLogic/Linf/	L∞ω syntax, semantics, operations, countability predicates, quantifier rank
InfinitaryLogic/Lomega1omega/	Lω1ω syntax, semantics, operations, embedding, quantifier rank
InfinitaryLogic/Scott/	Atomic diagrams, back-and-forth equivalence, Scott formulas/sentences, rank, height
InfinitaryLogic/Karp/	Karp’s theorem and corollaries for countable structures
InfinitaryLogic/ModelExistence/	Consistency properties, model existence, completeness, omitting types
InfinitaryLogic/ModelTheory/	Löwenheim–Skolem, Hanf numbers, counting models
InfinitaryLogic/Admissible/	Admissible fragments, Barwise compactness, Nadel bound
InfinitaryLogic/Descriptive/	Borel complexity of structure space, satisfaction, isomorphism; Silver-Burgess dichotomy (splitting lemma, Cantor scheme, silverBurgessDichotomy; 1 sorry: borel_to_closed_reduction in GandyHarrington.lean)

Resources

• Blueprint (web) · Blueprint (pdf)
• API docs
• Dependency graph

References

• Barwise, J. (1975). Admissible Sets and Structures. Springer-Verlag.
• Karp, C. R. (1964). Languages with Expressions of Infinite Length. North-Holland.
• Karp, C. R. (1965). Finite-Quantifier Equivalence. In The Theory of Models, 407–412.
• Keisler, H. J. (1971). Model Theory for Infinitary Logic. North-Holland.
• Keisler, H. J. & Knight, J. F. (2004). Barwise: Infinitary Logic and Admissible Sets. Bulletin of Symbolic Logic, 10(1), 4–36.
• Marker, D. (2016). Lectures on Infinitary Model Theory. Cambridge University Press.
• Nadel, M. E. (1974). Scott sentences and admissible sets. Annals of Mathematical Logic, 7(2–3), 267–294.