This is a transcription of notes from a talk I gave on November 1, 2013 to the interdisciplinary logic seminar at the University of Connecticut. I gave a general introduction to Reverse Mathematics and then spoke about my work with Alaeddine Saadaoui and Sean Sovine on the logic of implications between subsystems in in Reverse Math. This post is essentially my speaking notes for the talk.
Part 1. Reverse Mathematics
Reverse Mathematics is a program in mathematical logic that analyzes theorems of ordinary mathematics, with two goals:
 Determine which axioms are required to prove particular theorems.
 Examine the internal combinatorial character of particular theorems from the perspectives of computability and formal arithmetic.
The method to achieve these goals is to use secondorder arithmetic to study “countable analogues” of theorems. The idea is that we have a base system, $B$, a theorem $T$, and an axiom $A$, all in the same language, such that neither $T$ nor $A$ is provable in $B$. We show that $T$ is provable from $B$ together with $A$, and that $A$ is provable from $B$ together with $T$. The first of these is an ordinary mathematical proof, with care to verify that the methods can be formalized in $B$ and $A$. The second proof is known as a reversal. When both the proof of $T$ from $A$ and the reversal have been proved, we see that $T$ and $A$ are equivalent, relative to $B$. Thus $A$ is necessary for any proof of $T$ over $B$ in the precise sense that any other axiom which proves $T$ when added to $B$ will also imply $A$.
Some details
We formalize $B$, $T$, and $A$ within “second order arithmetic”, $Z_2$, which we treat as a twosorted firstorder theory.
Syntax
The language of secondorder arithmetic, $L_2$, has two sorts of objects: “numbers” and “sets”, with:
 Binary function symbols for addition and multiplication
 Constant number symbols for $0$ and $1$
 Equality and order ($<$) relation symbols for numbers
 A set membership relation
Semantics
We use Henkinstyle semantics. An $L_2$structure $M$ is thus of the form
$$ (\mathbb{N}^M, S^M, +^M, \times^M, 0^M, 1^M, <^M, \in^M)$$
where $(\mathbb{N}^M, +^M, \times^M, 0^M, 1^M, <^<)$ is a structure in the language of firstorder Peano arithmetic, and $S^M \subseteq P(\mathbb{N}^M)$. If $(\mathbb{N}^M, +^M, \times^M, 0^M, 1^M, <^<)$ is the standard model of Peano arithmetic then $M$ is called an $\omega$model.
Notice that no equality symbol for sets is included. One reason for this omission is that, when we work in secondorder arithmetic, we think of each set that exists in a model as "decidable" in some sense. This is closely related to the ability to use any set in a model as a parameter to form additional sets. Sets that are definable over a model, but don't exist in the model, cannot be used as parameters in this way.
For two sets $A$ and $B$, we have
$$
A = B \quad \equiv \quad (\forall n)[n \in A \leftrightarrow n \in B].
$$
Even if we are able to decide membership in $A$ and $B$ separately, we cannot in general decide if they are extensionally equal.
Axioms
The standard base system, $\mathsf{RCA}_0$, has three kinds of axioms
 $\mathsf{PA}^$, the finite list of axioms for a discrete ordered semiring.
 A weak set of set existence axioms (formally, the $\Delta^0_1$ comprehension scheme)
 A weak set of induction axioms (formally, the $\Sigma^0_1$ induction scheme).
In what senses is $\mathsf{RCA}_0$ weak?
 It has an $\omega$model in which all sets are computable.
 Each computable function that is provably total in $\mathsf{RCA}_0$ is primitive recursive (in fact, $\mathsf{RCA}_0$ is $\Pi^0_2$ conservative over $\mathsf{PRA}$).
 The proof theoretic ordinal of $\mathsf{RCA}_0$ is $\omega^\omega$.
However, $\mathsf{RCA}_0$ is strong enough to prove lemmas that enable us to encode mathematical objects in ways similar to computable and constructive mathematics.
For example, within $\mathsf{RCA}_0$, we have natural defintions of “$R$ is a countable commutative ring” and “$X$ is a complete separable metric space”.
Example of a reverse mathematics result
The result will use three principles:
 Every countable commutative ring has a maximal ideal.
 Every bounded, increasing sequence of rational numbers converges to some real number.
 ACA: If $\phi(n)$ is an arithmetical formula (that is, a formula without any set quantifiers) then the set $\{n : \phi(n)\}$ exists.
