Fact-checked by Grok 2 weeks ago

Infinitary logic

Infinitary logic is a branch of mathematical logic that extends classical first-order logic by permitting formulas of transfinite length, most notably through infinite conjunctions and disjunctions, while typically restricting quantifiers to finite sequences in its primary variants.^[1] This allows for greater expressive power, enabling the formulation of concepts that are inexpressible in standard first-order logic, such as the characterization of specific uncountable structures up to isomorphism.^[1] The syntax of infinitary logics, such as L_{\kappa,\omega}, is built from a set of variables indexed by ordinals less than a cardinal \kappa, predicate and function symbols, and logical connectives including negation, finite conjunctions and disjunctions, infinite conjunctions (\bigwedge) and disjunctions (\bigvee) over sets of formulas of cardinality less than \kappa, and quantifiers (\forall, \exists) applied to finitely many variables.^[2] Semantics are defined via the standard Tarskian satisfaction relation, extended inductively to handle infinite connectives, where a structure satisfies an infinite conjunction if it satisfies every conjunct, and similarly for disjunctions.^[1] Notable variants include L_{\infty,\omega}, which allows arbitrary infinite lengths for connectives but finite quantifiers, and L_{\omega_1,\omega}, which confines infinite operations to countable cardinality, making it particularly useful for studying countable models.^[2] Unlike first-order logic, infinitary logics generally lack the compactness theorem, as there exist theories with all finite subsets satisfiable but the entire theory inconsistent.^[1] However, they retain a form of the downward Löwenheim-Skolem theorem: for any structure M and infinitary fragment F (with formulas having finitely many free variables), there exists an elementary submodel N \prec M with |N| \leq |F| + \aleph_0.^[1] A landmark result is Scott's isomorphism theorem, which states that every countable structure is definable up to isomorphism by a sentence in L_{\omega_1,\omega}.^[1] These logics occupy an intermediate position between first-order and second-order logic, offering tools to analyze categoricity, stability, and homogeneity in model theory without invoking full set-theoretic quantification.^[2] Infinitary logic was introduced by Dana Scott and Alfred Tarski in 1958.^[3] The development of infinitary logic gained momentum in the mid-20th century, with seminal contributions from H. J. Keisler's 1971 monograph Model Theory for Infinitary Logic, which systematized the model theory of logics with countable conjunctions and finite quantifiers, and J. Barwise's 1975 work Admissible Sets and Structures, which connected infinitary logic to admissible ordinals and recursion theory.^[2] Subsequent research has explored applications in descriptive set theory, generalized quantifiers, and the boundaries of logical expressiveness, highlighting infinitary logic's role in bridging proof theory and model theory.^[1]

Introduction

Overview and Motivation

Infinitary logic extends classical first-order logic by permitting formulas of transfinite length, including infinite conjunctions and disjunctions, and in certain variants, infinite sequences of quantifiers. This generalization, first formalized for propositional calculi with infinite expressions, allows for the construction of languages L_{\kappa,\lambda} where conjunctions and disjunctions have length less than cardinal \kappa and quantifier blocks have length less than \lambda. Unlike standard first-order logic, which restricts all syntactic operations to finite lengths, infinitary logics enhance expressive power to capture properties that require infinitely many conditions simultaneously.^[4]^[5] The primary motivation for infinitary logic arises from the expressive limitations of finitary first-order logic L_{\omega,\omega}, which cannot adequately describe certain structural properties in uncountable models or infinite axiom systems. For instance, first-order logic fails to express well-foundedness in linear orders or to achieve categoricity for structures of uncountable cardinality without additional infinitary mechanisms. Infinitary variants like L_{\infty,\omega} address this by allowing arbitrary infinite conjunctions and disjunctions while keeping quantifiers finite, thus enabling the concise formulation of infinite axiomatizations—such as the infinite set of axioms defining the real numbers as the unique complete ordered field—within a single sentence. This extension preserves some desirable semantic properties while overcoming the inability of finitary logic to handle such global features.^[6] In model theory, infinitary logic facilitates deeper analysis of stability and classification, such as through Scott sentences that characterize countable structures up to isomorphism using countable conjunctions. In set theory, it plays a crucial role in characterizing large cardinals; for example, the compactness theorem for L_{\kappa,\kappa} holds if and only if \kappa is a strongly compact cardinal, linking logical properties to foundational assumptions like the continuum hypothesis. These applications highlight infinitary logic's utility in bridging syntax and semantics for infinite structures, where finitary methods fall short.^[6]^[7]

Historical Development

The origins of infinitary logic can be traced to Ernst Zermelo's work in the 1930s, where he introduced infinite conjunctions and disjunctions as tools for formalizing proofs in set theory, aiming to capture the "logic of the infinite" beyond finitary restrictions.^[8] In his 1930 paper, Zermelo proposed a hierarchical system of expressions using infinite logical operations to axiomatize set theory, emphasizing maximality principles that relied heavily on the axiom of choice to handle transfinite constructions without collapsing to finitary methods. This approach marked an early departure from traditional first-order logic, influenced by Zermelo's commitment to the axiom of choice as essential for infinitary reasoning, though it remained somewhat informal and tied to set-theoretic foundations.^[8] The prehistory of infinitary logic from 1885 to 1955 involved scattered contributions that laid groundwork through generalized quantifiers and extensions of first-order systems, notably by Leopold Löwenheim, Thoralf Skolem, and Alfred Tarski. Löwenheim's 1915 theorem implicitly allowed for generalized quantifiers in restricting models, while Skolem's 1920 work on relativization further explored non-standard interpretations that anticipated infinitary expressiveness.^[9] Tarski, building on these, developed ideas in the 1930s–1950s for logics with infinite operations, including quantifiers over uncountable domains, which influenced the semantic foundations of infinitary systems without fully formalizing them as a distinct logic.^[9] Post-1950 developments formalized infinitary logic as a robust extension of first-order logic, beginning with Dana Scott's seminal 1965 paper introducing the language L_{\omega_1,\omega}, which permits countable conjunctions and disjunctions but finite quantifier strings, enabling precise characterizations of countable structures up to isomorphism via Scott sentences.^[10] H.J. Keisler's 1971 monograph Model Theory for Infinitary Logic systematized the model theory for logics with countable conjunctions and finite quantifiers, while J. Barwise's 1975 work Admissible Sets and Structures connected infinitary logic to admissible ordinals and recursion theory. Around the same time, Michael Morley and Robert Vaught advanced compactness results for infinitary logics in their 1962 work on homogeneous models, showing that certain theories admitting models of specific cardinalities also admit saturated ones, bridging model theory and infinitary expressiveness.^[11] These efforts revealed deep connections to large cardinals, as the compactness of logics like L_{\kappa,\kappa} characterizes strongly compact cardinals, a link first explored by William Hanf and Scott in the 1960s.^[12] Recent advancements up to 2023 have explored connections between inner model theory and forcing, particularly in addressing the continuum hypothesis. W. Hugh Woodin's 2011 results on the ultimate L conjecture use forcing extensions and inner models to argue that large cardinals cannot refute the continuum hypothesis in canonical inner models, providing evidence for its consistency relative to stronger axioms.^[13] This work highlights infinitary logic's foundational role in calibrating the boundaries between forcing and descriptive inner models, influencing ongoing debates on the continuum's value.^[12]

