This introductory chapter covers a wide range of topics, from basic notational conventions and coding in arithmetic to important classical results. The well-known theorems, such as Gaifman's splitting theorem, Arithmetized Completeness Theorem, or Friedman's Embedding Theorem are discussed without proofs. Proofs are given for less known facts, like Blass-Gaifman and Ehrenfeucht lemmas. The chapter also presents a systematic introduction to recursively and arithmetically saturated models, resplendent models, and satisfaction classes.
Keywords: coding in arithmetic, Blass-Gaifman Lemma, Ehrenfeucht Lemma, arithmetic saturation