Doing Reverse Mathematics

The goal of this part of the seminar is to "do" some reverse mathematics. This isn't so different from doing "normal" mathematics, except that you have one hand tied behind your back, so to speak:

• We can't just "do" induction or comprehension whenever we want. Subsystems of second order arithmetic have restricted induction and comprehension principles, and we need to make sure we respect these restrictions.
• We can't construct any mathematical structures we want. We have to make sure all the structures we want to work with are encodable within second-order arithmetic.

Doing reverse mathematics is also about meta-theory:

• reversals, i.e., proving axioms from theorems;
• separations, i.e., showing that an axiom doesn't follow from the others.

This is a lot, and not really all that reasonable to cover in two hour-long sessions, but to get a taste of all of these components, I'd like to look at a particular reversal:¹

Weak König's Lemma (WKL) is equivalent to Lindenbaum's Lemma (LL) with respect to computable mathematics (RCA₀).

We'll begin with an informal presentation of this reversal (i.e., in "normal" mathematics) and then look at what needs to be done to make this a formal theorem of the meta-theory of RCA₀, the subsystem of second-order arithmetic that captures doing mathematics in the world where all sets are computable.

Weak König's Lemma (WKL) is a fairly intuitive set-theoretic result about infinite binary trees.

Lemma. (WLK) Every infinite binary tree has an infinite path.

Proof sketch. (in "normal" mathematics) Suppose we're given an infinite binary tree 𝑇. Because 𝑇 is infinite, it must have a left subtree 𝑇₀ or a right subtree 𝑇₁. If it has both, then one of these two subtrees is infinite. Without loss of generality, let's say the left subtree 𝑇₀ is infinite. By induction, 𝑇₀ has an infinite path 𝑃 (since 𝑇₀ is an infinite binary tree). Therefore, therefore 0𝑃 (i.e., the path 𝑃 with 0 concatenated to the front) is an infinite path in 𝑇. ∎

A key feature of this proof: in order to extend the path we're building, we need to reason about whether or not a binary tree is infinite. That is, if we're given choice between 𝒯₀ and 𝒯₁, we have to be able to choose one that's infinite. We'll come back to this. First, in order to aid what follows, we'll make WKL a bit more formal.

Definition. Let 𝑏₁, 𝑏₂ ∈ {0, 1}* be finite binary strings. We say 𝑏₁ is an initial segment of 𝑏₂, written 𝑏₁ ≺ 𝑏₂, if there is a binary string 𝑐 such that 𝑏₁𝑐 = 𝑏₂. For example, 01100 is an initial segment of 011000110.

Definition. A tree is a set 𝑇 ⊂ {0, 1}* which is closed under initial segments, i.e., if 𝑏 ∈ 𝑇 and 𝑐 ≺ 𝑏 then 𝑐 ∈ 𝑇.

Definition. A path is a function 𝑃 : ℕ → {0, 1} such that

𝑃(0) 𝑃(1) … 𝑃(𝑘 - 1) ∈ 𝑇

for every 𝑘 ∈ ℕ.

Proof sketch. (WKL, slightly more formal) let 𝑇 be an infinite binary tree. Define 𝑇₀ = { 𝑏 : 0𝑏 ∈ 𝑇 } and 𝑇₁ = { 𝑏 : 1𝑏 ∈ 𝑇 }. Note that both 𝑇₀ and 𝑇₁ are binary trees. And since 𝑇 is infinite, 𝑇₀ or 𝑇₁ is infinite. Suppose without loss of generality that 𝑇₀ is infinite. By induction, there is a path 𝑃′ in 𝑇₀. Define 𝑃(0) = 0 and, for 𝑖 ∈ ℕ⁺, 𝑃(𝑖 + 1) = 𝑃′(𝑖). Then 𝑃 is a path in 𝑇. ∎

Next up, Lindenbaum's lemma (LL).

Definition. A completion of a theory 𝒯 is a theory 𝒯* ⊃ 𝒯 which is consistent:

∄ϕ . 𝒯 ⊢ ϕ and 𝒯 ⊢ ¬ϕ

complete:

∀ ϕ . 𝒯 ⊢ ϕ or 𝒯 ⊢ ¬ϕ

and closed under logical consequence.

Lemma. (LL) Every consistent theory has a completion.

Proof sketch. We might already see that this lemma has a similar flavor to WKL, so let's use WKL to prove it.

