What's a magical theorem in logic?

Question

Some theorems are magical: their hypotheses are easy to meet, and when invoked (as lemmas) in the midst of an otherwise routine proof, they deliver the desired conclusion more or less straightaway—like pulling a rabbit from a hat. Here are five examples. Some are from outside of logic, but each is often useful within logic.

Baire Category Theorem. In any completely metrizable topological space, each nonempty open set is nonmeager.

Gödel's Diagonal Lemma. If a theory $T$ relatively interprets Robinson's arithmetic, then for each first order formula $\varphi(x,v_1,\dots,v_n)$ in the language of $T$, there is a $\psi(v_1,\dots,v_n)$ such that $T$ proves the sentence $\forall v_1 \dots \forall v_n[\psi(v_1,\dots,v_n) \leftrightarrow \varphi(\overline\psi,v_1,\dots,v_n)]$, where $\overline\psi$ is the code of $\psi$.

König's Tree Lemma. Every finitely splitting tree of infinite height has an infinite branch.

Knaster–Tarski Theorem. Every monotone nondecreasing operator on the powerset of a set has a fixed point.

Mostowski Collapsing Lemma. If $E$ is a well founded, set like, and extensional binary class relation on a class $M$, then there is a unique transitive class $N$ such that $(M, E)$ is isomorphic to $(N, \in)$.

Let's list other magical theorems that every logician can wield. Students among us will thereby learn of useful results that might otherwise escape their attention until much later. (There is related question here. But it and most of its answers don't focus on theorems useful in logic.) Please treat only one theorem per answer, and write as many answers as you like. Don't just link to Wikipedia or whatever; give a pithy statement. If possible, keep it informal. Bonus if the theorem isn't well known, or if you show it in action.

Answer 1

The Compactness Theorem

Funny that no one mentioned it so far. I find the Compactness Theorem magical, actually:

A first order theory $T$ has a model if and only if every finite subset of $T$ has a model.

This let's you derive the finite form of Ramsey's theorem from the infinite form. That is magic. For most applications of this kind, the Compactness Theorem for propositional calculus is actually enough.

Compactness for first-order logic and propositional logic are actually equivalent (over ZF). In fact, there is a rather large collection of equivalent results:

• Boolean Prime Ideal Theorem
• The Ultrafilter Lemma
• The Stone Representation Theorem
• The Tychonoff Theorem for compact Hausdorff spaces

The Compactness Theorem is strictly weaker than the Axiom of Choice, but it is not provable in plain ZF. This is often used to show that certain results are weaker than the Axiom of Choice. For example, it can be used to show that the existence of non-measurable sets is weaker than the Axiom of Choice (by an old result of Sierpiński).

Answer 2

I think the fact that an elementary topos has finite colimits is magical. The definition of topos only asks for finite limits, but abracadabra! The magician pulls finite colimits from the hat.

(What's that I hear you say? You don't think topos theory is a part of modern logic? Really? Truly? Well, you know where the "down" button is.)

Answer 3

The Shoenfield Absoluteness Theorem

$\Pi^1_2$ and $\Sigma^1_2$ statements are absolute for transitive models of set theory.

Thus, a $\Pi^1_2$ statement is true (in $V$) if and only if it is true in $L$ (the constructible universe). Since $L$ satisfies the Axiom of Choice, every true $\Pi^1_2$ statement is consistent with the Axiom of Choice. This fact is often used to show that assuming the Axiom of Choice is often completely harmless in mathematical practice. Examples of $\Pi^1_2$ theorems include

• The (classical) Brouwer Fixed Point Theorem
• The separable Hanh-Banach Theorem
• Ascoli's Theorem
• The existence of algebraic closures for countable fields
• The existence of prime or maximal ideals for countable rings
• König's Tree Theorem
• Ramsey's Theorem
• The Completeness Theorem for countable first-order languages

and many, many more...

The Shoenfield Absoluteness Theorem is often used in conjunction with forcing. Indeed, if a $\Pi^1_2$ or $\Sigma^1_2$ statement can be forced in an extension, then it must have already been true in the ground model. Other absoluteness results are used in this way too. For example, the original proof of the Baumgartner-Hajnal Theorem (see here and here) combines forcing and the absoluteness of well-founded relations.

Answer 4

Cut elimination shows that if a sentence is provable in first-order logic, it is provable with a particularly nice type of proof in a natural deduction system without the "cut" rule, which is essentially modus ponens in that system. In particular these proofs have the subformula property – every formula in the entire proof is a subformula of the formula being proved.

