Explicit Definability

In mathematics and logic, how do we pin down a concept with absolute precision? This fundamental question leads to a crucial distinction between two ways of defining something: the direct blueprint versus a set of inescapable clues. The former, known as an explicit definition, provides a concrete formula for a concept. The latter, an implicit definition, offers a set of rules or axioms that so perfectly constrain a concept that only one interpretation is possible. This raises a profound question: are these two approaches fundamentally different, or are they two sides of the same coin? Could a concept be uniquely determined by rules yet remain impossible to express with a single formula?

This article delves into the heart of this logical puzzle. The first chapter, "Principles and Mechanisms," will unpack the formal meanings of explicit and implicit definability, culminating in Beth's Definability Theorem—a cornerstone result proving their equivalence in first-order logic. We will explore how the Craig Interpolation Theorem provides the machinery to convert implicit clues into an explicit blueprint. The second chapter, "Applications and Interdisciplinary Connections," will demonstrate the power of this idea, showing how the drive for explicit definition is a unifying theme across mathematics, physics, and even the foundational construction of Gödel's constructible universe.

Imagine you're trying to describe a new idea, say, the concept of a "prime number," to someone who only understands basic arithmetic: addition, subtraction, multiplication, and division. You could do it in two ways. The first way is direct: you hand them a blueprint. You say, "A number $p$ is prime if it's greater than 1 and its only positive divisors are 1 and itself." This is a clear, explicit formula. Given any number, they can test it against your formula.

The second way is more subtle. Instead of giving them the formula, you give them a set of rules and stories involving your new concept. "Prime numbers are the building blocks of all other numbers." "There's no largest prime number." "Every number can be written as a unique product of these special numbers." You might add many such rules. Now, suppose your rules are so cleverly chosen, so perfectly constraining, that for the world of whole numbers, they leave no wiggle room. The concept of "prime number" is the only concept that could possibly satisfy all your rules simultaneously. You haven't given the blueprint, but you've constrained the world so tightly that the concept is uniquely determined. You've defined it implicitly.

In logic and mathematics, we grapple with this same distinction, but with more rigor and far-reaching consequences. When can we say a concept is truly definable? This question leads us to two fundamental notions: explicit and implicit definability.

Let's make our analogy more precise. Suppose we have a language, let's call it $L$, which contains the concepts we already understand—things like order ($$) or addition ($+$). We want to introduce a new concept, a new relation $R$.

An ​​explicit definition​​ is the blueprint. It's an $L$-formula $\varphi(\bar{x})$—a statement written entirely in our old, familiar language $L$—that serves as a stand-in for $R$. We assert that for any objects $\bar{x}$, $R(\bar{x})$ is true if and only if $\varphi(\bar{x})$ is true.

But there's a crucial distinction we must make. Is this definition meant to work in just one specific context, or in all possible contexts allowed by a theory? Consider a language $L$ with no symbols other than equality. Let our new concept be a property $R(x)$. In the specific world of the natural numbers $\mathbb{N}$, we can explicitly define $R$ as "the empty set" using the formula $\varphi(x) \equiv (x \neq x)$, since no number is unequal to itself. So, in this single structure, $R$ is perfectly definable. However, what if our "theory" $T$ is just the general theory of infinite sets, which says nothing about $R$? This theory allows for many different "worlds" (models). In one such world, $R$ could be empty, but in another, it could be non-empty. Since no single $L$-formula can work for all these allowed worlds, $R$ is not explicitly definable over the theory $T$. This difference between a local definition in one structure and a global definition across a whole theory is fundamental.

This brings us to the detective's approach. An ​​implicit definition​​ doesn't give you the blueprint $\varphi$. Instead, it gives you a theory $T'$—a set of axioms—in the new language $L' = L \cup \{R\}$. These axioms are the clues. We say $R$ is implicitly defined if these clues are so powerful that they uniquely determine what $R$ must be in any given context.

What does this mean? Imagine you have a complete description of a world in the old language $L$. We'll call this an $L$-structure, $\mathcal{A}$. An implicit definition means that there is at most one possible way to interpret the new concept $R$ on top of $\mathcal{A}$ that is consistent with the axioms in $T'$. If two detectives are given the same base structure $\mathcal{A}$ and the same rulebook $T'$, they must come to the exact same conclusion about $R$. If they could possibly disagree—if there were two different valid interpretations of $R$, say $R_1$ and $R_2$—then the definition would not be implicit. The clues would be ambiguous.

