We introduce and develop the basic concepts and techniques of intuitionistic and classical first order logic. Priority is given to the synctactic/deductive notions, through the study of the natural deduction system and the sequent calculus. The semantic notions are subsequently introduced in the case of classical logic. On that ground we develop Zermelo-Fraenkel axiomatic set theory and the elementary part of computability theory. More in detail: A1 Formalization of logical reasoning in the framework of first order languages: logical operators, equality and deduction rules A2 Trees and mathematization of syntactic notions A3 Natural deduction systems A4 Intuitionistic Logic and Classical Logic A5 Proving non classical deducibility: truth tables A6 Completeness and decidability of classical propositional calculus A7 Sequent calculus A8 Cut elimination theorem and applications A9 Herbrand and Hilbert-Ackermann theorems A10 Truth-value semantics and completeness A11 Skolem’s tranformations and the resolution method B1 Hilbert’s style deduction systems B2 Definitional extensions and syntactic interpretations B3 Classical set-theoretic semantics B4 Relations between interpretations B5 Compactness C1 The Zermelo-Fraenkel axionatic system C2 Ordinals and natural numbers C3 Induction and recursion C4 Well-founded sets C5 Cardinal numbers C6 The Axiom of Choice D1 Primitive recursive and recursive functions D2 Register machines and Turing machines D3 Coding programs and computations D4 Kleene’s normal form theorem D5 Undecidable problems D6 Undecidability of Horn’s logic.