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

August 18 (Wednesday)

David Schmidt gives introduction to the course, on behalf of Torben Amtoft, and hands out the syllabus.
A brief motivation for why to study this course; this includes the development of a specification, written in First Order Logic (FOL), of the square root function.
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 20 (Friday)

Homework 1 out.
David Schmidt will cover 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 23 (Monday)

Torben Amtoft (on video from K-State Online) will cover Sections 2.1 and 2.5: valid and sound arguments; the use of counterexamples to demonstrate non-consequence.
Slides.

August 25 (Wednesday)

Torben Amtoft (on video from K-State Online) will 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. The formal deductive system F; the software Fitch. Elimination and introduction rule for the identity predicate.
Slides.

August 27 (Friday)

Homework 1 in (paper part should be turned in to the front office).
Homework 2 out.
Torben Amtoft (on video from K-State Online) will cover Chapter 3: Negation, Conjunction, Disjunction. Compare "\/" to "exclusive or". Ambiguities in FOL, and how to resolve them. The game in Tarski's world.
Slides.

August 30 (Monday)

Class cancelled (instructor stranded in Detroit due to air traffic delay)

September 1 (Wednesday)

Torben Amtoft is back in town, and after a brief introduction handed back Graded Homework 1.
Then started on Chapter 4, stating DeMorgan's laws which can be verified using truth tables.

September 3 (Friday)

Homework 2 in. Homework 3 out.
State some equivalences: commutativity, associativity, distributivity, etc; these are tautological equivalences. The notion of a tautology.
Using DeMorgan, and double negation, a sentence can be converted to Negation Normal Form (NNF). Using the distributive laws, a sentence can be converted into Conjunctive Normal Form (CNF).

September 6 (Monday)

Student holiday (Labor Day)

September 8 (Wednesday)

Graded Homework 2 handed back, and (almost) concluded Chapter 4.
Elaborate on the notion of CNF, convenient to check whether a sentence is a tautology.
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).

September 10 (Friday)

Homework 3 in. Homework 4 out.
Discuss the hierarchy of "consequences" (similar to Figure 4.1) which is reflected in the Fitch rules Taut Con, FO Con, Ana Con.
Cover Chapter 5, introducing two crucial proof principles: proof by cases; proof by contradiction (indirect proof).

September 13 (Monday)

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".

September 15 (Wednesday)

Graded Homework 3 given back, going through Exercises 4.8 and 4.27. Working through some examples of how to construct proofs using the rules given: first prove a general pattern, which was used twice in Exercise 4.27; next prove one of the four arguments which constitute DeMorgan's laws.

September 17 (Friday)

Homework 4 in. Homework 5 out.
Return to Chapter 5, presenting non-trivial instances of "proof by contradiction" and "proof by cases". Present a formal proof for one more of the arguments which constitute DeMorgan's laws. Discuss the relationship between formal and informal proofs.

September 20 (Monday)

A sentence which can be proved from no premises is a logical truth. Reminder: never reuse sentences from a subproof which has ended (Fitch actually prevents that). Start on Chapter 7, introducing two new connectives: "->" (which might be pronounced "implies") and "<->" (to be pronounced "if and only if", abbreviated "iff").

September 22 (Wednesday)

Graded Homework 4 given back, going through Exercise 6.14.
Cover Sections 8.1 and 8.2: Elimination and Introduction rules for -> and <->.

September 24 (Friday)

The notion of truth-functional completeness (Section 7.4).
Wrap up Part I of the book, also give a few hints for HW 5.

September 27 (Monday)

Homework 5 in.
Go through selected exercises from Chapter 8, in particular 8.48 and 8.50.

September 29 (Wednesday)

Distribute the first 9 pages of Lecture notes on Program Verification, and cover Sections 1-3: writing specifications; the notion of Hoare triples; the three-stage approach to software engineering.

October 1 (Friday)

Graded Homework 5 given back. Homework 6 out.
Cover Sections 4-5 of Lecture notes on Program Verification: motivated by a program computing the factorial function, we introduce the crucial notion of loop invariants.

October 4 (Monday)

Test I. (Amtoft has no office hours today)

October 6 (Wednesday)

Cover Section 6 of Lecture notes on Program Verification: we 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.

October 8 (Friday)

Homework 6 in. Homework 7 out.
Cover Section 7 of Lecture notes on Program Verification: illustrated by examples, 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.

