Previous: Infinitely Large Primes

We’ve seen how to use Łoś’s theorem to prove properties of hyperstructures. We’ve also seen how to use it to prove limitations of first-order logic. Today we’re going to see a major meta-logical application of Łoś’s theorem: proving the compactness theorem! In my opinion, this proof is the most elegant proof of first-order compactness out there. We’ll also see a few other meta-logical results relating to ultraproducts. However, if you’re just interested in learning about more properties of the hypernaturals, then you can skip this post without missing out on anything major!

What is compactness?

A logic is compact if any finitely satisfiable set of sentences is satisfiable. If somebody hands you an infinite set of sentences, and you know how to construct a model to satisfy any finite subset of these sentences, then you can conclude that there must be a model that satisfies all those sentences at once. Compactness is interesting because it allows you to prove surprising results (like that true arithmetic has nonstandard models) from very obvious facts (that any finite set of natural numbers has an upper bound). It also lets you prove the completeness theorem, which says that what you can prove from first-order axioms is exactly what logically follows from those axioms.

Countable Theories

First we’ll prove the compactness theorem for countable theories. I’m including it because it’s conceptually simpler than the proof of the general case. However, it’s not necessary for understanding the general proof, so if you just want to see that you can jump ahead to the next section.

Suppose T is a countably infinite theory that’s finitely satisfiable.
T is countable, so choose an enumeration of T’s sentences: T = {φ₁, φ₂, φ₃, …}.

T is finitely satisfiable, so there’s a model that satisfies φ₁. Call this model M₁.
There’s also a model M₂ that satisfies both φ₁ and φ₂.
And a model M₃ that satisfies φ₁, φ₂, and φ₃.
And so on.

Take the ultraproduct of (M₁, M₂, M₃, …) and call it M.
For every n in N, φ_n is satisfied by all models from M_k on. (For instance, φ₄ is satisfied by M₄, M₅, M₆, and so on.)
This is a cofinite set, so (by Los’s theorem) φ_n is satisfied by M.

But φ_n was a totally arbitrary sentence inside T. So M satisfies all of T!

So T is satisfiable. But not only do we get this result, we also have an explicit example of a model that satisfies all of T, which we can start analyzing to prove other properties of.

Compactness for any theory

The proof uses a fact that I haven’t proven yet: If X is a set whose every finite subset has nonempty intersection, then there’s some ultrafilter that extends it. Luckily, it’s easily proven. Start by closing X under supersets (notice that every finite subset of X still has nonempty intersection). Then close it under intersection, and you now have a filter that extends X. (Verify that this really is a filter for bonus points!) And in Part 3 of this series we proved that every filter has an ultrafilter extension. So there’s an ultrafilter U that contains X.

Alright, on to the proof.

Let L be any first-order language and S be any set of L-sentences that is finitely satisfiable. We’re going to build an ultraproduct that satisfies S. This requires three ingredients: an index set I, and a set of L-structures (M_i)_i∈I indexed by I, and an ultrafilter U on I. We’ll go through these one at a time.

1. The index set I

I will be the set of all finite subsets of S. This is interestingly different from what we’ve seen before. Previously our indices were always natural numbers. But here our indices are sets of sentences in the language of the structure! This means that we’re going to end up looking at models that look like M_{φ,ψ,θ}, where φ,ψ, and θ are sentences in S.

2. The component structures (M_i)_i∈I

So, our indices are finite subsets of S. And S is finitely satisfiable. So for each index F (each finite subset of S), there’s a model M_F that satisfies everything in F. This is how we get our component structures.

For instance, if φ, ψ, and θ are three sentences in S, then {φ,ψ,θ} is an index, and M_{φ,ψ,θ} is any structure that satisfies φ∧ψ∧θ. ∅ is also a finite subset of S, so it’s an index and has a corresponding structure M_∅, which can be any L-structure whatsoever.

To briefly rehash, the important feature of our choice of component structures is that they have the following property: For any finite subset F of S, M_F ⊨ φ for every φ in F.

3. The ultrafilter U on I

The choice of ultrafilter here is really important. Our component structures were carefully chosen so that each structure satisfies the finite set of sentences that is its index. This guarantees us that for any sentence φ in S, the set of component structures whose indices contain φ all satisfy φ. This is the set of component structures whose indices are finite supersets of {φ}.

