This course covers the metatheory of formal languages and inferences---in particular, the relationship between truth and proof. We review induction, recursion, and basic definitions for formal languages. Then we investigate the syntax (formalized proofs) and semantics (satisfiability and truth) of sentential and predicate logic. The culmination of the course comes in two results: the soundness and completeness theorems for first order logic. The soundness theorem states that every sentence that can be proven is true, while the completeness theorem states that every true sentence can be proven within the formal system. Additional topics include the compactness theorem, the Lowenheim-Skolem theorems, and non-standard model of arithmetic.