Proofs and Computations

Spring 2004




Tuesdays,
11:45-1:45pm
GC 3306
Sergei Artemov
GC 4329, 212-817-8661
sartemov@gc.cuny.edu
The main goal of the course is to provide a uniform coverage of the basic Proof Theory, Proof and Provability Logics, connections between proofs and verified programs, proofs and modal epistemic logics. An educated and active participant will be brought to the leading edge of research in this area by the end of the semester. The course will be followed by a research seminar on Tuesdays 2:30 p.m.

Prerequisites: a basic knowledge of the first order logic up to the completeness theorem, a familiarity with the computability theory up to the Halting Problem.



Reading
1. D. van Dalen, Logic and Structure, Springer-Verlag, any of the third to fifth editions. A perfect introductory text in logic. There is an additional arithmetic and Incompleteness chapter existing as a Technical Report available which I have a kind permission to use for our course. This book corresponds to Sections 1-5 in the Program.

2. C.Smorynski, Self-Reference and Modal Logic, Springer-Verlag, Berlin, 1985. A pretty good exposition of the Provability Logic in 1976-1985, too old to be the primary source on the subject. Covers Sections 2,4-7 of the Program.

3. G.Boolos, The Logic of Provability, Cambridge University Press, 1993. The latest monograph on Provability Logic written by an MIT professor. Covers advances in the first order provability logic. Corresponds to Sections 1-8 of the Program.

4. D.de Jongh and G.Japaridze, Logic of Provability, in S.Buss, ed., Handbook of Proof Theory, Elsevier, 1998. A very good survey of the Provability Logic and Algebras. Covers Sections 6-9 of the Program, but with little details though. Available on-line.

5. S.Artemov, Explicit provability and constructive semantics, Bulletin of Symbolic Logic, volume 7, No.1, pp. 1-36, 2001. This is a comprehensive introduction to proof polynomials and Logic of Proofs. Plenty of history and motivations. Available on my webpage for downloading. Covers Section 10 with all the details.

6. R.Iemhoff. Provability logic and admissible rules. PhD thesis , University of Amsterdam, 2001. Available for downloading. Covers 13.

7. A.S.Troelstra, Realizability. In S.Buss, ed., Handbook of Proof Theory, Elsevier, pp. 407-474, 1998. A survey, covers 14.

8. S.R.Buss, Bounded Arithmetic, Bibliopolis, Naples 1986. 221+v pages. Revision of Ph.D. thesis. Covers 16. When we get to this point you will be provided with an alternative reading as well.