This book aims to be an introduction to model theory which can be used without any background in logic. We start from scratch, introducing first-order logic, structures, languages etc. but move on fairly quickly to the fundamental results in model theory and stability theory. We also decided to cover simple theories and Hrushovski constructions, which over the last decade have developed into an important subject. We try to give the necessary background in algebra, combinatorics and set theory either in the course of the text or in the corresponding section of the appendices. The exercises form an integral part of the book. Some of them are used later on, others complement the text or present aspects of the theory that we felt should not be completely ignored. For the most important exercises (and the more difficult ones) we include (hints for) solutions at the end of the book. Those exercises which will be used in the text have their solution marked with an asterisk.

The book falls into four parts. The first three chapters introduce the basics as would be contained in a course giving a general introduction to model theory. This first part ends with Chapter 4 which introduces and explores the notion of a type, the topology on the space of types and a way to make sure that a certain type will not be realized in a model to be constructed. The chapter ends with Fraïssé's amalgamation method, a simple but powerful tool for constructing models.

This book is about the deep connections between proof theory and recursive function theory. Their interplay has continuously underpinned and motivated the more constructively orientated developments in mathematical logic ever since the pioneering days of Hilbert, Gödel, Church, Turing, Kleene, Ackermann, Gentzen, Péter, Herbrand, Skolem, Malcev, Kolmogorov and others in the 1930s. They were all concerned in one way or another with the links between logic and computability. Gödel's theorem utilized the logical representability of recursive functions in number theory; Herbrand's theorem extracted explicit loop-free programs (sets of witnessing terms) from existential proofs in logic; Ackermann and Gentzen analysed the computational content of ε-reduction and cut-elimination in terms of transfinite recursion; Turing not only devised the classical machine-model of computation, but (what is less well known) already foresaw the potential of transfinite induction as a method for program verification; and of course the Herbrand–Gödel–Kleene equation calculus presented computability as a formal system of equational derivation (with “call by value” being modelled by a substitution rule which itself is a form of “cut” but at the level of terms).

That these two fields—proof and recursion—have developed side by side over the intervening seventy-five years so as to form now a cornerstone in the foundations of computer science, testifies to the power and importance of mathematical logic in transferring what was originally a body of philosophically inspired ideas and results, down to the frontiers of modern information technology.

The treatment of our subject—proof and computation—would be incomplete if we could not address the issue of extracting computational content from formalized proofs. The first author has over many years developed a machine-implemented proof assistant, Minlog, within which this can be done where, unlike many other similar systems, the extracted content lies within the logic itself. Many non-trivial examples have been developed, illustrating both the breadth and the depth of Minlog, and some of them will be seen in what follows. Here we shall develop the theoretical underpinnings of this system. It will be a theory of computable functionals (TCF), a self-generating system built from scratch and based on minimal logic, whose intended model consists of the computable functions on partial continuous objects, as treated in the previous chapter. The main tool will be (iterated) inductive definitions of predicates and their elimination (or least-fixed-point) axioms. Its computational strength will be roughly that of ID<ω, but it will be more adaptable and computationally applicable.

After developing the system TCF, we shall concentrate on delicate questions to do with finding computational content in both constructive and classical existence proofs. We discuss three “proof interpretations” which achieve this task: realizability for constructive existence proofs and, for classical proofs, the refined A-translation and Gödel's Dialectica interpretation. After presenting these concepts and proving the crucial soundness theorem for each of them, we address the question of how to implement such proof interpretations.