With those definitions, we have:
Theorem. Principles 1, 2, and 3 are equivalent over $\mathsf{RCA}_0$.
Many theorems of this sort are known.
Big five subsystems
An interesting phenomenon is that many (countable analogues of) mathematical theorems are equivalent to one of five particular systems, each of which is closely related to a philosophical program.
Acronym  Stands for  Philosophical program 

$\mathsf{RCA}_0$  Recursive comprehension axiom  “computable mathematics” 
$\mathsf{WKL}_0$  Weak König’s Lemma  “finitistic reductionism” 
$\mathsf{ACA}_0$  Arithmetical Comprehension Axiom  “predicativism” 
$\mathsf{ATR}_0$  Arithmetical Transfinite Recursion  “predicative reductionism” 
$\Pi^1_1\text{}\mathsf{CA}_0$  $\Pi^1_1$ comprehension  “impredicative analysis 
$\vdots$  $\vdots$  $\vdots$ 
$Z_2$  Full secondorder arithmetic 
Simpson has written about the role of these systems in the larger
“Gödel hierarchy”.
Historical development
Another way to find a perspective on Reverse Mathematics is to look at earlier research programs and historical developments from which it grew. These are arranged below in general order, but in many cases the programs overlapped both in chronology and in dependency of ideas. This table is a preliminary list that is not in any way complete, and I apologize for any omissions.
Pre1900  Early work on formal logic 
1900 ↓ ↓ 
Continued development of formal logic 
Foundational programs (Many, e.g. Hilbert, Brouwer, Weyl) 

Computable and constructive analysis (Many, e.g. Bishop, Markov) 

Proof theory (Many, e.g. Kleene, Kreisel, Feferman) 

Type theory, Higher order arithmetic (Many, e.g. Feferman, Friedman) 

1974, 1976 
“Big Five” subsystems proposed Friedman 
↓  Research in reverse mathematics and related areas e.g. formal arithmetic, computability, and proof theory. (Many researchers) 
1999  Subsystems of secondorder arithmetic Simpson 
Reverse Mathematics as a separate field of inquiry was established by Friedman (1974, 1976). Subsequent work by many people, including Simpson and several PhD students among others, was collected into Simpson’s 1999 monograph, which immediately became the standard reference for the field. The results collected there show it was clear by 1999 that Reverse Mathematics provides a useful framework for organizing many results in computable mathematics and proof theory using secondorder arithmetic as a tool.
A significant development in the last 15 years has been the discovery of mathematical theorems that are not equivalent to any of the big five subsystems. Examples include:
 Ramsey’s theorem for pairs (Seetapun, Cholak/Jockush/Slaman)
 Results from model theorem (Hirschfeldt/Shore/Slaman)
 A version of the finite intersection principle from set theory (Dzhafarov/M.)
These examples required the development of new techniques for constructing models, based on the the method of “forcing” used in many other areas of mathematical logic.
Examples are also known of theorems that are stronger than any of the big five subsystems, but still provable in $Z_2$. The large number of known results inspired the development of the Reverse Mathematics Zoo by Dzhafarov.
Now, in 2013, I think it can be safely said that Reverse Mathematics has become a mature field. We have powerful model construction techniques, a solid collection of previous results, but at the same time there are many nontrivial and interesting problems that remain (I will post on some of these in a separate blog post).
Part 2. The modal logic of Reverse Mathematics
One difficulty with the proliferation of Reverse Mathematics results is that it can be difficult to keep track of them. Determining whether a question is open requires an extensive literature survey.
It would be nice to have a software system to record known results, which could tell whether a particular result is already known (perhaps implicitly) in the literature. The Reverse Mathematics Zoo is an initial version of such a system. A vital component of these systems is a sort of automated theorem prover that can combine results from separate papers in a routine way to produce a more complete description of the knowledge implicit in the literature.
To make progress, one key question is to characterize the underlying logic of implications between subsystems. This characterization might allow for a correctness proof of the theorem proving component of the software, and might help with creating an efficient implementation.
For convenience, the remainder of the talk will use a convention in which the base subsystem is incorporated into each subsystem. This simplifies the two central kinds of Reverse Mathematics results:
 Subsystem $A$ implies subsystem $B$: every $L_2$structure that satisfies $A$ also satisfies $B$. In this set of notes, we will write this as $A \Rightarrow_s B$.
 Subsystem $A$ does not imply subsystem $B$: there is an $L_2$structure that satisfies $A$ but does not satisfy $B$. We will write this as $A \not\Rightarrow_s B$.