So we have two ways of capturing a concept: the engineer's blueprint (explicit definition) and the detective's inescapable conclusion (implicit definition). For a long time, mathematicians wondered: are these really different? Is it possible to have a concept that is uniquely determined by a set of rules, yet impossible to write down as a single, explicit formula?

The answer, in the world of first-order logic, is a resounding and beautiful "No!" This is the content of the ​​Beth Definability Theorem​​, a cornerstone of model theory. The theorem states:

A relation $R$ is implicitly definable by a theory $T'$ if and only if it is explicitly definable by $T'$.

This is a profound statement about the relationship between meaning and syntax in logic. It tells us that there are no elusive, ineffable concepts that are uniquely specified but not expressible. If a set of axioms pins down a concept completely, then there must exist a formula in the base language that is its blueprint. The detective's unique solution can always be reverse-engineered into the engineer's blueprint.

The "if" part of the theorem is easy to see. If you have an explicit formula $\varphi$, that formula itself guarantees uniqueness. Any valid interpretation of $R$ must match what $\varphi$ says, so there can only be one. The truly magical part is the "only if" direction: the fact that uniqueness alone is enough to guarantee that a formula exists. How on earth can we be sure of that?

The proof of Beth's theorem is not just a clever trick; it reveals a deep mechanism at the heart of logic. It shows us how, given an implicit definition, we can actually construct the explicit formula. The engine that drives this construction is another famous result: the ​​Craig Interpolation Theorem​​.

Imagine two people, Alice and Bob, are having a debate. Alice makes a statement $A$. Bob makes a statement $B$. Suppose we can prove that if Alice's statement $A$ is true, then Bob's statement $B$ must also be true ($A \models B$). The Craig Interpolation Theorem says that if this is the case, there must exist a "bridge" statement, an interpolant $I$, such that:

1. Alice's statement implies the bridge statement ($A \models I$).
2. The bridge statement implies Bob's statement ($I \models B$).
3. Crucially, the bridge statement $I$ is written only in the vocabulary that Alice and Bob have in common.

How does this help us find the blueprint for $R$? The argument is a beautiful piece of logical judo.

1. ​​The Setup​​: We start with our theory $T'$ that implicitly defines $R$ over the language $L$. We introduce a "clone" of our language, where the relation $R$ is replaced by a new symbol $R'$. Let's call the theory in this cloned language $T''$.

