Infinitary Logic #
This library formalizes infinitary logic, including:
- L∞ω: Infinitary logic with arbitrary conjunctions/disjunctions
- Lω₁ω: Countable infinitary logic (countable conjunctions/disjunctions)
- Scott sentences and Scott rank for characterizing countable structures
Main Results #
- Every countable structure in a relational countable language has a Scott sentence that characterizes it up to isomorphism.
- The Scott rank of a countable structure is a countable ordinal (< ω₁).
- L∞ω is the union of all Lκω for cardinals κ; Lω₁ω = L(ℵ₁)ω.
The unconditional API is recovered via countableRefinementHypothesis (proved in
Scott/RefinementCount.lean). Conditional _of variants taking
CountableRefinementHypothesis as a hypothesis are also available.
Organization #
L∞ω (Linf/) #
Linf/Syntax.lean: Syntax of L∞ω formulas with arbitrary index typesLinf/Semantics.lean: Semantics (Realize)Linf/Operations.lean: Operations (relabel, castLE, subst, FO embedding)Linf/Countability.lean: IsCountable and IsKappa predicates
Lω₁ω (Lomega1omega/) #
Lomega1omega/Syntax.lean: Syntax of Lω₁ω formulas with ℕ-indexed connectivesLomega1omega/Semantics.lean: Semantics (Realize)Lomega1omega/Operations.lean: Operations (relabel, castLE, subst)Lomega1omega/Embedding.lean: Embeddings between Lω₁ω and L∞ω
Scott sentences (Scott/) #
Scott/AtomicDiagram.lean: Atomic types for relational languagesScott/BackAndForth.lean: Back-and-forth equivalenceScott/Formula.lean: Scott formula constructionScott/Code.lean: Countable formula codes (FormulaCode, encoding, BFEquiv bridge)Scott/Sentence.lean: Scott sentence and characterization theorem (_ofvariants)Scott/RefinementCount.lean: CRH theorem + unconditional Sentence-level wrappersScott/Rank.lean: Scott rank definition and boundsScott/QuantifierRank.lean: Quantifier rank bounds on Scott formulasScott/Height.lean: Scott height, canonical Scott sentence, sr/SR
Karp's theorem (Karp/) #
Karp/PotentialIso.lean: Potential isomorphism definitionKarp/Theorem.lean: Karp's theorem (potential iso ↔ L∞ω-equivalence)Karp/CountableCorollary.lean: Countable structures corollary
Model existence (ModelExistence/) #
ModelExistence/ConsistencyProperty.lean: Consistency property axioms (C0)-(C7)ModelExistence/HenkinConstruction.lean: Henkin construction infrastructure (maximal consistent sets)ModelExistence/Theorem.lean: Model existence theoremModelExistence/Completeness.lean: Karp completeness and omitting types
Model theory (ModelTheory/) #
ModelTheory/LowenheimSkolem.lean: Downward Löwenheim-Skolem for Lω₁ωModelTheory/Hanf.lean: Hanf numbers and Morley-Hanf boundModelTheory/CountingModels.lean: Scott rank and model countingModelTheory/CountingCountable.lean: Counting theorem for all countable modelsModelTheory/MorleyCounting.lean: Morley's counting theorem (≤ ℵ₁ or 2^ℵ₀)
Admissible sets (Admissible/) #
Admissible/Fragment.lean: Abstract admissible fragmentsAdmissible/Compactness.lean: Barwise compactness and completenessAdmissible/NadelBound.lean: Nadel bound on Scott height
Descriptive set theory (Descriptive/) #
Descriptive/StructureSpace.lean: Coding space for countable structures on ℕDescriptive/Measurable.lean: Measurable space structure on the coding spaceDescriptive/Topology.lean: Topological structure on the coding spaceDescriptive/Polish.lean: Polish space and standard Borel space instancesDescriptive/SatisfactionBorel.lean: Borel complexity of Lω₁ω satisfactionDescriptive/BFEquivBorel.lean: Borel complexity of BF-equivalenceDescriptive/IsomorphismBorel.lean: Isomorphism is Borel under bounded Scott heightDescriptive/ModelClassStandardBorel.lean: Model classes are standard BorelDescriptive/CountingDichotomy.lean: Conditional counting dichotomy (Silver–Burgess)Descriptive/SatisfactionBorelOn.lean: Generic satisfaction measurability for carrier-parametric spacesDescriptive/FiniteCarrier.lean: Finite-carrier counting via permutation orbits; combined dichotomyDescriptive/SilverBurgess.lean: Silver-Burgess dichotomy (1 sorry: Borel→closed reduction)