Captain's Log: Logical Foundations of Programming, Spring 2004

January 23 (Friday)

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.

January 26 (Monday)

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.

January 28 (Wednesday)

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

January 30 (Friday)

Homework 1 in. Homework 2 out.
Covered Sections 2.2-2.4, giving examples of how to derive a conclusion from a set of premises, thereby demonstrating that the given argument is valid. The formal deductive system F; the software Fitch. Elimination and introduction rule for the identity predicate.

February 2 (Monday)

University closed, due to snow.

February 4 (Wednesday)

Covered Chapter 3: Negation, Conjunction, Disjunction. Compared "\/" to "exclusive or". Ambiguities in FOL, and how to resolve them. The game in Tarski's world.

February 6 (Friday)

Homework 3 out. Graded Homework 1 back.
Started on Chapter 4. DeMorgan's laws (verified using truth tables). 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): for two sentences to be TW-equivalent they must be equivalent in Tarski's world; to be logically equivalent they must be equivalent in all possible worlds; to be tautologically equivalences they must be equivalent for all combinations of truth values (thereby in all possible worlds, and even some impossible worlds!)

February 9 (Monday)

Homework 2 in.
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.

February 11 (Wednesday)

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

February 13 (Friday)

Homework 3 in. Homework 4 out. Graded Homework 2 back.
Discussed the relationship between formal and informal proofs; then embarked on Chapter 6: formal proofs involving the boolean connectives. Covered most of Sections 6.1-6.3, presenting various elimination and introduction rules. Disjunction elimination corresponds to "proof by cases"; negation introduction corresponds to "proof by contradiction".

February 16 (Monday)

Continued Chapter 6, presenting the remaining proof rules (introduction & elimination). Notion of subproof; never reuse sentences from a subproof which has ended! A sentence which can be proved from no premises is a logical truth.

February 18 (Wednesday)

Finished Chapter 6, working through some examples of how to construct proofs using the rules given (in particular, proving the four arguments that constitute DeMorgan's laws).

February 20 (Friday)

Homework 4 in. Homework 5 out. Graded Homework 3 back, going through Exercises 4.8, 4.27, 4.43.
Covered Section 7.1, introducing one more connective: "->" (which might be pronounced "implies").

February 23 (Monday)

Cover Section 7.2, introducing the final connective: "<->" (to be pronounced "if and only if", abbreviated "iff"). Cover Sections 8.1 and 8.2: Elimination and Introduction rules for -> and <->.

February 25 (Wednesday)

The notion of truth-functional completeness (Section 7.4).
Give a few hints for HW 5, in particular sketch Exercise 8.50 (quite similar to Exercise 8.52).

February 27 (Friday)

Distribute Lecture notes on Program Verification (part I) and cover Sections 1-3 there: writing specifications; the notion of Hoare triples; the three-stage approach to software engineering.

March 1 (Monday)

Homework 5 in.
Start on Section 4 of Lecture notes on Program Verification (part I). Emphasize the crucial role of loop invariants for program verification. Example program: one computing the factorial function.

March 3 (Wednesday)

Graded Homework 4 back.
Go through selected exercises from Homeworks 4 & 5, in particular Exercise 8.52.
Continue covering Lecture notes on Program Verification (part I): proof rules for valid annotations (Section 4.3).

March 5 (Friday)

Test I.
Homework 6 out.

March 8 (Monday)

More about how to well-annotate programs, going through the example from Appendix A, Question 1, in Lecture notes on Program Verification (part I).

March 10 (Wednesday)

Graded Test I back (solution key).
One more example of how to well-annotate programs: Appendix A, Question 3, in Lecture notes on Program Verification (part I).

March 12 (Friday)

Homework 6 in. Homework 7 out.
Cover Section 5 of Lecture notes on Program Verification (part I), giving an example of how to develop a program together with its correctness proof, and showing that the methodology even enables us to construct an efficient program.

March 15 (Monday)

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

March 17 (Wednesday)

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?)

March 19 (Friday)

Homework 7 in. Homework 8 out. Graded Homework 6 back.
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.

March 22--26

Spring break

March 29 (Monday)

