Beth Definability Theorem

In the formal worlds of logic and mathematics, how do we give meaning to a new concept? We can do so syntactically, through the mechanical rules of proof, or semantically, through the lens of truth and interpretation. These two worlds are beautifully bridged by theorems of soundness and completeness, allowing us to equate what is provable with what is true. This article delves into a fundamental question at the heart of formal expression: the nature of definition itself. We often define concepts explicitly, providing a direct formulaic translation, but we can also define them implicitly, by stating properties so restrictive that they pin down the concept's meaning uniquely in any context. This raises a crucial knowledge gap: if a concept is uniquely determined by a set of axioms, must there also exist a single, explicit formula that defines it?

This article explores the definitive "yes" to this question, as provided by the Beth Definability Theorem. In the first chapter, "Principles and Mechanisms," we will unpack the theorem's meaning, contrasting implicit and explicit definitions, and revealing the elegant proof mechanism that relies on the Craig Interpolation Theorem. Following this, the chapter on "Applications and Interdisciplinary Connections" will showcase the theorem's profound impact, connecting it to the absolute limits of logic discovered by Gödel and Tarski, its creative power in constructing mathematical universes, and its role in characterizing the very nature of first-order logic itself.

Imagine you are playing a game of chess. You have pieces and a set of rules. A bishop moves diagonally, a pawn moves forward, and so on. You don't need to know anything about medieval history or the role of bishops to play the game. You just need to follow the rules, moving symbols around on a board. This is the world of ​​syntax​​. In logic, this is the world of formal proofs. We have a set of axioms (starting positions) and inference rules (legal moves), and a proof is simply a sequence of formulas where each step is justified by the rules. When we can produce a formula $\varphi$ starting from a set of premises $\Gamma$ by following these rules, we write $\Gamma \vdash \varphi$, which reads "$\Gamma$ proves $\varphi$". It’s a purely mechanical process.

But, of course, that's not the whole story. The symbols mean something. The chess piece we call a "king" represents a king, and the goal of the game, checkmate, represents the capture of that king. This is the world of ​​semantics​​—the world of truth and meaning. In logic, we ask whether a statement is true in some particular context, or "model." A model is a universe, a self-contained reality where our symbols have concrete interpretations. A statement is semantically entailed by a set of premises, written $\Gamma \models \varphi$, if in every possible universe where all the statements in $\Gamma$ are true, the statement $\varphi$ is also forced to be true. This isn't about following rules; it's about a necessary consequence in the realm of meaning. The definition of truth in a model, a beautiful recursive construction, was laid out by the great logician Alfred Tarski.

For a long time, a central question in logic was: Do these two worlds—the syntactic game of proofs and the semantic universe of truth—perfectly align? The spectacular answer is yes, at least for first-order logic. This is guaranteed by two profound meta-theorems: ​​soundness​​ ($\Gamma \vdash \varphi$ implies $\Gamma \models \varphi$), which tells us our proof system doesn't produce lies, and ​​completeness​​ ($\Gamma \models \varphi$ implies $\Gamma \vdash \varphi$), which tells us our proof system is powerful enough to discover every truth that follows from our premises. This beautiful correspondence means we can shuttle back and forth between the two worlds. We can take a question about truth—a semantic question—and turn it into a question about provability—a syntactic one, and vice versa. This equivalence is the stage upon which our story unfolds.

How do we introduce a new idea into our language? Let's say we have a language for arithmetic with symbols for 'zero', 'add', 'multiply', and 'less than' ($\lt$). Now, suppose we want to introduce a new symbol, '$\le$', for "less than or equal to."

The most straightforward way is an ​​explicit definition​​. We simply declare that $x \le y$ is a shorthand for the formula $x \lt y \lor x = y$. We have provided a direct translation, a formula in the old language that is equivalent to our new symbol. The new symbol is just an abbreviation. Formally, we say a new relation symbol $R$ is explicitly defined by a theory $T$ if there is a formula $\theta(\bar{x})$ in the old language such that the theory proves the equivalence $T \models \forall \bar{x}\,(R(\bar{x}) \leftrightarrow \theta(\bar{x}))$.

But there is another, more subtle way. Instead of giving a direct definition, we could just state some fundamental properties of our new concept. For the concept of a "group inverse" in algebra, for instance, we don't write down a giant formula for it. Instead, we write an axiom: $\forall x \, \exists y \, (x \cdot y = e)$, where $e$ is the identity element. This axiom implicitly characterizes the inverse. We say a concept is ​​implicitly definable​​ if the set of axioms we write down about it are so restrictive that they completely pin down its meaning. In any universe (model) that satisfies our axioms, the interpretation of the new concept is uniquely determined by the interpretation of the old concepts. If you and I build two different models of the axioms, but our models agree on all the old concepts, we must find that we have, without coordinating, created the exact same interpretation for the new concept.

