Logic II (LGIC 320 / MATH 571)
(University of Pennsylvania, Spring 2017)
Practical Information
- Lecturer: Stepan Kuznetsov, visiting from Steklov Mathematical Institute, Moscow
- Lectures ended on April 27.
- Office hours in the end of the semester: (subject to change, please check the day before!)
- Friday, April 28: 2:30 PM – 5:00 PM
- Monday, May 1: 12:00 NOON – 2:00 PM
- Tuesday, May 2: out of office
- Wednesday, May 3: 12:00 NOON – 2:00 PM
- Thursday, May 4: 11:45 AM – 5:00 PM (deadline for final assignment)
- Lectures: every Tuesday and Thursday at 3:00–4:20PM, classroom 4C6 DRL
- Office hours (for questions and discussions): Tuesday and Thursday, 2:20–3:00PM, 4:20–5:00PM (40 min before
and after each class), or by appointment
- Last class on April 27 (rescheduled from March 21) will be held in room 2N36 DRL at 3:00–4:20PM.
Midterm
- Handed out on February 28.
- If you missed this class, contact the lecturer to get your personal assignment.
- Deadline:
March 16, 6:00PM EST extended: Friday March 24, 6:00PM EST.
- The assignment should be done in written form. (Submissions by email welcome.)
- The midterm forms ⅓ of the resulting grade.
Final Exam
- Handed out on April 21.
- If you missed this class, contact the lecturer to get your personal assignment.
- Deadline: May 4, 5:00PM EST.
- The assignment should be done in written form. (Submissions by email welcome.)
- The final forms ⅔ of the resulting grade.
- Questions welcome during the office hours, by appointment, or by email.
- Errata:
- in Tasks 4 and 5 (in all assignments) the axiom A → A should
be A ⇒ A;
- in Task 3, assignments 2 and
5, the last formula should be K ⊢ A instead of
K4 ⊢ A.
Course Materials
- Preliminary outline
- Lecture notes:
- Lectures 1–5: Propositional Intuitionistic Logic (Jan 12, 17, 19, 24, 26)
- Lectures 6–10: λ-calculus, Natural Deduction, and the Curry – Howard Correspondence (Jan 31, Feb 2, 7, 9, 14)
— see notes by Sørensen and Urzyczyn below
- Lectures 11–15: First Order Intuitionistic Logic (Feb 16, 21, 23, 28, Mar 2)
- Lectures on Gentzen-Style Sequent Calculi
(Here you can find the calculi, Harrop's and Herbrand's theorems. For a detailed cut elimination proof (in LJ) and the Gödel – Gentzen translation of
FO-CL into FO-Int, see beamer slides below.)
- Lectures on Modal Logic (Apr 13, 18)
- Beamer slides:
- Exercises:
- Additional reading:
- A. Chagrov, M. Zakharyashchev. Modal Logic. Clarendon Press, Oxford, 1997.
- D. van Dalen. Logic and Structure (5th edition). Springer, 2013.
- Handbook of Mathematical Logic, ed. by J. Barwise. Elsevier, 1999.
- Stanford Encyclopedia of Philosophy
- M. H. B. Sørensen, P. Urzyczyn. Lecture Notes on the Curry – Howard Isomorphism
(Studies in Logic and the Foundations of Mathematics, vol. 149). Elsevier, 2006.
(A preliminary version, as lecture notes for ESSLLI '99, is available
online.)
- D. Gabbay, V. Shehtman, D. Skvortsov. Quantification in Nonclassical Logic, vol. 1.
Draft of the 2nd edition. Download: .ps,
.pdf.
- G. Takeuti. Proof Theory (Studies in Logic and the Foundations of Mathematics, vol. 81). North-Holland (Elsevier), 1987.
- G. Restall. An Introduction to Substructural Logics
Routledge, 2000.
- L. Beklemishev, D. Gabelaia. Topological interpretations of provability logic.
arXiv preprint 1210.7317, 2012.
- M. Kanovich, S. Kuznetsov, V. Nigam, A. Scedrov. On the proof theory of non-commutative subexponentials.
Abstract for Dale Fest!60th (seminar in honor of the 60th birthday of Dale Miller), Paris, 2016.
- Some classic texts: