Captain's Log: Logical Foundations of Programming, Fall 2003

August 20 (Wednesday)

Introduction to course; Syllabus handed out. Why study this course? Example of how a specification of the square root function may be encoded in FOL.
Before next time: read the introduction of LPL, start playing with the software, and preferably start reading a bit of Chap 1.

August 22 (Friday)

Homework 1 out. Covered Sections 1.1-1.5.
Three worlds (including Tarski's world) presented, together with corresponding variants of FOL. Important concepts: individual constants (names), function symbols (with arity), predicates (with arity). Terms are built from constants and function symbols (can be nested); an atomic sentence is a predicate applied to one or more terms.

August 25 (Monday)

Covered Sections 2.1 and 2.5.
Valid and sound arguments. The use of counterexamples to demonstrate non-consequence.

August 27 (Wednesday)

Gave examples of how to derive a conclusion from a set of premises, thereby demonstrating that the given argument is valid. (Read Sections 2.2-2.4.)

August 29 (Friday)

Homework 1 in. Homework 2 out. Finished Sections 2.2-2.4.
Formal vs. informal reasoning. The formal deductive system F; the program Fitch. Elimination and introduction rule for the identity predicate.

September 1 (Monday)

Student/University holiday

September 3 (Wednesday)

Covered Chapter 3: Negation, Conjunction, Disjunction. Compared "\/" to "exclusive or". The game in Tarski's world. Ambiguities in FOL, and how to resolve them. DeMorgan's law (verified using truth tables).

September 5 (Friday)

Graded pen & paper part of Homework 1 back. Homework 2 in. Homework 3 out.
Started on Chapter 4. Stated some equivalences: commutativity, associativity, distributivity, etc. These are tautological equivalences. We also introduced the notions of logical equivalence and TW-equivalence, forming a hierarchy (cf. Figure 4.1)

September 8 (Monday)

Finished Chapter 4. The hierarchy of "necessities" in Figure 4.1. The notion of a tautology (a simple, though not very powerful, way to detect logical necessity), defined using truth tables. Tautological, logical, and TW-consequence, forming a hierarchy similar to the one of Figure 4.1 and reflected in the Fitch rules Taut Con, FO Con, Ana Con. Sentences in Negation Normal Form (NNF). Using the distributive law, a sentence can be converted into Conjunctive Normal Form (CNF); then it's cheap to check whether it is a tautology.

September 10 (Wednesday)

Cover Chapter 5, introducing two crucial proof principles: proof by cases; proof by contradiction (indirect proof).

September 12 (Friday)

Graded pen & paper part of Homework 2 back. Homework 3 in. Homework 4 out.
Covered Sections 6.1-6.3: elimination and introduction rules for conjunction, disjunction, negation, contradiction. Dsjunction elimination corresponds to "proof by cases"; negation introduction corresponds to "proof by contradiction".

September 15 (Monday)

Announced Exam 1, to be held on Wednesday, October 8.
Finished Chapter 6, working through some examples of how to construct proofs using the rules given. A sentence which can be proved from no premises is a logical truth.

September 17 (Wednesday)

Graded pen & paper part of Homework 3 back.
Introduced two new connectives: "->" (which might be pronounced "implies") in Section 7.1; "<->" (to be pronounced "if and only if", abbreviated "iff") in Section 7.2. The notion of truth-functional completeness (Section 7.4).

September 19 (Friday)

Homework 4 in. Homework 5 out.
Covered Sections 8.1 and 8.2: Elimination and Introduction rules for -> and <->. More examples of proofs.

September 22 (Monday)

Wrapped up part I of the textbook, by going through some homework exercises. Agreed on having "review sessions" each Tuesday, 5-6pm.

September 24 (Wednesday)

Started on Part II of the book: motivated by the desire to express the four Aristotelian forms (Section 9.5) in FOL we introduced variables (Section 9.1) and forall/exists quantifiers (Section 9.2), resulting in the definition (p.231) of a well-formed formula (wff).

September 26 (Friday)

Graded pen & paper part of Homework 4 back. Homework 5 in. Homework 6 out.
Finish Chapter 9, in particular covering the notion of free and bound variables (Section 9.3). Begin on Chapter 10 (in the presence of quantifiers, which arguments are valid?)

September 29 (Monday)

Truth and consequences in the presence of quantifiers: while the tautological approach is still of (limited) use (Section 10.1), we shall focus on the crucial notion of first-order consequence (Section 10.2) which will be captured by the proof rules introduced in Chapter 13. To prove consequences that are due to the intrinsic meaning of predicate symbols, one can use the axiomatic method (Section 10.5).

October 1 (Wednesday)

Cover Exercise 8.52, illustrating proper uses of TautCon and AnaCon. Various quantifier equivalences, including DeMorgan (Sections 10.3 and 10.4).

October 3 (Friday)

Homework 6 in. Homework 7 out.
Wrap up the first 10 chapters of the book. Go through Exercises 8.48, 8.50, and essentially 10.20.

October 6 (Monday)

Class canceled as instructor out of town. Prepare for Wednesday's exam.

October 8 (Wednesday)

Exam I.

October 10 (Friday)

Class canceled as instructor out of town.

October 13 (Monday)

Student holiday

October 15 (Wednesday)

More advanced examples of translation from English into FOL, covering Sections 11.1-11.5.

October 17 (Friday)

Homework 7 in. Homework 8 out.
Translations using function symbols (Section 11.6). Universal elimination and Existential introduction (Section 12.1); Existential instantiation (Section 12.2).

October 20 (Monday)

Graded Exam I handed back (Suggested solutions).

October 22 (Wednesday)

Recapitulate method of Existential instantiation (Section 12.2), reflected in the Elimination rule for the Existential quantifier (Section 13.2). The method of General conditional proof (Section 12.3), reflected in the Introduction rule for the Universal quantifier (Section 13.1). Examples of proofs with quantifiers (cf. Section 13.3): we derived 2 of the 4 DeMorgan inferences.

October 24 (Friday)

Graded pen & paper part of Homework 7 back. Homework 8 in. Homework 9 out.
More examples of proofs with quantifiers, including the tricky interaction between existential instantiation and general conditional proof (Section 12.4).

October 27 (Monday)

Reviewed selected parts of the challenging Homework 8: Exercise 11.4 (3,5,7); Exercise 11.17 (2,6,9); Exercise 11.18 (1,3).

October 29 (Wednesday)

Continued reviewing selected parts of Homework 8 (also see here for feedback): Exercise 11.18 (3); Exercise 11.19 (1,3,5); Exercise 11.26 (1,2,5,6,9,10); Exercise 11.39 (4).

October 31 (Friday)

Homework 9 in. Homework 10 out.
Mention, and illustrate by examples, that our proof system is sound and complete (Section 13.4). The Barber Paradox (p.333), with deep implications for modern mathematics...

November 3 (Monday)

Embark on Part III of the course, starting with induction on natural numbers (Section 16.3): if we prove Q(0), and prove that Q(n) implies Q(n+1), then Q holds for all natural numbers! We saw an example (sum of angles in polygons) where the base case is '3' (rather than '0' or '1').
The textbook contains a minor error: on p. 454, the first natural number is defined to be zero, but Proposition 4 only holds if the first natural number is assumed to be one.

November 5 (Wednesday)

The general principle of induction (Section 16.1). Gave some examples of inductive definitions, in particular we looked at ambig-wffs (p.444). Motivated the concept of an inductive proof, using the domino analogy. Proved by induction that no ambig-wff ends with a negation sign; we needed an auxiliary result stating that the empty string is not an ambig-wff.

November 7 (Friday)

Graded pen & paper part of Homework 9 back (feedback here). Homework 10 in.
Continue on Induction, working through Exercise 16.18.

November 10 (Monday)

Induction principle for lists. Distribute Supplementary Notes on Induction.

November 12 (Wednesday)

Graded Homework 10 back, going through the questions (suggested solutions can be found here). Homework 11 out.

November 14 (Friday)

Exam II.

November 17 (Monday)

TEVAL (if you were not there, you can go to the front office and fill out the questionnaire).
Graded Exam II handed back (Suggested solutions).

November 19 (Wednesday)

Introduction to program verification: writing specifications; the notion of Hoare triples; the three-stage approach to software engineering. Distribute Lecture notes on Program Verification.
A brief reminder of lists: the append function, and the induction principle (we started proving that append is associative).
No office hours today.

November 21 (Friday)

Homework 11 in. Homework 12 out.
Continue program verification, covering Section 16.5 of LPL: program properties can be verified by induction in the number of times a loop is executed!

November 24 (Monday)

Emphasized the crucial role of loop invariants for program verification. Example program: one computing the factorial function. Reading material: Lecture notes on Program Verification (Section 4).
No review session Tuesday afternoon.

November 26 (Wednesday)

Student holiday

November 28 (Friday)

Student/University holiday (Thanksgiving)

December 1 (Monday)

Continued covering Lecture notes on Program Verification: proof rules for valid annotations (Section 4.3); the notion of a well-annotated program. Went through another example of how to well-annotate programs (Appendix A, Question 1).

December 3 (Wednesday)

Embarked on Section 5 of Lecture notes on Program Verification, giving an example of how to develop a program together with its correctness proof. Went through yet another example of how to well-annotate programs (Appendix A, Question II).
Graded Homework 11 back (suggested solutions here).

December 5 (Friday)

Homework 12 in.
Continued Section 5 of Lecture notes on Program Verification, showing that the methodology even enables us to construct an efficient program.

December 8 (Monday)

Graded Homework 12 back (suggested solutions here).
Show how the use of Hoare triples and quantifiers enables us to express secrecy of data as well as integrity of data; distribute Lecture notes on Logic for Security.
We have now covered all of the material of the course :)

December 10 (Wednesday)

Last day of class. We looked back at the course and discussed potential improvements.

December 15 (Monday)

Exam III (Final), 11:50am to 1:20pm in N122