Remember that we’re ultimately aiming to show that each φ is satisfied by the ultraproduct model. By Łoś’s theorem, it suffices to show that the set of component models that satisfy φ is U-large (is in our chosen ultrafilter). Conclusion: we want to make sure that for any φ in S, the set of all finite supersets of {φ} is U-large.

How do we know that there exists any ultrafilter that for every φ contains the set of all finite supersets of {φ}? We apply the finite intersection property! Denote by S_F the set of all finite supersets of F. Take any finite set of singletons {{φ₁}, {φ₂}, {φ₃}, …, {φ_n}}. Is the intersection of S_{φ1}, S_{φ2}, S_{φ3}, …, S_{φn} empty? No: the set {φ₁, φ₂, φ₃, …, φ_n} is in of all of them! So the set { S_{φ} | φ ∈ S } has the finite intersection property, and thus there’s some ultrafilter that extends it. And that’s the ultrafilter we want!

Finalizing things

We’ve now got everything we need to build the structure that satisfies S. Take the ultraproduct Π(M_F)_F∈I/U. This structure satisfies S. Why?

Consider any φ in S. By Łoś’s theorem, φ is satisfied if a U-large set of the component models satisfy φ. And we know that a U-large set of component models satisfy φ, because φ is satisfied in every model whose index contains φ, i.e. the set of models whose indices are supersets of {φ}. So we’re done!

More implications

The remainder of this post will not be necessary to understand the rest of the series. I want to present a few miscellaneous meta-logical results that relate to ultraproducts that don’t quite fit anywhere else.

First: every finite structure is its own ultrapower. Let’s see why.

Suppose M is a finite structure. Denote by M^I/U the ultrapower of M over any arbitrary index set I. First of all, we can easily see that M and M^I/U have the same cardinality: if |M| = n for some finite n, then there’s a sentence affirmed by M that says “There are exactly n distinct things”. For instance, if M has exactly two elements, then M ⊨ ∃x ∃y (x≠y ∧ ∀z (z=x ∨ z=y)). Łoś tells us that M^I/U also affirms this sentence, so M^I/U also has exactly n distinct things.

Furthermore, any finite structure M of size n can be categorically specified up to isomorphism by a single first-order sentence of the form ∃x₁∃x₂…∃x_n (∀x (x = x₁ ∨ … ∨ x = x_n) ∧ (x₁ ≠ x₂ ∧ … x_n-1 ≠ x_n) ∧ ψ(x₁, …, x_n) ], where ψ specifies the behavior of all relation, function, and constant symbols. Here’s an example for a simple finite structure:

We have four elements, so we use four variables, x₁ x₂ x₃ and x₄ to specify the structure.

Since M satisfies this sentence, Łoś tells us that M^I/U also affirms this sentence, meaning that M^I/U and M are isomorphic. So in other words, every finite structure is its own ultrapower (up to isomorphism). 

What about infinite structures? The situation is the exact opposite! No infinite structure is its own ultrapower.

Let M be an infinite structure and *M be its ultrapower. Add a constant for every object in M. The ultraproduct construction tells you how constants from M translate to constants in *M: for each constant c, if c refers to m in M, then c refers to [m, m, m, …] in *M.

Now we want to construct a new element of *M by writing a sequence that contains infinitely many elements of M, each appearing only finitely many times. Crucially, here we must assume that the index set is the same size as or smaller than M! If we have too many indices, then we aren’t going to be able to refer to each element in our original model only a finite number of times. So for instance, this argument won’t work for the ultrapower ℕ^ℝ/U.

Now, this new element we’ve constructed is distinct from each constant, because they only agree in finitely many place. The constants covered all of M, but they don’t cover all of *M. So M and *M are not isomorphic!

And some more

These next results relate ultraproducts to compactness and definability.

Fix a first-order language L and consider a class C of L-structures. Say that a set of sentences X is C-satisfiable if there’s a structure in C that satisfies all of X. We say that C is compact if for every set A of L-formulas, finite C-satisfiability implies C-satisfiability. This is a different notion from the compactness discussed in the compactness theorem; the ordinary compactness theorem tells us that for every first-order language L, the class of all L-structures is compact. But it doesn’t tell us anything about other more restricted classes of L-structures.

For instance, let L be the language with an empty signature (no constants, functions or relations). This language is extremely simple: essentially the only contentful sentences you can make are about finite cardinalities. E.g. you can say “there are at least three things” with “∃x ∃y ∃z (x≠y ∧ x≠z ∧ y≠z)” and “there are at most three things” with “∀x ∀y ∀z ∀w (x=y ∨ x=z ∨ x=w ∨ y=z ∨ y=w ∨ z=w)”.

