# A primer to the set-theoretic multiverse philosophy put forward by Joel David Hamkins

Notes accompanying the 50th meeting of the Curry Club Augsburg. We gratefully acknowledge Daniel Albert, Cat Cozzi, Raphael Engel, Jonas Eschenburg, Alexander Hilpert, Matthias Hutzler and Florian Niggl, who with their participation in the meeting and reading of earlier drafts substantially contributed to this note. We are also indebted to the participants of the Reddit thread were this note was discussed, in particular to /u/louiswins [more will be added as we incorporate the suggestions], and to Marlou Gijzen and Enrique Pablo.

## Prehistory

In the beginning of the 20th century, mathematicians made a
disturbing discovery: Ordinary reasoning, as practiced by humans when
talking mathematics, is *inconsistent*, that is, using ordinary
reasoning we can prove the bogus statement 1 = 0. This discovery, known as Russell’s
paradox, plunged mathematics into a foundational crisis: The entire
landscape of human mathematics had been built upon ordinary reasoning.
How could in face of this basic inconsistency its results be
trusted?

Only about thirty years later, the mathematical community converged
to a solution. They adopted the notion of *formal proofs* as the
gold standard to judge whether mathematical arguments are correct. (At
least in principle. In practice, mathematicians still write their proofs
in natural languages like English, as it is intensely cumbersome to
write down formal proofs on paper. But a trained logician will know how
to formalize informal proofs, and mathematicians know what kind of
reasoning to avoid because it would not be formalizable. With the
emergence of proof assistants such as Agda, Coq, Isabelle/HOL, Lean,
Mizar and NuPRL over the past years, we are entering the golden age of
formal proofs.)

A formal proof has to follow strict syntactic rules, using only
certain axioms and certain logical inferences. Logicians study a large
zoo of such formal systems, each prescribing axioms and inferences, and
compare their strength. Among others, a formal system which is
sufficiently powerful to carry out almost all of current mathematics
is `ZFC`

, Zermelo–Fraenkel set theory with the axiom of
choice. (Alternatives include various flavors of type theory, such as
homotopy type theory, or systems like `ETCS`

, which adopts a
category-theoretic perspective on set theory. Each of these systems has
unique features rendering them particularly suited to some schools of
thought; however, for much of everyday mathematics, those particular
features don’t matter much.)

Among the axioms of `ZFC`

are:

∃

*x*. ∀*y*. ¬(*y*∈*x*)∀

*x*. ∀*y*. ∃*w*. (*x*∈*w*∧*y*∈*w*)∀

*x*. ∃*z*. ∀*w*. ((∀*y*. (*y*∈*w*⇒*y*∈*x*))⇒*w*∈*z*)

Without training in formal logic, these are hard to read. Hence we will restate them in English, and also agree to use English as a proxy for formal language in the rest of this note.

There is an

*x*such that for every*y*, it is not the case that*y*is an element of*x*. (More succinctly: “There is a set which is empty.”)Given any sets

*x*and*y*, there is a set which contains*x*and*y*.Given any set

*x*, there is a set which contains all subsets of*x*.

And among the logical inference rules of `ZFC`

are:

From

*φ*∧*ψ*deduce*φ*.Modus ponens: From

*φ*and*φ*⇒*ψ*deduce*ψ*.Law of excluded middle: Deduce

*φ*∨ ¬*φ*.

There are a
couple of more axioms and inference rules to `ZFC`

, but
the complete list is still quite short. It is somewhat astonishing that
almost all results of current mathematics can be proven using only this
few ingredients.^{1}

We write “`ZFC`

⊢ *φ*” to express
that there is a `ZFC`

-proof of a mathematical statement *φ*, and we write “`ZFC`

⊬ *φ*” to express
that there is no such proof. For instance, we have `ZFC`

⊢ (There are infinitely many primes)
and `ZFC`

⊬ (2+2=5).^{2}

Metamathematical discussions about `ZFC`

