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: "exactly ℵ₀ elements exist." 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:

"Exactly countably many elements": ⋁_{n∈ω} "exactly n elements" (infinite disjunction)
Every finite property can be stated: ⋁_{F finite} "isomorphic to F"

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	Big conjunction	Infinitary and
⋁	U+22C1	Big disjunction	Infinitary or
L_{κλ}	—	Infinitary language	Parameterized logic
ω	U+03C9	Omega	First infinite ordinal
ω₁	—	Omega-one	First uncountable ordinal
∞	U+221E	Infinity	Unbounded
≅	U+2245	Isomorphism	Structural equality
σ_M	—	Scott sentence	Defines M up to ≅

Metatheory. Completeness fails: no finitary proof system for L_{ω₁ω}. Compactness fails: can express "finitely many" by ¬(infinitely many). Downward Löwenheim-Skolem holds for L_{ω₁ω}. Interpolation holds for L_{ω₁ω}. The number of types (in the sense of model theory) can be uncountable. Lopez-Escobar: L_{ω₁ω}-formulas on Polish spaces are exactly Borel-measurable.

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. No finitary axiomatization. Compactness failure limits standard techniques. Truth definition requires transfinite recursion. Formulas may be hard to construct explicitly. Less developed proof theory. Beyond L_{ω₁ω}, the theory becomes highly set-theoretic. Practical applications are limited compared to finitary logics.