The cut elimination theorem and its generalizations are key tools in proof theory. Gentzen proved cut elimination in 1934 and used it as part of his consistency proof of Peano arithmetic; there is a nice survey article "The art of ordinal analysis" by Michael Rathjen in Proc. ICM 2006.

The cut elimination theorem can be used to give nice proofs of the Craig interpolation theorem and other theorems from logic; one exposition is Chapter 6 of "Logic for Computer Science" by Jean Gallier.

Answer 5

The Low Basis Theorem

You mentioned König's Tree Lemma in the question. There is a very useful refinement that is common in computability theory and related areas:

Every computable infinite subtree of $\{0,1\}^{<\infty}$ has an infinite branch with a low Turing degree.

A set $A$ has low Turing degree if the halting problem relative to $A$ has the same Turing degree as the (unrelativized) halting problem. In particular, a set that has low Turing degree is incomplete (does not compute the halting set). Thus, the Low Basis Theorem is often used to show that a particular problem has a solution which has strictly lower complexity than the halting problem.

Another interesting feature of the Low Basis Theorem is that it is iterable. Indeed, the therorem relativizes very easily. Since being low relative to a low degree is the same as being plainly low, the theorem can be applied multiple times in a row to achieve the same outcome.

Also note that it is very important that the tree be a subtree of $\{0,1\}^{<\infty}$ (or, more generally, that the tree is computably bounded). Indeed, there are computable finitely branching subtrees of $\mathbb{N}^{<\infty}$ all of whose infinite branches compute the halting set. However, the Kreisel Basis Theorem guarantees that every computable finitely branching subtree of $\mathbb{N}^{<\infty}$ with infinite height has an infinite branch which is computable from the halting set.

An interesting application of the Low Basis Theorem is that Peano Arithmetic (PA), Zermelo-Fraenkel set theory (ZF), and all other consistent axiomatizable theories have completions that have low degree, and hence do not compute the halting set.

Answer 6

Kleene's recursion theorem says, informally, that when we write a program for a computable function we may assume that the program already has access to its own source code.

More formally, the theorem says that if $f\colon \mathbb{N} \to \mathbb{N}$ is a total computable function (which we view as a method that constructs a program $f(e)$ from a program $e$) there is some program $e_0$ such that the computable function with program $e_0$ is the same function as the function with program $f(e_0)$.

A trivial application: if $f(e)$ is a program that simply outputs $e$ and stops, the program $e_0$ outputs its own source code.

One of the magical applications of the recursion theorem is the lemma on effective transfinite recursion in hyperarithmetical theory, which is one of the key tools in that setting.

Answer 7

The Truth Lemma

The result says that what's true in a forcing extension $M[G]$ is just what's forced to be true by the path of the generic filter $G$. More precisely:

Suppose $M$ is a countable transitive model of $\text{ZFC}$, $\mathbb{P} \in M$ a forcing poset, $\varphi(x_1, \dots, x_n)$ a set theoretical formula, and $\tau_1, \dots, \tau_n$ a sequence of $\mathbb{P}$-names in $M$. If a filter $G$ on $\mathbb{P}$ meets each dense subset of $\mathbb{P}$ in $M$, then $\varphi(\tau_1^G, \dots, \tau_n^G)$ holds in $M[G]$ iff $G$ hits a $p$ that forces $\varphi(\tau_1, \dots, \tau_n)$.

In fact, $M$ just needs to satisfy a rich enough finite subtheory of $\text{ZFC}$. (How rich depends on $\varphi$.) Therefore the existence of suitable $M$ follows from the Reflection Theorem, which can be proved in $\text{ZFC}$ without assuming that $\text{ZFC}$ has a countable transitive model.

With a result known as the Definability Lemma, the Truth Lemma implies that every partial order forces $\text{ZFC}$. That is, $\text{ZFC}$ holds in every $M[G]$—no matter the $M$, $\mathbb{P}$, or $G$. This is key to showing that $M[G]$ is always the smallest transitive extension of $M$ satisfying $\text{ZFC}$ and containing $G$ as an element. Thus, in diverse circumstances one may build the partial order $\mathbb{P}$ of attempts to construct a desired object, argue that the object exists in any extension of $M$ containing a filter $G$ as in the lemma, and thereby obtain the actual existence of the desired object in a model where the axioms of ZFC still hold. Magic!

Answer 8

Ramsey's Theorem