and other formal
systems are typically carried out in very weak foundations such
as `PRA`

, *primitive-recursive arithmetic*. Among
other reasons, this is because we want to shield those discussions from
hypothetical inconsistencies in strong foundations such
as `ZFC`

. Only few people, the group of ultrafinitists, make
the case that even `PRA`

might be inconsistent.

## Incompleteness phenomena

The switch from naive informal reasoning to formal reasoning has put mathematics on a firm foundation. However, the formal approach is not without its own issues. Namely it faces an inherent incompleteness which is provably not fixable.

**Definition.** A formal system *S* is *inconsistent* if and
only if it proves a contradiction: *S* ⊢ ⊥. (The symbol “⊥” is pronounced “bottom” and is informally
also written “↯”. It denotes a false-by-definition statement. One can
think of it as “1 = 0”.) A system *S* is *consistent* if and only
if it is not inconsistent, that is, if there is no *S*-proof of ⊥.

Most formal systems include the rule “ex falsum quodlibet” which
allows to derive a proof of any statement whatsoever from a proof of
⊥. Hence inconsistent systems are not
very useful from the point of view of ensuring the correctness of
mathematical arguments, since an inconsistent system (with ex falsum
quodlibet) proves any statement whatsoever. `ZFC`

, and indeed
systems which are much stronger than `ZFC`

, are believed to
be consistent.

**Theorem.** (Gödel’s first incompleteness theorem)
Let *S* be a reasonable^{3} formal system. Then there are
mathematical statements *φ* such
that, if there is an *S*-proof
of *φ* or if there is an *S*-proof of ¬*φ* (the negation of *φ*), then *S* is inconsistent.

Phrased contrapositively, if *S* is consistent, then there is
neither an *S*-proof of *φ* nor an *S*-proof of ¬*φ*. In this sense *S* is *incomplete*: The
system *S* keeps shtum on *φ*, it neither proves nor
refutes *φ*.

This situation is analogous to board games where sometimes the system of rules also keeps shtum on certain issues which occur during play. In this case, players can make up a new rule on the fly, a rule of their choice, and the same possibility is available in logic:

If *φ* is a statement which
is independent of a formal system *S*, in the sense that *S* neither proves nor refutes *φ*, then both *S*+*φ* and *S*+¬*φ*, the new systems obtained by
adding *φ* respectively ¬*φ* to the axioms, are again
consistent systems. We could continue in this fashion: Each of the two
new systems is again incomplete, hence can be consistently extended in
two distinct ways, and so on. None of these systems stands out, there is
no canonical reason to prefer one over the other. Which system to prefer
is a matter of taste.

Gödel’s incompleteness theorem applies to every reasonable formal
system, hence in particular to `ZFC`

, thus `ZFC`

is incomplete. However, this phenomenon shouldn’t be regarded as a
defect of `ZFC`

, perhaps to be overcome by adding suitable
axioms, because every consistent extension of `ZFC`

will
again be incomplete. Incompleteness is a fundamental feature of the
formal approach to reasoning.

There are many examples for statements which are independent
from `ZFC`

, from several subjects:

(logic) “The system

`ZFC`

is consistent.”^{4}(computer science) “The value of BB(1919) is 1 + ⋯ + 1.”, where BB is the Busy Beaver function, and the sum comprises BB(1919) summands.

^{5}(number theory) “A certain specific equation, involving only addition and multiplication of integers, does not have a solution in the natural numbers.”

(information theory) “The Kolmogorov complexity of the string

*s*is more than*L*.”, where*L*is a certain large enough constant and*s*is any specific string of Kolmogorov complexity more than*L*.(set theory) “The continuum hypothesis holds.”

Wikipedia also lists examples from order theory, abstract algebra, measure theory, topology and functional analysis. The continuum hypothesis is particularly prominent and will be reviewed in the next section.

The hydra
game provides an additional instructive example, though not for a
statement which is independent of `ZFC`