2. ​​The Contradiction​​: The implicit definition of $R$ means that in any world, if $R$ and $R'$ both satisfy the rules of the theory, they must be identical. This gives us a powerful entailment: $T' \cup T'' \models \forall \bar{x}\,(R(\bar{x}) \leftrightarrow R'(\bar{x}))$. In plain English, the combined theories prove that $R$ and its clone $R'$ must be the same relation.

3. ​​The Interpolation​​: Now we focus on just one direction of this equivalence, for some new objects (constants) $\bar{c}$: $T' \cup T'' \cup \{R(\bar{c})\} \models R'(\bar{c})$. This looks just like the setup for Craig's theorem!

   • Alice's statement $A$ is "$R(\bar{c})$ is true, and it follows the rules of $T'$." The language is $L \cup \{R, \bar{c}\}$.
   • Bob's statement $B$ is "$R'(\bar{c})$ is true, assuming it follows the rules of $T''$." The language is $L \cup \{R', \bar{c}\}$.
   • The common language is just $L \cup \{\bar{c}\}$.

4. ​​The Blueprint Appears​​: Craig's theorem tells us there must be an interpolant—a formula $\varphi(\bar{c})$ written only in the common language $L \cup \{\bar{c}\}$—that bridges the gap. This formula $\varphi(\bar{x})$ is precisely the explicit definition we were looking for! The two conditions of the interpolant, $A \models \varphi(\bar{c})$ and $\varphi(\bar{c}) \models B$, translate directly into $T' \models \forall\bar{x}\,(R(\bar{x}) \rightarrow \varphi(\bar{x}))$ and $T' \models \forall\bar{x}\,(\varphi(\bar{x}) \rightarrow R(\bar{x}))$.

This "interpolation machine" is guaranteed to work. We can even test it on a simple case. If we start with a theory $T$ where $R$ is already explicitly defined by a formula $S(x,y)$, the interpolation machine dutifully processes the logic and hands us back the formula $\varphi(x,y) = S(x,y)$. It successfully "rediscovers" the blueprint that was there all along.

This beautiful equivalence is a testament to the structure of first-order logic, but like any powerful tool, it's important to understand its scope and limitations.

First, the framework is remarkably flexible. What if our definition isn't universal, but depends on certain ​​parameters​​? For example, defining the "integers between $a$ and $b$." The Beth-Craig machinery handles this with ease. We simply treat the parameters as new constants in our base language $L$, and the entire process works perfectly, yielding a defining formula that depends on these new constants.

Second, we must be careful not to confuse definability with another concept: ​​conservativity​​. A theory $T'$ that defines a new symbol $R$ is conservative over a base theory $T$ if it doesn't prove any new sentences in the original language $L$. Definitional extensions are often conservative, but they don't have to be. For instance, we could have a theory $T'$ that both (1) introduces an axiom stating "there exists a least element" and (2) defines $R(x)$ to be "x is the least element". This theory $T'$ implicitly defines $R$, so by Beth's theorem, an explicit definition exists. However, $T'$ is not conservative over the general theory of linear orders, because it now proves the new $L$-sentence "there exists a least element," which is not always true for all linear orders. Beth's theorem is about the relationship between $R$ and $L$ within $T'$; it doesn't constrain what else $T'$ might say about $L$.

Finally, this deep connection between implicit and explicit definability is a special property of first-order logic. It relies on a foundational property called the ​​Compactness Theorem​​. If we move to more expressive logical systems, like infinitary logics where we can write infinitely long sentences, this connection can break. In such logics, it's possible to write a set of rules that implicitly define a concept for which no finite blueprint (i.e., a standard first-order formula) can ever be written. This shows us that the beautiful unity we've uncovered is not a universal truth of all possible logic, but a specific and profound feature of the logical language that underpins so much of modern mathematics.

We have spent some time exploring the logical machinery of explicit definability, this beautiful and precise idea about what it means to truly specify a mathematical object. But what is it all for? Does this abstract notion ever leave the lofty realm of set theory and logic to do honest work in the world? The answer, you will not be surprised to hear, is a resounding yes. The quest for explicit definition—the drive to move beyond merely knowing that something exists to being able to write down its blueprint—is a fundamental and unifying theme across all of science and mathematics. It is the difference between being told there is a treasure buried on an island and being handed a map with an "X" marking the spot.

Let's begin our journey with some simple, familiar landscapes. Imagine you have sorted all the real numbers into three bins: the negative numbers, the positive numbers, and zero. You have partitioned the real number line. This partition implies some rule, an equivalence relation, where all the numbers in a single bin are "related" to one another. But what is that rule, explicitly? We can say, "two numbers are related if they are in the same bin," but this is just repeating the result. We want the mechanism. A little thought reveals an explicit definition: two numbers $x$ and $y$ are related if and only if $xy > 0$ or $x = y = 0$. There it is—a concrete formula, an explicit test you can apply to any pair of numbers. We have replaced a description with a definition.

This same impulse appears in more dynamic settings. In topology, we often build complex paths by sticking simpler ones together. Suppose you have paths $f$, $g$, and $h$. You can define a new path by first combining $f$ and $g$, and then tacking on $h$. This is a perfectly good recursive definition, $(f \cdot g) \cdot h$. But if you wanted to program a computer to draw this path, or to analyze its properties, you would need a single, explicit recipe. You'd need to know, for any given moment in time $t$ between 0 and 1, exactly where you are. By unwrapping the nested definition, we arrive at a clear, piecewise formula telling us to traverse $f$ in the first quarter of the time, $g$ in the second quarter, and $h$ in the final half. A similar process of "currying" allows us to take a function of two variables, $f(x, y)$, and re-imagine it as a function that takes $x$ and gives back a new function of $y$. Again, the abstract idea is made concrete with an explicit formula. In all these cases, we translate an implicit, high-level process into an explicit, workable instruction set.

This drive for explicitness is not just about convenience; it is often the key to unlocking deeper problems. Consider the world of measure theory, the foundation of modern probability. We might start with a simple collection of sets, $\mathcal{F}$, whose properties we understand. We then add a new, complicated set $S$ that was not in our original collection. To do mathematics, we need a new, consistent collection of "measurable" sets that includes both our old collection and this new set. The standard way to do this is to take the "$\sigma$-algebra generated by $\mathcal{F}$ and $S$," which is implicitly defined as the smallest $\sigma$-algebra containing both. This definition is correct, but frustratingly abstract. If someone hands you a set, how can you tell if it's in this new collection? The breakthrough comes from finding an explicit characterization: every set in this new, larger collection can be written in the form $(A \cap S) \cup (B \cap S^c)$, where $A$ and $B$ are sets from our original, simpler collection $\mathcal{F}$. Suddenly, the abstract has become concrete. We have a constructive blueprint for every single object in our new universe, which is an indispensable tool for building theories of integration and probability on more complex spaces.

The same story plays out in the fields of physics and engineering. Many physical systems—from a vibrating guitar string to the quantum state of an electron in an atom—are described by differential operators. A fundamental example is the Laplacian operator, $A = -\frac{d^2}{dx^2}$, on some domain. To ensure our physics is well-behaved, we must restrict this operator to a domain of "nice" functions, for instance, functions in the Sobolev space $H^2$ that are zero at the boundaries. Now, what if we need to study a more complex system governed by the operator applied twice, $A^2$? The abstract definition of its domain is simple: it is the set of functions $f$ in the domain of $A$ such that $Af$ is also in the domain of $A$. This is an implicit definition. To solve actual equations, we need to know, explicitly, what properties a function must have to be in this new domain. The work of analysis is to translate this implicit condition into an explicit one. In this case, it turns out to be a beautiful and intuitive result: the functions must be even "nicer" than before (they must be in $H^4$), and they must satisfy an additional boundary condition related to the operator itself—their second derivatives must also be zero at the endpoints. This explicit characterization is not just a mathematical curiosity; it is the prerequisite for solving the kinds of fourth-order differential equations that model the bending of beams and the mechanics of plates.

So far, we have seen how making things explicit provides power and clarity. But the story takes a fascinating turn when we reach the very foundations of mathematics, where we discover that some things simply resist being made explicit. The Axiom of Choice is a powerful tool that asserts the existence of certain objects without giving any recipe for constructing them. It is the ultimate non-constructive tool. A classic example is the well-ordering of the real numbers. The Axiom of Choice guarantees that there exists a bijection between the real numbers $\mathbb{R}$ and some ordinal number—in other words, the real numbers can be arranged in a neat, well-ordered list. However, Zermelo-Fraenkel set theory with the Axiom of Choice (ZFC), our standard framework for mathematics, provides no formula, no explicit definition, for such an ordering. It is known to be consistent with ZFC that no "simple" definable well-ordering of the reals exists. This is a profound gap between existence and definability. We have the promise of a treasure, but no map at all.

This tension leads to one of the most stunning intellectual achievements in logic: Gödel's constructible universe, $L$. If our universe is filled with these ethereal, undefinable objects, Gödel asked, what if we were to build a new universe containing only the definable ones? To do this, he first had to make the very notion of "definability" perfectly explicit. He showed that the entire, seemingly boundless concept of first-order definability could be captured by the repeated application of a handful of concrete, primitive set-building operations. Starting with nothing, and at each stage adding only the sets that could be explicitly defined from the sets already built, he constructed a universe, layer by layer.

And the payoff? In this "tame" universe, $L$, built entirely from explicit definitions, the ghosts of non-constructibility vanish. One can write down a formula that explicitly well-orders the entire universe. As a result, the Axiom of Choice is not an axiom but a provable theorem in $L$. Furthermore, because the construction is so controlled, one can perform a precise census of the sets at each stage. This allows for a counting argument that proves the Generalized Continuum Hypothesis, another famous proposition that is independent of ZFC. By embracing explicit definability as a constructive principle, Gödel showed that if ZFC is consistent, then so is ZFC plus AC and GCH.

This notion of explicit definability even has practical consequences for how we structure our mathematical theories. When we introduce new notation or a new function into a formal system, we want to be sure we are not inadvertently adding a new, hidden axiom that strengthens the system. The theory of definitional extensions in logic tells us exactly when this is safe: we can add a new function symbol to a theory, like Peano Arithmetic, without changing its strength, provided that the function is explicitly definable by a formula in the original language and the theory is strong enough to prove that the definition yields a unique value for every input. This ensures that our "definitions" are truly just convenient shorthands, not Trojan horses smuggling in new mathematical truths.

From sorting numbers on a line to building entire universes of sets, the concept of explicit definability is a golden thread. It is the engine of discovery, the tool that translates abstract properties into concrete forms we can analyze, compute with, and understand. It reveals the structure hidden within our mathematical objects and, in its limitations, reveals the very structure of mathematical truth itself. It is, in the end, the embodiment of the deep scientific desire not just to know that, but to understand how.