Preliminaries

Notation and the Axiom of Choice

In infinitary logic, standard notation employs ellipses (⋯) for informal representations of infinite expressions, while formal indexed notations such as \bigvee_{\gamma < \delta} A_\gamma for infinite disjunctions and \bigwedge_{\gamma < \delta} A_\gamma for infinite conjunctions are used to denote operations over indexed families of formulas \{A_\gamma : \gamma < \delta\}, where \delta is an ordinal.^[3]^[14] These symbols extend the finite connectives \vee and \wedge to infinitary settings, allowing the construction of formulas that capture properties requiring infinitely many conditions simultaneously. For instance, an infinite conjunction of atomic formulas might be written as \bigwedge_{n < \omega} P(x_n), expressing that a sequence satisfies a predicate at every finite stage.^[4] Cardinality parameters play a central role in defining the scope of infinitary operations: \kappa bounds the length of conjunctions and disjunctions, while \lambda limits the size of blocks of quantifiers, typically with infinite cardinals \lambda \leq \kappa.^[3] This leads to languages like \mathcal{L}_{\kappa,\lambda}, where formulas permit conjunctions or disjunctions over fewer than \kappa subformulas and quantifier prefixes of length less than \lambda. For example, in \mathcal{L}_{\omega_1,\omega}, countable infinite conjunctions are allowed, but quantifiers remain finite, enabling the expression of properties requiring infinitely many simultaneous conditions, such as the standard model of arithmetic via \bigwedge_{m,n < \omega} (s^m 0 + s^n 0 = s^{m+n} 0).^[14]^[3] Many foundational results in infinitary logic rely on the axiom of choice (AC), particularly for ensuring distributivity properties over infinite operations and the existence of well-orderings in proofs involving transfinite inductions or model constructions.^[3] For instance, AC facilitates the well-ordering of index sets in infinite disjunctions, allowing proofs of completeness theorems by selecting canonical representatives from equivalence classes of models. Without AC, certain existential quantifier eliminations or compactness arguments may fail, as they require choosing elements from uncountably many nonempty sets.^[14] Choice-free alternatives, such as those employing filter methods like Q-filters in place of direct selection, have been developed for specific subsystems, particularly in countable infinitary epistemic logics, but they often limit applicability to languages with restricted cardinalities or fail to achieve full completeness without additional assumptions.^[15] These approaches highlight the foundational trade-offs, where avoiding AC preserves constructivity but restricts the expressive power and generality of theorems compared to ZFC-based developments.^[3]

Signature and Formal Languages

In infinitary logic, the foundational structure is provided by a signature, which specifies the non-logical symbols available for constructing terms and formulas. A signature σ consists of disjoint sets of constant symbols C, function symbols F, and relation symbols R, together with an arity function a: F ∪ R → ℕ that assigns to each function symbol in F a finite positive arity (the number of arguments it takes) and to each relation symbol in R a finite positive arity (including 0 for constants, though constants are separately listed in C).^[16] This setup mirrors the signatures used in first-order logic but serves as the basis for extending to infinitary constructions.^[14] The formal language over a signature σ incorporates an alphabet comprising the symbols from σ along with logical symbols. These logical symbols include the equality predicate = (binary), negation ¬, implication → (or equivalently, infinite conjunctions ∧_I and disjunctions ∨_I for index sets I of cardinality less than κ), universal quantifiers ∀x (and infinite blocks ∀{x_i : i ∈ I} for |I| < λ), existential quantifiers ∃x (and infinite blocks ∃{x_i : i ∈ I} for |I| < λ), a set of variables of cardinality κ {v_α : α < κ}, and parentheses for grouping.^[17]^[3] The infinitary nature emerges in the allowance of infinite conjunctions and disjunctions, as well as infinite quantifier blocks, while maintaining finite arities for non-logical symbols.^[14] Terms in the language are formed finitarily via recursive rules, ensuring no infinite constructions within them. Specifically, every variable is a term; every constant symbol c ∈ C is a term; and if f ∈ F has arity n and t_1, ..., t_n are terms, then f(t_1, ..., t_n) is a term. No further compositions are permitted, distinguishing terms from the potentially infinitary formulas built upon them.^[14] This finitary restriction on terms preserves the standard algebraic structure while allowing infinitary expressiveness in the propositional and quantificational aspects of formulas.^[18] For example, a simple signature for arithmetic might include constants 0 and 1 (arity 0), binary function symbols + and × (arity 2), and no relation symbols beyond equality.^[14] Similarly, for set theory, the signature could consist solely of the binary relation symbol ∈ (arity 2), with no constants or functions, enabling the expression of foundational axioms through infinitary means.^[14] These examples illustrate how signatures tailor the language to specific mathematical domains without altering the underlying infinitary logical framework.^[16]

Syntax and Semantics

Infinitary Languages L_{\kappa,\lambda}