Let 𝒯 be a consistent theory and let ϕ₀, ϕ₁,… be an enumeration of the sentences in our language.

Our approach is to build a binary tree in which each branch is a decision as to whether we should add a given sentence ϕ or its negation ¬ϕ to 𝒯. An infinite path then represents a choice for all sentences, giving us a completion.

Now let's fix some notation: we'll write ϕ[0] for ¬ϕ and ϕ[1] for ϕ. For a binary string 𝑏 ∈ {0, 1}ᵏ, we can consider the theory

𝒯[𝑏] = 𝒯 + ϕ₀[𝑏(1)] + ϕ₁[𝑏(1)] + … + ϕₖ[𝑏(𝑘)]

Define the set 𝑇 = { 𝑏 : 𝒯[𝑏] is consistent }. This is an infinite binary tree (you may need to think about this for a second), so by WKL it has a path 𝑃. The set { ϕᵢ[𝑃(i)] : i ∈ ℕ } is a completion of 𝒯. ∎

There's a fair amount of mathematical symbology in the above proof, but it basically says: WKL gives us a way of choosing which sentences to add to our completion. And in the same way that proving WKL requires us to determine which of two trees is infinite, proving LL requires us to determine which of two theories is consistent.

Now, for the main event of this section, the reversal.

Theorem. LL implies WLK.

Proof sketch. Proving a reversal often comes down to a trick, or a "gadget." In this case, we need to define a theory whose completion defines a path through a given tree 𝑇.

We work over a theory with nullary relations (i.e., constants) of the form 𝐿₀, 𝐿₁, … We think of 𝐿ᵢ as "go left at the 𝑖th level." That way, if we get a completion 𝒯* of a theory 𝒯, we can read off a path 𝑃 as

𝑃(i) = 𝟙[𝐿ᵢ ∈ 𝒯*]