October 11 (Monday)

Student holiday (Columbus Day)

October 13 (Wednesday)

Graded Test I back.
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).

October 15 (Friday)

Graded Homework 6 given back.
Continue Chapter 9, getting more familiar with quantifiers, with focus on how to translate numeric quantifiers such as "at least two" or "exactly one".

October 18 (Monday)

Formalize the extension of FOL, giving the definition of a well-formed formula (wff) and introducing the notion of free and bound variables (Section 9.3).

October 20 (Wednesday)

Homework 7 in. Homework 8 out.
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 Chapters 12 and 13. 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 22 (Friday)

Finish Chapter 10, with focus on various quantifier equivalences, including DeMorgan (Sections 10.3 and 10.4).
Graded Homework 7 given back.

October 25 (Monday)

Cover Exercises 6 and 7 from Homework 7, giving formal proofs of the correctness of programs by well-annotating them.
Start on Chapter 11, with an example of an English sentence whose translation into FOL requires both universal and existential quantification.

October 27 (Wednesday)

Homework 8 in.
Continue Chapter 11, with emphasis (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. Which one to choose is often determined by context; the corresponding translations are not FO-equivalent though in certain cases they may be TW-equivalent.

October 29 (Friday)

Homework 9 out.
Finish Chapter 11 (except that Section 11.7 is not covered), giving more examples of translations from English into FOL, in particular translations using function symbols (Section 11.6). We also encounter a "donkey sentence" which has to be paraphrased before it becomes obvious how to translate it.

November 1 (Monday)

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

November 3 (Wednesday)

The methods of General conditional proof and Universal generalization (Section 12.3), reflected in the Introduction rule(s) for the Universal quantifier (Section 13.1). We used the new rules to derive 2 of the 4 DeMorgan inferences. We highlighted some of the ambiguities of Exercise 11.26.

November 5 (Friday)

Homework 9 in. Homework 10 out.
Graded Homework 8 back; use Exercises 10.14, 10.10, 10.13 to illustrate that our proof system is sound and complete (Section 13.4).

November 8 (Monday)

More examples of proofs with quantifiers (cf. Section 13.3), including the tricky interaction between existential instantiation and universal generalization (Section 12.4).

November 10 (Wednesday)

The Barber Paradox (p.333), with deep implications for modern mathematics in that it expels us from "Cantor's paradise": naive set theory leads to contradictions!
One more "DeMorgan inference" (p.355), showing Ex~P(x) from ~AxP(x). 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!
Emphasize (stated p.???) that worlds must be non-empty (as otherwise too many laws would break down).

November 12 (Friday)

Homework 10 in. Graded Homework 9 back, covering some of the questions from Exercises 11.19 and 11.26.
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 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 15 (Monday)

TEVAL (if you were not there, you can go to the front office and fill out the questionnaire).
Graded homework 10 back, going through most of the exercises.

November 17 (Wednesday)

Test II. Homework 11 out.

November 19 (Friday)

Continue induction on natural numbers, giving an example (sum of angles in polygons) where the base case is '3' (rather than '0' or '1'). We argued that the induction principle is valid, based on the fact that any non-empty set of natural numbers has a least element.

November 22 (Monday)

Graded Test II back (model solutions).
Briefly discuss selected exercises from the upcoming Homework 11.

November 24-26 (Wednesday-Friday)

Thanksgiving holiday

November 29 (Monday)

Cover the general principle of induction (Section 16.1), giving some examples of inductive definitions, for instance ambig-wffs (p.444) but in particular lists (Section 3 of Lecture notes on Induction).

December 1 (Wednesday)

Prove 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 L(p) <= C(p) + 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!

December 3 (Friday)

Homework 11 in. Homework 12 out.
Cover induction on lists (Section 3 in Lecture notes on Induction), proving properties about the append function.
Prove that every third fibonacci number is even, something which requires a slightly different formulation of induction (Section 2.1 in Lecture notes on Induction).

December 6 (Monday)

Verification of programs with procedures, using Section 9 in Lecture notes on Program Verification.
Graded Homework 11 back.

December 8 (Wednesday)

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.

December 10 (Friday)

Homework 12 in.
Course review.
Verification of programs manipulating arrays, using Section 10 in Lecture notes on Program Verification.

December 16 (Thursday)

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