, but for a statement
which is independent of *Peano arithmetic* (`PA`

).
This system is vastly weaker than `ZFC`

, but still capable of
proving most concrete results about numbers.

The hydra game is a certain finitary mathematical game in which Heracla fights an evil hydra. When Heracla chops off one of its heads, a certain precise rule governs in which way new heads grow. Playing the game gives the impression that, except for occasional drops, the number of heads grows exponentially and that winning against the hydra is impossible. However:

Heracla does have a winning strategy.

Moreover,

*every*strategy will eventually result in a win for Heracla; no matter in which order Heracla carries out her chopping, after finitely many steps no heads remain.Statements 1 and 2 can be proven within

`ZFC`

(which is why we presented them as facts), but not within`PA`

. For each number*n*,`PA`

proves that Heracla can win against every hydra with*n*initial heads, but these proofs get longer and longer with increasing*n*.`PA`

doesn’t recognize a single unifying reason for these individual facts, and indeed doesn’t prove that Heracla can win against every hydra.^{6}

## The continuum hypothesis and its traditional dream solution

A fundamental observation in set theory, due to its founder Georg
Cantor, is: Not all infinities are alike, some infinities are larger
than others. Sizes are measured by so-called *cardinal numbers*,
and the cardinal number line starts like this:

The finite cardinals: 0, 1, 2, ...

The first infinite cardinal number: ℵ

_{0}. There are ℵ_{0}many natural numbers.The second-smallest infinite cardinal number: ℵ

_{1}.The infinite cardinal number immediately succeeding ℵ

_{1}: ℵ_{2}.And so on.

^{7}

Somewhat surprisingly, ℵ_{0}
is not only the number of naturals, but also the number of integers,
even though intuitively, there are about twice as many integers than
naturals. In fact, there are also only ℵ_{0} many rationals, even though
intuitively there should be infinitely many more rationals than integers
(observing that between any two integers, infinitely many rationals
fit). These phenomena can be neatly illustrated by Hilbert’s
hotel, and we invite readers unfamiliar with these intriguing facts
to pause and ponder Hilbert’s hotel.

Where do the reals fit in, how large is the set of all real numbers?
This is a nontrivial question. The standard notation for the size of the
set of real numbers is “𝔠” (for
“continuum”, another term for the real number line). This cardinal is at
least ℵ_{0}, for the plain
reason that it is not the case that there are only finitely many reals.
In fact, we know more: The cardinal 𝔠
is equal to the power 2^{ℵ0} (two to the power
of ℵ_{0}), and Cantor’s
celebrated *diagonal argument* shows that 𝔠 is strictly larger than ℵ_{0}: 𝔠 > ℵ_{0}. But which cardinal is
it? Is 𝔠 = ℵ_{1}? Or is 𝔠 = ℵ_{2}? Or is 𝔠 some even larger cardinal?

The hypothesis that there is no infinity between ℵ_{0} and 𝔠 (that is, that 𝔠 is the infinity directly succeeding ℵ_{0}, hence that 𝔠 = ℵ_{1}) is known as the
*continuum hypothesis* (`CH`

). When Cantor pioneered
the study of set theory, he didn’t manage to prove the continuum
hypothesis, and he also didn’t manage to refute it. We now know that
Cantor didn’t have a chance:

`CH`

is independent of `ZFC`

.

In 1938, Gödel proved that there is no

`ZFC`

-proof of ¬`CH`

.In 1963, Cohen proved that there is no

`ZFC`

-proof of`CH`

.

(Both of these metamathematical arguments can be carried out
in `PRA`

with only one extra assumption, namely the
consistency of `ZFC`

.^{8} They are nowadays best
understood using the notion of *models of ZFC*,
reviewed in the next section.)

Is `CH`

*true*? In the platonic heaven of all sets,
is there an infinity strictly between ℵ_{0} and 𝔠? A platonist can ask this question, but if
their only way to obtain reliable knowledge about the platonic heaven is
by `ZFC`

