**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 jack@nyu.edu. 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:** (September 24) Cantone-Omodeo-Schwartz Chapter 2, **Sections** (a) The propositional calculus (b.i-iii); Introduction to the predicate calculus; Goedel Completeness Theorem; Some examples of predicate proof.

**Week 4:** (October 1) Cantone-Omodeo-Schwartz Chapter 2, **Sections** (b.iv-viii) Proof of the Goedel completeness theorem.

**Week 5:** (October 8) Cantone-Omodeo-Schwartz Chapter 3, **Sections** (b.ix-xii) Consequences of the Goedel completeness theorem; Herbrand's theorem; Predicate calculus with equality as a built-in; Set theory as an axiomatic extension of predicate calculus.

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