Infinitary Logic Formalization Blueprint
1 Infinitary Logic
This project formalizes results in infinitary logic in Lean 4 using Mathlib. The primary focus is the logic \(\mathcal{L}_{\omega _1\omega }\), which extends first-order logic with countable conjunctions and disjunctions, though the formalization treats the more general \(L_{\infty \omega }\) (allowing arbitrary conjunctions and disjunctions) where possible.
1.1 Main Results
The formalization establishes five headline theorems:
Scott characterization. Every countable structure is characterized up to isomorphism by a sentence of \(\mathcal{L}_{\omega _1\omega }\) (Theorem 9).
Scott rank below \(\omega _1\). The Scott rank of any countable structure is a countable ordinal (Theorem 11).
Karp’s theorem. Two structures are \(L_{\infty \omega }\)-equivalent if and only if there exists a back-and-forth system between them (Theorem 16).
Model existence. Every consistent set of sentences of \(\mathcal{L}_{\omega _1\omega }\) has a model (Theorem 17).
Countable refinement hypothesis. The back-and-forth hierarchy on any countable structure stabilizes in countably many steps (Theorem 8).
1.2 Back-and-Forth Equivalence
Back-and-forth equivalence at ordinal levels, following Karp [ Kar65 ] .
Back-and-forth equivalence \(\sim _\alpha (a,b)\) for tuples \(a \in M^n\), \(b \in N^n\) at ordinal \(\alpha \), defined by transfinite recursion: atomic agreement at \(0\), forth-and-back extension at successor, conjunction at limit.
1.3 Scott Formulas and Sentences
Scott formulas and their characteristic property, following Marker [ Mar16 , Ch. 2 ] .
The Scott formula \(\sigma _\alpha (a)\) for a tuple \(a \in M^n\) and ordinal \(\alpha {\lt} \omega _1\): an \(\mathcal{L}_{\omega _1\omega }\)-formula mirroring the recursive definition of \(\sim _\alpha \).
For countable \(M\) and \(\alpha {\lt} \omega _1\): \(\sigma _\alpha (a)\) is realized by \(b\) in \(N\) if and only if \(\sim _\alpha (a,b)\).
By ordinal induction using limitRecOn: the zero case reduces to atomic diagrams, the successor case uses the forth/back quantifier structure of the Scott formula, and the limit case uses countable infimum.
1.4 Self-Stabilization
For any countable \(L\)-structure \(M\), there exists \(\alpha {\lt} \omega _1\) such that \(M\) self-stabilizes completely at \(\alpha \): for every \(n\) and tuples \(a, a' \in M^n\), \(\sim _\alpha (a,a') \iff \sim _{\alpha +1}(a,a')\).
For each triple \((n, a, a')\), the first failure ordinal is \(0\) or a successor. Take the supremum over countably many triples; \(\sup + 1 {\lt} \omega _1\).
1.5 Scott Sentence
The stabilization ordinal of a countable structure \(M\): the least ordinal \(\alpha \) such that \(\sim _\alpha \) on \(0\)-tuples characterizes isomorphism among countable structures.
The Scott sentence of \(M\): the Scott formula for the empty tuple at the stabilization ordinal, \(\sigma _{\alpha _0}(\langle \rangle )\).
Assuming the countable refinement hypothesis: the Scott sentence of a countable structure \(M\) characterizes \(M\) up to isomorphism among countable structures, i.e., \(N \models \sigma _M \iff M \cong N\).
By the Scott formula characterization at the stabilization ordinal, plus the CRH-conditional stabilization result.
2 Countable Refinement
The countable refinement hypothesis and its consequences for Scott rank.
2.1 Countable Refinement Hypothesis
For any countable relational language \(L\), countable \(L\)-structure \(M\), tuple size \(n\), and tuple \(a \in M^n\), the set of refinement ordinals \(\{ \varepsilon {\lt} \omega _1\mid \exists (N, b)\, \sim _\varepsilon (a,b) \wedge \neg \sim _{\varepsilon +1}(a,b)\} \) is countable.
From self-stabilization: witnesses at \(\alpha _0\) persist at all \(\alpha _0 + k\). The chain \(\alpha _0, \alpha _0+1, \ldots \) has limit \(\gamma {\lt} \omega _1\) which is itself a limit ordinal, giving BFEquiv at \(\gamma \) and hence at all ordinals.
Note: Despite its name, the “Countable Refinement Hypothesis” is fully proved in this formalization. The name is historical: it was originally an open conjecture about the countability of refinement ordinals. The proof here proceeds via self-stabilization and transfinite induction.
This countability result drives the downstream stabilization argument: since only countably many ordinals can witness a strict refinement, the hierarchy must stabilize below \(\omega _1\).
The Scott sentence of a countable structure \(M\) characterizes \(M\) up to isomorphism among countable structures (unconditional corollary of CRH).
Instantiate the conditional characterization theorem with the proved Countable Refinement Hypothesis.
2.2 Scott Rank and Height
The Scott rank of a countable structure \(M\): \(\mathrm{sr}(M) = \sup _{m \in M}(\mathrm{er}(m) + 1)\), where \(\mathrm{er}(m)\) is the element rank.
For any countable \(L\)-structure \(M\), \(\mathrm{sr}(M) {\lt} \omega _1\).
By the Countable Refinement Hypothesis, each element rank is countable, and the Scott rank is their supremum.
The Scott height of a countable structure \(M\): the least ordinal \(\alpha \) such that \(\sim _\alpha (a,b) \Rightarrow \sim _{\alpha +1}(a,b)\) for all tuples \(a,b\) in any countable structures.
For any countable \(L\)-structure \(M\), \(\mathrm{sh}(M) {\lt} \omega _1\).
By the Countable Refinement Hypothesis, the BF-equivalence hierarchy stabilizes at a countable ordinal for each tuple size, and the Scott height is their supremum.
3 Karp’s Theorem
Karp’s theorem characterizes \(L_{\infty \omega }\)-equivalence via back-and-forth systems, following Karp [ Kar65 ] .
A potential isomorphism between \(L\)-structures \(M\) and \(N\): a nonempty family of finite partial maps (pairs of same-length tuples) preserving atomic type and closed under extension in both directions.
\(L_{\infty \omega }\)-equivalence: \(M\) and \(N\) satisfy the same \(L_{\infty \omega }^w\) sentences, where \(w\) is the universe of the index types.
\(M\) and \(N\) admit a potential isomorphism if and only if they are \(L_{\infty \omega }^w\)-equivalent (satisfy the same \(L_{\infty \omega }\) sentences with index types in universe \(w\)).
Forward: a potential isomorphism witnesses agreement on all \(L_{\infty \omega }\) sentences by induction on formula complexity. Backward: BFEquiv at all ordinals gives a potential isomorphism via the game-tree family.
4 Model Existence
Model existence and completeness for \(\mathcal{L}_{\omega _1\omega }\), following Keisler [ Kei71 ] .
If a countable set \(S\) of \(\mathcal{L}_{\omega _1\omega }\) sentences in a countable language belongs to a consistency property with equality axioms, then \(S\) has a countable model.
Henkin construction: extend the language with constants, extend \(S\) to a maximal consistent set, build a term model, verify via truth lemma.
A sentence in a countable language that belongs to some consistency property with equality axioms has a countable model.
Specialize the model existence theorem to the singleton theory \(\{ \varphi \} \) and extract the sentence from the resulting model.
4.1 Omitting Types
A structure \(M\) omits a type \(p\) (a set of formulas in one free variable) if no element of \(M\) realizes all formulas in \(p\) simultaneously.
Given a countable consistent theory \(T\) in a countable language and a countable collection of non-isolated types, there exists a countable model of \(T\) that omits all the given types.
Build a term model via the model existence theorem, then derive a contradiction for any element that would realize all formulas in an omitted type.
5 Löwenheim–Skolem
The downward Löwenheim–Skolem theorem for \(\mathcal{L}_{\omega _1\omega }\).
The naming function for the extended language \(L[[M]]\): each element \(m \in M\) is named by the constant symbol \(\operatorname {con}(m)\).
Given a countable model \(M\) of an \(\mathcal{L}_{\omega _1\omega }\) sentence \(\varphi \) in a countable language, one can construct a countable model in the same universe as \(M\) via language expansion \(L[[M]]\) and the model existence theorem.
The key step is the language expansion: extend \(L\) with a constant for each element of \(M\) to form \(L[[M]]\), which remains countable. A naming function witnessing the constants lets us build a consistency property in \(L[[M]]\); the model existence theorem then produces a fresh countable term model \(N\), which we restrict back to \(L\).
Given a countable model \(M\) of a countable \(\mathcal{L}_{\omega _1\omega }\) theory \(T\) in a countable language, one can reconstruct a countable model in the same universe as \(M\) via language expansion \(L[[M]]\) and the model existence theorem.
Same language-expansion strategy as the sentence version: lift the entire theory to \(L[[M]]\), use the naming function to build a consistency property witnessing all sentences, apply model existence for the countable term model, then restrict the \(L[[M]]\)-structure back to \(L\).
6 Admissible Fragments
Compactness and completeness for countable admissible fragments of \(\mathcal{L}_{\omega _1\omega }\), following Barwise [ Bar75 ] . Background on the Nadel bound for admissible fragments can be found in Nadel [ Nad74 ] .
An admissible fragment of \(\mathcal{L}_{\omega _1\omega }\): a collection of sentences closed under subformulas, negation, quantification, and countable conjunction/disjunction, with a compactness axiom for finite subsets.
If every \(A\)-finite subset of a theory \(T \subseteq A\) has a model, then \(T\) has a model.
Direct application of the compactness property of the admissible fragment to the finite-satisfiability hypothesis.
A countable theory in an admissible fragment that belongs to a consistency property has a countable model.
Extract the consistency property witness and apply the model existence theorem to obtain a countable term model.
7 Hanf Numbers
Hanf numbers measure how large a model a sentence must have before it has arbitrarily large models.
A sentence \(\varphi \) has arbitrarily large models if for every cardinal \(\kappa \) there is a model of \(\varphi \) of cardinality \(\geq \kappa \).
\(\kappa \) is a Hanf bound for \(\varphi \) if having a model of cardinality \(\geq \kappa \) implies having arbitrarily large models.
The Hanf number of a sentence \(\varphi \): the least cardinal that is a Hanf bound.
Every \(\mathcal{L}_{\omega _1\omega }\) sentence has a Hanf bound (and therefore a Hanf number).
Case split: if \(\varphi \) has arbitrarily large models then any cardinal is a bound; otherwise there is a cutoff cardinal above which no models exist, so the premise is vacuously false.
7.1 Morley–Hanf Bound
Status: conditional. This result depends on MorleyHanfTransfer, an explicit hypothesis packaging Erdős–Rado partition calculus and Ehrenfeucht–Mostowski functor machinery not yet formalized in Lean or Mathlib.
Conditional on the Morley-Hanf transfer hypothesis, \(\beth _{\omega _1}\) is a Hanf bound for every \(\mathcal{L}_{\omega _1\omega }\) sentence.
Given a model of size \(\geq \beth _{\omega _1}\), the transfer hypothesis directly yields arbitrarily large models.
8 Counting Models
Counting the number of models of a Scott sentence up to isomorphism. The theorem morley_counting_dichotomy (a counting-models dichotomy in the style of Morley) is formalized in Lean but is not included as a blueprint node; it serves as a schematic boundary result.
Status: schematic. The dichotomy statement quantifies over cardinals and does not correspond to a single blueprint-trackable proof obligation.
If \(M\) stabilizes completely at \(\alpha {\lt} \omega _1\) and \(\sim _\alpha (\bar{a},\bar{b})\) holds, then \(M \cong N\).
Complete stabilization at \(\alpha \) lets us upgrade \(\sim _\alpha \) to \(\sim _\gamma \) for all \(\gamma {\lt} \omega _1\), then apply Karp’s theorem.
If all countable models of \(\varphi \) have Scott height \(\leq \alpha {\lt} \omega _1\), then isomorphism is equivalent to \(\sim _\alpha \).
The forward direction follows from \(\sim \) being an invariant of isomorphism. For the reverse, the Scott height bound gives complete stabilization at \(\alpha \) for both models, so we apply the stabilization-bound theorem.
9 Proof System for Admissible Fragments
A proof system for admissible fragments of \(\mathcal{L}_{\omega _1\omega }\), following Barwise [ Bar75 ] .
A sentence \(\varphi \) is derivable from theory \(T\) in admissible fragment \(A\). The proof system includes structural, propositional, infinitary, quantifier (omega-rule), equality, and classical rules.
A theory \(T\) is \(A\)-consistent if \(\bot \) is not derivable from \(T\) in fragment \(A\).
If \(\varphi \) is derivable from \(T\) in fragment \(A\), then \(\varphi \) is true in any model of \(T\) equipped with a naming function.
By induction on the derivation. The quantifier cases use the semantic roundtrip for openBounds and the naming function.
A full Barwise fragment: an admissible fragment containing all \(\mathcal{L}_{\omega _1\omega }\) sentences, equipped with the chain closure property for consistency.
The family of \(A\)-consistent subsets of a full Barwise fragment forms a ConsistencyPropertyEq.
Each consistency property axiom (C0–C7) is verified by assuming the extension is inconsistent and deriving a contradiction via the proof system rules.
A countable \(A\)-consistent theory in a full Barwise fragment of a countable language has a countable model.
Construct a ConsistencyPropertyEq from the full Barwise fragment, then apply the model existence theorem.
10 Descriptive Set Theory
Borel complexity of satisfaction, back-and-forth equivalence, and isomorphism on the coding space for countable structures.
The coding space for countable \(L\)-structures on \(\mathbb {N}\): for each relation query, whether the relation holds on that tuple.
For a countable relational language, the set of codes in the structure space satisfying a given \(\mathcal{L}_{\omega _1\omega }\) sentence is measurable (Borel).
By structural induction on the sentence, using that atomic formulas are clopen and the Borel \(\sigma \)-algebra is closed under countable unions and intersections.
The set of code pairs where \(\sim _\alpha \) holds is measurable for \(\alpha {\lt} \omega _1\).
By transfinite induction on \(\alpha \), matching the definition of \(\sim \): the zero case uses countable intersection over atomic indices, the successor case uses the induction hypothesis with countable quantifier alternation, and the limit case uses a countable intersection since \(\alpha {\lt} \omega _1\).
If all countable models of \(\varphi \) have Scott height \(\leq \alpha {\lt} \omega _1\), then the set of isomorphic pairs within \(\mathrm{Mod}(\varphi ) \times \mathrm{Mod}(\varphi )\) is measurable.
The isomorphic-pair set restricted to \(\mathrm{Mod}(\varphi )\) equals the \(\sim _\alpha \) set restricted to \(\mathrm{Mod}(\varphi )\), by the bounded Scott height theorem. Both components are measurable.
10.1 Standard Borel Structure
The structure space carries the product topology, which makes it a Polish space when the language has countably many relation symbols.
For a countable relational language, the structure space is a Polish space.
The structure space is a countable product of copies of \(\{ 0,1\} \), which is compact and metrizable, hence Polish.
The model class of any \(\mathcal{L}_{\omega _1\omega }\) sentence inherits a standard Borel structure.
For any \(\mathcal{L}_{\omega _1\omega }\) sentence \(\varphi \), the set \(\mathrm{Mod}(\varphi )\) is clopenable in the structure space.
\(\mathrm{Mod}(\varphi )\) is measurable (by satisfaction is Borel) and the structure space is Polish + Borel, so any measurable set is clopenable.
For any \(\mathcal{L}_{\omega _1\omega }\) sentence \(\varphi \), the subtype \(\mathrm{Mod}(\varphi )\) is a standard Borel space.
A measurable subset of a standard Borel space is standard Borel.
10.2 Counting Models
The Silver–Burgess dichotomy, taken as a hypothesis, yields a counting theorem for coded \(\mathbb {N}\)-models with bounded Scott height.
On any standard Borel space, a Borel equivalence relation has either at most countably many equivalence classes or exactly \(2^{\aleph _0}\).
The equivalence relation on coded \(\mathbb {N}\)-models of \(\varphi \) where two codes are related iff their decoded structures are \(L\)-isomorphic.
If the Silver–Burgess dichotomy holds, then for any \(\mathcal{L}_{\omega _1\omega }\) sentence whose \(\mathbb {N}\)-models all have Scott height \(\leq \alpha {\lt} \omega _1\), the number of isomorphism classes among coded \(\mathbb {N}\)-models is either \(\leq \aleph _0\) or exactly \(2^{\aleph _0}\).
The model class is standard Borel and the isomorphism relation is Borel (by bounded Scott height), so Silver–Burgess applies directly.
For structures on \(\operatorname {Fin} n\), the isomorphism relation is the orbit of \(\operatorname {Sym}(\operatorname {Fin} n)\), a finite union of graphs of continuous maps, hence Borel.
If the Silver–Burgess dichotomy holds, then for any \(\mathcal{L}_{\omega _1\omega }\) sentence whose countable models all have Scott height \(\leq \alpha {\lt} \omega _1\), the total number of isomorphism classes of countable models is either \(\leq \aleph _0\) or exactly \(2^{\aleph _0}\).
Combine the \(\mathbb {N}\)-coded result (via BF-equivalence Borelness) with finite-carrier orbit arguments for each \(\operatorname {Fin} n\) tier.
For any \(\mathcal{L}_{\omega _1\omega }\) sentence \(\varphi \), the number of isomorphism classes of countable models is either \(\leq \aleph _1\) or exactly \(2^{\aleph _0}\).
Stratify by Scott height. For each \(\alpha {\lt} \omega _1\), BF-equivalence at level \(\alpha \) is Borel with \(\leq \aleph _0\) or \(2^{\aleph _0}\) classes. Iso classes with height \(\leq \alpha \) inject into BF classes. Union over \(\omega _1\) strata gives \(\leq \aleph _1\).
The combined theorem extends the coded \(\mathbb {N}\)-model result to all countable models by adding finite-carrier tiers (isomorphism on \(\operatorname {Fin} n\) structures is Borel via the orbit of \(\operatorname {Sym}(n)\)). Bridge theorems (codeModel, iso_of_codeModel_eq, codeModel_surjective) establish that AllCodedIsoClasses faithfully represents all isomorphism classes of countable models. The Silver–Burgess dichotomy (silverBurgessDichotomy) is proved modulo one sorry in the Borel-to-closed reduction (silver_core_polish), which requires the Gandy–Harrington topology or equivalent descriptive-set-theoretic infrastructure not yet available in Mathlib. Once this is filled, morley_counting becomes fully unconditional.
Bibliography
- Bar75
Jon Barwise, Admissible sets and structures: An approach to definability theory, Perspectives in Mathematical Logic, Springer-Verlag, 1975.
- Kar65
Carol R. Karp, Finite-quantifier equivalence, The Theory of Models (J. W. Addison, Leon Henkin, and Alfred Tarski, eds.), North-Holland, 1965, pp. 407–412.
- Kei71
H. Jerome Keisler, Model theory for infinitary logic: Logic with countable conjunctions and finite quantifiers, Studies in Logic and the Foundations of Mathematics, vol. 62, North-Holland, 1971.
- Mar16
David Marker, Lectures on infinitary model theory, Lecture Notes in Logic, vol. 46, Cambridge University Press, 2016.
- Nad74
Mark E. Nadel, Scott sentences and admissible sets, Annals of Mathematical Logic 7 (1974), 267–294.