-proofs, then by the independence of `CH`

from `ZFC`

they will never know.

With Gödel’s and Cohen’s observations, research on the continuum
hypothesis took a new direction. As it was now known that it is
impossible to settle the conjecture one way or another, set theorists
pursued the vision that `ZFC`

should be extended by
additional axioms. These new axioms should be strong enough to
settle `CH`

(prove `CH`

or refute `CH`

)
while at the same time be well-motivated, mathematically elegant, yield
a satisfying theory, and not be obviously biased toward `CH`

or ¬`CH`

.

Of course, by Gödel’s fundamental incompleteness theorem reviewed
above, no formal system can settle *all* mathematical questions;
but one could hope that some extension of `ZFC`

settles most
of the most pressing set-theoretic questions, certainly relatively basic
questions such as `CH`

.

This research program has produced, and continues to produce, a host of intriguing potential new axioms. However, no clear winner has emerged, no proposal met all requirements. For instance, all of the following proposals for new axioms have been rejected:

“

`CH`

”. This proposal is obviously biased toward`CH`

. It is also oddly specific, yielding an answer for the question “what is 2^{ℵ0}?” (namely ℵ_{1}), but leaving the related questions “what is 2^{ℵ1}?”, “what is 2^{ℵ2}?” and so on undecided.“¬

`CH`

”. This proposal is obviously biased toward ¬`CH`

. It is also not very definitive, because while it tells us that there is some infinity between ℵ_{0}and 𝔠, it doesn’t tell us anything about the properties of this extra infinity, nor does it tell us how many infinities between ℵ_{0}and 𝔠 exist.“

*V*=*L*”. This proposal states that every set is*constructible*. Very roughly, a set is constructible if and only if it can be described in set-theoretic terms using only sets which have already been described in this manner, breaking the recursion with the empty set. For instance, the set of all even numbers, the set of all prime numbers, and indeed every set which can be mentioned in a discussion are constructible. However, without the axiom*V*=*L*, there is no reason why all sets should be constructible. The axiom*V*=*L*implies`CH`

, and it also settles a variety of related set-theoretic questions. However, most set theorists, among them Penelope Maddy with her motto “maximize!”, feel that*V*=*L*imposes an undue restriction on the set-theoretic landscape, in particular because it is inconsistent with certain beautiful and important*large cardinal axioms*.

The multiverse philosophy proposes a different research program; posits an intriguing new stance on the status of the continuum hypothesis (and related questions); and also explains why the traditional dream solution of finding rewarding new axioms which would settle many important independent statements is unlikely to ever be attained.

Very briefly, to a zeroth approximation, the multiverse position is
that we should embrace all possible extensions of `ZFC`

equally, without preferring one over the other. However, this terse
summary is missing an important semantic aspect from which much of the
fascination and usefulness of the multiverse philosophy derives from. A
proper exposition requires the notion of a *model of
ZFC*, reviewed in the next section.

## The multiverse philosophy

**Definition.** A *model* of `ZFC`

is
a collection *M* together with a
binary relation on *M* such that
the axioms of `ZFC`

are satisfied for *M* and this relation.

By convention, the elements of *M* are called “sets”, or “sets
of *M*”, or “what *M* believes to be sets”, or “*M*-sets”, and the relation is written
“∈”, exactly as the ordinary membership
relation. However, as the examples will illustrate, the elements needn’t
actually be sets. (This linguistic usage is common in other branches of
mathematics as well. For instance, elements of a vector space are always
called “vectors”, even though they don’t need to be the special kind of
vectors taught in school.) Every particular model of `ZFC`

can be pictured as a specific set-theoretic universe in which we can do
mathematics.

We write “*M* ⊨ *φ*”
to express that a statement *φ*
holds in the world of a `ZFC`

