Getting acquainted with strong logical formalisms, their theoretical properties and limits and their use for modeling and specification in computer science
Limits of first-order definability, syntax and semantics of second-order logic, expressive power of second-order logic, second-order arithmetic, simple type theory, typed lambda calculi, interactive theorem proving in higher-order logic
This is an advanced course in logic. Firm knowledge of classical first-order logic (formulas, models, proofs) is a prerequisite.