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