CM30071Logic and Its Applications
1 Textbooks and Other Sources
The official textbook is:
- Logic in Computer ScienceModelling and Reasoning about Systems
Michael Huth, Mark Ryan
Cambridge University Press
You might find useful some parts of the book:
- Proofs and Types
Jean-Yves Girard, Yves Lafont, Paul Taylor
Some material is in the paper:
- Basic Proof Theory With Applications to Computation
in Logic of Computation
H. Schwichtenberg, ed.
NATO ASI Series F 157,
- Springer-Verlag, 1997.
Slides by Carsten Führmann:
Some notes of mine:
This course only has two lectures per week because students are supposed to do some reading by themselves; please follow the suggestions for exercises and reading that you find here!
8.4.08 There will be extra tutorials on Friday 11.4 and on Friday 18.4, at 13:15 in 3WN 3.8.
3 Course Info
In the following, I will link some material distributed or used in the past for this and other courses: please disregard any information related to the organisation of those courses: it is not valid any more. Also, keep in mind that I might change the presentation, sometimes substantially. The material that we cover and that you are supposed to understand is clearly indicated below.
Lectures, Topics and Suggested Exercises
29.1.08Lecture 1 Introduction to the course.
5.2.08Lecture 2 Language of propositional logic and truth tabling, further introduction to the course.
8.2.08Lecture 3 Definition of proof system, two rules of natural deduction (and and implication introduction).
12.2.08Lecture 4 Rules of natural deduction: and and implication elimination, or introduction and elimination; examples.
- Prove, in the natural deduction proof system that we have seen so far, the tautologies:
- (A ∧ (B ∨ C)) → ((A ∧ B) ∨ (A ∧ C));
- ((A ∧ B) ∨ (A ∧ C)) → (A ∧ (B ∨ C));
- (A ∨ (B ∧ C)) → ((A ∨ B) ∧ (A ∨ C));
- ((A ∨ B) ∧ (A ∨ C)) → (A ∨ (B ∧ C)).
15.2.08Lecture 5 Exercises and reductio ad absurdum rule.
- Try to prove all the tautologies (not just those listed in connection to natural deduction) that you find in my notes (for an old course) and in this exercise sheet (for an old course).
- Try to prove Peirce's law: (((A → B) → A) → A).
- Please bring in class the exercises you found most difficult and we'll see what we can do.
19.2.08Lecture 6 Exercise on Peirce's law and definition of sequent.
- Write some formulae and prove, in natural deduction, that they are equivalent to their De Morgan duals; please bring to the next lecture the cases for which you have difficulties.
- Do Homework 1 in this exercise sheet (for an old course), without looking at the solutions (try to find, for Peirce's law, a different proof from the one seen in class).
- Do exercises 4.6 and 4.8 in my notes (for an old course).
22.2.08Lecture 7 Exercises and a reminder of soundness and completeness theorems.
26.2.08Lecture 8 Comments and suggestions about proving a soundness theorem. Introduction to the sequent calculus.
- Prove soundness for the natural deduction system for propositional classical logic in my notes (for an old course), by structural induction on proofs.
29.2.08Lecture 9 Gentzen additive sequent system for propositional classical logic.
- Try to prove in the given system all the propositional tautologies that you find in my notes (for an old course) and in this exercise sheet (for an old course).
- Prove the soundness of the implication-left rule.
4.3.08Lecture 10 Comments on the coursework; hint about proving the soundness theorem for natural deduction.
- Please have a look at the coursework suggested literature and try quickly to form groups.
7.3.08Lecture 11 Quantifier rules for the sequent calculus.
- Prove in the system we saw in class all the tautologies of exercise 6.7 in my notes (for an old course).
- In particular, prove that ∃x.∀y.(p(x) → p(y)).
11.3.08Lecture 12 The cut rule and an introduction to cut elimination.
- Prove that the cut rule is sound.
- Find the general shape of proofs of Statman tautologies, in the cut-free sequent calculus (you can find an accessible definition of Statman tautologies at p. 14 of this paper, read Definition 3.7 and Example 3.8). How do these proofs grow in the size of Statman tautologies?
14.3.08Lecture 13 Tutorial about the sequent calculus.
- Solve the two exercises in this test (they are indicative of real exam exercises).
8.4.08Lecture 14 Motivation and general idea of the cut elimination theorem.
- You find what I presented in class in Wainer's paper (Sect. 3, do not pay much attention to the different cut rank, there are several variants).
11.4.08Lectures 15 and 16 Main cases of the cut elimination theorem and completeness theorem, both for propositional logic; solution to problem 1 in this test.
- You will find what I presented in class in Wainer's paper (Sect. 3 and 1).
15.4.08Lecture 17 Introduction to modal logic and definition of Kripke model and forcing.
- Führmann's slides (part 4) contain the definitions and notions about modal logic, but the best treatment is in the textbook.
- Do the examples at pp. 18 and 21 in Führmann's slides (part 4).
18.4.08Lectures 18 and 19 Validity of formulae in modal logic; Curry-Howard isomorphism; solution to problem 3 in this past exam.
- Prove the statements in the last slide of Führmann's slides (part 4) `Correspondence Theory´.
- About the Curry-Howard isomorphism, please read Chapter 3 of Proofs and Types, especially section 3.5.
22.4.08Lecture 20 Coursework presentation.
25.4.08Lectures 21 and 22 Coursework presentations.
29.4.08Lectures 23 and 24 Coursework presentations.
2.5.08Lectures 25 and 26 Tutorial, Q&A.
Material Covered and to Be Prepared for the Exam
- Propositional logic and truth tabling: any source will do fine, for example the slides by Führmann, Part 1.
- Proof system: read up to Definition 2.2, and following explanations, in The Complexity of Propositional Proofs by Alasdair Urquhart.
- Natural deduction: Führmann's slides, Part 2.
- Sections 4 and 6 of my notes (for an old course).
- Soundness and completeness for natural deduction: Führmann's slides, Part 3 (only the statements of the two theorems and what is necessary to understand them, ignore the rules for the quantifiers).
- Statement and meaning of the cut elimination theorem, and the general idea of its proof: section 3 in Wainer's paper.
- Completeness theorem for propositional logic (general idea of the proof): section 1 in Wainer's paper.
- Modal logic: Führmann's slides, Part 4 and textbook.
The coursework has been set on 4 March 2008 (in class and on this web page) and it should be handed in on 28 April 2008 at 12:00.
- Topic 1NP vs coNP Kris Nobes, Mike Davis and Rich Harris (group A) and Ute Kandler, Rok Orel (group B); presentation on 25.4 (during the lecture time and following hour).
- Topic 2Frege vs extended Frege Adam Gundry, Tom McLean, Peter Dennis, Robert Mead; presentation on 29.4 (during the lecture time).
- Topic 3The correspondence between natural deduction and sequent calculus Remi Bernal, Jean-François Marquet; presentation on 22.4 (during the lecture time).
- Topic 4The undecidability of first order logic Zong Guo, Matthew Barsby, Daniel Fowles, Tor Erik Linnerud; presentation on 29.4, from 12:15 to 13:05, in room 1WN 3.12.
5 Office Hours
When you want to talk to me, just drop me an email and we'll arrange for an appointment.
2.5.2008 Alessio Guglielmi email (replace AT by @)