Various quantifier equivalences, including DeMorgan (Sections 10.3 and 10.4). The axiomatic method (Section 10.5) enables us to prove consequences that (unlike first-order consequences) are due to the intrinsic meaning of predicate symbols.

March 31 (Wednesday)

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

April 2 (Friday)

Class canceled (University Open House).
Homework 9 out.

April 5 (Monday)

Homework 8 in. Graded Homework 7 back.
Translations using function symbols (Section 11.6). Saw an example of a "donkey sentence" which had to be paraphrased before it became obvious how to translate it.

April 7 (Wednesday)

Universal elimination and Existential introduction (Section 12.1), the latter leading to a discussion of Fermat's Last Theorem. Existential instantiation (Section 12.2), reflected in the Elimination rule for the Existential quantifier (Section 13.2).

April 9 (Good Friday)

The method of General conditional proof (Section 12.3), reflected in the Introduction rule for the Universal quantifier (Section 13.1). We used the new rules to derive 2 of the 4 DeMorgan inferences.

April 12 (Monday)

Homework 9 in. Homework 10 out.
More examples of proofs with quantifiers (cf. Section 13.3), including the tricky interaction between existential instantiation and general conditional proof (Section 12.4). One more DeMorgan inference.

April 14 (Wednesday)

Mention, and illustrate using Exercises 10.14, 10.10, 10.13 (from Homework 8), that our proof system is sound and complete (Section 13.4).

April 16 (Friday)

Graded Homework 8 back.
The Barber Paradox (p.333), with deep implications for modern mathematics (naive set theory leads to contradictions!)
The fourth DeMorgan inference, showing Ex~P(x) from ~AxP(x). (p.355, where it is also mentioned that this inference is not accepted by "intuitionists" as it doesn't give us any clue about which x satisfies ~P; in general intuitionists don't like the ~Elim rule but we shall not follow their restricted approach!)

April 19 (Monday)

TEVAL (if you were not there, you can go to the front office and fill out the questionnaire).
Homework 10 in, cover Exercise 13.31 (first giving informal proof).
For Homework 9, we went through a few questions, taken from Exercises 11.4, 11.11, 11.16.

April 21 (Wednesday)

Test II.

April 23 (Friday)

Homework 11 out.
We start on the exciting topic of induction, a special case of which we have seen already in the proof principle for program invariants: if P holds after zero loop iterations, and if P holds after k+1 loop iterations provided that P holds after k loop iterations, then P holds after any number of loop iterations.
We covered Section 16.3 in the textbook, dealing with induction on natural numbers: 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.

April 26 (Monday)

The general principle of induction (Section 16.1), giving some examples of inductive definitions; in particular we looked at ambig-wffs (p.444). Proved by induction that with C(p) the number of connectives in an ambig-wff and with L(p) the number of propositional letters in an ambig-wff, it holds that C(p) >= L(p) - 1.

April 28 (Wednesday)

Continue covering induction from various perspectives. Look at Exercise 16.18 from the upcoming homework; we realized that the result cannot be proved as it is and that we need to prove a stronger property, telling not only that the sum of the first n cubes is a square but also what it is the square of!

April 30 (Friday)

Homework 11 in. Homework 12 out. Graded Homework 10 back.
Distribute Lecture notes on Induction; cover Section 3 introducing induction on lists.

May 3 (Monday)

Continue induction on lists (Section 3 in Lecture notes on Induction), proving that the append function is associative. Proved that every third fibonacci number is even, something which requires a slightly different formulation of induction (Section 2.1 in Lecture notes on Induction). Briefly cover some of Homework 11.

May 5 (Wednesday)

Verification of programs manipulating arrays, using Lecture notes on Program Verification (part II). (Keep in mind that in annotations, two kinds of variables occur; those in typewriter font are those that occur in the program.)

May 7 (Friday)

Homework 12 in.
Show how the use of Hoare triples and quantifiers enables us to express secrecy of data as well as integrity of data, as described in Lecture notes on Logic for Security.

May 10 (Monday)

Last day of class.
Graded Test II back (solution key).
Graded Homeworks 11 & 12 back.

May 12 (Wednesday)

No class (instructor out of town).

May 21 (Friday)

11:50am-1:40pm (N122): Final exam.