This leads to a deep and beautiful question. If we succeed in implicitly defining a concept—if our axioms are strong enough to uniquely fix its meaning in every possible context—does that guarantee that an explicit definition must also exist? Is it always possible to "solve" our axioms for the new concept and write it down as a formula in the old language?

The answer is a resounding "yes," and this is the content of the ​​Beth Definability Theorem​​. It states, quite simply:

​​In first-order logic, if a concept is implicitly definable, then it is explicitly definable.​​

This is a remarkable result about the nature of formal expression. It tells us that in the world of first-order logic, there are no "ghosts" in the machine. There are no concepts that are perfectly determined by a set of rules, yet are somehow ineffable and impossible to write down as a single formula. If you can constrain a concept's meaning completely, you can spell that meaning out. The two notions of definability, one semantic (implicit) and one syntactic (explicit), collapse into one. But how on earth could one prove such a thing? The path is not direct; it is a beautiful detour through a seemingly unrelated idea.

The key to unlocking Beth's theorem is a result of stunning elegance called the ​​Craig Interpolation Theorem​​. Suppose you have two statements, $A$ and $B$, and you know that whenever $A$ is true, $B$ must also be true ($A \models B$). The interpolation theorem says that there must exist a "middle-man" statement, an ​​interpolant​​ $I$, that forms a logical bridge: $A \models I$ and $I \models B$. But here is the magical part: the interpolant $I$ can only use the language—the symbols and vocabulary—that $A$ and $B$ have in common.

Imagine two experts, one speaking only about physics ($A$) and the other only about biology ($B$), but they share the common language of mathematics. If a complex physical principle $A$ always implies a complex biological outcome $B$, Craig's theorem guarantees there must be a purely mathematical statement $I$ that explains the connection. The physical statement implies the mathematical one, and the mathematical one implies the biological one.

So, how does this help us prove Beth's theorem? The proof is a masterpiece of logical judo.

1. Suppose our new symbol $R$ is implicitly defined by a theory $T$ in a language $\mathcal{L} = \mathcal{L}_0 \cup \{R\}$, where $\mathcal{L}_0$ is our old language.

2. Now, we play a game. We create a perfect "clone" of $R$, let's call it $R'$, and a corresponding clone of our theory, $T'$, where every mention of $R$ is replaced by $R'$.

3. What does the implicit definition of $R$ tell us? It says that in any model where both theory $T$ and its clone $T'$ are true, the interpretations of $R$ and its clone $R'$ must be identical. Why? Because they are both expansions of the same underlying $\mathcal{L}_0$ structure, and the implicit definition demands a unique interpretation. This gives us a powerful entailment: $T \text{ and } T' \models \forall \bar{x}\,(R(\bar{x}) \leftrightarrow R'(\bar{x}))$

4. We have our setup for Craig's theorem! The entailment can be rearranged into an implication between a formula using only $\mathcal{L}_0 \cup \{R\}$ and a formula using only $\mathcal{L}_0 \cup \{R'\}$. The language they have in common is just the old language, $\mathcal{L}_0$.

5. We apply Craig's theorem. It tells us there must exist an interpolant formula, let's call it $\theta(\bar{x})$, written only in the shared language $\mathcal{L}_0$. This interpolant acts as the bridge: the statement about $R$ implies $\theta(\bar{x})$, and $\theta(\bar{x})$ implies the statement about $R'$.

6. This interpolant $\theta(\bar{x})$ is our explicit definition! It's a formula in the old language $\mathcal{L}_0$ that is provably equivalent to $R(\bar{x})$. The magic of the interpolation theorem is that by forcing the bridge formula to be in the shared language, it distills the very essence of what $R$ means, "eliminating" the new symbol and expressing it in terms of the old.

This interplay between definability and interpolation leads to some astonishing consequences. Consider an extreme case of Craig's theorem. Suppose we have a statement $A$ written in a language $L_A$ (say, about chemistry) and a statement $B$ written in a completely disjoint language $L_B$ (say, about economics). The only symbol they share is the logical symbol for equality, $=$. Now, suppose we discover that $A \models B$. What could the interpolant possibly be?

It can't talk about chemicals or markets. It can only talk about the one thing they have in common: equality. A sentence using only equality can only talk about the size of the universe! It can say things like "There are at least 5 elements," or "There are at most 5 elements." For the chemical statement $A$ to imply the economic statement $B$, they must be linked by some hidden constraint on the cardinality of the worlds in which they can be true. For example, perhaps theory $A$ is only true in infinite universes, and theory $B$ happens to be true in all infinite universes. The interpolant would then be a sentence of pure equality that asserts the universe is infinite. This is a profound insight into the hidden structure of logical consequence.

