Infinitary Logic

In the familiar world of first-order logic, our sentences are always finite constructions. While powerful, this limitation means that certain fundamental mathematical ideas, like the very concept of "finiteness," elude its grasp, creating a significant gap in its expressive capabilities. This naturally leads to a compelling question: what if our logic could build sentences from infinitely many pieces? Answering this question opens the door to infinitary logic, a realm where infinite conjunctions and disjunctions are permitted, granting us unprecedented descriptive power.

This article embarks on a journey into this powerful domain. In the first section, "Principles and Mechanisms," we will explore the fundamental tools of infinitary logic, discovering how it can express concepts previously out of reach, but at the cost of treasured properties like the Compactness Theorem. Following this, the "Applications and Interdisciplinary Connections" section will reveal how these seemingly abstract tools provide a unique lens on mathematical structures and forge a surprising and profound bridge to the theory of computation.

In our journey through the world of logic, we often treat our tools—the connectives like AND ($\wedge$), OR ($\vee$), and quantifiers like FOR ALL ($\forall$)—as if they are building blocks. In the familiar world of first-order logic, we are only ever allowed to use a finite number of these blocks at a time. We can say "this AND that," or even a very long but ultimately finite list of conjunctions. We can say "for all $x_1$, and for all $x_2$, ..., and for all $x_{100}$." But we can never say "for all infinitely many variables" at once, nor can we construct a single sentence that is an infinite chain of ANDs or ORs.

This is a powerful and surprisingly effective limitation. Yet, in many areas of science and mathematics, the infinite is a central concept. We talk of infinite series, infinite-dimensional spaces, and sets with infinitely many members. It's natural to wonder: what if our logic could do that, too? What if we could build sentences out of infinitely many pieces?

This is not just an idle fantasy. Consider a simple, fundamental concept: ​​finiteness​​. Can you write a sentence in first-order logic that is true in all finite universes, and false in all infinite ones? The surprising answer is no. You can write a sentence $\psi_n$ that says "there are at least $n$ things" for any given $n$. For instance, $\psi_3 \equiv \exists x_1 \exists x_2 \exists x_3 (x_1 \neq x_2 \wedge x_1 \neq x_3 \wedge x_2 \neq x_3)$ You can even write a sentence $\chi_m$ that says "there are exactly $m$ things." But you cannot write a single sentence that means "the universe is finite," period. The concept seems to slip through the grasp of first-order logic.

Let's grant ourselves a new power. Let's invent a logic, which we'll call ​​$L_{\omega_1, \omega}$​​, that allows us to string together a countably infinite number of propositions with ORs. The notation $\omega_1$ refers to the first uncountable number, and $\omega$ is the first infinite (countable) number. So, $L_{\omega_1, \omega}$ lets us take disjunctions ($\vee$) of any countable set of formulas, while keeping our quantifier blocks ($\forall, \exists$) finite, just like before.

With this new tool, expressing finiteness becomes easy! We can say "The universe has exactly 1 element, OR it has exactly 2 elements, OR it has exactly 3 elements, OR..." and just let this go on forever. Formally, we write this as a single, magnificent, infinite sentence:

$\varphi_{\mathrm{fin}} := \bigvee_{m=1}^{\infty} \chi_m$

where each $\chi_m$ is the first-order sentence for "there are exactly $m$ elements." Any structure that satisfies $\varphi_{\mathrm{fin}}$ must satisfy one of its disjuncts, $\chi_m$, for some specific $m$. This forces the structure to have a finite size, $m$. And any finite structure of size $m$ will certainly satisfy $\chi_m$, and therefore the whole disjunction $\varphi_{\mathrm{fin}}$. We've done it! We've captured the essence of finiteness in a single sentence.

This power is not just for esoteric mathematics. Imagine a huge control panel with a countably infinite row of switches, $p_0, p_1, p_2, \ldots$. We can think of a "true" proposition $p_i$ as a switch that is flipped ON. Can we write a single logical statement that is true if and only if only a finite number of switches are ON? In ordinary propositional logic, no. But with infinitary logic, it's straightforward. We can say: "Either the set of ON switches is $\{p_0\}$, OR it's $\{p_1\}$, OR it's $\{p_0, p_1\}$, OR..." listing every possible finite set of switches. This is another countably infinite disjunction, and it perfectly captures the property of having finitely many switches on.