Infinitary languages L_{\kappa,\lambda} extend first-order logic by permitting conjunctions and disjunctions of cardinality less than a cardinal \kappa and quantifier prefixes of length less than a cardinal \lambda, where \kappa and \lambda are typically infinite cardinals greater than or equal to \aleph_0. These languages are constructed over a fixed first-order signature consisting of relation symbols, function symbols, and constants, with variables ranging over a set of cardinality at most \kappa. The syntax begins with atomic formulas, which are equations t = s or atomic relations R(t_1, \dots, t_n) where t, s, t_i are terms built from variables, constants, and function applications in the standard finite way.^[3] Formulas in L_{\kappa,\lambda} are defined recursively as follows: atomic formulas are in L_{\kappa,\lambda}; if \phi is a formula, then \neg \phi is a formula; if \phi and \psi are formulas, then \phi \land \psi and \phi \lor \psi are formulas; if \{\phi_i \mid i < \mu\} is a set of formulas with \mu < \kappa, then \bigwedge_{i < \mu} \phi_i and \bigvee_{i < \mu} \phi_i are formulas; and if \phi is a formula and \nu < \lambda, then for any sequence of distinct variables x_1, \dots, x_\nu (possibly infinite), \forall x_1 \dots x_\nu \phi and \exists x_1 \dots x_\nu \phi are formulas, where the quantifiers bind any free occurrences of the x_i in \phi. This construction ensures that every formula has fewer than \lambda free variables, and sentences are those with no free variables.^[3] A representative example of an infinitary formula is the infinite quantifier alternation \forall x_1 \exists y_1 \forall x_2 \exists y_2 \cdots \phi(x_1, y_1, x_2, y_2, \dots), where the quantifier string has length \omega and \phi is a first-order formula; this is admissible in L_{\kappa,\lambda} for \lambda > \omega. Such formulas capture properties requiring unbounded alternation, beyond the finite depth of first-order logic.^[3] The semantics of L_{\kappa,\lambda} follows a Tarski-style satisfaction relation extended to infinitary cases, defined for structures \mathcal{M} over the signature (with universe M and interpretations of symbols) and assignments s mapping free variables to elements of M. For atomic formulas, satisfaction is standard; \mathcal{M}, s \models \neg \phi if \mathcal{M}, s \not\models \phi; \mathcal{M}, s \models \phi \land \psi (or \bigwedge \Phi) if \mathcal{M}, s \models \phi and \mathcal{M}, s \models \psi (or all \psi \in \Phi); and \mathcal{M}, s \models \exists x_1 \dots x_\nu \phi if there exists a sequence a_1, \dots, a_\nu \in M such that \mathcal{M}, s[x_i \mapsto a_i] \models \phi, with the universal quantifier defined dually via negation. For infinite conjunctions, satisfaction requires every component to hold, often relying on the axiom of choice for uniformizing witnesses in existential cases, though direct recursion suffices for the definition. Truth in a model \mathcal{M} for a sentence \phi is \mathcal{M} \models \phi (with empty assignment), and validity holds if true in all models.^[3] Key parameters distinguish variants: in L_{\omega_1, \omega}, conjunctions and disjunctions may have cardinality less than \aleph_1 (at most countable), but quantifier strings are finite, enabling expressions like countable conjunctions of atomic properties to define Scott sentences for countable structures. In contrast, L_{\infty, \omega} allows arbitrary (possibly uncountable) conjunctions and disjunctions but restricts quantifiers to finite lengths, emphasizing infinitary Boolean combinations over first-order quantification. For L_{\kappa, \kappa}, both operations extend to cardinality less than \kappa, balancing expressive power in connectives and quantifiers, as formalized in early treatments of predicate infinitary logics.^[3]

Hilbert-Type Deductive Systems

In infinitary logic, a Hilbert-type deductive system provides a syntactic framework for deriving theorems from axioms using inference rules, extending the classical first-order Hilbert system to accommodate infinite conjunctions and disjunctions in the language L_{\kappa,\lambda}. The system consists of a set of axiom schemata and a collection of inference rules, where proofs are typically transfinite sequences of formulas of length less than \kappa. The axioms include all standard first-order logical axiom schemata, such as those for propositional connectives (extended to finite combinations), equality, and quantifiers (e.g., \forall x (\phi \to \psi) \to (\forall x \phi \to \forall x \psi) for appropriate \phi, \psi), as well as infinitary-specific schemata to handle infinite connectives. For infinite conjunctions, key axioms are \bigwedge_{i < \mu} \phi_i \to \phi_j for each j < \mu < \kappa and any formulas \{\phi_i \mid i < \mu\}, and similarly for disjunctions, \phi_j \to \bigvee_{i < \mu} \phi_i. Additional infinitary axioms incorporate distributivity laws, such as Chang's laws for the distribution of infinite conjunctions over finite disjunctions (e.g., \bigwedge_{i < \kappa} (\phi_i \vee \psi) \to (\bigwedge_{i < \kappa} \phi_i) \vee \psi) and their duals, ensuring compatibility with the semantics of infinitary formulas. Generalization axioms extend to infinite blocks in certain variants, allowing \forall-introduction over infinitary subformulas, though quantifiers remain finite in the standard setup.^[19] Inference rules preserve the logical structure across infinite expressions. Modus ponens allows derivation of \psi from \phi and \phi \to \psi. Universal generalization permits inferring \forall x \phi from \phi, applicable even when \phi involves infinite connectives. Infinitary rules include conjunction introduction, where from the premises \{\phi_i \mid i < \mu < \kappa\} (each previously derived), one infers \bigwedge_{i < \mu} \phi_i, and the dual disjunction elimination rule. These rules enable handling infinite premises directly in proofs.^[19] Proofs are defined as sequences \langle \sigma_\alpha \mid \alpha < \nu < \kappa \rangle where each \sigma_\alpha is either an axiom or obtained by applying an inference rule to earlier elements in the sequence, allowing transfinite inductions for derivations involving infinite steps. A formula \sigma is a theorem if it appears in some proof, denoted \vdash \sigma. Theories in this context are sets T of sentences closed under logical consequence, meaning if \Delta \subseteq T with |\Delta| < \kappa and \Delta \vdash \sigma, then \sigma \in T; such closure ensures consistency with the deductive system. As an example, consider deriving the infinitary theorem \bigwedge_{n < \omega} \forall x (P(x,n) \to Q(x)) \to \forall x \bigwedge_{n < \omega} (P(x,n) \to Q(x)) in L_{\omega_1, \omega}. Start with the premises \{\forall x (P(x,n) \to Q(x)) \mid n < \omega\} via conjunction introduction to obtain \bigwedge_{n < \omega} \forall x (P(x,n) \to Q(x)). Apply the first-order axiom schema \forall x (\phi \to \psi) \to (\phi \to \forall x \psi) (with free variable adjustment) iteratively for each n, then use infinite conjunction axioms and modus ponens to distribute the universal quantifier inward, yielding the consequent after generalization. This deduction relies on the infinitary rules to manage the countable conjunction.^[19]

