ABSTRACT. The first is to use forcing techniques to prove model theoretic results in ZFC. Force a model theoretic result to be consistent by a tool such as Martin's axiom, collapsing cardinals or a specific forcing with high model theoretic content. Then use iterated elementary embeddings of the model of set theory to show the model theoretic result is absolute between V and a well-chosen model. Deduce it holds in ZFC. Applications include various extensions of results for $L_{\omega_1,\omega}$ to analytically presented AEC, a new proof of Harrington's theorem on Scott rank of counterexamples to Vaught's conjecture and the development of a new notion of algebraic closure for $L_{\omega_1,\omega}$ that better explains $\aleph_1$-categoricity.

The second is the use of model theory to avoid some apparent uses of descriptive theory or combinatorics. An example is the development locally finite abstract elementary classes to simplify and improve results of Hjorth on the characterizing cardinals. As a corollary we get radically new amalgamation spectra.

This talk represents several projects done in various pieces with S. Friedman, M. Koerwien, P. Larson, C. Laskowski and S. Shelah. 

ABSTRACT. Recently, various restrictions of the primitive recursive set functions relating to feasible computation have been proposed, amongst them the Safe Recursive Set Functions (Beckmann, Buss, Friedman), the Predicatively Computable Set Functions (Arai), and the Cobham Recursive Set Functions (Beckmann, Buss, Friedman, Müller, Thapen - this is work in progress). In this talk I will describe ideas how some of these classes can be captured as the \sigma_1-definable set functions in suitable restrictions of Kripke-Platek set theory, by elementary proof-theoretic means. In particular, I will describe a theory whose \Sigma_1-definable set functions are exactly the Safe recursive Set Functions, and another theory whose \Sigma_1 definable set functions are characterised by the Cobham Recursive Set Functions. The latter result is joint work in progress with Sam Buss, Sy-David Friedman, Moritz Müller, and Neil Thapen.

ABSTRACT. The ordinal H(1) is a tad bigger than the Bachmann-Howard ordinal, and in fact it appeared already in the 1950 article by Heinz Bachmann which inspired Howard's ordinal analysis of ID1. Aczel conjectured that also H(1) should be a prominent proof-theoretic ordinal. In this talk I will present a range of systems of proof-theoretic strength H(1), focusing on systems of sets and types. A common theme is that these systems capture a kind of predicative closure taking one generalized positive inductive definition as a given totality.