Schedule & Readings
CS6860 - Fall 2015

Date	Topic	Notes
Aug 25	-Introduction to the course	Lecture 1 Notes From Frege to Godel: A Source Book in Mathematical Logic, 1879-1931. Mathematical Logic, Stephen Cole Kleene. First-Order Logic, Raymond M. Smullyan.
Aug 27	-Smullyan's Propositional Calculus	Lecture 2 Notes Formulas of Propositional Logic, Raymond M. Smullyan.
Sept 1	-Recommended reading -Styles of proof	Lecture 3 Notes Transformation rules, from Introduction to Metamathematics by Stephen Cole Kleene. Proof of concept, from New Scientist, Jacob Aron, 29 Aug 2015.
Sept 3	-Minimal propositional calculus	Lecture 4 Notes Proofs in Propositional Logic, lecture slides by Pierre Casteran.
Sept 8	-Minimal propositional calculus continued	Lecture 5 Notes
Sept 10	-iPC and mPC -Computational content	Lecture 6 Notes
Sept 15	-Computational content of any(t)	Lecture 7 Notes Proof and computation rules, Sections 2.2-2.3 from Intuitionistic completeness of first-order logic, Robert Constable and Mark Bickford. In the Annals of Pure and Applied Logic, vol. 165, January 2014.
Sept 17	-Intuitionistic logic -Constructive logic	Lecture 8 Notes On the meaning of the logical constants and the justifications of the logical laws, Per Martin-Lof.
Sept 22	-Propositional Calculus as a programming language	Lecture 9 Notes Lambda calculus and topics, excerpt from a 6110 lecture.
Sept 24	-Evidence semantics -New semantics for iPC -Classical PC	Lecture 10 Notes
Sept 29	-Gilvenko's theorem -Building proofs by evidence term	Lecture 11 Notes
Oct 1	-Evidence terms	Lecture 12 Notes
Oct 6	-Visser rules	Lecture 13 Notes Admissible rules in the implication-- negation fragment of intuitionistic logic, Petr Cintula and George Metcalfe, Annals of Pure and Applied Logic, v.162, pgs 162-171, 2010. Intuitionistic completeness of first-order logic, excerpt from the tech report version.
Oct 8	-Completeness	Lecture 14 Notes Intuitionistic Completeness of First-Order Logic -- mPC Case, Robert Constable and Mark Bickford.
Oct 16	-More on completeness and the intersection type	Lecture 15 Notes
Oct 20	-More on completeness and iFOL	Lecture 16 Notes On Weak Completeness of Intuitionistic Predicate Logic, G. Kreisel, Journal of Symbolic Logic, Vol. 27(2), June 1962.
Oct 22	-Computable functions -More on completeness	Lecture 17 Notes
Oct 27	-Dummett and intuitionism	Lecture 18 Notes
Oct 29	-Second-order intuitionistic logic	Lecture 19 Notes
Nov 3	-Second-order intuitionistic logic	Lecture 20 Notes
Nov 5	-More second-order intuitionistic logic	Lecture 21 Notes
Nov 10	-More second-order logic	Lecture 22 Notes Proof and extract from Nuprl
Nov 12	-Relating classical and constructive logic	Lecture 23 Notes
Nov 17	-Classical and constructive logic	Lecture 24 notes Lecture notes from 5860
Nov 17	-Second order logic	Lecture 25 notes
Nov 24	-Second-order logic proof	Proof of exists theorem, still under revision, may still have small errors. Proof of same theorem in Nuprl
Nov 26	Thanksgiving
Dec 1	-Type Theory	Generating Event Logics with Higher-Order Processes as Realizers, Mark Bickford and Robert Constable. Constructive Type Theory Background The Type Base and Undecidability in Type Theory, Abhishek Anand.
Dec 3	-Protocols	Generating Event Logics with Higher-Order Processes as Realizers, Mark Bickford, Robert Constable, and David Guaspari. Event structure over Process Models, Robert Constable. Pages 15-22,24, and 27 discussed in class.

---