-model *M*. For instance, “*M* ⊨ ∃*x*. ∃*y*. *x* ∈ *y*”
expresses that there is some *M*-set *x* such that there is a further *M*-set *y* such that *x* is an element of *y*, as judged by the binary relation
coming with *M*. The requirement
that the axioms of `ZFC`

hold in *M* can also be succinctly stated
as “*M* ⊨ `ZFC`

”.

Here are two non-examples for models of `ZFC`

.

Let

*M*be the singleton collection containing ♡ as its only element. Declare “♡ ∈ ♡” to be true. This structure doesn’t satisfy the axioms of`ZFC`

, for instance because one of the axioms requires that there is an empty*M*-set, but the only candidate, namely ♡, is inhabited.The axioms of

`ZFC`

are also not satisfied if instead we declare “♡ ∈ ♡” to be false. While this structure does validate the axiom that there should be an empty*M*-set, it doesn’t validate the axiom that for every given*M*-sets*x*and*y*, there should be an*M*-set*w*which contains*x*and*y*: Given ♡ and ♡, there should be an*M*-set*w*which contains ♡ and ♡, but the only candidate is, by the new declaration, empty.Let

*M*be the empty collection. This structure doesn’t validate the axiom that there should be an empty*M*-set, simply because there aren’t any*M*-sets.

The prototypical example for a model of `ZFC`

is the
following structure, even though it is only available to a platonist:
Let *M* be the collection of all
sets in the platonic heaven, and declare “*x* ∈ *y*” to be true if and
only if, in the platonic heaven, the set *x* actually is an element of the
set *y*.

In principle, in constructing a model of `ZFC`

we are free
in our choice which elements to deem *M*-sets and which membership
relations to impose. However, the requirement that the resulting
structure should validate the axioms of `ZFC`

puts strong
constraints on our choices. For instance, as soon as we include a
certain *M*-set *x*, we are required to also include
an *M*-set *y* which contains *x*, and then in turn an *M*-set which contains *y*, and so on.

As discussed above, the formal system `ZFC`

leaves many
mathematical statements undecided – there are many statements which are
neither proved nor refuted by `ZFC`

. In contrast, every model
of `ZFC`

takes a definitive stance on each statement: For
every mathematical statement *φ*, the expression “*M* ⊨ *φ*” has a definitive
truth value.

A beginning student of philosophy might find the concept of a set to
be intuitively clear. However, the paradoxes of naive set theory such as
Russell’s paradox alluded to in Section 1 demonstrate that the informal
notion of a set is actually ill-specified. The axioms
of `ZFC`

try to capture the vague intuition about sets in a
formal manner, but in view of incompleteness phenomena they fail to pin
down a single coherent concept of sets. We can consider each model *M* of `ZFC`

to each be a
complete determination of some coherent concept of sets, namely the
concept of *M*-sets, making it
manifest that the informal notion of sets can be spelled out in a host
of non-equivalent ways.

Set theorists have developed powerful tools for constructing new
models of `ZFC`

out of given ones, similarly to how monoid
theorists construct new monoids out of given ones or how geometers
construct new manifolds out of given ones. (For instance, given a
monoid *A*, there is the
cartesian product monoid *A* × *A*, or given a
ring *R*, there is the
polynomial ring *R*[*X*].)

The two most important such tools are *inner models* and
*forcing models*, pioneered by Gödel and Cohen, respectively. By
the technique of inner models, every given model *M* of `ZFC`

can be thinned
down to obtain a smaller model *L*^{M} in which the
continuum hypothesis holds. By forcing, every given model *M* can be extended to obtain a larger
model *M*[*G*] in which
the continuum hypothesis fails.^{9}

It is by these constructions that we know that the continuum
hypothesis is independent of `ZFC`

: If there would be
a `ZFC`

-proof of `CH`

, then `CH`

would
hold in every model of `ZFC`

(since every model
of `ZFC`

validates the axioms of `ZFC`

and hence
also all of their consequences), but it doesn’t in the models obtained
by Cohen. Conversely, if there would be a `ZFC`