Beth's theorem reveals the remarkable coherence of first-order logic. It assures us that what can be implicitly fixed can be explicitly stated. Yet, this power has limits. Tarski's Undefinability Theorem shows that some concepts, like the notion of "truth" itself for a sufficiently rich language like arithmetic, are so powerful that they cannot be defined within that language, neither explicitly nor implicitly. Logic, therefore, presents us with a fascinating landscape: a world where implicit meaning beautifully resolves into explicit form, but which is bounded by horizons of inexpressibility, beyond which the language cannot go to describe itself.

After our journey through the mechanics of the Beth Definability Theorem, you might be left with a tantalizing question: So what? What good is knowing that implicit definability is the same as explicit definability? It might seem like a technical point, a fine-tuning of a logician's dictionary. But nothing could be further from the truth. The Beth theorem is not an endpoint; it is a gateway. It marks a crucial signpost on the map of mathematical thought, helping us navigate the vast and wild terrain of what can be known, what can be said, and what can be built. In this chapter, we will embark on an expedition into this territory, exploring the profound consequences of definability in the worlds of computation, the grand architecture of mathematics, and the very nature of logic itself.

Our first stop is a place of humbling limits. The Beth theorem gives us a wonderful, positive guarantee: if a concept is uniquely pinned down by our axioms, we can write a formula for it. But what if a concept cannot be pinned down by a single formula? The most famous example of such a phenomenon is the notion of "truth" itself.

Imagine you have the language of arithmetic—with numbers, addition, and multiplication. You can write down statements, like "$2+2=4$" (which is true) or "$1=0$" (which is false). You can even assign a unique number, a Gödel number, to every possible statement. Now, you ask a simple question: Can I write a single formula in the language of arithmetic, let's call it $\text{True}(x)$, that can look at the Gödel number $x$ of any statement and correctly tell me if that statement is true?

The answer, discovered by the great logician Alfred Tarski, is a resounding no. There is no such formula. Tarski showed, with a brilliant argument that formalizes the ancient liar's paradox ("This statement is false"), that any theory strong enough to talk about its own syntax cannot define its own truth predicate. To try to do so would lead to an inescapable contradiction. Truth, in a sense, is always one level above the language it describes.

This isn't just a philosophical curiosity; it has a hard, computational edge. In the world of computer science, we know there are problems that are "undecidable"—problems for which no computer program can be written that will always halt and give a correct yes/no answer. The most famous is the Halting Problem: can we write a program that determines if any other given program will eventually halt or run forever? Alan Turing proved this is impossible.

What's the connection? There is a deep and beautiful link between definability in arithmetic and computability. Every computable property corresponds to a set of numbers that is definable by a specific, simple type of formula in arithmetic. Now, follow the logic: if we had a computer program that could decide which arithmetic statements are true, then the set of Gödel numbers of true statements would be a computable set. And if it were a computable set, it would be an arithmetically definable set. But this would mean we have found our $\text{True}(x)$ formula! And that's impossible, as Tarski showed. Therefore, no such computer program can exist. The undefinability of truth implies that the set of all arithmetic truths is uncomputable—it is a mountain of complexity that no single algorithm can ever conquer.

These results sketch the boundaries of our formal world. They reveal that there are different shades of inexpressibility. For instance, the set of halting programs is definable in the standard model of arithmetic (that is, we can write a formula that is true for exactly those numbers), but it is not "representable" in a system like Peano Arithmetic, meaning the theory cannot prove for every program whether it halts or not. This highlights a subtle but crucial gap between what is true in a mathematical world and what is provable within a fixed set of axioms for that world.

Faced with these walls, what's a mathematician to do? The answer is as simple as it is profound: climb. If a language cannot describe its own truth, perhaps a richer language can. This is precisely what happens in different axiomatic systems. For example, in the familiar Zermelo-Fraenkel set theory (ZFC), one cannot define a truth predicate for all of set theory—this would be a "truth set," and Tarski's theorem forbids it. However, if we move to a stronger system like Gödel-Bernays set theory ($GB$), which allows for the existence of "proper classes" that are too large to be sets, we can indeed define a "truth class." We have stepped outside the system of sets to a higher vantage point from which we can survey the whole landscape of set-theoretic truth.

This idea of using definability as a tool, a way to gain perspective and power, finds its ultimate expression in one of the most astonishing constructions in all of mathematics: Gödel's Constructible Universe, denoted by the letter $L$.

