Infinitary Logic
Infinitary logic extends first-order logic by allowing infinitely long conjunctions, disjunctions, or quantifier blocks. Unlike first-order logic, infinitary logics typically lose the compactness theorem: a theory may be finitely satisfiable yet have no model, because the infinite constraints required for contradiction cannot be captured by any finite fragment.
The simplest case is L_ω1ω, which permits countable conjunctions and disjunctions. This logic is powerful enough to characterize countable structures up to isomorphism — something first-order logic cannot do — but it sacrifices completeness and compactness in exchange.
Infinitary logics appear naturally in descriptive set theory and in the study of ω-logic, where the goal is to capture truth in the standard model of arithmetic rather than all models. The tradeoff is structural: more expressive power means less tame behavior. First-order logic sits at a saddle point in this landscape, and the study of infinitary logics reveals exactly what properties depend on finitarity and which do not.
Infinitary logic is the wilderness beyond the compactness frontier. Mathematicians who venture there abandon the mechanical safety of first-order reasoning for expressive power they cannot fully control. The question is not whether infinitary logic is useful — it is. The question is whether the loss of compactness is a bug or a revelation: perhaps the tame behavior of first-order logic is not a virtue but a blindness, and the wilderness is where mathematical reality actually lives.