The theorem has two forms.

Finite form. For all nonzero $n, k, m \in \mathbb{N}$ there is a nonzero $r \in \mathbb{N}$ such that, for each set $R$ of size $r$ and each $k$-coloring of the $n$-element subsets of $R$, there is a homogeneous set of size $m$.

Ininite form. For all nonzero $n, k \in \mathbb{N}$, each infinite set $W$, and each $k$-coloring of the $n$-element subsets of $W$, there is an infinite homogeneous set.

Frank Ramsey's original paper was titled On a problem of formal logic, so it should be no surprise that the famous theorem and its generalizations have magical applications in logic. For example, Ramsey's Theorem, the Erdős-Rado Theorem, and their more esoteric extensions, are often used in model theory to establish the existence of indiscernible elements.

[Please expand this!!!]

Answer 9

The Guaspari–Lindström Interpretability Theorem

For the sake of intelligibility, the statement here isn't as general as it could be.

Suppose $S$ and $T$ are consistent recursive extensions of $\text{ZFC}$. Then $T$ interprets $S$ iff $T$ proves each $\Pi_1$ consequence of $S$.

Set theorists use this to gauge the consistency strength of "natural" extensions of $\text{ZFC}$, which are (as far as people can tell) prewellordered under the relation of interpretability. In other words, the natural extensions form a well ordered hierarchy of degrees of interpretability. This is amazing, since it's easy to construct natural extensions that seem to have nothing in common—say, $\text{ZFC + }$"projective determinacy" and $\text{ZFC + }$"a supercompact cardinal exists."

[Someone with expertise, please edit and expand.]

Answer 10

Birkhoff's HSP Theorem

I liked the preservation theorems personally. Birkhoff's HSP theorem which identifies model classes of certain equational theories as being those classes (known in universal algebra as varieties) closed under homomorphisms (H), (iso to) subalgebras (S), and (iso to) products (P) is the one I remember most easily. There are other versions (e.g. for quasivarieties) as well. I hope this is magical enough for you.

Gerhard "Ask Me About System Design" Paseman, 2011.08.29

Edit: François asked me to include my comment within Gerhard's answer. I'll try to be brief. Just as algebraic theories can be described à la Lawvere as certain categories $T$ with finite products, and models of $T$ as finite product preserving functors $T \to Set$, it is of interest to consider "left exact theories" (aka "essentially algebraic theories") which are categories $T$ with finite limits, whose models are finitely continuous functors $T \to Set$. The theories of posets and of categories are examples of essentially algebraic theories.

It is known which categories are categories of models of some essentially algebraic theory, and this is the content of Gabriel-Ulmer duality. There is in fact a precise (bicategorical) contravariant equivalence between the bicategory of finitely complete categories, and the bicategory of locally finitely presentable categories. The concept of filtered colimit plays a crucial role in this development.

A sample theorem within this general theory which extrapolates Birkhoff's Variety Theorem is that a class of structures over a multi-sorted functional signature is a finitary quasi-variety (i.e., definable by Horn clauses over equational predicates) if and only if it is closed under products, subobjects, and filtered colimits within the category of all structures. For a reference, see Adámek and Rosicky, Locally Presentable and Accessible Categories, theorem 3.22.

Todd "I'm Happy to Oblige" Trimble

Answer 11

The Montague–Lévy Reflection Theorem

The theorem applies to all cumulative hierarchies, but let's focus on the special case of the $V_\alpha$ hierarchy.

Let $\varphi_1, \dots, \varphi_n$ be set theoretical formulas in at most $k$ variables. $\text{ZF}$ proves that for all ordinals $\alpha$ there is a $\beta > \alpha$ such that, if $b_1, \dots, b_k$ are in the set $V_\beta$, then $V_\beta \vDash \varphi_i[b_1, \dots, b_k]$ just in case $\varphi_i[b_1, \dots, b_k]$ is really true.

