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

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

Exams