This newfound expressive power is thrilling. We can now describe concepts that were previously elusive. But as in all great stories, power comes at a price. In logic, one of the most beautiful and profound properties we lose is called ​​compactness​​.

The ​​Compactness Theorem​​ for first-order logic is a cornerstone of modern logic. It states that if you have an infinite set of sentences (a theory), and if every finite subset of those sentences can be satisfied, then the entire infinite set can be satisfied simultaneously. Think of it as a principle of peaceful coexistence. If any small group of your requirements can be met, then all of your requirements, no matter how numerous, can be met all at once. It’s an incredibly non-obvious and useful fact. It is the secret engine behind countless results in mathematics, from algebra to topology.

But in $L_{\omega_1, \omega}$, this beautiful harmony shatters.

Let's build a theory. We'll take our new sentence, $\varphi_{\mathrm{fin}}$, which insists that the universe must be finite. Then, let's add to it all the first-order sentences $\psi_n$ that say "there are at least $n$ elements," for every single natural number $n=1, 2, 3, \ldots$. Our theory is the infinite set of sentences:

$T = \{\varphi_{\mathrm{fin}}\} \cup \{\psi_1, \psi_2, \psi_3, \ldots\}$

Now, let's test the Compactness Theorem. First, is every finite subset of $T$ satisfiable? Let's pick one, say $\Gamma_0$. It will contain $\varphi_{\mathrm{fin}}$ and a finite number of the other sentences, perhaps $\{\psi_5, \psi_{100}, \psi_{1000}\}$. The strongest of these is $\psi_{1000}$, which demands at least 1000 elements. Can we find a model for $\Gamma_0$? Of course! A universe with exactly 1000 elements will do just fine. It's finite, so it satisfies $\varphi_{\mathrm{fin}}$, and it has at least 1000 elements, so it satisfies $\psi_{1000}$ (and $\psi_5$ and $\psi_{100}$). Every finite subset of $T$ is happy; it can always find a model.

Now for the big question: is the entire theory $T$ satisfiable? To satisfy all of $T$, a universe would have to satisfy $\varphi_{\mathrm{fin}}$, meaning it must be finite. But it must also satisfy $\psi_n$ for every $n$. It must have at least 1 element, at least 2, at least 3, ... at least a billion, and so on, for all natural numbers. This forces the universe to be infinite!

So, our theory $T$ demands that its models be both finite and infinite. This is a flat-out contradiction. The theory $T$ has no model; it is unsatisfiable.

Here we have it: a set of sentences where every finite subset has a model, but the whole set does not. This is a spectacular failure of the Compactness Theorem. Our leap into the infinite has come at the cost of one of logic's most treasured properties. Similar paradoxes emerge in other powerful systems, like second-order logic, which also allows quantification over properties and relations, giving it enough strength to define finiteness and, as a result, lose compactness.

Why does this happen? Why is first-order logic so beautifully compact, while these stronger logics are not? The answer lies in the very nature of what we call a "proof."

In first-order logic, a proof is a finite thing. It's a list of statements, each one an axiom or derived from previous statements by a rule. Even if you are proving something from an infinite list of assumptions, any single proof you write down will only ever refer to a finite number of them. If you manage to prove a contradiction (like $p \wedge \neg p$) from a giant, infinite theory $\Gamma$, you must have done so using only a finite piece of it, say $\Gamma_0 \subseteq \Gamma$. This is called the ​​finite character​​ of the proof system.

