A study of sentential and predicate logic designed to train students to use procedures and systems (trees, natural deduction, axiomatic systems) for determining logical properties and relations, and to give students an understanding of syntactic and semantic metatheoretical concepts and results relevant to those procedures and systems.