The courses have three aims. First, teaching students how to reason using linear, intuitionistic, co-intuitionistic, and classical logic, and possibly the axiom of choice. Second, familiarizing students with the way of thinking internal to category theory. Third, showing some contemporary mathematical theories in action by means of the principles above.
Expected learning outcomes
Formalization abilities, use of a logical calculus, knowledge of the limits of logical mechanization.
SAT problems; the DPLL algorithm; SAT-solvers. Tarski semantics for first order theories. Theories and examples of theories. Diagrams and Compactness; ultraproducts and applications. First results in model-theory (Lowenheim_Skolem theorems, preservation theorems, Los-Vaught test). Herbrand theorem. Unification, Resolution, Paramodulation. The Superposition Calculus. Applications to word problems, the Knuth-Bendix algorithm.