-proof of
¬`CH`

, then ¬`CH`

would hold in every model
of `ZFC`

, but it doesn’t in the models obtained by Gödel.

Summarizing, common to all models of `ZFC`

is that, by
definition, they validate the axioms of `ZFC`

. But regarding
the statements which are independent of `ZFC`

, each model can
take their own stance. Some models validate `CH`

while others
validate ¬`CH`

.

We are now in a position to introduce the set-theoretic multiverse and to appreciate the multiverse philosophy.

The set-theoretic multiverse is the entirety of all models
of `ZFC`

. The multiverse philosophy posits that we should
take the multiverse seriously; that we shouldn’t venture for new axioms
to add to `ZFC`

, but that we should embrace all models
of `ZFC`

; and that we should understand statements which are
independent of `ZFC`

by studying how they behave when
traveling the multiverse.

This point of view will be illustrated in the next section, where we will make the notion of voyaging through the multiverse precise.

## Traveling the multiverse

The notion of voyaging through the multiverse can be usefully
captured in terms of modal logic. Given a mathematical statement *φ*, by “◇*φ*” we mean that *φ* holds in *some* extension
of the universe; by “□*φ*” we
mean that *φ* holds in
*every* extension of the universe. There are several possible
choices for what “extension” could mean; a common one is to mean
“forcing extension”. (Because set theorists aren’t afraid of special
cases, the “trivial extension”, which passes from a given model *M* to the same model *M* again, is also deemed a valid
extension for the purposes of defining “◇” and “□”.)

For instance, “*M* ⊨ ◇*φ*” means that *φ* holds in some forcing
extension *M*′ of *M*. It means that even if *φ* might not hold in *M*, we can force it to be true by
passing from *M* to some
neighboring universe *M*′.

As a further example, “*M* ⊨ ◇□*φ*”,
parenthesized “*M* ⊨ (◇(□*φ*))”, means
that *M* has a forcing
extension *M*′ such that every
further forcing extension *M*″
of *M*′ validates *φ*. That is, starting at *M*, we can travel to a larger
universe *M*′ such that every
universe reachable from *M*′ (in
particular *M*′ itself)
validates *φ*. (As we only
consider *extensions*, not inner models, all the roads are
one-way streets. When moving in the multiverse, we are always trekking
upwards, to larger and larger universes.)

A fundamental observation about the multiverse is that every
mathematical statement is either a *switch*, a *button* or
the *negation of a button*.

A

*switch*is a statement*φ*such that □(◇*φ*∧◇¬*φ*), properly parenthesized □((◇*φ*)∧(◇(¬*φ*))). That is, no matter where we travel to from the current universe, there will always be a road to a universe in which*φ*holds and there will always be a road to a universe in which*φ*does not hold. We can toggle the truth of*φ*like we can toggle a light switch.A

*button*is a statement*φ*such that □◇□*φ*, parenthesized □(◇(□*φ*)). That is, no matter where we travel to from the current universe, there will always be a road to a universe such that*φ*holds there and in every further universe reachable from there. A button can be pressed, but once pressed cannot be unpressed.

The continuum hypothesis is an example for a switch, and following
the multiverse philosophy *the continuum hypothesis is no longer an
open problem*. Set theorists have a rich experience with models in
which `CH`

holds, with models in which `CH`

does
not hold, how to pass from models of the first kind to models of the
second and vice versa, and which further changes to a model (side
effects) are effected by such a passage.

We conclude with a number of notable features of the multiverse.

Every model of

`ZFC`

believes itself to be enormous, containing uncountable sets such as the reals, containing all cardinal numbers, containing all ordinal numbers, and so on. In particular it believes itself to contain uncountably many sets. In fact, it believes itself to contain a proper class’ worth of sets. (This is because the statement “¬∃*w*. ∀*x*.*x*∈*w*”, expressing that there is no set of all sets, is a theorem of`ZFC`

, hence holds in every model.)And indeed, for every model

