# Introduction to Formal Logic

## Schedule

1. (2 Oct) Introduction, why is logic important? Sequent calculus for propositional logic.
2. (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.
3. (16 Oct) Sequent calculus for predicate logic with equality, lots of practicing.
4. (23 Oct) Semantics of predicate logic, soundness of most of the rules of sequent calculus.
5. (6 Nov) Negation normal form. A proof search algorithm.
6. (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.
7. (20 November) Subformula Replacement, Skolemization.
8. (27 November) No new material, extra exercises.
9. (29 November) Midterm exam.
10. (4 December) Discussion of exam.
11. (6 December) Instead of Exercises: Proof permutations, normal forms, cut elimination, Herbrand's theorem.
12. (11 December) Natural deduction, Introduction to Intuitionistic Logic.
13. (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.
14. (7 January) Extra exercise class. (14.15)
15. (8 January) Lambda calculus, higher-order logic.
16. (15 January) Embedding of logic operators in higher-order logic. Some requently used axioms and proof techniques.
17. (22 January) Curry-Howard isomorphism, Demonstration Coq.
18. (1 February, 15.15). Extra exercise class preparing for the exam of Feb. 4th.

## Slides

• 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 .

## Exercises

In order to pass, you have to be present at most of the exercises, and pass the final exam and the midterm exam.

## Exams

The midterm exam was on November 29th, 12.15-14.00. Exam for the second part is set on Feb. 4th, 10.15-12.00. On Feb. 15th, 11.15-13.00, there will be chance to redo the first exam. Note that in all cases you have to do the exam on Feb 4th, also if you want to redo the first exam.