This page will be updated from time to time during the term. The
original start-of-term version is also available.
Time and Place
Fridays, 10:30–11:20, RCH 308.
(Except Nov. 8; the IA will be busy marking midterms.)
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).
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
for sensitive and/or confidential information.
Assignments and solutions. Record of marks (grade computations may be
Additional material (e.g., copies of overheads, etc.) will be posted
from time to time.
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
Tutorial Center (MC 4065)|
Hours: Mon., 10:00–11:00
||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 re-evaluation 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.
Written assignments: 35%.
Normally due in class on Tuesdays.
See the assignments page for
additional information, including the (somewhat unusual)
distribution of problems and marks.
Midterm: 25%. Thursday, Nov. 7, 4:30–6:20pm, in
RCH 301. Seating assignments to be posted to Odyssey.
Final exam: 40%. Tuesday, Dec. 17, 12:30–3:00pm, MC 1056.
Academic Integrity and Students with Disabilities
This courses adheres to the UW policies on
Academic Integrity and Students with Disabilities.
(This outline will be annotated with times and readings, as the course
- Course overview. Readings: H&R, §1.1
- The place of logic in mathematics, including computer
- Formal vs. informal logic.
- Basic (propositional) logic.
Readings: H&R, §§1.1, 1.3, 1.4.1, 1.4.2.
stuff of propositional logic: propositions and
Well-formed formulas. Values of formulas.
Properties of formulas and their relationships.
Reading: Laws of Boolean algebra
A first formal proof system—Resolution.
Reading: Propositional Resolution
(full version, with minor revisions: 24/9/19).
- Predicate logic (first order)
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æ.
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.
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,
Relation to other formal deductive systems.
- Using logic in math/CS
Notes on Peano Arithmetic and on formal lists (preliminary version)
Lists and other stuctures.
- Definability. Limits to definability.
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 Church-Turing Thesis.
- Non-primitive recursive functions; non-recursive
Undecidability in computation and in logic. Gödel's Theorem.
- Programming = Proof ?
- The Curry-Howard Correspondence.
Propositions as types.
- Constructive logic as a foundation for computation.
Implications for design of programming languages.
- Computing proofs.