Examination of the basic notions of soundness and completeness, first for sentential and then for propositional logic. Turning to the question of decision procedures for logical formulae, the concept of recursive function, which emerges in the work of Church and Turning, provides the essential link between logic and theory of computation. The course culminates with Godel's Incompleteness Theorems, which demonstrate the intrinsic limitations of the logical method. Offered in alternate years.