Course Outline
This page will be updated from time to time during the term. The
original startofterm version is also available.
Time and Place
Lectures:
TuTh 1:00–2:20, ML 349 OPT 309.
Tutorials:
Fridays, 10:30–11:20, RCH 308.
(Except Nov. 8; the IA will be busy marking midterms.)
Resources
Textbooks (optional)

M. Huth and M. Ryan, Logic in Computer Science (2nd ed.),
Cambridge University Press, 2004.

G. Dowek, Proofs and Algorithms: An introduction to logic and
computability, Springer, 2011.
These are available for purchase (optional) at the UW store. The
Davis Centre library has copies on reserve (electronic for Dowek,
bound for Huth/Ryan).
Electronic fora

Piazza:
for questions and discussion from students, and announcements,
discussion and answers from instructors.

Note that Piazza posts are completely public, and may be read by
anyone anywhere.

Learn:
for sensitive and/or confidential information.

Assignments and solutions. Record of marks (grade computations may be
unreliable).
Other
Additional material (e.g., copies of overheads, etc.) will be posted
from time to time.
Role
 Name
 Email
 Contact

Instructor

Jonathan Buss
 jfbuss

DC 3353, x34428.
Hours: Mon., 1:00–2:00, Wed., 10:00–11:00,
or by appointment, or just drop by.

Instr. Asst. and TA

Stephanie McIntyre
 srmcintyre

Tutorial Center (MC 4065)
Hours: Mon., 10:00–11:00 11:00–12:00.

TA

Jan Gorzny Yetian Wang
 jgorzny yetian.wang
 n/a

ISC

Dalibor Dvorski
 ddvorski
 MC 4102, x36816

For questions regarding course material and/or logistics, do any/all of

If your question has general interest,
post to the course Piazza page.

See the instructor, at the above times or by arrangement.
(Dropping by can work, too!)

See the IA in the Tutorial Center, or via other arrangement.
To request a reevaluation of marking, or to discuss your progress in
the course, contact the instructor.
For administrative issues, including illness forms and accommodation
for religious holidays, see either the instructor or the ISC.
For other issues, or if nothing applies, please contact the instructor.
Grading summary:
Academic Integrity and Students with Disabilities
This courses adheres to the UW policies on
Academic Integrity and Students with Disabilities.
Course Topics
(This outline will be annotated with times and readings, as the course
progresses.)
 Course overview. Readings: H&R, §1.1

 The place of logic in mathematics, including computer
science.
 Formal vs. informal logic.
 Basic (propositional) logic.

Readings: H&R, §§1.1, 1.3, 1.4.1, 1.4.2.
 The
stuff
of propositional logic: propositions and
truth values.

Wellformed formulas. Values of formulas.

Properties of formulas and their relationships.
Reading: Laws of Boolean algebra
(updated: 17/9/19).

A first formal proof system—Resolution.
Reading: Propositional Resolution
(full version, with minor revisions: 24/9/19).
 Predicate logic (first order)

Readings:
H&R, §§2.1, 2.2, 2.4.
Optional: Dowek: §§ 1.2.1–2, 1.3,
2.1. (This presentation has greater generality, different
notation, and far fewer examples than H&R. Caveat lector.)
Overheads on values of quantified formulæ.
 The
stuff
of predicate logic: domains and quantification.
 Extending propositional syntax and semantics. Examples in
math and CS.
A look at Resolution for predicate logic. ⟨Omitted.⟩
 Formal proofs via Natural Deduction


Deduction rules for propositional logic and predicate logic.
Examples.
Readings:
H&R, §§1.2, 2.3. (Propositional summary: p. 27.)
Dowek, §1.4. (For a variation, see §1.6.)
 Properties of deductive systems: soundness, completeness,
and compactness.

Relation to other formal deductive systems.
 Using logic in math/CS

Readings:
Notes on Peano Arithmetic and on formal lists (preliminary version)
 Arithmetic.
Orderings.
Lists and other stuctures.
 Definability. Limits to definability.
 Computation

Readings:
Dowek, §§3.1, 3.2, 3.4.1. Also see §3.4.2.
Notes on recursive functions.
Notes interpretation of recursive
functions, and on the incompleteness of mathematics.
 Recursive functions. Relations to other computational
modes; the ChurchTuring Thesis.
 Nonprimitive recursive functions; nonrecursive
functions.

Undecidability in computation and in logic. Gödel's Theorem.

 Programming = Proof ?

 The CurryHoward Correspondence.
Propositions as types
.
 Constructive logic as a foundation for computation.
Implications for design of programming languages.
 Computing proofs.