*M*, there is no*M*-set which could contain all*M*-sets. However it turns out that every model is merely countable from the point of view of a sufficiently larger model. This phenomenon is the*mirage of uncountability*.Every model

*M*of`ZFC`

believes itself to be well-founded, meaning that there is no infinite descending chain of the form*x*_{0}∋*x*_{1}∋*x*_{2}∋ ⋯ of an*M*-set which contains some*M*-set which contains some further*M*-set which … This is because well-foundedness is an axiom of`ZFC`

. But it turns out that every model is ill-founded from the perspective of some other model. This phenomenon is the*mirage of well-foundedness*.By Gödel’s second incompleteness theorem, the system “

`ZFC`

+ ‘`ZFC`

is inconsistent’” is a consistent formal system. (We don’t consider this system to be trustworthy, for instance because it proves the statement “`ZFC`

is inconsistent”, which we believe to be false. However, despite not being*sound*, it is still consistent.) By Gödel’s completeness theorem, every consistent formal system has a model. Hence there are models of`ZFC`

which validate the statement “`ZFC`

is inconsistent”. Such models are called*self-hating*.Some models validate the curious maximality principle ◇□

*φ*⇒ □*φ*, parenthesized (◇(□*φ*)) ⇒ (□*φ*). These worlds are maximal in the sense that every statement which could (after passing to a larger universe) become permanent (hold from then on in every even larger universe) is already permanent.There is a certain Turing machine

*P*, which can be written down explicitly, such that for every function*f*: ℕ → ℕ, there is some universe in which*P*computes precisely*f*. Hence every function whatsoever is computable from the point of view of a suitable universe. The algorithm which*P*implements is called the*universal algorithm*.Instead of only looking up, we can also look down and introduce the notion of a

*ground*of a model*M*: A ground of*M*is an inner model*M*′ of*M*such that*M*arises from*M*′ by forcing. Every model*M*has a trivial ground, namely*M*itself, but the existence of nontrivial grounds is an interesting question. Digging deeper, we define the*mantle*of a model as the intersection of all its grounds.We could then entertain the idea of an

*ancient paradise*, quoting Hamkins: “This position holds that there is a highly regular core underlying the universe of set theory, an inner model obscured over the eons by the accumulating layers of debris heaped up by innumerable forcing constructions since the beginning of time. If we could sweep the accumulated material away, on this view, then we should find an ancient paradise. The mantle, of course, wipes away an entire strata of forcing, and so if one subscribes to the ancient paradise view, then it seems one should expect the mantle to exhibit some of these highly regular features.”However, this appealing notion is dispelled by one of the basic results of

*set-theoretic geology*: Every model whatsoever is the mantle of some other model of`ZFC`

. “[This] theorem shows that by sweeping away the accumulated sands of forcing, what we find is not a highly regular ancient core, but rather: an arbitrary model of set theory. In particular, since every model of set theory is the mantle of another model, one can prove nothing special about the mantle, and certainly, it need be no ancient paradise.”

## Further reading

Paper by Joel David Hamkins on the multiverse philosophy, and more details on

*V*=*L*Fan fiction by Eliezer Yudkowsky about a team of multiverse-traveling superheros.

`ZFC`

is a formal system about*sets*. How can we even*state*theorems about numbers, such as the binomial formula, or about other mathematical objects such as functions or geometric spaces in`ZFC`

? The answer is by*encoding those objects as sets*, similar to how images can be encoded in binary. For instance, the number zero can be encoded as the empty set {}; the number one can be encoded as the set {{}} which contains exactly one element, namely the encoding of zero; the number two can be encoded as the set {{}, {{}}} which contains exactly two elements, namely the encoding of zero and the encoding of one; and so on.↩︎To verify that there is a

`ZFC`

-proof of the infinitude of primes is an exercise in formal logic, easily solvable by anyone with the relevant training.To verify that there is no

`ZFC`

