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

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

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

- in Tasks 4 and 5 (in all assignments) the axiom

- 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 intoFO-Int , see beamer slides below.) - Lectures on Modal Logic (Apr 13, 18)

**Beamer slides:**- Cut Elimination in Intuitionistic Predicate Logic (Mar 28)
- Using Cut Elimination: Gödel – Gentzen translation done syntactically (Apr 5)
- Non-Commutative Linear Logic with Subexponentials (Apr 11)
- Gödel – Löb Provability Logic (Apr 20, 25)
- More Semantics for Modal Logics: Sahlqvist's theorems (without proofs);
topological semantics for
**S4**and**GL**(Apr 27)

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

- A. Chagrov, M. Zakharyashchev.
**Some classic texts:**- K. Gödel. Über
formal unentscheidbare Sätze der
*Principia Mathematica*und verwandter Systeme, I.*Monatschefte für Mathematik und Physik*38:173–198, 1931. - G. Gentzen.
Untersuchungen
über das logische Schließen, I.
*Mathematische Zeitschrift*39(2):176–210, 1935. - J. Lambek.
The mathematics
of sentence structure.
*American Mathematical Monthly*65(3):154–170, 1958. - S. A. Kripke.
A completeness
theorem in modal logic.
*Journal of Symbolic Logic*24(1):1–14, 1959. - R. M. Solovay.
Provability interpretations of modal logic.
*Israel Journal of Mathematics*25(3):287–304, 1976. - J.-Y. Girard.
Linear logic.
*Theoretical Computer Science*50(1):1–101, 1987.

- K. Gödel. Über
formal unentscheidbare Sätze der