Many interesting combinatorial theorems can be expressed in the language of Z $\sb2$, formal second order arithmetic. Unlike formulas of first order arithmetic, formulas of second order arithmetic can refer to sets of integers. This thesis analyzes formalizations of many theorems of countable combinatorics, determining which set existence axioms are necessary in their proofs. The framework of axioms used here consists primarily of the subsystems RCA $\sb0$, WKL $\sb0$, and ACA $\sb0$. Much of the pioneering work done in these subsystems is due to Friedman and Simpson. In many cases it is possible to show that a theorem is equivalent to a set comprehension axiom over the weak base system RCA $\sb0$. Results of this sort, called reverse mathematics, leave no doubt as to what set existence axioms are necessary in a proof. A surprising number of theorems of countable combinatorics yield results of reverse mathematics. The combinatorial theorems analyzed include various infinite marriage theorems and related results concerning infinite graphs and partial orders. Several results of infinite Ramsey theory, including Hindman's theorem and Milliken's theorem, are also considered. In some cases, independence results are proven, using model theoretic techniques developed in the thesis.