Key Properties

Completeness Theorems

In infinitary logic L_{\kappa,\lambda}, the weak completeness theorem asserts that a sentence \phi is semantically valid if and only if it is provable in the associated Hilbert-type deductive system, where proofs may involve conjunctions and disjunctions of length less than \kappa. This holds provided that \kappa is a regular cardinal, ensuring that the language remains closed under the operations used in the proof system. The theorem generalizes the classical Gödel completeness result for first-order logic to infinitary settings. The proof proceeds via a Henkin-style construction adapted for infinite languages. Starting from a consistent set of sentences, one expands the language by adding Skolem constants for each infinitary quantifier prefix in the formulas, indexed by sequences of length less than \lambda. The regularity of \kappa guarantees that the expanded language has cardinality at most \kappa, allowing a maximal consistent theory to be obtained through transfinite recursion of length \kappa. A model is then built by interpreting the constants as elements satisfying the witness conditions, with the axiom of choice used to select these Skolem functions and ensure the existence of the required sequences. Strong completeness, which states that for any theory \Gamma, \Gamma \vdash \phi if and only if \phi holds in every model of \Gamma (or equivalently, every consistent theory has a model), fails for most infinitary logics without additional assumptions. For L_{\kappa,\lambda}, it holds relative to theories of cardinality less than \kappa when \kappa is regular, but counterexamples exist for larger theories; for instance, in L_{\omega_1,\omega}, there are uncountable consistent sets whose countable subsets are satisfiable but the whole set is not. These proofs also rely on the axiom of choice; without it, the Henkin construction may fail for L_{\infty,\omega}, as selecting witnesses for infinite conjunctions of existential formulas requires non-constructive choices, leading to consistent theories without models in ZF alone. The completeness theorems in infinitary settings imply generalized Löwenheim-Skolem results: if a theory in L_{\kappa,\omega} with \kappa regular is consistent, it has a model of cardinality at most \kappa, providing a downward size bound analogous to the first-order case but scaled to the infinitary cardinality.

Compactness and Strong Compactness

In first-order logic, the compactness theorem asserts that a theory is satisfiable if and only if every finite subset of it is satisfiable. This result carries over to the finitary infinitary logic L_{\omega,\omega}, where sentences involve only finite conjunctions, disjunctions, and quantifiers. However, the theorem fails for infinitary extensions such as L_{\omega_1,\omega}, which permits countable conjunctions and disjunctions but only finite strings of quantifiers. The failure arises because infinite connectives allow expressions that capture global properties not approximable by finite subsets. A canonical example demonstrating this failure in L_{\omega_1,\omega} involves a language with countably many constants c_i for i < \omega and an additional constant d. Consider the theory T consisting of the sentences \neg (c_i = c_j) for all i \neq j < \omega, \neg (d = c_i) for each i < \omega, together with the infinitary sentence \forall v \bigvee_{i < \omega} (v = c_i), which asserts that every element is equal to one of the c_i. Every finite subset of T is satisfiable: if the infinitary sentence is included, the finitely many distinctness and inequality sentences can be satisfied by interpreting the relevant c_i distinctly and assigning d to the interpretation of some unexcluded c_j, with the domain being \{c_i \mid i < \omega\}; without it, add d as a distinct element. Yet T as a whole is unsatisfiable, as the infinitary sentence confines the domain to \{c_i \mid i < \omega\}, while the inequalities require d to differ from all c_i, leaving no possible interpretation for d. This highlights how countable disjunctions enable the expression of countability, leading to inconsistencies not detectable finitely.^[14] Another illustration of compactness failure involves uncountable collections in L_{\omega_1,\omega}, such as a theory enforcing distinctness via an uncountable set of pairwise inequalities over constants c_\alpha for \alpha < \omega_1. While each finite subset is satisfiable in a finite domain, combining this with mechanisms to bound the domain size (via countable approximations) can render the full theory unsatisfiable, underscoring the breakdown beyond finite approximations. In broader infinitary logics like L_{\infty,\omega}, which allow arbitrary-length conjunctions but finite quantifiers, compactness fails similarly for theories relying on non-compact cardinals, as finite or small subsets may admit models while the entire theory does not due to the inability to "glue" uncountably many constraints consistently. To address such limitations, infinitary logics admit generalized compactness notions tied to large cardinals. For an uncountable cardinal \kappa, the logic L_{\kappa,\kappa} is \kappa-compact if a theory is satisfiable precisely when every subtheory of cardinality less than \kappa is satisfiable. This property holds for L_{\kappa,\kappa} if and only if \kappa is a strongly compact cardinal, a large cardinal notion originally motivated by logical considerations. Strongly compact cardinals exceed measurables in strength and imply the existence of many weakly compacts below them.^[20] The equivalence between \kappa-compactness of L_{\kappa,\kappa} and strong compactness of \kappa relies on set-theoretic constructions. One direction uses the defining feature of strong compactness: every \kappa-complete filter on any set can be extended to a \kappa-complete ultrafilter. This enables building models via generalized ultraproducts, where a \kappa-satisfiable theory yields a satisfying ultraproduct by averaging models over the ultrafilter, preserving infinitary formulas up to length \kappa. The converse proceeds by considering specific theories in L_{\kappa,\kappa} whose satisfiability encodes filter extension problems; if the logic is \kappa-compact, such theories force the ultrafilter existence, yielding the cardinal property. These proofs highlight the interplay between logical semantics and ultrafilter techniques. In logics like L_{\infty,\omega}, compactness fails at non-strongly compact cardinals, as one can construct theories (e.g., involving uncountable families of almost-disjoint sets or type-omission requirements) that are <\kappa-satisfiable for some regular \kappa but globally unsatisfiable without fine-measure extensions. Such failures have applications to omitting types in infinitary logic: if a theory in L_{\kappa,\lambda} is \kappa-satisfiable and a type is omitted in every model of subtheories of size <\kappa, then compactness ensures the type can be omitted in a full model, facilitating constructions in descriptive set theory and homogeneity results.^[20] Strong compactness in infinitary contexts differs from weak compactness, which characterizes indescribability or tree properties rather than full filter extensions. For instance, while strong compactness ensures \kappa-compactness for L_{\kappa,\kappa} with arbitrary infinitary connectives, weak compactness aligns with compactness-like properties for restricted fragments like L_{\kappa,\omega} (allowing only finite quantifiers but \kappa-length connectives), often requiring only weak inaccessibility for basic versions, though full weak \kappa-compactness demands the stronger cardinal. This distinction underscores how quantifier complexity modulates the set-theoretic strength needed for logical compactness.^[20]