Our goal is to understand the logic underlying $\Rightarrow_s$ and $\not\Rightarrow_s$. We will call this logic slogic.
Syntactically, we look at a system in which we take an alphabet $\Sigma$ of propositional variables, each of which is intended to stand for a subsystem. We do not expect a “logic” to look within the subsystems. We only want it to work with the relationships that follow in a routine way from implication and nonimplication results that are already known.
Semantics
With the Reverse Mathematics Zoo in mind, we want a logic that is compatible with what we know at each moment of time. Consider our knowledge at any point in time:
 We know many implications and nonimplications between subsystems, but not all.
 We know many $L_2$ structures, but we do not know all the subsystems that hold in each one.
 Our knowledge changes over time.
These considerations suggest the semantics that we should look at.
Let $\Sigma$ be an alphabet of propositional variables that are intended to stand for subsystems. The formulas of slogic will be of the forms $\phi \Rightarrow_s \psi$ and $\phi \not\Rightarrow_s \psi$, where $\phi$ and $\psi$ are propositional formulas in that alphabet. A valuation is a function from $\Sigma$ to $\{T,F\}$. As usual, each propositional formula is true or false in each valuation. A frame is a nonempty set of valuations.
The satisfaction predicate of each $L_2$ structure gives a valuation, if we associate each propositional variable in $\Sigma$ with a subsystem. The intended interpretations of slogic are frames obtained by choosing a nonempty set of $L_2$ structures and forming the frame of the corresponding valuations.
In the situation where we do not know whether a particular subsystem is satisfied by a particular $L_2$ structure, we can consider two “possible” or “virtual” $L_2$ structures, one in which the subsystem is true and one in which it is false. Each of these options gives a valuation. Of course, some valuations obtained this way may not come from actual $L_2$ structures. This is to be expected, because we wish to look at all valuations that are consistent with our current knowledge, and we do not have full knowledge of reality. Therefore, we look at a semantics involving all possible frames.
The primary questions are then:
 Find a deductive system that is sound and complete for these semantics.
 Understand the properties of the resulting logic.
Modal logic
Although the motivation for the semantics we use is based on the intended application, the semantics exactly match the common semantics for modal logic, if we interpret $\phi \Rightarrow_s \psi$ to mean $\Box(\phi \to \psi)$ and interpret $\phi \not\Rightarrow_s\psi$ to mean $\lnot \Box(\phi \to \psi)$. This brings out the fact that $\Rightarrow_s$ is a form of strict implication, a wellstudied topic in model logic. (In fact, the “S” in S4 and S5 stands for “strict implication”, which is the context in which the axioms were developed; the use of $\Box$ as the primary modal operator came later.)
The only difference between our semantics and the modal logic semantics of Kripke frames is that we do not have an accessibility relation between the valuations in our frames. However, because we do not consider nested implications, we may simply let every valuation be visible from every other valuation, turning our frames into Kripke frames that satisfy the same nonnested modal formulas. In this way, we can interpret our slogic as a fragment of S5.
It would therefore be possible to use a deductive system for S5 to study slogic. The difficulty with that approach is that the deductive system would not match the intension of the logic – a proof in S5 might not look anything like a typical proof in Reverse Mathematics. Worse, the deductive rules for S5 might use formulas with nested modalities in order to derive formulas without nested modalities. Such derivations would be sound, but their intermediate steps would be meaningless in the intended interpretation of our logic. We thus look for deductive systems that match the intended interpretation more closely.
It is straightforward to create a tableaustyle deductive system modeled after the presentation by Mints (1992). This system matches the intension of slogic quite closely. In particular, each refutation tableau can be read directly as an argument in Reverse Mathematics. Combining this tableau system with the standard interpretation of modal logic into firstorder logic, we obtain the following theorems:
 There is a complete and sound deductive system for slogic under the semantics described.
 This logic is decidable, compact, and has a finite model property.
