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 65).
Morley counting. An \(\mathcal{L}_{\omega _1\omega }\) sentence has \(\leq \aleph _1\) or exactly \(2^{\aleph _0}\) isomorphism classes of countable models (Theorem 70).
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.3 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 57, 58).
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 71).
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 73).
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 76, 77, 78).
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 54, 55).
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 79).
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
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.3: 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.3 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 11.2 (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 11.2).
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\) 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.
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 hard direction follows Marker’s route (Theorem 4.25 of [ Mar16 ] ) 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.25). \(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 11.2 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 11.2 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 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) 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].
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.26 and Corollary 4.27 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. 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; 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.27 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.27 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.
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.