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

August 22 (Monday)
Syllabus handed out. A brief motivation for why to study this course, sketching two examples (square root, array maximum) of how to use First Order Logic (FOL) for the specification of software.
Before next time: read the introduction of LPL (the text book), start playing with the software, and preferably start reading a bit of Chap 1.
August 24 (Wednesday)
Revised version of syllabus handed out.
We covered Chapter 1 (Sections 1.1-1.5) of textbook. A number of worlds (including Tarski's world) presented, together with corresponding variants of FOL (used as running examples throughout course).
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 26 (Friday)
Homework 1 (& Quiz 1) out.
Wrap up Chapter 1 (cover Exercises 1.16 and 1.17).
Cover Sections 2.1 and 2.5: an argument has a number of premises and one conclusion, and we distinguish between valid (some of which are also sound) and invalid arguments; counterexamples are used to demonstrate that a given argument is invalid (that is, the conclusion is "non-sequitur").
(You may take a look at Slides from last year.)
August 29 (Monday)
Cover 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. For formal proofs, we use the deductive system F, implemented as the software Fitch (tuned for Tarski's world). Elimination and introduction rule for the identity predicate.
(You may take a look at Slides from last year.)
August 31 (Wednesday)
Cover Chapter 3: Negation, Conjunction, Disjunction. Compare "\/" to "exclusive or". Ambiguities in FOL (and in English), and how to resolve them.
(You may take a look at Slides from last year.)
September 2 (Friday)
Homework 1 (& Quiz 1) in. Homework 2 out.
Start on Chapter 4, stating DeMorgan's laws which can be verified using truth tables, and also some other (tautological) equivalences: commutativity, associativity, distributivity, etc.
Using DeMorgan, and double negation, a sentence can be converted to Negation Normal Form (NNF).
Do Exercises 4.31(7) and 4.34.
September 5 (Monday)
Labor Day: student/university holiday
September 7 (Wednesday)
Continue Chapter 4. The notion of a tautology. Using the distributive laws, a sentence can be converted into Conjunctive Normal Form (CNF), convenient for checking whether a tautology. Dually, we have Disjunctive Normal Form (DNF).
Graded Homework 1 back.
No review session this afternoon.
September 9 (Friday)
Homework 2 in. Homework 3 out.
Finish Chapter 4. We introduce the notions of logical equivalence and TW-equivalence, forming a hierarchy (similar to Figure 4.1, p.102): 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 equivalent they must be equivalent for all combinations of truth values (thereby in all possible worlds, and even some impossible worlds!) Similarly, we have a hierarchy of "necessities" (Figure 4.1), illustrated by Exercise 4.8, and a hierarchy of "consequences" which is reflected in the Fitch rules Taut Con, FO Con, Ana Con.
Sunday (Sep 11) is the last day for full refund.
September 12 (Monday)
Cover Chapter 5, introducing two crucial proof principles: proof by cases; proof by contradiction (indirect proof).
September 14 (Wednesday)
Cover 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". Do Exercise 6.5.
September 16 (Friday)
Homework 3 in. Homework 4 out. Graded Homework 2 back.
Continue Chapter 6, working through some examples of how to construct proofs using the rules given: Exercises 6.18, 6.28, 6.19 (the latter proves a general pattern which was used twice in Exercise 4.27).
September 19 (Monday)
Finish Chapter 6, with more examples of how to construct proofs: we did it for each of the 4 arguments which constitute DeMorgan's laws. Reminder: never reuse sentences from a subproof which has ended (Fitch actually prevents that).
September 21 (Wednesday)
Start on Chapter 7, introducing two new connectives: "->" (which might be pronounced "implies") and "<->" (to be pronounced "if and only if", abbreviated "iff"). Briefly touch on Exercises 7.12 & 7.21.
Today, Amtoft's office hours are 3:30pm-4:30pm.
September 23 (Friday)
Homework 4 in. Homework 5 out.
Cover most of Sections 8.1 and 8.2: how to reason about -> (examples in Exercise 8.1), formalized by Elimination and Introduction rules which were applied in Exercise 8.19 and Exercises 8.7&35.
September 26 (Monday)
Graded Homeworks 3 & 4 back.
Finish Sections 8.1 and 8.2: Elimination and Introduction rules for <->, with example applications (like Exercise 8.29); in particular, discuss how to prove a chain of biconditionals (cf. Exercise 8.15). Prove Excluded Middle (Exercise 6.33).
Last day to drop out without a W being recorded.
September 28 (Wednesday)
The notion of truth-functional completeness (Section 7.4), doing Exercises 7.26 & 7.30 & 7.32.
Soundness and completeness of the formal system F (Section 8.3, omitting the proofs of the theorems). Do Exercise 8.50, showing the power and convenience of TautCon.
This completes Part I of the textbook
September 30 (Friday)
Homework 5 in; do Exercises 8.30 (showing the tremendous power of "Proof by Contradiction") and 8.52 (showing proper use of TautCon).
Distribute Lecture notes on Program Verification, and cover the first 4 pages: writing specifications as Hoare triples; the notions of partial correctness (never get a wrong result) versus total correctness (always get the right result); the three-stage approach to software engineering.
October 3 (Monday)
Student holiday
October 5 (Wednesday)
Graded Homework 5 back.
Motivated by a program for computing the factorial function, we introduce the crucial notion of loop invariants, as described in Section 5 of Lecture notes on Program Verification (we also briefly covered Question V there).
Today, Amtoft's office hours are 4pm-5pm.
October 7 (Friday)
Test I.
October 10 (Monday)
Graded Test I back.
Homework 6 out.
Repeated the proof principles for loop invariants, stated in Section 5.2 of Lecture notes on Program Verification; we applied these principles to the program given in Question III there.
October 12 (Wednesday)
Present an example of how to develop a program together with its correctness proof, then show that the methodology even enables us to construct an efficient program (Section 6 of Lecture notes on Program Verification).
October 14 (Friday)
Homework 6 in. Homework 7 out.
Cover Section 7 of Lecture notes on Program Verification: illustrated by examples (like Question V from Appendix), we introduce the notion of valid assertions (defined by proof rules); showing that a program is well-annotated is a formal and fine-grained way of proving its correctness.
Discuss the general relationship between formal and informal proofs.
October 17 (Monday)
Brief appetizer for 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). We also address how to translate claims such as "at least two".
Class stops at 11am. Amtoft's office hours today are from 3pm to 3:30pm.
October 19 (Wednesday)
Continue (and finish) Chapter 9, getting more familiar with quantifiers. In addition to expressing the four Aristotelian forms, we address how to translate numeric claims such as "exactly one" or "at most one". Sketch the definition of a well-formed formula (wff), and introduce the notion of free and bound variables (Section 9.3).
October 21 (Friday)
Homework 7 in. Homework 8 out. Graded Homework 6 back.
Present various quantifier equivalences, including DeMorgan (Sections 10.3 and 10.4).
October 24 (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). A first-order consequence (FO consequence for short) is an argument which remains valid if the predicates in question (except for the identity "=") are consistently replaced by other (even nonsense) predicates; the proof rules to be introduced in Chapters 12 and 13 enable us to prove all FO consequences (and nothing but FO consequences).
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.
October 26 (Wednesday)
Graded Homework 7 back.
Embark on Chapter 11, looking at English sentences whose translation into FOL requires both universal and existential quantification. Emphasis will be (cf. Section 11.5) on the difference between "weak" (for all x there exists a y that works for that x) and "strong" (there exists a y that works for all x) readings of an English sentence.
October 28 (Friday)
Homework 8 in. Homework 9 out.
Elaborate on the difference between strong and weak readings: the corresponding translations are not FO-equivalent, though in certain cases they may be TW-equivalent. In general, the proper translation into FOL of an English sentence is often determined by context, as illustrated by Exercise 11.43.
Revisit Exercise 1.15(5), and show that in the presence of quantifiers, we can do without function symbols, but at the cost of making our life more miserable due to extra quantifiers, as illustrated by Exercise 11.29(2).
We encounter a "donkey sentence" (p.301) which has to be paraphrased before it becomes obvious how to translate it: even though the sentence strongly suggests the use of an existential quantifier, this will not work and we have to use a universal quantifier instead.
Exercise 11.45 considers two seemingly non-equivalent English sentences and shows them to be equivalent; the key part is our ability to infer Ex~P(x) from ~AxP(x). Lesson to be learned: claiming ExQ(x) does not entail that we have any idea about the name of the object satisfying Q!
This finishes Chapter 11 (except that Section 11.7 is not covered).
Today is the last day to drop the course.
October 31 (Monday)
We embark on the proof rules for the quantifiers:
November 2 (Wednesday)
Mention that our proof system is sound and complete (Section 13.4).
More examples of proofs which use the newly introduced rules for quantifiers (cf. Section 13.3), like two of the four "DeMorgan inferences"; also discuss the tricky interaction between existential instantiation and universal generalization (Section 12.4).
November 4 (Friday)
Do the remaining two DeMorgan inferences, the last of which showing Ex~P(x) from ~AxP(x). This inference (cf. p.355) 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!
Do Exercises 12.28 and 12.13, presenting variants of "The Barber Paradox" (p.333) which has deep implications for modern mathematics in that it expels us from "Cantor's paradise": naive set theory leads to contradictions!
Prove (almost!) the equivalence between two alternative ways of expressing "there exists at most one P".
November 7 (Monday)
Homework 9 in.
Finish the proof of equivalence between two alternative ways of expressing "there exists at most one P". Cover the issue of axiomatization (Section 12.5), illustrated by comparing Exercise 13.32 (use of AnaCon) to Exercise 13.33 (use of an axiom), and by Exercise 12.37 where we gave axioms for "MoreSides". Then discuss troublesome questions from Exercise 11.20 in HW 9.
November 9 (Wednesday)
Graded Homework 8 back.
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 Section 8 in Lecture notes on Program Verification.
November 11 (Friday)
Test II.
November 14 (Monday)
Graded Homework 9 back. Homework 10 out.
Verification of programs with procedures, using Section 9 in Lecture notes on Program Verification. Also show, using a board simulation, how to implement recursive procedures.
November 16 (Wednesday)
Verification of programs reading arrays, in particular develop a program for finding the maximum element of an array (Section 10.1 in Lecture notes on Program Verification).
November 18 (Friday)
Graded Test II back.
Verification of programs modifying arrays (Section 10.2 in Lecture notes on Program Verification).
November 21 (Monday)
Homework 10 in (no Quiz).
Wrap up the material on program verification, by finishing the example program from Sect. 10.2 which rearranges an array so that the largest element is first.
Then 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 Q holds after zero loop iterations, and if Q holds after k+1 loop iterations provided that Q holds after k loop iterations, then Q holds after any number of loop iterations.
We cover 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!
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 23-25 (Wednesday-Friday)
Thanksgiving holiday
November 28 (Monday)
TEVAL. Homework 11 out. Notes on induction handed out.
Continue induction on natural numbers, with examples including Exercise 16.15, and an application (sum of angles in polygons) where the base case is '3' (rather than '0' or '1').
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!
November 30 (Wednesday)
Graded Homework 10 back.
We introduce immutable lists (cf. Section 3 in Lecture notes on Induction): first we give an inductive definition of lists, using which we write some recursive functions manipulating lists, like "sumlist" and "removezero" (cf. the upcoming homework); next we state the induction principle for lists, and prove by induction that for all lists x, sumlist(removezero(x)) = sumlist(x).
December 2 (Friday)
More examples of induction: Define the 'append' function '++' for concatenating two immutable lists; prove by induction that this function has 'nil' as neutral element (that is, not only is nil ++ x = x for all x, as the definition of '++' prescribes, but also x ++ nil = x holds for all x). Exercise 16.1 (induction is a pleasant principle!) and Exercise 16.2 (where premises are inconsistent). Define the fibonacci function on natural numbers, argue (without explicitly invoking the induction principle) that exactly every third fibonacci number is even, and introduce the "golden ratio" as a preparation for giving a formula for the fibonacci numbers.
December 5 (Monday)
Homework 11 in (including Quiz 11); we covered Exercise 10 (simultaneous construction & verification of an array program).
We state, and prove, a formula for the value of the n'th fibonacci number, something which would be virtually impossible to do without the induction principle (a slightly different formulation of which is required, cf. Section 2.1 in Lecture notes on Induction).
As an appetizer for future encounters with logic (though not part of the exam material in this course), we also introduce CTL (computation tree logic).
December 7 (Wednesday)
Amtoft out of town from today, but Chris will be there to give back Graded Homework 11, and answer other questions you may have.
December 9 (Friday)
Last day of semester. Class canceled.
December 13 (Tuesday)
Test III (Final exam), 11:50am-1:40pm.

Torben Amtoft