Textbook: Concrete set logic: a proof verifier and its application to the basic theorems of analysis. By Domenico Cantone, Eugenio Omodeo, and J.T. Schwartz (Draft manuscript)
You can E-mail me at email@example.com. The course text is on-line at http://www.settheory.com/intro.html
There will be no examinations. Grades will be assigned on the basis of a final paper, on a subject related to the course, to be selected in consultation with the instructor. A final project proposal is due in week 8. Finished final projects are due one week after the last class. Students actively interested in Computational Logic, perhaps for a dissertation in this area, may wish to undertake a programming project, to be worked out in consultation with the instructor.
Week 1: (September 10) Cantone-Omodeo-Schwartz Chapter 1, Sections (a-d); (e.i.a) The Choice Operator; (e.i.b) Ordinal and Cardinal Numbers in Set Theory.
Week 2: (September 17) Cantone-Omodeo-Schwartz Chapter 1, Sections (e.i.b contd.) Ordinal and Cardinal Numbers in Set Theory; (e.i.c) Hereditarily finite sets; (e.ii) Use of 'Theories'; (e.iii) Survey of the major sequence of definitions and proofs.
Week 3:Week 6: (October 15) Cantone-Omodeo-Schwartz Chapter 3, Sections (a) The syntax and semantics of proofs; (b.i-iii) The Davis-Putnam algorithm and some related elementary decision algorithms; (h) 'Blobbing' more general formulae down to a specified decidable or semi-decidable sublanguage of set theory.
Week 7: (October 22) Cantone-Omodeo-Schwartz Chapter 3, Sections (b.iv) Elementary Boolean theory of sets; (b.v) Quantified predicate formulae involving predicates of one argument only; (b.vii) Multilevel syllogistic.
Week 8: (October 29) Handout: Some example proofs
Final project proposals due this week
Week 9: (November 5) Cantone-Omodeo-Schwartz Chapter 3, Sections (b.xi) Decidable extensions of MLSS; (b.xiii) Proof by equality; (b.xiv) Proof by monotonicity.
Week 10: (November 12) Cantone-Omodeo-Schwartz Chapter 3, Sections (c) The resolution method; (d) Universally quantified predicate formulae involving function symbols of one argument only;
Week 11: (November 19) Cantone-Omodeo-Schwartz Chapter 3, Section (g) A decision algorithm for ordered Abelian groups
Week 12: (November 26) Handout: More example proofs
Week 13: (December 3) Cantone-Omodeo-Schwartz Chapter 3, Sections (b.xxi) Tableau Methods; (b.xxii) Algebraic deduction; (i) Deduction by semi-symbolic computation
Week 14: (December 10) Cantone-Omodeo-Schwartz Chapter 3, Sections (b.xviii) Two decidable quantified languages: Presburger arithmetic and Behmann's elementary quantified set theory.