In other words, $V_\beta$ is a $(\varphi_1, \dots, \varphi_n)$-elementary substructure of the universe $V$. (By the Second Incompleteness Theorem, if $\text{ZF}$ is consistent, then it can't prove that a full elementary substructure of $V$ exists.) Hence you can't characterize the universe: there are always arbitrarily large rank initial segments that behave just like the universe, with respect to whatever condition you invent.

The Reflection Theorem is very useful, for instance in proving that $\text{ZF}$ isn't finitely axiomatizable unless it's inconsistent. If if $T$ is a finite axiomatization, then $\text{ZF}$ proves by reflection that $T$ has a set model, and hence (since $T$ axiomatizes $\text{ZF}$) so does $T$. By the Second Incompleteness Theorem, $T$ is inconsistent. Hence, so is $\text{ZF}$.

Answer 12

The fundamental theorem of Ehrenfeucht-Fraisse games. It seems innocuous (because of the game formulation?) but the applications never stop. It provides a natural way to prove a property is not expressible in a logic. It is one of the tools of classical model theory that is also used in finite model theory. In the related notions of bisimulation and simulation, we have a cornerstone concept of concurrency theory and program verification.

Answer 13

Some theorems are magical: their hypotheses are easy to meet, and when invoked (as lemmas) in the midst of an otherwise routine proof, they deliver the desired conclusion more or less straightaway—like pulling a rabbit from a hat.

Perhaps to meet the sheer poetic requirement, Well-ordering theorem which states that "any set can be well-ordered" remains 'hands-down' as any meta-logician's top answer. In terms of historical perspective it has taken the logical house by maelstrom (with seemingly counter-intuitive offshoot of Banach-Tarski paradox at first) resulting from Axiom of Choice(AC) as mentioned by John bell in the SEP chronology:

1904/1908 Zermelo introduces axioms of set theory, explicitly formulates AC and uses it to prove the well-ordering theorem, thereby raising a storm of controversy.

Answer 14

The Feferman-Vaught theorem is a fairly magical result in logic since it allows one to figure out the truth value of a first order formula in a product of structures in terms of the individual structures and the type of product used. More generally, the Feferman-Vaught technique can be used to analyze complex structures based on their components. There are different versions of the Feferman-Vaught theorem, so I should say that the Feferman-Vaught theorem is a class of theorems or a technique rather than an individual result. This technique was developed by Feferman and Vaught in the well-known paper The first Order Properties of Products of Algebraic Systems. The following result is a version of the Feferman-Vaught theorem for reduced products. For this result, we will need the following definition. If $\psi(x_1,...,x_n)$ is a formula and $\prod_{i\in I}\mathcal{A}_{i}/Z$ is a reduced product, then for $[f]_{1},...,[f]_{n}\in\prod_{i\in I}\mathcal{A}_{i}/Z$, let $\|\psi([f]_{1},...,[f]_{n})\|=\{i\in I|\mathcal{A}_{i}\models\psi(f_{1}(i),...,f_{n}(i))\}/Z$. In other words, $\|\psi([f]_{1},...,[f]_{n})\|\in I/Z$ is the Boolean value of $\psi([f]_{1},...,[f]_{n})$.

For each formula $\phi(x_{1},...,x_{n})$ there is a sequence of formulas $(\theta;\psi_{1},...,\psi_{m})$ such that

• the formulas $\psi_{i}$ have at most the variables $x_{1},...,x_{n}$ free

• $\theta=\theta(y_{1},...,y_{m})$ is a formula in the language of Boolean algebras and

• If $I$ is a set and $Z$ is a filter on $I$ and $\mathcal{A}_{i}$ is a first order structure for $i\in I$, then for $[f_{1}],...,[f_{n}]\in\prod_{i\in > I}\mathcal{A}_{i}/Z$, we have $$\prod_{i\in > I}\mathcal{A}_{i}/Z\models\phi([f_{1}],...,[f_{n}])$$ if and only if $$P(I)/Z\models\theta(\|\psi_{1}([f_{1}],...,[f_{n}])\|,...,\|\psi_{m}([f_{1}],...,[f_{n}])\|).$$

The above result also holds for the limit reduced power and the Boolean product (see the paper Sheaf Constructions and Their Elementary Properties for more details on this result). An immediate consequence of this result is that reduced products preserve elementary equivalence. In particular, direct products, direct powers, and reduced powers all preserve elementary equivalence and elementary embeddings. I posted this result since I recently used an application of a version of the Feferman-Vaught theorem to produce a result about ultrapowers and limit reduced powers.

Answer 15

This example is for me sheer wizardry: Given a class of relational structures of the same type, all with finite underlying universes and including one with a one-element universe, such a class has unique cancellation as well as unique kth roots (AxC iso BxC implies A iso B, A^k iso B^k implies A iso B). Lovasz came up with the results in the 1960's, and for me the only explanation to the magic is that he came up with the proof first and then the statements later. I hope that kind of magic is allowed for an answer.

Gerhard "Ask Me About System Design" Paseman, 2011.08.29