Program outline
Week 1
Fundamentals of MetalogicJohn Slaney
- Metatheory of classical first-order logic, including completeness theorem
- Basics of proof theory
- The Joy of Sets
Michael Norrish
- Computability, recursiveness, Turing machines
- Diagonalisation
- Peano Arithmetic and Gödel numbering
- Undecidability of first-order logic
- Incompleteness of Peano Arithmetic
Rajeev Gore
- Kripke models, Hilbert calculi, Frame correspondences
- Tableaux-based decisions procedures
- Propositional linear temporal logic
Anupam Das
- Propositional logic, semantics and proofs.
- Soundness and completeness.
- First-order logic and some formal theories.
- The sequent calculus and cut-elimination.
- Perspectives.
Week 2
Overview of Automated ReasoningPeter Baumgartner
- Automated propositional theorem proving
- Automated first-order theorem proving
- Reasoning with arithmetic constraints by quantifier elimination
John Slaney
- Philosophical motivation
- Routley-Meyer semantics
- Paraconsistency and the γ rule
- Deviant theories of arithmetic
Dirk Pattinson
- Constructive Reasoning by Example
- BHK interpretation
- Natural Deduction for FOL
- Goedel Gentzen
- Heyting Arithmetic
- Realisability Interpretation
- Disjunction Theorem
- Heyting Arithmetic in Higher Types
- Modified Realisability
Tomasz Jarmużek
- Tomasz Jarmużek
- TBA
- TBA
- TBA