The tableaustyle proof system used to prove these results is also particularly amenable to automated theorem proving. Tableaux can be converted in a straightforward algorithmic manner to naturalsounding prose proofs.
Two fragments relevant to Reverse Mathematics
Our interest in slogic comes from its application to Reverse Mathematics. Although we define the syntax very broadly, including all propositional formulas, two fragments are of particular interest:
 Fragment $\mathcal{F}_1$ consists of formulas of the forms $A \Rightarrow_s B$ and $A \not \Rightarrow_s B$ where $A$ and $B$ are individual propositional variables. This is the purely strictimplicational and strictnonimplicational fragment.
 Fragment $\mathcal{F}_2$ consists of formulas of the forms $\phi \Rightarrow_s B$ and $\phi \not\Rightarrow_s B$, where $\phi$ is a nonempty conjunction of propositional variables and $B$ is a propositional variable.
Fragment $\mathcal{F}_2$ is of interest because of “splitting” theorems in Reverse Mathematics. For example, it is known that there are subsystems $\mathsf{RT}^2_2$, $\mathsf{SRT}^2_2$, and $\mathsf{COH}$ such that $\mathsf{RT}^2_2$ is equivalent, over $\mathsf{RCA}_0$, to $\mathsf{SRT}^2_2 \land \mathsf{COH}$, but is strictly stronger than either $\mathsf{SRT}^2_2$ or $\mathsf{COH}$. This sort of result can be captured directly in $\mathcal{F}_2$.
We obtain the following theorems.
Theorem. The following three rules give a sound and complete deductive system for $\mathcal{F}_1$:
 I: For each $X \in \Sigma$, deduce $X \Rightarrow_s X$.
 HS: From $X \Rightarrow_s Y$ and $Y \Rightarrow_s Z$, deduce $X \Rightarrow_s Z$.
 N: From $X \not\Rightarrow_s Z$, $X \Rightarrow_s W$, and $Z \Rightarrow_s Y$, deduce $W \not\Rightarrow_s Z$.
Theorem. The following four rules give a sound and complete deductive system for $\mathcal{F}_2$:
 I: For each $X \in \Sigma$, deduce $X \Rightarrow_s X$.
 W: From $\phi \Rightarrow_s B$, deduce $\psi \Rightarrow_s B$, if every conjunct of $\phi$ occurs in $\psi$.
 HS: From $\phi \land A \Rightarrow_s Z$ and $\psi \Rightarrow_s A$, deduce $\phi \land \psi \Rightarrow_s Z$.
 N: From $\phi \not\Rightarrow_s Z$, $\phi \land X \Rightarrow_s Y$, and $\phi \Rightarrow_s W$ for each conjunct $W$ of $\psi$, deduce $\psi \not\Rightarrow_s Y$.
References
 Mints, Grigori. A short introduction to modal logic. CSLI Lecture Notes, 30. Stanford University, Center for the Study of Language and Information, Stanford, CA, 1992. x+93 pp. ISBN: 093707375X MR 1199568
 Simpson, Stephen G. Subsystems of second order arithmetic. Second edition. Perspectives in Logic. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009. xvi+444 pp. ISBN: 9780521884396 MR 2517689
 Simpson, Stephen G. The Gödel hierarchy and reverse mathematics. Kurt Gödel: essays for his centennial, 109–127,
Lect. Notes Log., 33, Assoc. Symbol. Logic, La Jolla, CA, 2010. 2668193
Carl, this is really very nice, and I like it a lot.
Thanks, Joel.
I saw that you’ll be speaking on this at the JMM (http://jointmathematicsmeetings.org/amsmtgs/2160_abstracts/1096031603.pdf), and I shall look forward to it.