This syntactic property (about proofs) is directly linked to the semantic property of compactness (about truth and models). The link is forged by another famous result, Gödel's Completeness Theorem, which says that a theory is unsatisfiable if and only if you can prove a contradiction from it. If a theory $\Gamma$ is unsatisfiable, you can prove a contradiction. Because the proof is finite, it only used a finite subset $\Gamma_0$. This means that finite subset $\Gamma_0$ is itself sufficient to cause a contradiction, and is therefore unsatisfiable. This is exactly the contrapositive of the Compactness Theorem!. So, the compactness of first-order logic is, in a deep sense, a consequence of the finitary nature of its proofs.

Now, what happens when we step into logics that can "feel" the infinite? Think of a new kind of proof rule, an ​​infinitary rule​​. For example, the ​​$\omega$-rule​​: from the infinite list of premises $\varphi(0), \varphi(1), \varphi(2), \ldots$, you are allowed to infer the conclusion $\forall x\, \varphi(x)$.

Let's see how this breaks everything. Consider the set of sentences: $\Gamma = \{\varphi(0), \varphi(1), \varphi(2), \ldots\} \cup \{\neg \forall x\, \varphi(x)\}$ Is this set consistent? Using the $\omega$-rule, we can take all the infinitely many premises $\varphi(0), \varphi(1), \ldots$ and derive $\forall x\, \varphi(x)$. But we also have $\neg \forall x\, \varphi(x)$ as a premise! This is a direct contradiction, so the set $\Gamma$ is inconsistent.

But what about its finite subsets? Take any finite subset of $\Gamma$. It will contain $\neg \forall x\, \varphi(x)$ and only a finite number of the others, say $\{\varphi(0), \varphi(5), \varphi(42)\}$. From this finite set, you cannot use the $\omega$-rule to conclude $\forall x\, \varphi(x)$. A finite collection of instances is not enough. So every finite subset is perfectly consistent!

This is exactly the same pattern we saw with the failure of compactness. The infinitary nature of the $\omega$-rule breaks the finite character of proofs. Logics like $L_{\omega_1, \omega}$ and second-order logic behave as if they have this kind of infinitary power baked into their semantics. They can "check" an infinite number of conditions at once, a feat impossible for finitary proofs. This is why they cannot have a finitary, sound, and complete proof system, and it is the deep reason why they are not compact.

We have seen that first-order logic possesses two remarkable properties: the ​​Compactness Theorem​​ and another called the ​​Downward Löwenheim-Skolem Theorem​​ (which, put simply, says that if a theory has an infinite model of any size, it must also have a small, countable one). We've also seen that attempts to increase expressive power, for example by moving to $L_{\omega_1, \omega}$ or second-order logic, cause us to lose one or both of these properties.

For a long time, this seemed like a collection of interesting but perhaps disconnected facts. Was it just a coincidence? The answer, delivered by the Swedish logician Per Lindström in the 1960s, is a resounding "no."

​​Lindström's Theorem​​ is one of the most profound results in all of logic. It provides a complete characterization of first-order logic, revealing the deep unity behind its properties. The theorem states:

First-order logic is the ​​strongest possible​​ logic that has both the Compactness property and the Downward Löwenheim-Skolem property.

This is a stunning revelation. These properties are not just quirky features of first-order logic; they are its defining signature. Any logic that you can dream up that tries to be more expressive—that can define a class of structures that first-order logic cannot—is forced to sacrifice either compactness or Löwenheim-Skolem. It’s as if there is a conservation law in the world of logic: you can have maximum expressiveness, or you can have these nice model-theoretic properties, but you cannot have it all.

The proof of Lindström's theorem is a beautiful piece of reasoning that itself uses the properties of compactness and Löwenheim-Skolem to fence in any potential competitor. The argument, in essence, is a proof by contradiction. Suppose there were a logic $\mathcal{L}$ that was stronger than first-order logic but still had these two properties. Because it's stronger, it must be able to tell apart two structures, $A$ and $B$, that first-order logic considers indistinguishable. The proof then cleverly constructs a new, larger, hybrid structure that contains disjoint copies of both $A$ and $B$. Using the assumed compactness of $\mathcal{L}$, one shows this hybrid world can exist. Then, using the Löwenheim-Skolem property, one shrinks this world down to a countable size. In this smaller, simpler world, the two structures that $\mathcal{L}$ could supposedly tell apart are now so simple that they must be isomorphic (identical in structure). But the fundamental principle of any logic is that it cannot distinguish between isomorphic structures! This contradiction shows that our initial assumption—that a logic like $\mathcal{L}$ could exist—must be false.