That is, a completion is forced to choose a path (because it can't prove both 𝐿ᵢ and ¬𝐿ᵢ, but it must prove one of them).

It then comes down making sure that these choices "keep us in the tree." The trick: our theory describes where not to go to find an infinite path.

Let 𝑏 ∈ {0, 1}ᵏ be a binary string not in 𝑇 and define the sentence:

ψ[𝑏] = ¬(𝐿₀[𝑏(0)] ∧ 𝐿₁[𝑏(1)] ∧ … ∧ 𝐿ₖ[𝑏(𝑘)])

This sentences encodes the statement "don't go down a path which starts with 𝑏." We then define the theory

𝒯 = { ψ[𝑏] : 𝑏 ∉ 𝑇 }

This is a consistent theory (you may need to think about this for a second) so by LL it has a completion 𝒯*. We can define the function

𝑃(𝑖) = 𝟙[𝐿ᵢ ∈ 𝒯*]

Consider the binary string 𝑃(0) … 𝑃(𝑘). By definition of 𝑃,

𝒯* ⊢ 𝐿₀[P(0)] ∧ … ∧ 𝐿ₖ[P(𝑘)]

If 𝑃(0) … 𝑃(𝑘) ∉ 𝑇 then, by definition of 𝒯,

𝒯* ⊢ ¬(𝐿₀[P(0)] ∧ … ∧ 𝐿ₖ[P(𝑘)])

contradicting consistency. Therefore, implies 𝑃(0) … 𝑃(𝑘) ∈ 𝑇. Since 𝑘 was arbitrary, it follows that 𝑃 is a path in 𝑇. ∎

Part of the point here is that 𝑇 may have many paths, but we don't necessarily have a way of finding them. The theory we defined says where not to go, but doesn't give us a way of choosing an actual path. Applying LL forces a choice.

All this tells us that WKL and LL are, in some sense, logically equivalent. Denis Hirschfeldt says that WKL is the "combinatorial core" of LL; it acts like roadmap for what's "actually going on" in the proof. And what amazing─what reverse mathematics tells us─is that this roadmap is shared by many theorems, about compactness in the topological sense, about completeness in the logical sense, about properties of continuous functions, etc., etc.

But there's one aspect of what we've done so far that's very unsatisfying from a mathematical perspective: WKL and LL are already theorems of "normal" mathematics. Sure, we used WKL in a nontrivial way in the proof of LL, and vice versa, but formally defining "in a nontrivial way" is difficult. Ideally, we could worked in a setting where WKL and LL are not theorems but their equivalence still holds. In other words, if 𝒮 ⊬ WLK and 𝒮 ⊬ LL but 𝒮 ⊢ WLK ↔ LL, then we're guaranteed to have used WKL and LL nontrivially in proving the equivalence.

The system that's traditionally used which has this property is RCA₀, a subsystem of second-order arithmetic whose universe of sets is computable in a formal sense. In order to define this subsystem, we need to introduce the machinery of second-order arithmetic.

In this section, we're gonna do something kinda boring, we're gonna give a specification of a logical language, like we do in intro logic courses. I hope that this can be skimmed by those familiar with the concepts, and can be used as a more complete (albeit somewhat pedantic) presentation of second-order arithmetic than is typically given in (graduate) texts on reverse mathematics.

Subsystems of second order arithmetic are defined over the language ℒ₂, which has

binary functions	+, *
binary relation	<
constants	0, 1

and is defined over a set of number variables 𝕍 (written as lowercase letters) and a set of set variables 𝕊 (written as uppercase letters).

The set of terms 𝕋 is defined inductively:

0 ∈ 𝕋	(zero)
1 ∈ 𝕋	(one)
x ∈ 𝕍 implies x ∈ 𝕋	(number variables)
t₁, t₂ ∈ 𝕋 implies (t₁ + t₂) ∈ 𝕋	(addition)
t₁, t₂ ∈ 𝕋 implies (t₁ * t₂) ∈ 𝕋	(multiplication)

For example, (((x + 1) * 0) ∈ 𝕋).² The set of atomic formulas 𝔸 is defined inductively:

t₁, t₂ ∈ 𝕋 implies (t₁ = t₂) ∈ 𝔸	(equality)
t₁, t₂ ∈ 𝕋 implies (t₁ < t₂) ∈ 𝔸	(less-than)
t ∈ 𝕋 and X ∈ 𝕊 implies (t ∈ X) ∈ 𝔸	(element-of)

For example, (1 + y) ∈ X and (a * 0) = a are in 𝔸. The set of formulas 𝔽 is defined inductively:

ϕ ∈ 𝔸 implies ϕ ∈ 𝔽	(atomic)
ϕ₁, ϕ₂ ∈ 𝔽 implies (ϕ₁ ∧ ϕ₂) ∈ 𝔽	(conjunction)
ϕ₁, ϕ₂ ∈ 𝔽 implies (ϕ₁ ∨ ϕ₂) ∈ 𝔽	(disjunction)
ϕ ∈ 𝔽 implies (¬ϕ) ∈ 𝔽	(negation)
x ∈ 𝕍 and ϕ ∈ 𝔽 implies (∀x.ϕ) ∈ 𝔽	(universal number quant.)
x ∈ 𝕍 and ϕ ∈ 𝔽 implies (∃x.ϕ) ∈ 𝔽	(existential number quant.)
X ∈ 𝕊 and ϕ ∈ 𝔽 implies (∀X.ϕ) ∈ 𝔽	(universal set quant.)
X ∈ 𝕊 and ϕ ∈ 𝔽 implies (∃X.ϕ) ∈ 𝔽	(existential set quant.)

For example, ∃X.∀n(n ∈ X → ∃k.(k + k = n)) is a formula in 𝔽 (assuming the translation ϕ → ψ ≡ ¬ϕ ∨ ψ) which expresses that there is a set that contains only even numbers (though not necessarily all even numbers).

Every subsystem of second-order arithmetic we'll look at has the same base set of axioms ℬ:

∀n. 1 + n ≠ 0	(succ. is not zero)
∀m.∀n.(1 + m = 1 + n → m = n)	(succ. is injective)
∀m.0 + m = m	(def. addition)
∀m.∀n.((1 + m) + n = 1 + (m + n))	(def. addition)
∀m.0 × m = 0	(def. multiplication)
∀m.∀n.((1 + m) × n = n + (m * n))	(def. multiplication)
∀m.¬(m < 0)	(zero is minimum)
∀m.∀n.(m < n + 1 ↔ (m < n ∨ m = n))	(discreteness)
∀X.(0 ∈ X ∧ ∀n.(n ∈ X → 1 + n ∈ X) → ∀n(n ∈ X)	(2nd-Ord Induction)

The subsystems we'll consider differ in their induction and comprehension principles. The restriction on these axiom schemas comes from how "complex" of formulas we're allowed to use.

Definition. The ℱ-comprehension schema is the axiom schema consisting formulas of the form

∃X.∀n(n ∈ X ↔ ϕ(n))

where ϕ ∈ ℱ.

Definition. The ℱ-induction schema is the axiom schema consisting of formulas of the form

ϕ(0) ∧ ∀n.(ϕ(n) → ϕ(1 + n)) → ∀n.ϕ(n)

where ϕ ∈ ℱ.

The question then is: what does it mean for a formula to be more or less complex? Borrowing intuitions from computability theory, it comes down to quantifier alternation. The reason for this is deep³ but for our purposes it's sufficient to recognize checking satisfiability of ∃-statements and unsatisfiability of ∀-statements amounts to a search problem. This, in essence, means that the satisfiability problem becomes harder as you alternate quantifiers, which gives us a good measure of formula complexity.

One caveat: if we're using difficulty of the satisfiability problem as a measure of complexity, then quantifier-free is not the "least complex" class of formulas. This is because we easily solve the satisfiability problem for formulas with bounded quantifiers, i.e., when we know exactly how much searching we need to do. We'll use the following notation for bounded quantifiers:

∀(n < k).ϕ ≡ ∀n.(n < k → ϕ)

∃(n < k).ϕ ≡ ∃n.(n < k ∧ ϕ)

We define Σ⁰₀ = Π⁰₀ inductively:

ϕ ∈ 𝔽 and ϕ is quantifier-free implies ϕ ∈ Σ⁰₀

ϕ ∈ Σ⁰₀ and x ∈ 𝕍 and k ∈ 𝕋 implies ∀(x < k).ϕ ∈ Σ⁰₀

ϕ ∈ Σ⁰₀ and x ∈ 𝕍 and k ∈ 𝕋 implies ∃(x < k).ϕ ∈ Σ⁰₀

In other words, we close under bounded-quantifiers. This class of formulas has the property that the satisfaction problem is computable (and with a fairly predictable running time). For example

∃k < (1 + n).(k * m = n)

is a formula in Σ⁰₀ which expresses that m divides n. Note that we don't have to search above n for the value of k such that k * m = n, since n ≤ n * m when m > 0.

We define the sets Σ⁰ᵢ₊₁ and Π⁰ᵢ₊₁ inductively:

ϕ ∈ Π⁰ᵢ and x ∈ 𝕍 implies ∃x.ϕ ∈ Σ⁰ᵢ₊₁

ϕ ∈ Σ⁰ᵢ and x ∈ 𝕍 implies ∀x.ϕ ∈ Π⁰ᵢ₊₁

For example, a formula in Π⁰₅ is of the form ∀x.∃y.∀z.∃w.∀q.ϕ where ϕ has only bounded quantifiers.

All of this is in the interests of (this corollary of) Post's Theorem.⁴

Theorem. A set 𝑋 is computably enumerable if and only if it is definable by a Σ⁰₁ formula and is computable if it is also definable by a Π⁰₁ formula.

This theorem connects definability with computability. Sets which are definable by both a Σ⁰ᵢ and a Π⁰ᵢ formula are called Δ⁰ᵢ. These set classifications are part of what is called the arithmetic hierarchy, another term worth searching if you're interested in the connections between computability and definability.

The last thing we need to define RCA₀ is a special form of comprehension.

Definition. The Δ⁰ᵢ-comprehension schema is the axiom schema consisting formulas of the form

∀n.(ϕ(n) ↔ ψ(n)) → ∃X.∀n(n ∈ X ↔ ϕ(n))

where ϕ ∈ Σ⁰ᵢ and ψ ∈ Π⁰ᵢ.

You may be thinking: why can't we define Δ⁰ᵢ-comprehension as a ℱ-comprehension schema like above? This is because Δ⁰ᵢ is not a set of formulas, where as Σ⁰ᵢ and Π⁰ᵢ are.

Finally, we have enough machinery to define RCA₀:

RCA₀ ≡ ℬ + Σ⁰₁-induction + Δ⁰₁-comprehension

In light of the discussion above, this means RCA₀ is the subsystem of second-order arithmetic in which we can do comprehension for computable sets and induction for singly-existential statements.

(This is where we got in session 2)