Chapter ∞

# 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:

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

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

3. 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.

1. 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.”)

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

3. Given any set x, there is a set which contains all subsets of x.

And among the logical inference rules of `ZFC` are:

1. From φ ∧ ψ deduce φ.

2. Modus ponens: From φ and φ ⇒ ψ deduce ψ.

3. 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 reasonable3 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 any 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 any 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:

1. (logic) “The system `ZFC` is consistent.”4

2. (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

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

4. (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.

5. (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:

1. Heracla does have a winning strategy.

2. Moreover, any 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.

3. 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 any 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 any 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:

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

2. The first infinite cardinal number: 0. There are 0 many natural numbers.

3. The second-smallest infinite cardinal number: 1.

4. The infinite cardinal number immediately succeeding 1: 2.

5. 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’s not the case that there are only finitely many reals. In fact, we know more: The cardinal 𝔠 is equal to the power 20 (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`.

1. In 1938, Gödel proved that there is no `ZFC`-proof of ¬`CH`.

2. 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’s 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 have been rejected:

1. `CH`”. This proposal is obviously biased toward `CH`. It is also oddly specific, yielding an answer for the question “what is 20?” (namely 1), but leaving the related questions “what is 21?”, “what is 22?” and so on undecided.

2. ¬`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.

3. V = L”. This proposal states that any 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 any 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.) Any 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`.

1. 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 any 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.

2. 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, any model of `ZFC` takes a definitive stance on each statement: For any 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, any given model M of `ZFC` can be thinned down to obtain a smaller model LM in which the continuum hypothesis holds. By forcing, any 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 any model of `ZFC` (since any 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 any 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 any further forcing extension M of M validates φ. That is, starting at M, we can travel to a larger universe M such that any 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 any mathematical statement is either a switch, a button or the negation of a button.

1. 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.

2. 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 any 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.

1. Any 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 any model.)

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

2. Any model M of `ZFC` believes itself to be well-founded, meaning that there is no infinite descending chain of the form x0 ∋ x1 ∋ x2 ∋ ⋯ 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 any model is ill-founded from the perspective of some other model. This phenomenon is the mirage of well-foundedness.

3. 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, any 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.

4. Some models validate the curious maximality principle ◇□φ ⇒ □φ, parenthesized (◇(□φ)) ⇒ (□φ). These worlds are maximal in the sense that any statement which could (after passing to a larger universe) become permanent (hold from then on in any even larger universe) is already permanent.

5. There is a certain Turing machine P, which can be written down explicitly, such that for any function f : ℕ → ℕ, there is some universe in which P computes precisely f. Hence any function whatsoever is computable from the point of view of a suitable universe. The algorithm which P implements is called the universal algorithm.

6. 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. Any 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.”

1. `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.↩︎

2. 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.↩︎

3. 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.↩︎

4. 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.↩︎

5. This statement should be contrasted with the (very short) statement “BB(1919) = BB(1919)”. There is a trivial `ZFC`-proof of this latter statement.↩︎

6. 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.↩︎

7. 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.↩︎

8. 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.↩︎

9. 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.↩︎