-proof of 2 + 2 = 5 is a much more subtle issue. One way is to convince oneself that the axioms of`ZFC`

are*true*, and that the logical inferences allowed by`ZFC`

preserve truth. Then the existence of a`ZFC`

-proof of 2 + 2 = 5 would imply that the statement “2 + 2 = 5” is actually true, which is patently absurd. However, this so-called*semantic argument*is predicated on a sufficiently general notion of truth (pertaining to statements about infinite sets), and the existence of such a notion is subject to intense philosophical considerations.A different argument runs as follows: If there would be a

`ZFC`

-proof of 2 + 2 = 5, then, because there is also a (straightforward)`ZFC`

-proof of 2 + 2 ≠ 5,`ZFC`

would prove a contradiction. However, in the almost one hundred years of exploring`ZFC`

, no contradiction has ever been found. Indeed – set theorists haven’t found contradictions in much stronger systems than`ZFC`

. While these observations don’t constitute a proof, they cannot be easily dismissed.↩︎By “reasonable”, we mean that the system is sufficiently powerful to prove a certain minimal amount of arithmetical facts and that the correctness of alleged proofs can in principle be machine-checked (more precisely, that there is a Turing machine which can check the correctness of alleged proofs).

Among the reasonable formal systems are

`PRA`

,`HA`

(Heyting arithmetic),`PA`

(Peano arithmetic),`ZFC`

, various extensions of`ZFC`

, various flavors of type theory,`ETCS`

, and almost all other systems with an established name.Examples for non-reasonable systems include the empty system (which doesn’t have any axioms or inference rules, rendering it incapable of proving any statement at all) or, presupposing a philosophical notion of truth,

*true arithmetic*(which includes every true number-theoretic statement as an axiom and no others). Since there is no algorithm which could check whether any given number-theoretic statement is true, the correctness of alleged proofs in this system cannot be machine-checked.↩︎The independence of this statement is the content of Gödel’s second incompleteness theorem. This theorem states:

*Let**S*be a reasonable formal system which additionally satisfies the “Hilbert–Bernays–Löb condition”, such as`PA`

or`ZFC`

. If there is an*S*-proof of the consistency of*S*, then*S*is inconsistent.Hence a consistent system cannot prove its own consistency.↩︎

This statement should be contrasted with the (very short) statement “BB(1919) = BB(1919)”. There is a trivial

`ZFC`

-proof of this latter statement.↩︎Sometimes logicians study so-called

*infinitary formal systems*, which allow for proofs of infinite length. These systems are both interesting in their own right and also useful to deduce some results about ordinary formal systems, but they play a lesser role in foundations (since they presuppose a notion of infinity, which requires a foundation to begin with) and are not what is meant by*formal system*in this note.↩︎More precisely, the cardinal numbers are indexed by the

*ordinals*. In particular, there is a cardinal number larger than all of ℵ_{0}, ℵ_{1}, ℵ_{2}, and so on: This cardinal number is denoted “ℵ_{ω}”. This cardinal is succeeded by an even larger cardinal, ℵ_{ω + 1}, and this goes on for much, much longer.↩︎Even though most logicians believe that

`ZFC`

is consistent, in arguments which are to be carried out in`PRA`

the consistency of`ZFC`

has to be added as an explicit assumption. This is because, assuming that`ZFC`

is indeed consistent, there is no`PRA`

-proof of this fact: If there would, then there would also be a`ZFC`

-proof of the consistency of`ZFC`

, since`ZFC`

encompasses`PRA`

. But such a proof doesn’t exist by Gödel’s second incompleteness theorem.↩︎This is not quite correct: Cohen’s construction only works in case the initial model

*M*validates`CH`

. Hence, to turn an arbitrary model of`ZFC`

into one which validates ¬`CH`

, we first have to apply Gödel’s construction to obtain a model which validates`CH`

(this works irrespective of whether`CH`

holds in*M*) and then apply Cohen’s construction to that.↩︎