CM30071—Logic and Its Applications
1
Textbooks and Other Sources
The official textbook is:
- Logic in Computer Science—Modelling and Reasoning about Systems
2nd Edition
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
Available here.
Some material is in the paper:
- Basic Proof Theory With Applications to Computation
Stan Wainer
in Logic of Computation
H. Schwichtenberg, ed.
NATO ASI Series F 157,
- Springer-Verlag, 1997.
Slides by Carsten Führmann:
Some notes of mine:
2News
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.08There will be extra tutorials on Friday 11.4 and on Friday 18.4, at 13:15 in 3WN 3.8.
3Course 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.08—Lecture 1Introduction to the course.
5.2.08—Lecture 2Language of propositional logic and truth tabling, further introduction to the course.
8.2.08—Lecture 3Definition of proof system, two rules of natural deduction (and and implication introduction).
12.2.08—Lecture 4Rules 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.08—Lecture 5Exercises 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.08—Lecture 6Exercise 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.08—Lecture 7Exercises and a reminder of soundness and completeness theorems.
26.2.08—Lecture 8Comments 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.08—Lecture 9Gentzen 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.08—Lecture 10Comments 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.08—Lecture 11Quantifier 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.08—Lecture 12The 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.08—Lecture 13Tutorial about the sequent calculus.
- Solve the two exercises in this test (they are indicative of real exam exercises).
8.4.08—Lecture 14Motivation 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.08—Lectures 15 and 16Main 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.08—Lecture 17Introduction 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.08—Lectures 18 and 19Validity 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.08—Lecture 20Coursework presentation.
25.4.08—Lectures 21 and 22Coursework presentations.
29.4.08—Lectures 23 and 24Coursework presentations.
2.5.08—Lectures 25 and 26Tutorial, 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.
Past Exams
4Coursework
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.
Specification
Groups
- Topic 1—NP vs coNPKris 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 2—Frege vs extended FregeAdam Gundry, Tom McLean, Peter Dennis, Robert Mead; presentation on 29.4 (during the lecture time).
- Topic 3—The correspondence between natural deduction and sequent calculusRemi Bernal, Jean-François Marquet; presentation on 22.4 (during the lecture time).
- Topic 4—The undecidability of first order logicZong Guo, Matthew Barsby, Daniel Fowles, Tor Erik Linnerud; presentation on 29.4, from 12:15 to 13:05, in room 1WN 3.12.
5Office Hours
When you want to talk to me, just drop me an email and we'll arrange for an appointment.
2.5.2008Alessio Guglielmiemail (replace AT by @)