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
Headline results include:
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 countable consistent set of sentences of \(\mathcal{L}_{\omega _1\omega }\) in a countable language has a countable model (Theorem 17).
Countable refinement hypothesis. The back-and-forth hierarchy on any countable structure stabilizes in countably many steps (Theorem 8).
Silver’s theorem and the Silver–Burgess dichotomy. A Borel equivalence relation on a Polish space has countably many classes or a perfect set of pairwise-inequivalent points; on a standard Borel space the quotient has size \(\leq \aleph _0\) or exactly \(2^{\aleph _0}\) (Theorem 62).
Morley counting. An \(\mathcal{L}_{\omega _1\omega }\) sentence has \(\leq \aleph _1\) or exactly \(2^{\aleph _0}\) isomorphism classes of countable models (Theorem 68).
The Morley–Hanf theorem. \(\beth _{\omega _1}\) is a Hanf bound for every \(\mathcal{L}_{\omega _1\omega }\) sentence, over an arbitrary language with no side hypotheses (Theorem 31).
The exact Hanf number. \(\mathrm{Hanf}(\mathcal{L}_{\omega _1\omega }) = \beth _{\omega _1}\): the Morley–Hanf bound is sharp, by Marker’s Exercise 5.0.6 [ Mar16 ] beth ladder over the von Neumann hierarchy (Theorem 41).
Small models of every infinite size. A sentence with arbitrarily large models has, at every infinite \(\kappa \), a model of size exactly \(\kappa \) realizing only countably many complete \(\mathcal{L}_{\omega _1\omega }\)-types (Theorem 42).
Complete sentences and categoricity. Every small model of \(\varphi \) satisfies a complete sentence entailing \(\varphi \); a \(\kappa \)-categorical \(\varphi \) with arbitrarily large models has a complete completion with a \(\kappa \)-sized model, itself \(\kappa \)-categorical (Theorems 54, 55).
Craig interpolation. An entailment between \(\mathcal{L}_{\omega _1\omega }\) sentences over an arbitrary language has an interpolant whose function and relation symbols each lie in the intersection of the two sides’ occurrence sets (Theorem 81).
Lyndon interpolation. The polarity refinement, in the relation-polarity / logical-equality form: the interpolant’s positively (negatively) occurring relation symbols lie in the intersection of the two sides’ positive (negative) occurrences, with equality logical and unconstrained (Theorem 83).
Boundedness and undefinability of well-ordering. Chains of every countable length force a model with a relation-preserving map from \(\mathbb {Q}\); hence the order types of well-ordered models are uniformly bounded below \(\omega _1\), and no sentence defines the class of well-orders (Theorems 86, 87, 88).
The López–Escobar theorem. Over a countable relational vocabulary, a class of coded countable structures is Borel and isomorphism-invariant if and only if it is the model class of a single \(\mathcal{L}_{\omega _1\omega }\)-sentence (Theorems 51, 52).
Non-Borelness of the countable well-order class. The class of codes whose distinguished relation well-orders the carrier is not Borel in the logic space (Theorem 89).
1.2 Back-and-Forth Equivalence
Back-and-forth equivalence at ordinal levels, following Karp [ Kar65 ] ; the infinitary languages themselves are developed in Karp [ Kar64 ] .
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. The theorem is Scott’s [ Sco65 ] ; the presentation here follows the modern exposition in 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 [ Kar65 ] ; the statement formalized here is Theorem 1.2.1 of Keisler–Knight [ KK04 ] .
The formalization states the equivalence at an arbitrary common branching carrier equipped with codings of both structures, taking the disjoint sum as a corollary rather than as the definition. That is a presentation choice of this formalization, not part of the cited statement: the mathematical content is Karp’s.
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.
\(M \equiv _{L_{\infty \omega }}^w N\): the structures satisfy the same \(L_{\infty \omega }\) sentences whose infinitary connectives branch over carriers in universe \(w\). The quantifier over branching carriers sits outside the syntax.
\(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 whose infinitary connectives branch over carriers in universe \(w\)).
Forward: a potential isomorphism witnesses agreement on every formula over every carrier, by structural induction with the tuple in bound positions, so the universal case consumes forth and back directly. Backward: at the single carrier \(M \oplus N\), separating formulas are conjunctions indexed by one structure’s carrier and expressed at the common carrier along its coding.
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
Scaffolding, not yet theorems. This chapter records the interfaces for compactness and completeness over countable admissible fragments of \(\mathcal{L}_{\omega _1\omega }\), following Barwise [ Bar75 ] ; background on the Nadel bound is in Nadel [ Nad74 ] . The compactness principle is currently carried as a structure field and the Nadel bound as a typeclass hypothesis, so the nodes below state conditional interfaces rather than proved results. Replacing these by honest foundations is tracked in issues #18–#20.
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: proved, unconditionally. The theorem morley_hanf (31) states that \(\beth _{\omega _1}\) is a Hanf bound for every \(\mathcal{L}_{\omega _1\omega }\) sentence, over an arbitrary language with no side hypotheses. No extraction is consumed at all: any injective \(\mathbb {N}\)-sequence of the source is already fully indiscernible on the Morley seed (morleySeed_indiscernibleOn). The single substantive input is realizability of the seed’s Ehrenfeucht–Mostowski tail-template theory over every target order (morleySeedTailTemplateRealizable_holds). The latter is a Henkin-style construction in the spirit of Marker’s presentation of Morley’s omitting-types argument: an \(\omega \)-stage completion of the countable schema sentence universe — deciding each lifted template sentence and pinning a disjunct for every positive countable disjunction and a refuted conjunct for every negative countable conjunction — whose quotient term model carries a fully indiscernible sequence of Henkin constants satisfying a restricted truth lemma. Symbol countability is removed by running the construction in the sublanguage generated by the sentence’s own countably many symbols and expanding the resulting model back to the full language.
The historical conditional forms are retained: the original morley_hanf_of_transfer (36) with the bundled transfer hypothesis, and the split bridge hasArbLargeModels_of_restricted_extraction (37) consuming the (since refuted-in-ZFC) full-indiscernibility extraction residual plus a compactness oracle.
\(\beth _{\omega _1}\) is a Hanf bound for every \(\mathcal{L}_{\omega _1\omega }\) sentence, over an arbitrary language with no side hypotheses.
No extraction is consumed: an injective \(\mathbb {N}\)-sequence of the source is already fully indiscernible on the Morley seed. Seed-template realizability is the schema construction: the \(\omega \)-stage Marker/Henkin completion of the countable schema sentence universe (with pinned positive-disjunction and refuted-conjunct witnesses), its quotient term model with a restricted truth lemma, the fully indiscernible sequence of Henkin constants, and cross-source acceptance through a Skolem-universality mixin. Symbol countability is removed by running the construction in the sublanguage generated by the sentence’s own (countably many) symbols and expanding the model back.
The milestones of the schema construction behind the seed-realizability input:
In the quotient term model of the completed schema theory, realization of a staged-family formula on classes of closed terms is equivalent to membership of its lifted template sentence in the completion.
Structural induction threading the family membership: atoms via the term-model atomic interface and semantic sign transport; countable connectives via the completion’s pinned positive-disjunction and refuted-conjunct witnesses; universals via the Skolem-witness argument against a Marker certificate body.
The sequence of Henkin-constant classes in the schema term model is fully \(\mathcal{L}_{\omega _1\omega }\)-indiscernible on the countable schema family.
Realization at any two strictly monotone tuples transports through the sequence-realization bridge to membership of the two lifted template sentences, which the completion decides uniformly (tuple uniformity, by the two-interpretation Marker-body argument).
The Ehrenfeucht–Mostowski tail-template theory of the Morley seed is realizable: for every \(\mathcal{L}_{\omega _1\omega }\)-sentence \(\varphi \) with a model of size \(\geq \beth _{\omega _1}\) and every countable linear order \(J\), some model realizes the seed’s template theory along a \(J\)-indexed sequence. No symbol-countability assumptions.
The schema completion runs in the simultaneous symbol-generated sublanguage of \(\varphi \) (both sorts countable, proved not assumed) at an injective \(\mathbb {N}\)-sequence of the source model; the completed schema universe’s quotient term model carries a fully indiscernible sequence of Henkin constants satisfying the restricted truth lemma, and the model expands back to the full constants-expanded language. The degenerate empty-\(J\) case is served by the source model itself.
Assuming realizability of the EM tail-template theory of the Morley seed, every Lω₁ω sentence satisfied in a model of size \(\geq \beth _{\omega _1}\) has arbitrarily large models — with no extraction hypothesis: an injective sequence is already fully indiscernible on the seed.
Take any injective ℕ-indexed sequence of the source (it is fully indiscernible on the family \(\{ \varphi , x_0 \neq x_1\} \)), stretch along an ordinal of the target cardinality through the eventually-form template realized by the residual, and read off \(\varphi \) preservation and injectivity from the sequence-form equivalence.
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.
Assuming restricted source-side extraction and a per-target compactness oracle, every Lω₁ω sentence satisfied in a model of size \(\geq \beth _{\omega _1}\) has arbitrarily large models.
Extract a pairwise-distinct ℕ-indexed sequence restricted-indiscernible on the family \(\{ \varphi , x_0 \neq x_1\} \), stretch along an ordinal of the target cardinality, and read off \(\varphi \) preservation and injectivity from the sequence-form equivalence.
7.2 Sharpness: the Exact Hanf Number
Status: proved. The Morley–Hanf bound is exact: \(\mathrm{Hanf}(\mathcal{L}_{\omega _1\omega }) = \beth _{\omega _1}\) (Lomega1omegaHanfNumber_eq_beth_omega1, 41). The upper half (38) is immediate from the Morley–Hanf theorem. The lower half (40) is Marker’s Exercise 5.0.6: for each \(\alpha {\lt} \omega _1\) a single \(\mathcal{L}_{\omega _1\omega }\) sentence over countably many constants, unary levels indexed by the well order \(\alpha +2\), and one binary extensional edge relation has models of size exactly \(\beth _{\alpha +1}\) at the maximum (39). The maximal model is the von Neumann hierarchy: the levels are interpreted as the stages \(V_{\omega +\beta }\), whose cardinalities Mathlib already computes, shrunk to a \(\mathrm{Type}\)-\(0\) carrier; the upper bound is a well-founded induction on the level order with powerset steps at successors and countable unions at limits. The successor-cofinal supremum \(\sup _{\alpha {\lt}\omega _1}\beth _{\alpha +1} = \beth _{\omega _1}\) closes the argument.
\(\mathrm{Hanf}(\mathcal{L}_{\omega _1\omega }) \le \beth _{\omega _1}\): the global Hanf number of \(\mathcal{L}_{\omega _1\omega }\), over all languages and sentences, is at most \(\beth _{\omega _1}\).
Immediate from the Morley–Hanf theorem: \(\beth _{\omega _1}\) is a Hanf bound for every sentence, so it is a global Hanf bound, and the global Hanf number is the least such.
For every \(\alpha {\lt} \omega _1\) there is an \(\mathcal{L}_{\omega _1\omega }\) sentence whose models have size exactly \(\beth _{\alpha +1}\) at the maximum, so \(\beth _{\alpha +1} {\lt} \mathrm{Hanf}(\mathcal{L}_{\omega _1\omega })\).
Marker’s Exercise 5.0.6 ladder sentence over the level order \((\alpha +2)\): countably many constants enumerate the base level, adjacent levels descend along an extensional edge relation, and limit levels are covered. The von Neumann stages \(V_{\omega +\beta }\) (with Mathlib’s \(|V_o| = \beth ^{\mathrm{pre}}_o\)) give a model of size exactly \(\beth _{\alpha +1}\) after ‘Shrink‘ transport; conversely a well-founded induction on the level order bounds every level of every model by powerset and countable-union steps.
\(\beth _{\omega _1} \le \mathrm{Hanf}(\mathcal{L}_{\omega _1\omega })\).
The successor ordinals are cofinal in \(\omega _1\), so \(\beth _{\omega _1} = \sup _{\alpha {\lt}\omega _1} \beth _{\alpha +1}\), and each \(\beth _{\alpha +1}\) is a strict lower bound by the ladder-stage witnesses.
\(\mathrm{Hanf}(\mathcal{L}_{\omega _1\omega }) = \beth _{\omega _1}\): the global Hanf number of \(\mathcal{L}_{\omega _1\omega }\) over \(\mathrm{Type}\)-\(0\) languages is exactly \(\beth _{\omega _1}\).
Antisymmetry of the global upper bound (the Morley–Hanf theorem, via bounded Erdős–Rado and the Marker/schema completion) and the global lower bound (the beth ladder: countable-index syntax, von Neumann hierarchy witnesses, bounded spectra at every beth successor, and the cofinal supremum).
7.3 Small Models
Status: proved. Marker’s Theorem 5.2.5 [ Mar16 ] (exists_small_model_of_hasArbLargeModels, 42): a sentence with arbitrarily large models has models of every infinite size realizing only countably many complete \(\mathcal{L}_{\omega _1\omega }\)-types. The witnesses are the local Ehrenfeucht–Mostowski quotients of the Morley-seed schema source over highly order-transitive skeletons (linear ordered fields, supplied at every infinite cardinality by lexicographic Hahn-series subfields); the quotient is equivariant under order automorphisms of the skeleton, tuples are classified by countably many compressed term codes, and located term codes compute the carrier cardinality exactly. Arbitrary languages reduce along a uniform collapsing hom.
A sentence of \(\mathcal{L}_{\omega _1\omega }\) with arbitrarily large models has, at every infinite cardinal \(\kappa \), a model of cardinality exactly \(\kappa \) realizing only countably many complete \(\mathcal{L}_{\omega _1\omega }\)-types over the empty set, across all finite arities (Marker, Theorem 5.2.5).
The schema term source of the Morley seed over a highly order-transitive skeleton of size \(\kappa \) (every linear ordered field is highly order-transitive, by cut dilations; lexicographic Hahn-series subfields realize every infinite cardinality). The local EM quotient is equivariant under order automorphisms of the skeleton, so tuples are classified up to structure automorphism by countably many compressed term codes and each code fiber of realized types is a subsingleton; located term codes give carrier cardinality exactly \(\max (\aleph _0,\kappa )\). An arbitrary language is handled by taking the final structure to be a reduct along the uniform collapsing hom into the sentence’s generated sublanguage plus dummies, so smallness descends along the reduct.
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\), with conclusions permitted by the sentence set \(P\). The proof system includes structural, propositional, infinitary, quantifier (omega-rule), equality, and classical rules.
A theory \(T\) is \(P\)-consistent if \(\bot \) is not derivable from \(T\) with conclusions permitted by \(P\).
If \(\varphi \) is derivable from \(T\) over the permitted sentence set \(P\), 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.
The former full-fragment bridge (a “full Barwise fragment” carrying every sentence and a chain-closure hypothesis on \(A\)-consistency, with a completeness theorem over it) has been retired: chain closure fails for the full universe of a constants-expanded language, where the \(\omega \)-rule derives \(\bot \) from the union of a chain of consistent sets, so that structure was uninhabited there. The successors — the countable-completion kernel over a Henkin-closed sentence set, the source-fragment adapter in the constants-expanded universe, and the countable-signature graph-universe endpoint — assume consistency in the expanded or relationalized universe rather than in the base language, so no successor is recorded here as a replacement of the retired completeness node.
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.
Over a countable relational vocabulary, the class of coded countable models of an \(\mathcal{L}_{\omega _1\omega }\)-sentence is an isomorphism-invariant Borel subset of the standard Borel space of structures.
Measurability is formula induction on the standard Borel structure space (the satisfaction-measurability theorem); invariance is transport of realization along an isomorphism of the decoded structures.
10.1 López–Escobar
Status: proved, both directions. The theorem is López–Escobar’s [ LE65 ] . The hard direction follows Marker’s route (Theorem 4.3.7 of [ Mar16 ] ; Gao [ Gao09 , Theorem 11.3.6 ] is an alternative exposition) rather than an induction on the Borel hierarchy, which would not preserve isomorphism invariance. An invariant Borel class and its complement are analytic, hence branch projections of cylinder trees along the query code; each tree is coded as a projective (\(PC\)) class over the base language expanded by two disjoint tagged copies of a functional witness vocabulary, relationalized through the graph translation of the Craig layer. The base reducts of the coded class are exactly the original class — this converse is the sole consumer of isomorphism invariance — and the two tagged presentations have no common model, since gluing two expansions of a shared base model and passing to a countable fragment-elementary substructure would place a single code in a class and in its complement. Craig separation then produces a sentence of the shared vocabulary, which by the occurrence calculus contains only graph images of base relation symbols and therefore decodes back to an \(\mathcal{L}_{\omega _1\omega }\)-sentence over the base language. Both final inclusions use only the invariance-free forward presentation, so the whole theorem’s use of invariance stays concentrated in the disjointness lemma.
Over a countable relational vocabulary, every isomorphism-invariant Borel class \(B\) of coded countable structures is the model class of a single \(\mathcal{L}_{\omega _1\omega }\)-sentence.
Marker’s route (Theorem 4.3.7 of the 2016 book). \(B\) and its complement are Borel, hence analytic, so each is the branch projection of a cylinder tree along the query code. Each tree is coded by a sentence \(\Theta \) over the base language expanded by two disjoint tagged copies of a functional witness vocabulary (a constant, the successor, the code and branch functions, and a tree relation at every level), relationalized through the graph translation; the base reducts of \(\Theta \)’s models are exactly \(B\), the converse inclusion being where isomorphism invariance is consumed. The two presentations have no common model: gluing two tagged expansions of a common base model and passing to a countable fragment-elementary substructure would place one code in both \(B\) and its complement. Craig separation therefore yields a sentence of the shared vocabulary separating them, and that vocabulary consists only of graph images of base relation symbols, so the separator decodes to an \(\mathcal{L}_{\omega _1\omega }\)-sentence over the base language. Both inclusions then follow from the invariance-free forward presentation.
Over a countable relational vocabulary, a class of coded countable structures is Borel and isomorphism-invariant if and only if it is the class of models of a single \(\mathcal{L}_{\omega _1\omega }\)-sentence.
The forward direction is the hard theorem; the reverse is the easy direction.
Over a countable relational vocabulary, a class of coded countable structures is Borel and invariant under the logic action of \(S_\infty \) if and only if it is the class of models of a single \(\mathcal{L}_{\omega _1\omega }\)-sentence; equivalently, the Borel invariant classes are exactly the range of \(\mathrm{ModelsOf}\).
Rewrite action invariance as isomorphism invariance by the orbit-equals- isomorphism identity, then apply the previous equivalence.
10.2 Complete Sentences and Categoricity
Status: proved. The payoff of the small-model theorem (Marker, Theorem 5.2.5 applications): a small model’s countable companion — built from realized-type isolators, one countable controlling fragment, and the genuine fragment Löwenheim–Skolem theorem — is back-and-forth equivalent to it at every ordinal, and the companion’s canonical Scott sentence characterizes ARBITRARY models up to all-ordinal back-and-forth equivalence (the arbitrary-target stabilization kernel, where the fragment machinery upgrades countable-target Scott stabilization). Hence every small model of \(\varphi \) lies in a complete subclass of \(\mathrm{Mod}(\varphi )\), and \(\kappa \)-categorical sentences have \(\kappa \)-categorical complete completions.
Over a countable relational vocabulary, every model of \(\varphi \) realizing only countably many complete \(\mathcal{L}_{\omega _1\omega }\)-types satisfies a COMPLETE \(\mathcal{L}_{\omega _1\omega }\)-sentence entailing \(\varphi \).
The model’s countable companion (type isolators, the controlling fragment, fragment Löwenheim–Skolem) is back-and-forth equivalent to it at every ordinal; the companion’s canonical Scott sentence characterizes its arbitrary models up to all-ordinal back-and-forth equivalence (arbitrary-target stabilization), so any two of its models are \(L_{\infty \omega }\)-equivalent — completeness and entailment follow.
If \(\varphi \) has arbitrarily large models and is \(\kappa \)-categorical (\(\kappa \) infinite), there is a complete \(\psi \models \varphi \) with a model of cardinality exactly \(\kappa \), and \(\psi \) is itself \(\kappa \)-categorical (Marker, Theorem 5.2.5 applications).
The small-model theorem supplies a \(\kappa \)-sized model of \(\varphi \) realizing countably many types; the complete-subclass intermediate provides its complete Scott completion; categoricity of \(\varphi \) transfers to \(\psi \) since every \(\kappa \)-model of \(\psi \) is a \(\kappa \)-model of \(\varphi \).
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.3 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.4 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}\). Proved in this repository as ‘silverBurgessDichotomy‘, via the classical \(G_0\)-dichotomy route.
A Borel equivalence relation on a standard Borel space has at most \(\aleph _0\) classes or exactly \(2^{\aleph _0}\) — Silver’s theorem, fully proved via Miller’s classical category route.
Upgrade to a Polish topology and apply the Polish-space core (Kuratowski–Ulam, Mycielski, the \(G_0\)-dichotomy fusion).
The equivalence relation on all of the structure space where two codes are related iff the structures they decode on \(\mathbb {N}\) are \(L\)-isomorphic. Defined without reference to any sentence, so that perfectness of a set of codes is a property of the ambient space rather than of a refinement chosen to make one model class Polish.
The equivalence relation on coded \(\mathbb {N}\)-models of \(\varphi \) where two codes are related iff their decoded structures are \(L\)-isomorphic. It is the ambient relation restricted along the subtype inclusion.
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) and Silver’s theorem (gandy_harrington_for_relation) are fully proved, via Miller’s classical category route (Kuratowski–Ulam, Mycielski, the Kechris–Solecki–Todorcevic \(G_0\)-dichotomy); morley_counting is therefore unconditional, with axioms exactly [propext, Classical.choice, Quot.sound].
10.5 Thinness and Perfect Sets
The counting theorems above are stated cardinally. The underlying dichotomy is sharper: the “many classes” side is witnessed by a perfect set of pairwise inequivalent points. This section records the vocabulary for that witness, and a criterion for ruling it out.
A set \(A\) carries a perfect antichain for an equivalence relation \(r\) if some nonempty perfect \(P \subseteq A\) has pairwise \(r\)-inequivalent points.
A set \(A\) carries a Cantor antichain for \(r\) if there is a continuous \(f : 2^{\mathbb {N}} \to A\) sending distinct points to \(r\)-inequivalent ones. This is the constructive form the Cantor-scheme builders produce, and the load-bearing intermediary between perfect antichains and cardinality.
\(A\) is thin for \(r\) if it carries no perfect antichain.
A sentence \(\varphi \) is thin on its \(\mathbb {N}\)-models if the set of codes of \(\mathbb {N}\)-models of \(\varphi \) carries no perfect antichain for the ambient isomorphism relation on the structure space. Stated ambiently, so no Polish refinement of the model subtype enters the definition.
The Cantor antichain is the load-bearing intermediary in both directions: it is what the Cantor-scheme builders produce, and it is what a thinness proof must refute. The two chains are
with \(\mathtt{structureIsoSetoid}\) together with \(\mathrm{ModelsOf}\ \varphi \) specializing the ambient notions to \(\mathtt{IsThinOnNatModels}\).
If \(A\) carries a Cantor antichain for \(r\) in a Hausdorff space, then \(A\) carries a perfect antichain for \(r\). The range of the Cantor map is closed because a continuous injection out of a compact space into a Hausdorff space is a closed embedding, and it has no isolated points because accumulation points transport along that injection. Unlike the reverse implication, this needs no metric or completeness assumption.
The two directions of that equivalence cost very different hypotheses. Perfect antichain \(\to \) Cantor antichain goes through \(\mathtt{Perfect.exists\_ nat\_ bool\_ injection}\) and needs a complete metric space. The converse needs only that the ambient space is Hausdorff, which is why \(\mathtt{HasCantorAntichainOn}\) is worth keeping as a separate notion: a construction that produces one obtains the ambient perfect set without first exhibiting a metric.
A ranked thinness analysis of \(A\) for \(r\) is a rank \(\rho : X \to \mathrm{Ord}\) together with the evidence that \(\rho \) is \({\lt} \omega _1\) on \(A\), that each fixed-rank antichain inside \(A\) is countable, and that every Cantor antichain in \(A\) contains a continuously embedded Cantor subcopy on which \(\rho \) is bounded below \(\omega _1\). It packages hypotheses only; it asserts no conclusion.
If \(A\) admits a ranked thinness analysis for \(r\) in a complete metric space, then \(A\) is thin for \(r\).
A Cantor antichain contains a Cantor subcopy whose ranks are bounded by some \(\beta {\lt} \omega _1\), so that subcopy is the union of the countably many fixed-rank antichains below \(\beta \), each countable, hence countable. But it is an injective image of \(2^{\mathbb {N}}\), which is uncountable by diagonalization. So there is no Cantor antichain, and therefore no perfect antichain.
ThinRankAnalysis packages sufficient evidence for thinness, and ThinRankAnalysis.isThinOn proves the implication. Note that the cheap direction above does not weaken those hypotheses: isThinOn consumes perfect \(\to \) Cantor, the complete-metric direction.
Thinness also has a purely logical characterization, with no rank at all: a Borel class carries no perfect antichain exactly when every countable list of sentences realizes only countably many truth patterns on it. One direction is Silver’s dichotomy applied to equality of truth sequences, a Borel equivalence relation coarser than isomorphism; the other recovers the Cantor parameter of an antichain by sentences, through invariant analytic separation and López–Escobar. The class need not be isomorphism-invariant, and no Borelness of isomorphism is used (classical background: invariant separation and López–Escobar are Corollary 4.3.6 and Theorem 4.3.7 of Marker [ Mar16 ] , scatteredness is his Definition 3.3.1 and Corollary 3.3.10; the iterated separation-and-saturation argument is that of Gao [ Gao09 , Lemma 5.4.6 ] ; the spectrum formulation is assembled here). Countable spectra quantify over every list; they do not supply one list that classifies isomorphism, which together with thinness would force countably many classes.
Let \(C\) be a Borel class of coded structures over a countable relational language. Then \(C\) is thin for isomorphism — carries no perfect set of pairwise non-isomorphic structures — if and only if for every sequence \((\theta _n)_{n{\lt}\omega }\) of \(L_{\omega _1\omega }\)-sentences, only countably many truth sequences \((\mathbb {1}[c \models \theta _n])_{n}\) are realized by \(c \in C\). The class need not be isomorphism-invariant.
Thin to countable: the truth-sequence map of a fixed list is Borel, and equality of truth sequences is a Borel equivalence relation coarser than isomorphism, so Silver’s dichotomy on \(C\) gives either countably many truth sequences or a continuous Cantor antichain for isomorphism, which thinness excludes. Countable to thin: a perfect antichain yields a Borel Cantor isomorphism antichain \(f\); for each bit \(n\), the saturations of \(f[\{ x : x_n = 1\} ]\) and \(f[\{ x : x_n = 0\} ]\) are disjoint invariant analytic classes, separated by an invariant Borel set by iterated Lusin separation and saturation, hence by a sentence \(\theta _n\) via López–Escobar. The list \((\theta _n)\) then recovers every parameter, so its spectrum on \(C\) is uncountable.
The finite-arity form is the classical definition of scatteredness (Marker, Definition 3.3.1 and Corollary 3.3.10): a Borel class is thin exactly when every countable fragment realizes only countably many types of \(n\)-tuples on it, for every finite \(n\). The route is Marker’s Corollary 3.3.3: for a fixed fragment and arity, “realizing the same types” is a Borel equivalence relation refined by isomorphism, so Silver’s dichotomy either bounds the realized types or produces an isomorphism antichain. No Baire-property theorem for analytic sets is needed.
Let \(C\) be a Borel class of coded structures over a countable relational language. Then \(C\) is thin for isomorphism if and only if for every countable fragment \(F\) and every finite arity \(n\), only countably many \(F\)-types of \(n\)-tuples are realized in members of \(C\). The class need not be isomorphism-invariant.
Thin to countable: for fixed \(F\) and \(n\), the relation “\(c\) and \(d\) realize the same \(F\)-types of \(n\)-tuples” is Borel — every tuple of one has a matching tuple in the other, matching being agreement on the countably many members of the slice — and it is refined by isomorphism. Silver’s dichotomy on \(C\) gives either countably many classes, each realizing countably many types, or a continuous Cantor antichain for the relation, hence for isomorphism, which thinness excludes. Countable to thin: at arity zero, the fragment generated by a sentence list is countable and its spectrum determines the truth sequences of the list, so the sentence-spectrum characterization applies.
A generic constructor of ThinRankAnalysis is supplied, from ranks computed by coded well-orders presented continuously on each Cantor antichain (Definition 92); it is the bridge from analytic boundedness to thinness. No concrete instance is supplied: no model class is exhibited whose isomorphism rank admits such presentations, and producing one is the remaining mathematics rather than a packaging step.
The refined form of the boundedness field — a bound on a continuous injective subcopy of each Cantor antichain rather than on the antichain itself — is what makes Borel data along the antichain usable: countably many maps from Cantor space into countable discrete spaces with Borel fibres become simultaneously continuous after composing with one continuous injective self-map of Cantor space (CantorStabilization.exists_subcopy_continuous, by the Baire property of Borel sets and the fact that an uncountable Borel subset of a Polish space contains a Cantor copy). A construction may therefore choose the subcopy first and then treat such data as continuous.
Cardinal equality alone does not establish thinness in ZFC. Under \(\mathsf{CH}\) we have \(\aleph _1 = 2^{\aleph _0}\), so a quotient of exactly \(\aleph _1\) classes is compatible with a perfect antichain; under \(\neg \mathsf{CH}\), exact \(\aleph _1\) does rule one out. Separately, the cardinal interface forgets the witness: \(\mathtt{SilverBurgessDichotomy}\) concludes with a cardinal disjunction and retains nothing from which a perfect set could be extracted, so no theorem parameterized by it can produce a perfect-set witness.
10.6 Morley Counting with a Witness
The way past that obstruction is to bypass the cardinal interface entirely and apply the proved Polish-space core silver_core_polish directly. The model class is a Borel subset of the structure space, hence not Polish as a subtype, so a clopenable refinement is taken first, Silver runs there, and the Cantor antichain is carried back to the ambient space — the pipeline factored as silver_countable_or_cantorAntichain. Only the Cantor form is coarsened, where continuity is the sole topological clause; perfectness is recovered ambiently afterwards, so nothing here asserts that perfectness survives coarsening, which it does not.
For any \(\mathcal{L}_{\omega _1\omega }\) sentence \(\varphi \), either the \(\mathbb {N}\)-coded isomorphism classes number at most \(\aleph _1\), or the model class carries a perfect set of pairwise non-isomorphic models.
If there is no perfect set, then Silver applied to back-and-forth equivalence at each level \(\alpha {\lt} \omega _1\) must return a countable quotient, since a Cantor antichain there would transfer to isomorphism and yield a perfect set. The Scott-height stratification then bounds the isomorphism classes by \(\aleph _1\).
For each \(n\), either the isomorphism classes of \(\operatorname {Fin} n\)-models of \(\varphi \) are countable, or that model class carries a perfect set of pairwise non-isomorphic models.
Isomorphism on \(\operatorname {Fin} n\)-structures is a finite union of graphs of continuous permutation actions, hence Borel, so Silver applies to it directly on a clopenable refinement; the resulting Cantor antichain returns to the ambient space.
The two tiers differ only in the relation Silver is applied to. At \(\mathbb {N}\) it is back-and-forth equivalence at a level \(\alpha {\lt} \omega _1\) — what the Scott stratification makes Borel — and the antichain transfers to isomorphism, which refines it. At \(\operatorname {Fin} n\) isomorphism is itself Borel, a finite union of permutation graphs, so Silver applies to it directly.
For any \(\mathcal{L}_{\omega _1\omega }\) sentence \(\varphi \), either the isomorphism classes of countable models number at most \(\aleph _1\), or \(\varphi \) has a perfect set of pairwise non-isomorphic \(\mathbb {N}\)-models, or it has one of pairwise non-isomorphic \(\operatorname {Fin} n\)-models for some \(n\).
Combine the two per-tier witnessed dichotomies. If neither tier yields a perfect set, the \(\mathbb {N}\) tier contributes at most \(\aleph _1\) classes and the countably many finite tiers contribute at most \(\aleph _0 \cdot \aleph _0 = \aleph _0\) between them.
The finite-carrier alternative is not a formality: an infinite language can have continuum-many \(\operatorname {Fin} n\)-models and no \(\mathbb {N}\)-models at all, so a statement offering only an \(\mathbb {N}\)-tier perfect set would be false. Since a perfect antichain forces continuum-many classes, the cardinal form of Theorem 68 is recovered as the corollary morley_counting_or_perfect_cardinal, with the upper bound supplied by the ambient space; the converse fails, which is the sense in which the perfect alternatives carry strictly more information. The parameterized morley_counting is retained unchanged.
11 Craig Interpolation
Craig interpolation for \(\mathcal{L}_{\omega _1\omega }\): an entailment \(r_1 \models r_2\) admits an interpolant \(\theta \) whose vocabulary lies in the symbols shared by the two sides, with \(r_1 \models \theta \) and \(\theta \models r_2\).
The headline node holds over an arbitrary language, with no hypotheses on \(L\): both the function and the relation symbols of \(\theta \) lie in the intersection of the two roots’ occurrence sets. It is the relational core composed with a self-contained relationalization layer: every \(n\)-ary function symbol becomes an \((n{+}1)\)-ary graph relation \(G_f\), terms flatten to existential graph formulas, the totality/functionality axioms of the mentioned symbols translate the entailment (via structure reconstruction over the union of the two function-symbol sets), and back-translation \(G_f(\bar x,y) \mapsto f(\bar x){=}y\) returns the interpolant to \(L\) with the sharp occurrence bounds. Its disjunction form is the PC-separation corollary craig_pcSeparation.
Over an arbitrary language, an \(\mathcal{L}_{\omega _1\omega }\)-entailment \(r_1 \models r_2\) has an interpolant \(\theta \) whose function and relation symbols each lie in the intersection of the two roots’ occurrence sets, with \(r_1 \models \theta \) and \(\theta \models r_2\). No hypotheses on the language.
Relationalize: replace each \(n\)-ary function symbol \(f\) by an \((n{+}1)\)-ary graph relation \(G_f\), each term by its existentially-flattened graph formula, and add the totality/functionality axioms \(\mathrm{Ax}(F)\) of the mentioned function symbols. The entailment translates to \(\mathrm{Ax}(F_1) \wedge r_1^{\mathrm{rel}} \models \mathrm{Ax}(F_2) \to r_2^{\mathrm{rel}}\) — a model of the left side satisfying \(\mathrm{Ax}(F_2)\) carries the graph axioms of \(F_1 \cup F_2\), so it reconstructs to an \(L\)-structure where \(r_1 \models r_2\) applies. The relational core then yields a graph interpolant \(\theta _g\); its vocabulary bound passes through the exact occurrence identities and the shared-vocabulary identity \(\mathrm{relSym}(F_1,R_1) \cap \mathrm{relSym}(F_2,R_2) = \mathrm{relSym}(F_1 \cap F_2, R_1 \cap R_2)\); back-translating \(G_f(\bar x, y) \mapsto f(\bar x){=}y\) lands \(\theta \) in \(L\) with the sharp bounds, and both entailments transport through graph expansions.
The relational core below is proved over a purely relational language with no countability hypothesis, by an inseparability/finite-condition Henkin construction (a constant-free interpolant strips through the empty-support root gate), with ambient relation-symbol countability removed by passing to the sublanguage generated by the two roots’ countably many symbols. Its disjunction form, craig_pcSeparation_relational, is retained in exactly the shared-vocabulary packaging consumed by the projective-class work.
Over a purely relational language (arbitrarily many symbols), an \(\mathcal{L}_{\omega _1\omega }\)-entailment \(r_1 \models r_2\) has an interpolant \(\theta \) whose function and relation symbols lie in the intersection of the two roots’ occurrence sets, with \(r_1 \models \theta \) and \(\theta \models r_2\). No countability hypothesis on the language.
Assume no interpolant. The constant-expanded root pair is then inseparable at empty constant support; feeding it to the paired finite-condition Henkin construction yields a single model of both \(r_1\) and \(\neg r_2\), whose base reduct contradicts \(r_1 \models r_2\). Ambient relation-symbol countability is unnecessary: pass to the sublanguage generated by the two roots’ (countably many) symbols, apply the countable relational core there, and map the interpolant back along the inclusion.
11.1 Lyndon Interpolation
Status: proved, arbitrary languages. The polarity refinement of Craig: an interpolant may be required to respect the sign of every relation occurrence. What is proved here is the relation-polarity / logical-equality form of López–Escobar’s Theorem 4.1: relation symbols satisfy his clause (.4) in full — a symbol occurring positively (negatively) in the interpolant occurs positively (negatively) in both roots — while equality is treated as a logical symbol, belonging to neither polarity class, so his clause (.3), which additionally constrains where equality may occur, is deliberately not claimed. Nor is any theory-level form claimed: for \(\mathcal{L}_{\omega _1\omega }\) that is false (López–Escobar’s Theorem 6.3 exhibits disjoint \(PC_\Delta \) classes inseparable by an elementary class), so the sentence-level statement is sharp.
Polarity is tracked by a signed occurrence traversal on the existing syntax — antecedents flip the sign, quantifiers and the countable connectives preserve it, equality contributes nothing — so no negation-normal form is constructed. Its semantic content is that growing the positively-occurring relations and shrinking the negatively-occurring ones preserves truth. The proof refines the Craig engine rather than repeating it: only the separator class changes, and the countable-completion kernel is consumed unchanged. The arbitrary-language step reuses Craig’s relationalization layer verbatim, the key point being that the graph relations \(G_f\), which may occur with either polarity, back-translate into equalities and so vanish from the polarity bookkeeping.
Over an arbitrary language (no hypotheses whatsoever), an \(\mathcal{L}_{\omega _1\omega }\)-entailment \(r_1 \models r_2\) has an interpolant \(\theta \) whose function symbols lie in the intersection of the roots’ function occurrences, whose positively occurring relation symbols lie in the intersection of the roots’ positive occurrences, and whose negatively occurring ones lie in the intersection of the roots’ negative occurrences. This is the relation-polarity / logical-equality form of López–Escobar’s Theorem 4.1: relation symbols satisfy the full polarity condition (his clause (.4)), while equality is a logical symbol belonging to neither polarity class, so his clause (.3) — the equality-occurrence condition — is not claimed. No theory-level form is claimed either; it is false for \(\mathcal{L}_{\omega _1\omega }\).
Relationalize as for Craig and reuse the same semantic gate, then apply the relational Lyndon core in the graph language. The function-symbol bound comes from the unsigned graph bound, recovered from the two signed bounds and Craig’s exact occurrence identities with \(\mathrm{relSym}\)-intersection. The signed base-relation bounds come from two polarity facts about the translation: relationalization preserves base-relation polarity on the nose, and although the graph relations \(G_f\) may occur with either polarity (the functionality axioms use them negatively), back-translation sends \(G_f(\bar x, y)\) to the equality \(f(\bar x) = y\), which is polarity-free — so they vanish harmlessly. Both entailments are Craig’s graph-expansion arguments unchanged.
Over a purely relational language (arbitrarily many symbols), an \(\mathcal{L}_{\omega _1\omega }\)-entailment \(r_1 \models r_2\) has an interpolant \(\theta \) whose function symbols lie in the intersection of the roots’ function occurrences, whose positively occurring relation symbols lie in the intersection of the roots’ positive occurrences, and whose negatively occurring ones lie in the intersection of the roots’ negative occurrences. This is the relation-polarity / logical-equality form: relation symbols satisfy the full polarity condition, while equality is a logical symbol, belongs to neither polarity class, and its occurrence in the interpolant is unconstrained.
The Craig contradiction skeleton with a polarity-refined separator class: a separator must have its base positive occurrences inside \(P\) and its negative ones inside \(N\). Assume no interpolant; then the constant-expanded root pair is inseparable at empty support in the class maintained by the paired family, namely \((\mathrm{Pos}\, r_1 \cap \mathrm{Pos}\, r_2, \mathrm{Neg}\, r_1 \cap \mathrm{Neg}\, r_2)\) — the \(\Delta \)-root being \(\neg r_2\), whose polarity classes are exchanged. Feeding that pair to the polarity-refined finite-condition Henkin construction yields one model of \(r_1\) and \(\neg r_2\), contradicting the entailment. Ambient countability is removed by passing to the sublanguage generated by the two roots’ symbols and transporting the signed occurrence sets along the inclusion.
11.2 Malitz universal interpolation
Malitz’s Theorem 4.5 refines interpolation by quantifier class: if the consequent is universal, the interpolant may be taken universal too. The engine is a side-labelled budgeted pair — Feferman’s split-sequent invariant in semantic form — in which the interpolant’s class is paid for by the right root’s quantifier budget rather than established afterwards.
The companion relative existential preservation theorem (4.6) is not claimed; see the successor issue.
Over a relational language of arbitrary cardinality, an \(\mathcal{L}_{\omega _1\omega }\)-entailment \(\varphi \models \psi \) whose consequent is universal (\(\forall _1\): every quantifier occurrence a positive \(\forall \); countable conjunctions and disjunctions are not counted as quantifiers) has a universal interpolant \(\theta \), whose function and relation symbols lie in the intersections of the two roots’ occurrences.
This is López–Escobar / Malitz Theorem 4.5 in the function-free case. The relative existential preservation theorem (4.6) is not claimed here: it needs a relativization or two-sorted encoding that this development does not contain. No theory-level form is claimed.
Pass to the sublanguage generated by the two roots’ own symbols, which is countable because a single \(\mathcal{L}_{\omega _1\omega }\) sentence mentions only countably many, and apply the countable core; map the interpolant back along the inclusion, the quantifier class surviving both moves because restriction and language maps preserve signed occurrences exactly.
The core assumes no interpolant, whence the mapped root pair is inseparable for the side-labelled budgeted certificate; a budgeted separator would be universal (the right root \(\neg \psi \) carries no positive universal occurrence precisely when \(\psi \) is universal) and constant-free (the left root’s support is empty), so it would strip to the interpolant assumed absent. The inseparable pair seeds a Henkin completion whose quotient term model realizes \(\varphi \) and refutes \(\psi \), contradicting the entailment.
12 Undefinability of Well-Ordering
Marker’s consistency-property construction (Theorem 4.4.1 and Corollary 4.4.2 of [ Mar16 ] ): an \(\mathcal{L}_{\omega _1\omega }\)-sentence whose models contain well-ordered chains of every countable length has a model embedding the rationals positively into the distinguished relation. Consequently the well-ordered models of any sentence have uniformly bounded order type, and no sentence of \(\mathcal{L}_{\omega _1\omega }\) defines the class of well-orders.
All three nodes hold over an arbitrary language. The engine is a dedicated consistency property over the constants-expanded relational core, whose members carry the positive rational diagram \(\{ d_q {\lt} d_r : q {\lt} r\} \) together with a finite remainder whose mentioned rational constants sit, at every level \(\alpha {\lt} \omega _1\), on a chain with \(\alpha \)-sized margins in an approximating model (Marker’s gap condition \((*)\)); the fifteen closure fields are Exercise 4.28 of the 2013 notes. The fair Henkin enumeration and the quotient term model shared with the Craig kernel realize the completed diagram, and \(q \mapsto d_q^M\) is the rational map. Symbol countability is removed by the two-sorted generated sublanguage, and function symbols by the Craig relationalization layer, under which the distinguished base relation is preserved definitionally.
The three public results are deliberately separate in strength: the raw positive map (no injectivity claimed — that is a corollary under irreflexivity), the uniform order-type bound (the strong form), and undefinability (the weak form). The stronger induced-copy conclusion and the Borel-coded form of undefinability are tracked separately and are not claimed by these nodes.
Let \(\varphi \) be an \(\mathcal{L}_{\omega _1\omega }\)-sentence over an arbitrary language with a distinguished binary relation symbol \({\lt}\). If for every \(\alpha {\lt} \omega _1\) some model of \(\varphi \) contains a strictly \({\lt}\)-increasing chain of length \(\alpha \), then some nonempty model \(M \models \varphi \) carries a map \(f : \mathbb {Q} \to M\) with \(f(q) {\lt} f(r)\) whenever \(q {\lt} r\) — the raw positive relation-preserving conclusion (no injectivity is claimed; it is a corollary under irreflexivity).
A dedicated consistency property over the constants-expanded relational core: members are the base diagram \(\{ \hat\varphi \} \cup \{ d_q {\lt} d_r : q {\lt} r\} \) plus a finite remainder whose mentioned rational constants sit, for every \(\alpha {\lt} \omega _1\), on a chain with \(\alpha \)-margins in an approximating model (the gap condition \((*)\)). The fifteen closure fields are Marker’s Exercise 4.28 of the 2013 notes; the fair Henkin enumeration completes the base diagram; the quotient term model realizes it, and \(q \mapsto d_q^M\) is the map. Symbol countability is removed by the two-sorted generated sublanguage, and function symbols by the Craig relationalization layer (graph relations, totality/ functionality axioms, structure reconstruction), under which the distinguished base relation is preserved definitionally.
If every model of an \(\mathcal{L}_{\omega _1\omega }\)-sentence \(\varphi \) interprets the distinguished relation \({\lt}\) as a well-order, then there is a single countable ordinal \(\alpha \) strictly bounding the order type of every model’s interpreted relation.
Contrapositive of the rational-embedding theorem: were the order types unbounded below \(\omega _1\), every countable chain length would be realized, so some model of \(\varphi \) would embed \(\mathbb {Q}\) positively — and the negative rationals would descend strictly, contradicting well-foundedness. An order type \(\geq \alpha \) would re-embed the missing \(\alpha \)-chain via the order-type calculus.
For any language with a distinguished binary relation symbol \({\lt}\), no \(\mathcal{L}_{\omega _1\omega }\)-sentence has as models exactly the structures whose interpretation of \({\lt}\) is a well-order.
Such a sentence would satisfy the boundedness hypothesis, yielding a uniform countable bound \(\alpha \) on order types; but the comparison structure on \(\alpha + 1\) (every binary symbol the ordinal order, functions interpreted arbitrarily on the nonempty carrier) is itself a well-order of type \(\alpha + 1 \geq \alpha \) and would be a model, violating the bound.
The Borel-coded form is the descriptive-set-theoretic payoff, and it needs López–Escobar: the class of codes whose distinguished relation well-orders \(\mathbb {N}\) is not Borel. Were it Borel it would be \(\mathrm{ModelsOf} \varphi \) on codes; conjoining the infiniteness axiom (so no finite model escapes) and seeding a countable fragment-elementary substructure with the witnesses of any well-ordering defect — two incomparable unequal elements, or an infinite descending chain — transports that defect to a code of the class, so every model of the conjunction is in fact well-ordered. Corollary 4.4.2 then bounds all their order types by one countable \(\alpha \), which the comparison structure of type \(\alpha + \omega \) exceeds.
Over a countable relational vocabulary with a distinguished binary relation, the class of codes whose relation well-orders the carrier is **not** Borel in the logic space.
If it were Borel, López–Escobar would present it as \(\mathrm{ModelsOf} \varphi \) — but only over coded structures, whose carrier is \(\mathbb {N}\). Conjoin the \(\mathcal{L}_{\omega _1\omega }\) infiniteness axiom, so that no finite model escapes, and let \(M\) be any model of the conjunction whose relation is not a well-order. A well-order here is trichotomy plus well-foundedness, so the failure is witnessed either by two incomparable unequal elements or by an infinite descending chain; seed a countable fragment-elementary substructure with those witnesses and the failure survives, while the added conjunct keeps the substructure infinite, so it transports to a code lying in the class without being a well-order — a contradiction. Hence every model of the conjunction is well-ordered, and Marker’s Corollary 4.4.2 bounds all their order types by one countable \(\alpha \); the comparison structure of type \(\alpha + \omega \) transported to \(\mathbb {N}\) is a code of the class exceeding that bound.
Boundedness itself survives without any definability hypothesis on the class. A sentence-defined reduct class is isomorphism-invariant, so an arbitrary analytic \(A\) can never be presented as \(\mathrm{codeReduct}\ ''\ \mathrm{ModelsOf}\ \Theta \) exactly; but it can always be sandwiched between that class and an invariant envelope \(W \supseteq A\), and boundedness only ever consumes the sandwich. Taking \(W\) to be the well-order class gives the classical boundedness theorem for \(\Sigma ^1_1\) subsets of \(\mathrm{WO}\). Its immediate \(A = \mathrm{WO}\) consequence is that \(\mathrm{WO}\) is not analytic — it would then bound its own order types, which the supply of countably infinite order types exceeds — and non-Borelness follows because every Borel set is analytic. The node above is proved separately from López–Escobar and does not go through this one.
If \(A\) is an analytic set of codes, every one of which interprets the distinguished relation \({\lt}\) as a well-order of \(\mathbb {N}\), then a single countable ordinal \(\alpha \) strictly bounds the order type of every code in \(A\).
Put \(A\) in tree normal form and let \(\Theta \) be the resulting \(PC\) sentence over the graph language. Its reduct class is sandwiched, \(A \subseteq \mathrm{codeReduct}\, ''\, \mathrm{ModelsOf}\ \Theta \subseteq W\), for every isomorphism-invariant \(W \supseteq A\); take \(W\) to be the well-order class, which is invariant and contains \(A\) by hypothesis. The upper gate then says every model of \(\Theta \) is a coded well-order for the transported relation, the defect bridge in containment form lifts that to every model of \(\Theta \) conjoined with the infiniteness axiom, and Corollary 4.4.2 bounds all those order types by one countable \(\alpha \). The lower gate exhibits each code of \(A\) as the reduct of such a model, and \(\mathbb {N}\) is infinite, so the bound applies to it.
The same boundedness reaches trees. A code names a tree on \(\mathbb {N}\) through a distinguished unary relation, and the tree class is closed. The Kleene–Brouwer code sends a tree code to the code of the order that lists the tree’s nodes first, in Kleene–Brouwer order, and every other natural afterwards; each coordinate of the code depends on two membership bits, so the map is continuous. A well-founded tree has a well-ordered Kleene–Brouwer code, and its rank is at most the order type, so the bound on order types becomes a bound on tree ranks.
If \(A\) is an analytic set of codes, every one of which names a well-founded tree on \(\mathbb {N}\), then a single countable ordinal strictly bounds the rank of every tree named by a code in \(A\).
Send each code to the code of its Kleene–Brouwer order: the nodes of the tree first, in Kleene–Brouwer order, and every other natural afterwards. This map is continuous, each coordinate depending on two membership bits, so the image of \(A\) is analytic; it consists of well-orders, since the Kleene–Brouwer order of a well-founded tree is a well-order and the remainder is a copy of \(\omega \) placed after it. The boundedness theorem for coded well-orders bounds the order types by one countable ordinal, and the rank of each tree is at most the order type of its Kleene–Brouwer code.
The two boundedness theorems are Theorems 1.6.10 and 1.6.11 of Gao [ Gao09 ] , whose Exercise 1.5.7 is the Kleene–Brouwer equivalence used to pass between them.
That boundedness is what the thinness package of Section 10.5 needs on a Cantor antichain, whenever the rank in question is the order type of a continuously presented family of coded well-orders. Packaging the two together is the bridge between the chains, and it is generic: the presentation is quantified inside the antichain, so each antichain supplies its own coding rather than the whole space carrying a uniform one.
Suppose a rank \(\rho \) is \({\lt} \omega _1\) on \(A\) and each of its fixed-rank antichains inside \(A\) is countable, and suppose further that every continuous Cantor antichain \(f\) in \(A\) admits, on some continuously and injectively embedded Cantor subcopy \(e\), a presentation: a continuous map from \(2^{\mathbb {N}}\) to codes, all of them well-orders, whose order types are the ranks along \(f \circ e\). Then \(\rho \) is a ranked thinness analysis of \(A\) for \(r\).
Only the refined Cantor-antichain bound needs proving. Given an antichain, take its subcopy and presentation; the coding is continuous on all of \(2^{\mathbb {N}}\), which is analytic because it is closed in a Polish space, so boundedness for analytic families of coded well-orders bounds the order types — that is, the ranks along \(f \circ e\) — by a single countable ordinal. Return that same subcopy with the bound.
Bibliography
- Bar75
Jon Barwise, Admissible sets and structures: An approach to definability theory, Perspectives in Mathematical Logic, Springer-Verlag, 1975.
- Gao09
Su Gao, Invariant descriptive set theory, Pure and Applied Mathematics, CRC Press, 2009.
- Kar64
Carol R. Karp, Languages with expressions of infinite length, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1964.
- Kar65
to3em, 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.
- KK04
H. Jerome Keisler and Julia F. Knight, Barwise: infinitary logic and admissible sets, The Bulletin of Symbolic Logic 10 (2004), no. 1, 4–36.
- LE65
E. G. K. López-Escobar, An interpolation theorem for denumerably long formulas, Fundamenta Mathematicae 57 (1965), 253–272.
- 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.
- Sco65
Dana Scott, Logic with denumerably long formulas and finite strings of quantifiers, The Theory of Models (J. W. Addison, Leon Henkin, and Alfred Tarski, eds.), North-Holland, 1965, pp. 329–341.