Now let C be the class of all finite L-structures. Is this class compact?

If you said no, good job! For a finite n, let φ_n be the sentence that says “there are at least n things”, and consider the set of sentences A = {φ₁, φ₂, φ₃, …}. Every finite subset of A is satisfiable by a finite L-structure, but the entire set is clearly not satisfiable by any finite L-structure.

What if we add to C a single countably infinite L-structure M? Then our previous construction no longer works; the entire set A is now satisfied by this new member of C.

Alright, so that’s compactness for classes of structures. The relationship between this and ultraproducts is the following:

Any class of models that’s closed under ultraproducts is also compact.

For any language L and any finite n, consider the class of all L-structures of size n. The ultraproduct of a bunch of size-n L-structures is itself a size-n L-structure, so this class is closed under ultraproducts. And therefore it’s compact!

Now consider our example of the class of all finite structures in the language with empty signature. This was not compact, meaning that it cannot be closed under ultraproducts. This means that the ultraproduct of a bunch of finite structures is not necessarily finite! In particular, suppose that M₁ has one element, M₂ has two elements, M₃ has three elements, and so on. Then the ultraproduct of (M₁, M₂, M₃, …) will be an infinite model. We can also see this by applying Łoś’s theorem to the set of sentences {“There is at least 1 thing.”, “There are at least 2 things.”, “There are at least 3 things.”, …}.

A class C of L-structures is first-order definable if it is the set of all models of some set of L-sentences. First-order definability also relates to ultraproducts, in the following way:

If a class of L-structures is first-order definable, then it’s closed under ultraproducts.

The converse of this is that any class of structures that’s not closed under ultraproducts is not definable.

For any L, the class of finite L-structures is not closed under ultraproducts, so it’s not definable. This tells us that “finiteness” is not first-order definable.

The class of all models of PA is first-order definable, so it’s closed under ultraproducts. This means that even if you take an ultraproduct of infinitely many nonstandard models of PA, you still end up with a model of PA!

Okay, next up we come to the most exciting and powerful property of ultraproducts: countable saturation!

Next: All About Countable Saturation

Previous: Ultraproducts and Łoś’s Theorem

Let’s quickly review what we’ve learned so far.

The hypernaturals, *ℕ, are the ultrapower of ℕ with index set I = ℕ. The first-order language in use here is the language of Peano arithmetic: L = <{0}, {<}, {S,+,⋅}>. Łoś’s theorem from the last post tells us that *ℕ and ℕ are elementarily equivalent. In other words:

For every first-order sentence φ, ℕ ⊨ φ if and only if *ℕ ⊨ φ.

This tells us that *ℕ is not just a model of Peano arithmetic, which is a popular incomplete theory of arithmetic. It’s a model of TRUE arithmetic, the complete set of all first-order truths of arithmetic! Given the insane uncomputability of this theory (If T₀ is a Turing machine, and T_n+1 is a Turing machine with an oracle for T_n‘s halting problem, then true arithmetic is not computable by T_n for any finite n), it’s pretty remarkable that we have an explicit example of one of its nonstandard models!

Review over! Now let’s begin with some basic applications of Łoś’s theorem. We can say that a number x is prime in first-order logic: isPrime(x) can be translated as ∀y ∀z (y⋅z = x → (y = 1 ∨ z = 1)). We can also refer to any finite natural number by applying the successor function enough times to zero (e.g. 2 = S(S(0))). Since “2 is a prime” is first-order expressible and ℕ affirms its truth, so must *ℕ.

But remember that in *ℕ, 2 is the equivalence class of the sequence (2,2,2,2,…). Is it really true that for any a, b ∈ *ℕ, if a⋅b = [2,2,2,2,…] then one of a and b is 2 and the other is 1? This is probably not immediately obvious… What about (2,1,2,1,2,1,…)⋅(1,2,1,2,1,2,…)? Certainly this product is (2,2,2,2,…), but neither (2,1,2,1,2,1,…) nor (1,2,1,2,1,2,…) look very much like (1,1,1,1,…) or (2,2,2,2,…).

In fact they are the same. Let’s prove this very generally. Suppose p is any finite prime number, and consider the hypernatural [p, p, p, …], corresponding to the ordinary natural number p. Consider any two hypernaturals a and b such that a⋅b = p. We can choose representative sequences (a₀, a₁, a₂, …) and (b₀, b₁, b₂, …) such that their product is (p, p, p, …). In other words:

(a₀⋅b₀, a₁⋅b₁, a₂⋅b₂, …) = (p, p, p, …)

Since p is prime, we know that for each k, either (a_k = p and b_k = 1) or (a_k = 1 and b_k = p). Consider the set of indices A = { k ∈ ℕ | a_k = p }. Since each a_k is either 1 or p, the complement ℕ\A is equal to { k ∈ ℕ | a_k = 1 }. Now, since U is an ultrafilter, either A or ℕ\A is in U. In the first case, [a₀, a₁, a₂, …] = [p, p, p, …] = p. And in the second case, [a₀, a₁, a₂, …] = [1, 1, 1, …] = 1. The same argument applies for [b₀, b₁, b₂, …]. So for any two hypernaturals a and b such that a⋅b = p, both a and b are either 1 or p.

Okay, so we’ve proven that 2 is a prime number. That’s a relief! Let’s do something a bit more substantial now.

Consider the following first-order sentence: ∀x ∃y (y > x ∧ isPrime(y)). This sentence says that there are infinitely many primes, and (as first proven by Euclid) ℕ affirms its truth. So *ℕ ⊨ ∀x ∃y (y > x ∧ isPrime(y)).

Okay, so there are infinitely many hypernatural primes. This doesn’t sound so exciting… after all every ordinary prime is a hypernatural prime too, so didn’t we already know this? Sure, but if we look closely at what exactly the sentence says, it turns out that we get a bit more out of it than just that.

∀x ∃y (y > x ∧ isPrime(y)) says that for every number x, there’s a larger prime number y. Applying this in *ℕ, this means that all hypernatural numbers, even the infinitely large ones, have larger primes. Thus there are nonstandard primes in *ℕ, and in fact infinitely many nonstandard primes.

See if you can think of one for yourself before reading on.

.

.

.

Ok, here’s one: P = [2, 3, 5, 7, 11, 13, 17, …]. This sequence is eventually always larger than the sequence of any standard prime p = [p, p, p, p, …], so P is a nonstandard number. And P is also prime! The argument is very similar to the previous argument: take any two hypernaturals a and b such that a⋅b = k. Consider any representative sequences for a and b whose product is the sequence (2, 3, 5, 7, 11, …), and then consider the set of indices at which 1 appears in a’s sequence. If this set is in the ultrafilter, then a = 1 and b = k. If not, then a = k and b = 1.

Now, a challenge for you: construct an infinite ascending sequence of nonstandard primes starting at P.

And another challenge: construct an infinite descending sequence of nonstandard primes starting at P!

Hint for the first challenge: think about the hypernatural [3, 5, 7, 11, 13, 17, …].

Hint for the second challenge: think about the hypernatural [2, 2, 3, 5, 7, 11, …], or [2, 2, 3, 3, 5, 5, 7, 7, …].

While infinite ascending sequences of numbers can exist in ℕ, an infinite descending sequence of numbers can not, so we’ve identified a concrete difference between *ℕ and ℕ. And by Łoś’s theorem, this difference must not be first-order expressible in the language of PA. In other words, “there are no infinitely descending sequences of numbers” cannot be expressed in first-order.

This illustrates another usage of Łoś’s theorem: rather than starting with a first-order sentence that’s true of ℕ and using it to learn about *ℕ, we can start with some facts about *ℕ to learn about limitations of first-order logic!

Alright, what else? Suppose we have a hypernatural number k that has a sequence (k₀, k₁, k₂, …) such that some formula φ(x) holds of cofinitely many elements of the sequence. Then φ(x) also holds of k. This gives us some hypernatural numbers with awfully strange properties.

Consider the hypernatural E = [1, 2, 4, 8, 16, 32, 64, …]. Now consider the formulas that say “x is divisible by 2”, “x is divisible by 4”, “x is divisible by 8”, “x is divisible by 16”, and so on. Each of these formulas holds true of all but some initial segment of the sequence (1, 2, 4, 8, 16, 32, 64, …). This means that each of these sentences hold true of E. In other words, E is divisible by 2, by 4, by 8, by 16, by 32, and so on forever. In other words, E can be divided by 2 forever!