Expressive Power

Concepts Expressible in Infinitary Logic

Infinitary logic extends the expressive power of first-order logic by allowing infinite conjunctions and disjunctions, enabling the formulation of concepts that cannot be captured finitely. One such concept is well-foundedness of a binary relation \prec on a structure, which asserts the absence of infinite descending chains. First-order approximations, consisting of axioms forbidding descending chains of each finite length n, are consistent but, by the compactness theorem, admit models with infinite descending chains. Full well-foundedness cannot be axiomatized in L_{\omega_1,\omega}, requiring logics with infinite quantifier blocks such as L_{\omega_1,\omega_1}.^[3]^[21] This limitation is illustrated by Ehrenfeucht-Mostowski models, which construct structures with long sequences of indiscernibles that mimic well-founded relations in first-order theories but admit non-well-founded extensions, such as infinite descending chains.^[22] For instance, a first-order theory implying well-foundedness for countable models will, by compactness, have uncountable models violating it unless stronger logical resources are used. Such failures highlight why infinitary logic is essential for precise control over foundational properties in relations.^[3] In set theory, the axiom of foundation, which ensures the membership relation \in is well-founded, is expressed first-order as every non-empty set having an \in-minimal element; this equivalently rules out infinite descending \in-chains. While infinitary logics can express well-foundedness for general relations using stronger variants, the first-order formulation suffices in standard set theory.^[21]^[3] Infinitary logic also achieves categoricity for uncountable structures that first-order logic cannot. For algebraically closed fields of fixed characteristic and countable transcendence degree, the theory in L_{\omega_1,\omega} includes the first-order axioms plus infinitary sentences asserting the existence of countably many algebraically independent elements and dependence beyond that. For uncountable transcendence degree \kappa, extensions using generalized quantifiers in L_{\omega_1,\omega}(Q) ensure \kappa-categoricity.^[23] These infinitary conditions ensure the theory is \kappa-categorical, as any two models of cardinality \kappa are isomorphic, determined uniquely by the fixed parameters. First-order logic fails here, producing non-isomorphic models of varying transcendence degrees via Ehrenfeucht-Mostowski constructions with indiscernible sequences.^[24] Other structures benefit similarly. The class of torsion-free abelian groups of finite rank is axiomatizable in L_{\omega_1,\omega} by the first-order axioms excluding torsion (i.e., \forall x (nx = 0 \to x = 0) for each finite n) conjoined with the infinite disjunction \bigvee_{n < \omega} \phi_n, where each \phi_n is a first-order sentence expressing exact rank n via the existence of n \mathbb{Z}-independent elements and dependence of any n+1.^[25] This captures all finite ranks compactly, whereas first-order logic cannot axiomatize the entire class, as "finite rank" requires excluding infinite-dimensional cases, which compactness prevents. For non-Archimedean ordered fields, infinitary conjunctions axiomatize the theory by combining first-order ordered field axioms with conditions for infinitesimals, such as \exists \epsilon > 0 \bigwedge_{n < \omega} n\epsilon < 1, ensuring non-Archimedeanness without finite approximations sufficing alone in broader extensions. Finally, infinitary logic plays a key role in extensions of Peano arithmetic (PA). The standard model \mathbb{N} of PA is fully characterized up to isomorphism by a theory in L_{\omega_1,\omega}, using countable conjunctions to express the addition and multiplication tables exhaustively, such as \bigwedge_{m < \omega} \bigwedge_{n < \omega} s^m 0 + s^n 0 = s^{m+n} 0, alongside induction axioms.^[3] This provides a complete, categorical extension of PA, resolving incompletenesses in first-order formulations like Gödel's theorems, and enables consistency proofs via infinitary cut-elimination on these extended systems.^[26] Such extensions maintain conservativity over PA for \Pi_1^1 sentences while incorporating infinite schemas directly.^[27]

Applications in Model Theory