Lindström's theorem gives us a god's-eye view of the landscape of logics. It shows us that first-order logic is not just one system among many. It occupies a unique and privileged position, perfectly balanced between expressive power and well-behavedness. The journey into the infinite, while tempting and powerful, forces us to leave this elegant and compact fortress behind.

Now that we have grappled with the principles of infinitary logic, you might be asking yourself, "What is all this for?" It is a fair question. Why build these elaborate logical systems that allow for infinite sentences? Are they merely a playground for logicians, a cabinet of curiosities? The answer, you will be delighted to find, is a resounding no. Infinitary logic is not just a curiosity; it is a powerful lens that reveals a deeper, more textured reality about the nature of mathematical structures, and it builds an astonishingly beautiful bridge to the very heart of what it means to compute. Let us embark on a journey to see how.

One of the great triumphs—and, as we will see, limitations—of standard first-order logic is the Löwenheim-Skolem theorem. In essence, it tells us that first-order logic is rather poor at pinning down the size of infinite structures. If a first-order theory has one infinite model, it has infinite models of all sorts of different infinite sizes. For instance, the complete first-order theory of the natural numbers, $(\mathbb{N}, +, \cdot)$, not only has the familiar countable model we all know and love, but it also has strange, "non-standard" models that are uncountably large! This means that no sentence of first-order logic can ever serve as a unique and exclusive description of the natural numbers. First-order logic is a powerful tool, but its vision is a bit blurry when it comes to distinguishing between different infinities.

This is where infinitary logic, specifically $L_{\omega_1, \omega}$, steps onto the stage and performs a spectacular feat. For any countable structure, we can write a single sentence in $L_{\omega_1, \omega}$ that serves as its perfect, unique fingerprint. This sentence is called a ​​Scott sentence​​. Any other countable structure that satisfies this sentence must be, without exception, isomorphic to the original. It's as if we've finally found the right language to write the complete DNA of a structure.

How is this possible? The magic lies in the infinite conjunctions and disjunctions. A Scott sentence, in a sense, describes the structure from the "inside out." It enumerates every possible "local environment" that a finite collection of elements can find itself in, and it does this for tuples of all finite lengths. By taking a gigantic, countably infinite disjunction over all these environmental descriptions, the Scott sentence effectively provides a complete catalog of the structure's internal patterns. Any other structure that claims to be a model must possess an identical catalog, which turns out to be enough to force it to be an exact copy. This ability to uniquely characterize countable structures is a superpower that first-order logic can only dream of.

Of course, in physics and in logic, there is no free lunch. This immense descriptive power must come at a cost, and it is a steep one: we must abandon one of the most elegant and useful tools in the logician's arsenal, the ​​Compactness Theorem​​.

The Compactness Theorem for first-order logic is a thing of beauty. It states that if you have an infinite collection of axioms, and every finite handful of those axioms can be satisfied by some model, then the entire infinite collection of axioms can be satisfied simultaneously. It's an "optimist's theorem"—if all the local pieces fit, a global solution exists.

This theorem fails dramatically in $L_{\omega_1, \omega}$. And the reason for its failure is precisely the newfound power we just celebrated! Consider this delightfully simple set of sentences:

1. An infinite list of first-order sentences: "There is at least 1 element," "There are at least 2 elements," "There are at least 3 elements," and so on for all natural numbers. Together, these sentences say, "The structure is infinite."
2. A single $L_{\omega_1, \omega}$ sentence: "There is at most 1 element, OR there are at most 2 elements, OR there are at most 3 elements,..." This is a countable disjunction, $\bigvee_{n \in \omega} \text{there are at most } n \text{ elements}$, which simply says, "The structure is finite."