But how exactly does this work? The sequence (1, 2, 4, 8, 16, 32, 64, …) starts with a 1. So how could we divide it by 2? The key is to remember that hypernaturals are equivalence classes of sequences, not sequences. So any time we run into trouble with a particular sequence, we can jump to an equivalent sequence that solves our problem. To divide (1, 2, 4, 8, 16, 32, 64, …) by 2, we jump to the equivalent sequence (2, 2, 4, 8, 16, 32, 64, …), which is still a representative of E. Now we can divide by 2: E/2 = [1, 1, 2, 4, 8, 16, 32, …]. To divide by 2 again, we jump to the sequence (2, 2, 2, 4, 8, 16, 32, …). Then we get E/4 = [1, 1, 1, 2, 4, 8, 16, …]. We can keep doing this as many times as we like, and thus E is infinitely even! (Notice: another infinitely descending sequence of numbers.)

We can use a similar trick to construct a number that’s divisible by every standard natural number: simply consider M = [0!, 1!, 2!, 3!, 4!, 5!, …]. For any standard natural number n, the set of indices at which the sequence (0!, 1!, 2!, 3!, 4!, 5!, …) can be divided by n is cofinite. So M can be divided by n as well!

This lets us run a kind of fun argument. Remember how Euclid’s original proof of the infinitude of primes went? Imagine that there are finitely many primes. Then we can take their product and add 1, and we’ve constructed a new prime. Well, in *ℕ we can find multiples of infinite sets of numbers! One multiple of all standard prime numbers is [2, 2⋅3, 2⋅3⋅5, 2⋅3⋅5⋅7, 2⋅3⋅5⋅7⋅11, …] = [2, 6, 30, 210, 2310, …]. This is divisible by each standard prime, and is also not twice-divisible by any prime (e.g. you can’t divide it by 4). (Interestingly, it’s not the product of all finite primes; because it’s also divisible by some infinite primes! See if you can think of one such infinite factor.) Now add 1 to get X = [3, 7, 31, 211, 2311, …]. X cannot be divisible by any standard prime, meaning that it’s either divisible by a nonstandard prime, or is itself a nonstandard prime. So just as Euclid’s original proof showed that there can’t be only finitely many primes, this proves that there can’t be only finitely large primes.

Alright, let’s get a little more wild. In ℕ we know that for any number x, there’s a number y that’s divisible by all positive numbers up to and including x (for instance, y = x!). In other words, ℕ ⊨ ∀x ∃y ∀z ((z ≠ 0 ∧ z ≤ x) → (y div by z)), where “y div by z” is shorthand for ∃u (z⋅u = y). In other words, ℕ affirms that for every initial segment S with maximum element x, there’s a number that’s divisible by everything in S (for shorthand we can call this number “a multiple of S”).

Invoke Łoś: anything true in ℕ must also be true in *ℕ. This means that every initial segment of hypernaturals with a maximum element has a multiple! (See if you can do better: can you also prove that every initial segment of hypernaturals with a max has a product? What about initial segments without maximum elements?) For instance, there’s a number that’s divisible by every hypernatural number up to and including the hypernatural K = [0,1,2,3,4,5,…].

