Introduction to Type Theory and Higher-Order Logic

Introduction to Type Theory and Higher-Order Logic

Jørgen Villadsen (Technical University of Denmark, Denmark)

The history of type theory and higher-order logic includes the thoughts of prominent logicians like Russell, Ramsey, Carnap, Quine, Tarski, Gödel, Church, Turing and Montague working in mathematics, linguistics and philosophy. Later successful proof assistants were developed by Dick de Bruijn (AUTOMATH) and Mike Gordon (HOL) and numerous proofs of theorems in pure mathematics and correctness results in computer science have been formally checked. Usually higher-order logic extends first-order logic by admitting quantification over typed sets, relations and/or functions that are arbitrarily deeply nested. Types are often extended with polymorphism, dependent types and inductive types. Most of today’s advanced proof assistants are based on type theory or higher-order logic.

The course starts from simple type theory, covering its syntax, semantics, axiomatics, soundness and completeness, and then the state-of-the-art proof assistants Isabelle and Coq are introduced. Finally the relationships to independence-friendly logic, set theory and other advanced topics are described.