Now, pick any finite handful of sentences from this combined collection. It will contain a finite number of sentences from the first list (say, up to "at least $N$ elements") and the single sentence from the second list. A model with exactly $N$ elements will satisfy this handful perfectly. So, every finite subset has a model. By the Compactness Theorem, the whole collection should have a model. But it can't! A structure cannot be both infinite and finite at the same time. The infinitary disjunction allows us to express a property ("finiteness") that is fundamentally "un-compact," and the entire logical edifice of compactness comes tumbling down.

So far, our story has been one of trade-offs within logic itself. But the most profound application of infinitary logic takes us beyond its own borders, into the world of ​​computability theory​​. Here, infinitary logic becomes a tool not just for describing structures, but for measuring their intrinsic computational complexity.

Let's start with a simple question: what makes one structure more "complex" than another? Consider the rational numbers $(\mathbb{Q}, )$ and the integers $(\mathbb{Z}, )$. The rationals are dense and homogeneous; from a local perspective, every point looks the same. The integers have a discrete, rigid structure. Intuitively, the integers are more complex. Infinitary logic gives us a way to make this intuition precise through the notion of ​​Scott rank​​. The Scott rank of a structure is the transfinite "number" of steps in a back-and-forth game needed to tell every element apart from every other element that isn't its perfect twin (i.e., in the same automorphism orbit). A low, finite Scott rank, such as 2 for $(\mathbb{Q}, )$, signifies simplicity. A higher Scott rank signifies greater complexity.

This idea explodes into a field of its own when we consider computable structures—structures that can, in principle, be fully described and manipulated by a computer program. And here we meet a true marvel of modern logic: the ​​Harrison linear ordering​​. This is a structure that is, by its very definition, computable. You can write a program that decides the order between any two of its elements. And yet, it is one of the most monstrously complex countable structures known to exist.

How complex? Its Scott rank is $\omega_1^{CK} + 1$.

To appreciate how staggering this is, we must understand the symbol $\omega_1^{CK}$. This is the ​​Church-Kleene ordinal​​, the first "number" (ordinal) that a computer cannot reach. It is the supremum of all the "computable" ordinals. It represents the absolute limit of algorithmic processing. The fact that the Scott rank of the computable Harrison ordering is not just large, but that it actually surpasses this limit of computability, is a mind-bending revelation. It tells us that to write down the complete logical "fingerprint" of this computable object, we need to employ a descriptive process that is itself non-computable. The very act of distinguishing between certain elements in this structure requires a "non-computable limit step" in our back-and-forth analysis.

This is the bridge: infinitary logic provides a transfinite yardstick that measures the complexity of computable objects, and in doing so, reveals a deep and intricate layering of complexity that culminates at the boundary of what is even possible to compute. The effectiveness of our logical tools maps directly to the computational complexity of the objects we study. For instance, if we can prove two computable structures are isomorphic using a back-and-forth system whose properties are "computable with an oracle for the $\alpha$-th Turing jump," then the isomorphism itself will be computable with that very same oracle. The link is direct and quantitative.

Beyond these grand connections, infinitary logic also enriches the day-to-day toolkit of the working logician. Tools analogous to those in first-order logic, like the ​​Omitting Types Theorem​​, are generalized to the infinitary setting. Such theorems are powerful construction techniques that allow logicians to build models with highly specific properties—for example, a model of a theory that contains no elements of a certain undesirable "type." This allows for a much finer-grained analysis of what is possible within a logical theory. Furthermore, the back-and-forth method itself becomes a powerful constructive tool. For countable structures, the existence of a back-and-forth system is not just an abstract guarantee of isomorphism; it is a concrete recipe for building that isomorphism, step by painstaking step, a process that culminates in the union of all finite approximations at a "limit stage".

In the end, infinitary logic is far more than an abstract extension of familiar logic. It is a testament to the fact that when we push our mathematical languages to new limits, they don't just become more powerful; they become more insightful. They reveal the hidden costs of that power, like the loss of compactness, but they also unveil unexpected and breathtaking connections between disparate fields—linking the abstract world of mathematical structures to the concrete realities of computation. It is in these connections that we see the true unity and beauty of the logical enterprise.