What other first-order properties does ℕ have? Here’s one: ℕ is not dense. We can express this by saying ¬(∀x ∀z (x < z → ∃y (x < y ∧ y < z)). We can do better: ℕ affirms that ∀x ¬∃y (x < y ∧ y < S(x)). In other words, for any number x, x and its successor are counterexamples to density (they’re distinct numbers that have nothing between them).

So this must be true of hypernaturals as well! For any hypernatural, say K = [0,1,2,3,4,5,…], there’s no hypernatural between it and its successor K+1 = [1,2,3,4,5,6,…].

However, even though the hypernaturals are not dense, they do contain a dense subset! In fact, we can say something even stronger: no segment of the hypernaturals are dense, but nonetheless *ℕ has a dense subset!

Here’s a rough sketch for how to construct this dense subset. Take any nonstandard hypernatural, say K = [0, 1, 2, 3, 4, 5, …]. For any nonzero finite m, we can construct a hypernatural K_m a finite distance from K, such that K’ is divisible by m. Now we can construct n⋅K_m, and then (n/m)⋅K_m. The set { (n/m)⋅K_m | n, m ∈ ℕ } is a subset of the hypernaturals, and it has the order type of the positive rationals!

What other unusual hypernatural numbers can you discover?

Next, we will prove the compactness theorem using ultraproducts. It’s definitely the prettiest proof of compactness out there, so stay tuned!

Ultraproducts and Compactness

The analytic tableaux (also called truth tree) style of proof system is really nice. The tree structure tends to resemble the actual process of mathematical reasoning better than the Hilbert-style linear proof systems, and I find that the formal proofs are much easier to follow. For first-order logic (without equality), the system involves four new inference rules to deal with quantifiers. There are a few different logically equivalent choices for these rules, but here is my favorite:

Universal instantiation ∀
∀x φ(x)
⊢
φ(t)
(where t is any closed term – any term without free variables)

Existential instantiation ∃
∃x φ(x)
⊢
φ(a)
(where a is any new constant)

Negated universal ¬∀
¬∀x φ
⊢
∃x ¬φ

Negated existential ¬∃
¬∃x φ
⊢
∀x ¬φ

The instantiation rules are actually quite interesting. Suppose that you’re working in the language of ZFC. ZFC has no constant or function symbols, only a single binary relation symbol: ∈, interpreted as “is an element of”. This seems to raise a problem for using the instantiation rules. For universal instantiation, we can only apply it to closed terms. But a language with no constants has no closed terms! And looking at existential instantiation, there’s a similar problem: we’re supposed to derive φ(a), where a is a new constant, but our language has no constants!

So what’s up? Does the standard first-order analytical tableaux approach not work for simple languages like ZFC? Insofar as ZFC is a shining beacon of what first-order logic can accomplish, this is a little disconcerting.

Actually, the instantiation rules work exactly as stated for ZFC. The subtlety in their interpretation is that when running proofs, you are allowed to (and in fact, often must) expand the language. So when you do existential instantiation, you don’t choose a constant symbol that already exists inside your language. Instead, you add a totally new constant symbol to your language, and then declare that φ holds of this symbol. Similarly, you can do universal instantiation in a language with no closed terms, simply by expanding the language to include some constants.

Now, if we’re expanding the language in the course of the proof, then who’s to say that in the end our proof will still be valid for our original language? Well, suppose we’re working in some minimal language L that has no constants. Let T be our background theory (the set of non-tautologies that we’re taking as assumptions). When we do existential instantiation, we always create a new constant. Let’s call it a. We then expand the language into L’ = L ⋃ {a}, and we expand our assumptions to T’ = T ⋃ {φ(a)}. When we do universal instantiation, we either use an existing closed term or create a new one. In the second case, we create a new constant b and form a new language L’ = L ⋃ {b}. We also expand our assumptions to a new set T’ = T ⋃ {φ(b)}.

The important thing to note is that we haven’t done anything that invalidates any models of T! If T originally contained a sentence of the form ∀x φ(x), then adding c and declaring φ(c) doesn’t conflict with this. And if T originally contained a sentence of the form ∃x φ(x), then in every model of T at least one thing satisfies φ. So when we add a new constant c, that constant can just refer back to any of these φ-satisfiers.

You might think: “But hold on! How can we be sure that it’s safe to just add new constants? Couldn’t we expand the domain too much, in a way that’s inconsistent with our original theory?” The answer to this is that the domain doesn’t have to expand to accommodate new constants! These constants can refer to existing elements of the domain. For instance, suppose T contains six existential statements and a sentence that says there are exactly five objects. Each time we run existential instantiation on one of the six existential sentences, we create a new constant. So we’ll get six new constants. But these constants can refer to the same value! And since our theory already says that there are five objects, the models of our expanded theory will also contain exactly five objects, meaning that in every model of our original theory, the new constants will refer to elements of the domain that already exist. No domain expansion!

Ok, but how do we know that there isn’t some very complicated sentence ψ that was originally true in every model of T, but becomes false in some models of T’? To fully prove that this never happens, we could do induction over all sentences in the language, showing that any sentence that is entailed by T is also entailed by T’. But considering the details of the expansion process, and trying to come up with ways that the expansion might fail, is a good way to get an intuition for why this proof system works.

I’ll close with a few examples of using analytic tableaux to prove basic results in PA and ZFC. Think of this as a proof of concept! (Each of these proofs also uses some rules regarding equality, which are obvious enough despite that I haven’t explicitly defined them).

First, we show that PA proves ∀x (0 + x = x). This is nontrivial, despite that ∀x (x + 0 = x) is an axiom!

Next, a proof from ZFC that the empty set exists and is unique:

Now a proof from PA that addition is commutative. This one is shockingly complicated for such a simple concept, and requires three uses of induction, but this goes to show how basic the axioms of PA really are! If you look closely, you’ll also notice that this proof replicates the proof of ∀x (0 + x = x) from above!

Final example, here’s a PA proof that no number is its own successor. This rules out nonstandard models of arithmetic with one nonstandard number!