- (2 Oct) Introduction, why is logic important? Sequent calculus for propositional logic.
- (9 Oct) Semantics of propositional logic. Soundness and completeness of sequent calculus for propositional logic. Algorithm for checking provability of propositional formula. Some practicing with the algorithm.
- (16 Oct) Sequent calculus for predicate logic with equality, lots of practicing.
- (23 Oct) Semantics of predicate logic, soundness of most of the rules of sequent calculus.
- (6 Nov) Negation normal form. A proof search algorithm.
- (13 November) Koenigs lemma, proof that the proof search algorithm approximates a model when it does not find a proof. Completeness of sequent calculus. Compactness, some inexpressibility results based on compactness.
- (20 November) Subformula Replacement, Skolemization.
- (27 November) No new material, extra exercises.
- (29 November) Midterm exam.
- (4 December) Discussion of exam.
- (6 December) Instead of Exercises: Proof permutations, normal forms, cut elimination, Herbrand's theorem.
- (11 December) Natural deduction, Introduction to Intuitionistic Logic.
- (18 December) Sequent calculus for intuitionistic logic. Equivalence of natural deduction and sequent calculus for intuitionistic logic. Equivalence of natural deduction with TND or DNE and classical logic.
- (7 January) Extra exercise class. (14.15)
- (8 January) Lambda calculus, higher-order logic.
- (15 January) Embedding of logic operators in higher-order logic. Some requently used axioms and proof techniques.
- (22 January) Curry-Howard isomorphism, Demonstration Coq.
- (1 February, 15.15). Extra exercise class preparing for the exam of Feb. 4th.

- Slides about sequent calculus, as ps or pdf . I made some changes on 23 Oct, so you should reload them.
- Semantics of propositional logic, soundness and completeness of sequent calculus for propositional logic, as ps or pdf .
- Semantics of predicate logic, soundness and completeness of sequent calculus for predicate logic. ps or pdf .
- Subformula replacement, Skolemization ps or pdf .
- Natural deduction ps or pdf .
- Equivalence of natural deduction and sequent calculus, as ps or pdf .
- Higher-order logic, lambda calculus as ps or pdf .
- Use of higher-order logic, frequently used axioms and proof principles, inductive types. ps or pdf .

- Exercsises of October 4th, as ps or pdf .
- Exercises of October 18th, as ps or pdf .
- Excercises for October 25th, as ps or pdf .
- Excercises for November 22th, as ps or pdf . Here are examples of the two transformations: ps or pdf .
- Exercises of December 13th, as ps or pdf .
- Exercises of January 10th, as ps or pdf .
- Exercises of January 17th, as ps or pdf .