Proofs and Computations
Spring 2004
|
|
|
Tuesdays,
11:45-1:45pm GC 3306 |
|
|
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. |