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