Infinitary logic plays a pivotal role in model theory by enabling the formulation of theorems that extend classical first-order results to more expressive settings, particularly for uncountable structures. The omitting types theorem for L_{\omega_1,\omega} states that for a countable fragment \Delta of L_{\omega_1,\omega}(\tau), a satisfiable theory T \subset \Delta, and families of \Delta-formulas \{\Theta_n(\mathbf{v}_n) : n < \omega\}, if for every \Delta-formula \psi(\mathbf{v}) with T \vdash \exists \mathbf{v} \psi(\mathbf{v}) there exists \theta \in \Theta_n such that T \vdash \exists \mathbf{v} (\psi(\mathbf{v}) \wedge \theta(\mathbf{v})) for some n, then T \cup \{\forall \mathbf{v} \bigvee_{\theta \in \Theta_n} \theta(\mathbf{v}) : n < \omega\} is satisfiable, provided the theory is consistent and the types are non-realized under countability assumptions on the models.^[14] This result generalizes the first-order omitting types theorem and facilitates the construction of models avoiding certain types, crucial for studying properties like homogeneity and end extensions in uncountable cardinalities.^[14] A landmark application is the classification of theories via Scott's isomorphism theorem, which leverages L_{\omega_1,\omega}-sentences to characterize countable models up to isomorphism. Specifically, for any countable \tau-structure M, there exists an L_{\omega_1,\omega}-sentence \Phi_M such that for any countable \tau-structure N, N \models \Phi_M if and only if N \cong M, where \Phi_M is constructed as the Scott sentence capturing the back-and-forth relations and atomic diagrams of M.^[14] This theorem provides a syntactic characterization of isomorphism types for countable structures, enabling precise classification in contexts where first-order logic is insufficient, such as recursive or admissible structures.^[14] In Shelah's classification theory, infinitary logic underpins the analysis of stability and saturation by expressing forking independence through non-splitting extensions in abstract elementary classes (AECs) defined via L_{\omega_1,\omega}. Forking independence, approximated by non-splitting, satisfies properties like monotonicity, transitivity, and symmetry over stationary types in stable AECs, where categoricity in a regular cardinal \lambda implies \sigma-stability for LS(K) \leq \sigma < \lambda and the existence of \lambda-Galois saturated models.^[28] This framework classifies theories into stability hierarchies, with \omega-stability characterized by primary models over countable parameter sets and unique non-splitting extensions, facilitating the study of saturated models and type-definability in excellent classes.^[28] Infinitary logic connects to generalized quantifiers and continuous model theory by extending frameworks like L_{\omega_1,\omega}(Q), where Q denotes quantifiers such as the existential second-order quantifier, to capture categoricity in AECs and continuous structures via ultraproducts and elementary chains.^[29] In continuous logic, analogous to L_{\omega_1,\omega}, infinitary variants express metric properties and support omitting types for [0,1]-valued logics, linking to Shelah's stability spectrum.^[29] Examples include infinitary axiomatizations of \aleph_1-free abelian groups, where equivalence in L_{\infty,\omega} implies freeness, and topological spaces, axiomatized in L_{\omega_1,\omega} to define closure operators and separation axioms via infinite conjunctions of open set conditions.^[14]^[30]

Advanced Topics

Complete Infinitary Logics

In infinitary logic, a complete logic is one in which every semantically valid sentence is provable. The compactness property, ensuring models for arbitrary consistent theories (where every subset of size less than some cardinal is consistent), extends foundational results but generally fails in ZFC for infinitary logics. Seminal work established these notions through Hilbert-style deductive systems augmented with infinitary rules for conjunctions, disjunctions, and quantifiers.^[31] The prototypical example of a complete infinitary logic is L_{\omega,\omega}, the standard first-order logic, where Gödel's completeness theorem guarantees that every consistent theory has a model. This result relies on the finiteness of proofs and formulas, but it serves as the baseline for infinitary extensions. For L_{\omega_1,\omega}, which permits countable conjunctions and disjunctions, completeness holds under the axiom of choice (AC), as proved by Karp using a deductive system with infinitary axioms for quantifier exchange and distributivity. However, the compactness property requires large cardinal assumptions; for instance, partial compactness implies the existence of measurable cardinals, while full compactness for L_{\omega_1,\omega} is equivalent to the existence of an \omega_1-strongly compact cardinal.^[32] More generally, for L_{\kappa,\lambda} with strongly inaccessible cardinal \kappa, Vopěnka and Hájek established completeness within a Hilbert-type system, allowing proofs of infinitary sentences up to length less than \kappa. In contrast, when \kappa is singular, counterexamples exist showing that no such complete deductive system can be formulated, due to cofinality issues preventing the construction of maximal consistent sets. These failures highlight the sensitivity of infinitary logics to the regularity of index cardinals.^[33] The completeness of these logics has profound implications for proof theory, enabling the formalization of infinite deductions that capture model-theoretic properties like elementary equivalence in uncountable structures. In automated reasoning, complete infinitary systems facilitate algorithmic checks for consistency in infinite-domain problems, such as those in descriptive set theory, though computational limits arise beyond countable fragments.^[34]

Variants and Extensions

One prominent variant of infinitary logic extends the standard L_{\kappa,\lambda} framework by incorporating generalized quantifiers, which allow quantification over classes of sets rather than just existential or universal forms, enhancing expressive power for properties like cardinality or linear order in infinite structures.^[29] These extensions, such as L_{\kappa,\lambda}(Q) where Q denotes a generalized quantifier, preserve many model-theoretic properties like Łoś's theorem while enabling definitions of abstract elementary classes that capture stability-like behaviors beyond first-order logic.^[35] In parallel, infinitary logics often employ partial isomorphism systems in Ehrenfeucht-Fraïssé games, where back-and-forth relations involve partial embeddings of cardinality less than \kappa, providing a game-theoretic characterization of elementary equivalence for structures up to quantifier rank \lambda.^[1] Continuous logics represent another key extension, adapting infinitary frameworks to metric structures by valuing formulas in [0,1] with continuous connectives and quantifiers defined as suprema and infima, thus handling approximate satisfaction in non-discrete settings like Banach spaces.^[36] The infinitary variant, analogous to L_{\omega_1,\omega}, permits countable conjunctions and disjunctions of continuous formulas, allowing expression of analytic concepts such as the existence of a Schauder basis or non-reflexivity of operators, which finitary continuous logic cannot capture due to its finite syntactic restrictions.^[37] This logic supports an omitting types theorem for countable fragments via topological compactness, facilitating applications in model theory for separable metric spaces.^[38] Polyadic and cylindric algebras serve as algebraic counterparts to these infinitary logics, providing Boolean algebra-based semantics that model infinite substitutions and cylindrifications for higher-dimensional relations.^[39] In infinite-dimensional settings (dimension \alpha \geq \omega), quasi-polyadic equality algebras (QPEA_\alpha) and cylindric algebras (CA_\alpha) address representation problems through neat reducts and ultraproducts, solving infinitary versions of Tarski's cylindric algebra problems like non-finite axiomatizability of representable classes.^[40] These structures enable algebraic proofs of interpolation and amalgamation for infinitary theories, linking syntactic transformations to semantic embeddings in polyadic MV-algebras for infinite \alpha.^[40] Connections to higher-order logics arise through categorical interpretations of infinitary languages L_{\mu,\kappa,\lambda}, where formulas are modeled as functors in Heyting categories or topoi, bridging to type-theoretic semantics in systems like homotopy type theory (HoTT).^[41] Recent categorical work integrates infinitary model theory with HoTT's univalent foundations, using internal logics of (\infty,1)-categories to formalize generic models and completeness for infinitary fragments.^[41] In set theory, infinitary logics extend beyond strong compactness via characterizations of larger cardinals, such as measurable and supercompact ones, using compactness for omitting types in L^{\kappa,\kappa}.^[42] For instance, \kappa is \lambda-supercompact if L^{\kappa,\lambda} has the \lambda-omitting types property, while huge cardinals correspond to type omission in stronger fragments like L^{\kappa,\kappa} over extender models.^[42] These logics interact with forcing by preserving large cardinal properties under certain posets, as seen in preservations of extendible cardinals during iterated forcing extensions.^[43]

