Infinitary Logic

Origin. Developed in the 1960s-70s by Carol Karp, Dana Scott, and others. Extends first-order logic to allow infinitely long formulas — infinite conjunctions and disjunctions. Studies the boundary between first-order and second-order expressiveness. Key results: Scott's isomorphism theorem, Lopez-Escobar's theorem on invariant formulas.

Models. Infinite conjunctions and disjunctions. First-order logic allows only finite formulas. Infinitary logic permits: ⋀ᵢ∈I φᵢ (infinite conjunction), ⋁ᵢ∈I φᵢ (infinite disjunction). Can express properties impossible in finitary logic: "the domain is finite," "the domain is infinite," "every element is reachable from a by finitely many steps." Controlled by two cardinals: formula width and quantifier depth.

Formalism.

Notation L_{κλ}:

κ: maximum cardinality of conjunctions/disjunctions
λ: maximum length of quantifier sequences
L_{ωω} = first-order logic (both finite)
L_{ω₁ω}: countable conjunctions/disjunctions, finite quantifiers
L_{∞ω}: arbitrary conjunctions, finite quantifiers

Syntax of L_{ω₁ω}:

First-order syntax, plus:
If {φᵢ : i ∈ I} is a countable set of formulas, so are ⋀ᵢ∈I φᵢ and ⋁ᵢ∈I φᵢ

Examples:

"The domain is finite": ⋁_{n∈ω} "exactly n elements" (infinite disjunction)
"The domain is infinite": ⋀_{n∈ω} "at least n elements" (infinite conjunction)

Neither is a single first-order sentence, and "finite" is not even a first-order theory. Note the limit: L_{ω₁ω} still cannot say "the domain is countable" in the language of pure equality.

Scott sentences: Every countable structure M has a sentence σ_M in L_{ω₁ω} such that: N ⊨ σ_M iff N ≅ M Infinitary logic can pin down structures up to isomorphism.

Back-and-forth systems: L_{∞ω} equivalence = existence of back-and-forth system (partial isomorphisms). Ehrenfeucht-Fraïssé games generalize to infinitary case.

Fragments:

L_{ω₁ω}^{ω}: finite variable infinitary logic
Useful for characterizing complexity classes

Symbols.

Symbol	Unicode	Name	Meaning
⋀	U+22C0	N-ary logical and	Conjunction over an index set of admissible size
⋁	U+22C1	N-ary logical or	Disjunction over an index set of admissible size
L_{κλ}	—	Infinitary language	κ bounds conjunction width, λ bounds quantifier block length
ω	U+03C9	Small letter omega	First infinite ordinal; indexes the countable conjunctions
ω₁	—	Omega-one	First uncountable ordinal; the bound in L_{ω₁ω}
∞	U+221E	Infinity	Conjunctions of unbounded size
≅	U+2245	Approximately equal to / Isomorphism	Isomorphism of structures
⊨	U+22A8	True / Satisfies	Satisfaction, defined by transfinite recursion
σ_M	—	Scott sentence	The L_{ω₁ω} sentence characterizing M among countable structures
¬	U+00AC	Negation	Finitary connective, retained unchanged
∀	U+2200	Universal quantifier	Blocks of length below λ
∃	U+2203	Existential quantifier	Blocks of length below λ
I	—	Index set	Indexes the family conjoined or disjoined

Metatheory. The good behaviour is concentrated in L_{ω₁ω}. Karp gave a proof system for it with an infinitary conjunction rule and proved it complete; what fails is effectivity, not completeness, since the derivations are themselves infinite and the set of validities is not recursively enumerable, so no finitary calculus can do the job. Compactness fails outright: {"at least n elements" : n ∈ ω} together with "the domain is finite" is finitely satisfiable and unsatisfiable. Downward Löwenheim–Skolem survives — every satisfiable L_{ω₁ω} sentence has a countable model — and Barwise recovered a usable compactness theorem for countable admissible fragments, which is what makes admissible set theory the natural setting. Scott's isomorphism theorem (1965) gives every countable structure a sentence σ_M characterizing it up to isomorphism among countable structures. Lopez-Escobar (1965) proved interpolation for L_{ω₁ω}, and separately that the isomorphism-invariant Borel classes of countable structures are exactly those axiomatized by L_{ω₁ω} sentences — the theorem that ties the logic to descriptive set theory. Karp's theorem identifies L_{∞ω}-equivalence with the existence of a back-and-forth system of partial isomorphisms.

Applies to. Descriptive set theory. Model theory of specific structures. Classification of countable structures. Complexity theory (finite model theory). Characterizing algebraic properties. Abstract model theory.

Limitations. Compactness is gone, and with it the ultraproduct constructions, the standard nonstandard-model arguments and every existence proof that runs through finite satisfiability. Upward Löwenheim–Skolem fails too: a sentence saying every element is reached from a in finitely many successor steps has countably infinite models and no uncountable one, so cardinality can no longer be varied at will. No effective proof system is possible, since validity is not recursively enumerable, and Karp's completeness theorem covers only finite quantifier blocks — L_{ω₁ω₁}, which permits countably infinite blocks, has no comparable result. Above L_{ω₁ω} the model theory becomes a large-cardinal question rather than a logical one: L_{κκ} is compact precisely when κ is strongly compact, and the existence of such a cardinal is not provable in ZFC. L_{∞ω} has a proper class of formulas, so its satisfaction relation is not given by any single definition in ZFC and must be treated fragment by fragment.