This is the title of a two-parts talk I gave at the CMU Model Theory Seminar on Feb. 10, 17, 2014. I would like to thank Rami Grossberg for helpful discussions and comments on this work.

While Morley sequences are one of the basic tools of first order classification theory, their existence is a nontrivial fact. Shelah's original proof uses the cardinal ב_{(2|T|)+}, where |T| is the number of formulas in the underlying language. The need for such a big cardinal seems surprising. Grossberg, Iovino and Lessmann lowered that cardinal to ב_{δ}, where δ is lower than the above bound, and asked whether it is really necessary, at least for the class of simple unstable theories (for stable theories much less suffices). This can be reformulated as a problem within Friedman's reverse mathematics: Grossberg asked if existence of Morley sequences in simple theories is provable in (H(χ), ∈) when χ = (ב_{2} (|T|))^{+}.

In this series of talks, I will show that the answer is yes, by giving a new proof that does not need any "big" cardinal. The proof builds on a 47 year old idea of Gaifman, together with a rank function studied by Adler. I aim to make the talks reasonably self-contained and use only minimal background. Familiarity with forking will not be assumed.

- Rami Grossberg, José Iovino, Olivier Lessmann.
*A primer of simple theories*, Archive for Mathematical Logic 41 (2002), no. 6, 541-580. - Hans Adler.
*Thorn-forking as local forking*, Journal of Mathematical Logic 9 (2009), no. 1, 21--38.