What is $L$? It is a version of the mathematical universe built from the ground up with an uncompromising principle: to be is to be definable. One starts with nothing, the empty set ($L_0 = \emptyset$). Then, at each stage, the next level of the universe is formed by taking all the subsets of the previous level that can be defined using a first-order formula with parameters from that previous level. That is, $L_{\alpha+1} = \mathrm{Def}(L_\alpha)$. The entire constructible universe $L$ is the union of all these layers.

It is a universe of pure structure, with no room for ambiguity. And what happens in this definability-tamed world? Miracles. Two of the most notoriously difficult statements in mathematics—the Axiom of Choice (AC) and the Generalized Continuum Hypothesis (GCH)—cease to be independent axioms and become provable theorems! Gödel showed that the universe $L$ is a model of ZFC + GCH.

How is this possible? Take GCH, the statement that for any infinite cardinal $\kappa$, the number of its subsets ($2^\kappa$) is the very next largest infinity ($\kappa^+$). In the "wild" universe of ZFC, the power set operation is mysterious; it gives us all possible subsets, with no hint as to how many there might be. But in $L$, a subset of $\kappa$ can only exist if it is constructible, meaning it must appear at some stage $L_\alpha$. The magic of the proof, which uses a deep structural property of $L$ called the Condensation Lemma, is to show that any constructible subset of $\kappa$ must appear "early"—before stage $L_{\kappa^+}$. This puts a strict ceiling on how many such subsets there can be. The explosive, uncontrollable growth of the power set is tamed by the principle of definability, leading to a rigid and predictable continuum function where $2^\kappa = \kappa^+$ always holds. The very axioms of mathematics, like Separation and Replacement, are shown to hold in $L$ by formalizing this notion of definability with a satisfaction predicate that, in a classic Tarski-esque move, is definable at the next level up.

$L$ is perhaps the greatest testament to the creative power of definition, showing that by restricting ourselves to what is explicitly definable, we can reveal a universe of incredible order and clarity.

So far, we have seen definability's profound limits and its creative power. But this exploration leads to an even deeper question: what do these properties tell us about the nature of logic itself? This brings us to our final viewpoint, a pinnacle of metamathematics known as Lindström's Theorem.

First-order logic (FO), the logic we have been implicitly using, is the language of "for all" ($\forall$) and "there exists" ($\exists$). But one could imagine other logics—logics that allow infinitely long sentences, or logics with new quantifiers like "there exist uncountably many." What makes first-order logic so special?

Lindström's theorem gives a stunning answer: ​​First-order logic is the strongest possible logic that still has two "nice" properties​​:

1. ​​Compactness​​: If a set of sentences is finitely satisfiable (every finite subset has a model), then the whole set has a model. This is a powerful tool for building infinite structures out of finite pieces.
2. ​​Downward Löwenheim-Skolem Property​​: If a sentence has an infinite model, it must have a countable one. This allows us to study vast, uncountable structures by looking at their smaller, countable counterparts.

The Beth Definability Theorem is a crucial ingredient in the proof of Lindström's theorem. It establishes that first-order logic has a certain internal coherence—that its notions of implicit and explicit definability align perfectly. This coherence is part of what gives it this unique character. Another of these special properties is "relativization," the ability to coherently talk about what is true inside a definable piece of a larger structure.

What is the grand consequence of Lindström's theorem? It provides a universal acid for testing the limits of any "reasonable" logic. Suppose you invent a new logic, $\mathcal{L}$, that extends first-order logic and you prove it has the compactness and Löwenheim-Skolem properties. Then Lindström's theorem immediately tells you that your new logic is no more expressive than plain old first-order logic.

This has immediate, powerful consequences. We know from the compactness argument that first-order logic cannot define the property of "being a finite set" or "being a well-ordered set." Therefore, no logic that is compact and has the Löwenheim-Skolem property can define these properties either! Lindström's theorem takes a specific limitation of FO and elevates it to a universal law for a vast class of logics.

Our exploration, which began with the simple-sounding Beth Definability Theorem, has led us to the frontiers of mathematics and logic. We have seen that the concept of definability is a double-edged sword. Its limitations are responsible for the uncomputability of truth and the incompleteness of our most powerful axiomatic systems. Yet, its power, when harnessed, is a creative force capable of building entire mathematical universes like $L$, where deep and difficult questions find definitive answers.

Ultimately, Beth's theorem and its relatives, like those of Tarski and Lindström, are not just about formulas and symbols. They are about the structure of knowledge itself. They reveal a beautiful, intricate hierarchy in the logical universe, a world where the act of definition is the fundamental way we draw lines, build structures, and ultimately make sense of the infinite.