References

[1]
[PDF] A Primer on Infinitary Logic
These lectures are a brief survey of some elements of the model theory of the infinitary logics L∞,ω and Lω1,ω. It is intended to serve as an introduction to ...
[2]
Model theory for infinitary logic; logic with countable conjunctions ...
Aug 12, 2019 · Model theory for infinitary logic; logic with countable conjunctions and finite quantifiers. by: Keisler, H. Jerome. Publication date: 1971.
[3]
The sentential calculus with infinitely long expressions - EuDML
The sentential calculus with infinitely long expressions. D. Scott; Alfred Tarski · Colloquium Mathematicum (1958). Volume: 6, Issue: 1, page 165-170 ...
[4]
Karp Carol R.. Languages with expressions of infinite length ...
Aug 6, 2025 · Languages with expressions of infinite length. Studies in logic and the foundations of mathematics. North-Holland Publishing Company, Amsterdam ...
[5]
H. Jerome Keisler. Model theory for infinitary logic. Logic with ...
H. Jerome Keisler. Model theory for infinitary logic. Logic ... As you have access to this content, a full PDF is available via the 'Save PDF' action button.
[6]
[PDF] Infinitary logics and forcing
Jan 29, 2025 · Le livre de. Keisler [7] est notre référence sur ce sujet. Le premier résultat majeur que nous établissons dans cette th`ese est le Théor`eme d' ...
[7]
(PDF) “Mathematics is the Logic of the Infinite”: Zermelo's Project of ...
I also stress the fact that the second axiomatization of set theory provided by Zermelo in 1930 involved the use of extremal axioms of a very specific sort.
[8]
THE PREHISTORY OF INFINITARY LOGIC: 1885-1955
GREGORY H. MOORE. THE PREHISTORY OF INFINITARY LOGIC: 1885-1955. History is difficult ... because the connections that matter are usually numerous, often ...
[9]
[PDF] A. M. Turing Award Oral History Interview with Dana Stewart Scott ...
Nov 12, 2020 · Dana Scott: So 1932, October 11, 1932 is my birthdate. It's in ... Jumping back to logic, there's infinitary logic. That's another ...
[10]
Nagy, CBMS No. 19. Amer. Math. Soc, Providence, R. - Project Euclid
Feb 3, 2014 · The third basic result is the downward Löwenheim-Skolem-Tarski theorem that in a special case says that any infinite structure of a countable ...
[11]
[PDF] The Higher Infinite: Large Cardinals in Set Theory from Their ...
Dec 13, 2004 · This printing incorporates corrections of typographical and grammatical errors and cites a few advances. In the Chart of Cardinals there is now ...
[12]
To Settle Infinity Dispute, a New Law of Logic | Quanta Magazine
Nov 26, 2013 · “If forcing axioms are right, then the continuum hypothesis is false,” Koellner said. “And if the inner-model axiom is right, then the continuum ...Missing: infinitary | Show results with:infinitary
[13]
Infinitary Logic - Stanford Encyclopedia of Philosophy
Jan 23, 2000 · L(κ,λ) is the infinitary language obtained from L by permitting conjunctions and disjunctions of length < κ and quantifications [1] of length < λ.Definition and Basic Properties... · Finite-Quantifier Languages
[14]
[PDF] Lectures on Infinitary Model Theory
[22] H. J. Keisler, Model Theory of Infinitary Languages, North-Holland. Amsterdam, 1971. [23] H. J. Keisler and M. Morley, Elementary extensions of models ...
[15]
[PDF] Small Infinitary Epistemic Logics - Tai-Wei Hu
[19] Karp, C., (1964), Languages with Expressions of Infinite Lengths, North-Holland. Amster- dam. [20] Kaneko, M., and T. Nagashima, (1996), Game Logic and its ...
[16]
[PDF] Model Theory and Differential Algebra - Berkeley Math
Nov 3, 2000 · Definition 1 A signature σ is a quadruple (C,F,R,a) where C, F, and. R are disjoint sets (called the constant symbols, function symbols, and.
[17]
[PDF] HW3, Math 506, Fall 2016, Due 9/14
Sep 7, 2016 · (So Downward Löwenheim-Skolem fails). 1 A primer on infinitary logic. Given a signature τ we now define the infinitary language 多∞ω associated ...
[18]
[PDF] Model Theory - Berkeley Math
For τ a signature we define the free term τ-structure 디. T(τ) to be the τ ... (in the formal language L(τ)) that (N,0,1,+,·,<) is a discretely ordered ...
[19]
Languages With Expressions Of Infinite Length : Carol R. Karp
Nov 22, 2022 · Languages With Expressions Of Infinite Length. by: Carol R. Karp. Publication date: 1964. Publisher: North-Holland Publishing Company.<|control11|><|separator|>
[20]
The Higher Infinite: Large Cardinals in Set Theory ... - SpringerLink
The higher in?nite refers to the lofty reaches of the in?nite cardinalities of set t- ory as charted out by large cardinal hypotheses.Missing: compactness | Show results with:compactness
[21]
Chapter X Game Quantification 1. Infinite Strings of Quantifiers
that a relation is well-founded if and only if it has no infinite descending chains. ... that both of these logics can express the notion of well-foundedness.
[22]
[PDF] Ehrenfeucht-Mostowski models in Abstract Elementary Classes
It is essential for the foundations of simplicity theory and for the construction of indiscernibles in infinitary logic. We quote the first order version here; ...Missing: limitations | Show results with:limitations
[23]
Can Foundation be captured in $\mathcal L(\omega_1,\omega)
Jun 9, 2023 · Your Foundation axiom does not assert that there is no infinite descending sequence, but rather merely rules out sets at infinite ...How do these two principles of Foundation written in Lω1,ω compare?Does adding definability axiom expressed in infinitary language to ...More results from mathoverflow.net<|separator|>
[24]
[PDF] The complex numbers and complex exponentiation Why Infinitary ...
Abstract. Algebraically closed fields of a given characteristic are cat- egorical in each uncountable cardinality; up to isomorphism there is.
[25]
m-categoricity of theory of algebraically closed fields of fixed ...
Jan 21, 2013 · The basic idea is that an algebraically closed field is determined up to isomorphism by its characteristic and its transcendence degree. Now ...omega$- categoricity and algebraic closure - Math Stack ExchangeFor two algebraically closed fields, one is isomorphic to a subfield of ...More results from math.stackexchange.com
[26]
[PDF] Infinitary axiomatizability of slender and cotorsion-free groups
The classes of slender and cotorsion-free abelian groups are axiomatizable in the infinitary logics L∞ω1 and L∞ω respectively. The Baer-Specker group Zω is not ...Missing: rank | Show results with:rank
[27]
https://www.sciencedirect.com/science/article/pii/S0168007208001012
[28]
A standard model of Peano arithmetic with no conservative ...
A standard model of Peano arithmetic with no conservative elementary extension ... Model Theory for Infinitary Logic. North-Holland, Amsterdam (1971). Google ...
[29]
[PDF] Categoricity John T. Baldwin, Department of Mathematics, Statistics ...
Modern model theory began with Morley's [Mor65a] categoricity theorem: A first order theory is categorical in one uncountable cardinal κ (has a unique model.
[30]
[PDF] Generalized Quantifiers, Infinitary Logics, and Abstract Elementary ...
Dec 14, 2007 · In this paper we discuss extensions of first order logic both to infinitary logics and by adding some generalized quantifiers.<|separator|>
[31]
Chapter XV Topological Model Theory - Project Euclid
In Section 5.3 we present a complete axiomatization of the theory of the topological field of complex numbers. And finally, in Section 5.4, we show that all ...
[32]
The completeness theorem for infinitary logic
Mar 12, 2014 · It will be proven that a set of sentences of infinitary logic is satisfiable iff it is proof theoretically consistent. Since this theorem is ...
[33]
Infinitary first-order categorical logic - ScienceDirect.com
We present a unified categorical treatment of completeness theorems for several classical and intuitionistic infinitary logics with a proposed ...Missing: limitations | Show results with:limitations
[34]
How badly does compactness fail in $\mathcal{L}_{\omega_1\omega}
May 16, 2012 · I would like to get a better idea of how badly compactness fails in Lω1ω. Let Γ be an arbitrary set of sentences from Lω1ω. Let the ...Missing: example distinct
[35]
Infinitary logic at singular cardinals - MathOverflow
Feb 17, 2025 · Here L∞,λ refers to infinitary logic that allows conjunctions and disjunctions of any (set-sized) length, and allows quantification over sequences of variables ...Measuring subsets of a cardinal definable in infinitary logicSpecial version of $\Delta$-system Lemma for singular cardinalsMore results from mathoverflow.netMissing: counterexamples | Show results with:counterexamples
[36]
Completeness by Forcing | Journal of Logic and Computation
The completeness of the infinitary language ℒω1,ω was proved by Carol Karp in 1964.We express and prove the completeness of infinitary first-order logics in ...
[37]
Generalized quantifiers and pebble games on finite structures
In this paper, we study generalized quantifiers in the realm of finite structures and combine them with the infinitary logic L∞ωω to obtain the logics L∞ωω(Q), ...
[38]
[PDF] Model theory for metric structures
In the [0, 1]-valued continuous setting, connectives are continuous functions on [0, 1] and quantifiers are sup and inf. The analogy between this continuous ...
[39]
Omitting types for infinitary [0,1]-valued logic - ScienceDirect.com
Using topological methods, we prove an omitting types theorem for countable fragments of our infinitary logic. ... first-order continuous logic, which Ben ...
[40]
[PDF] arXiv:1512.00879v2 [math.LO] 9 Aug 2017
Aug 9, 2017 · While the compactness theorem fails for Lω1,ω, it is nevertheless true that many results from first-order model theory can be translated in some ...<|control11|><|separator|>
[41]
POLYADIC BOOLEAN ALGEBRAS - PNAS
A polyadic logic, to begin with, is defined as a pair. (A, I), where A is a polyadic algebra and I is a polyadic ideal in A. The motivation for this definition ...Missing: infinitary | Show results with:infinitary
[42]
[PDF] Cylindric and polyadic algebras, new perspectives - arXiv
Aug 31, 2013 · We prove the conclusion of theorem 2.7, for cylindric algebras solving the infinite dimensional version of the famous 2.12 problem in algebraic ...
[43]
[PDF] Categories for infinitary logic - DiVA portal
... axiom of choice, as it depends on a choice of representatives θ and η. Thus ... “Infinitary Logic”. In: The Stanford Encyclopedia of Philosophy. Ed. by ...
[44]
[PDF] model theoretic characterizations of large cardinals
Apr 3, 2019 · Jerome Keisler, Model theory for infinitary logic, Studies in Logic and the Foundations of Mathemat- ics, vol. 62, North-Holland Publishing ...<|control11|><|separator|>
[45]
[PDF] LARGE CARDINALS WITH FORCING
This chapter describes, following the historical development, the investigation of large cardinal hypotheses using the method of forcing.