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

January 12 (Wednesday)

Syllabus handed out. 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.

January 14 (Friday)

Homework 1 out.
We covered Chapter 1 (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 17 (Monday)

University Holiday (Martin Luther King)

January 19 (Wednesday)

After wrapping up Chapter 1 (did Exercise 1.17), we covered Sections 2.1 and 2.5: valid and sound arguments; the use of counterexamples to demonstrate non-consequence (did Exercise 2.2). (Slides from last year.)

January 21 (Friday)

Homework 1 in. Homework 2 out.
We 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. (Slides from last year.)

January 24 (Monday)

Graded Homework 1 back.
We covered Chapter 3: Negation, Conjunction, Disjunction. Compare "\/" to "exclusive or". Ambiguities in FOL (and in English), and how to resolve them. The game in Tarski's world.

January 26 (Wednesday)

We shall 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).

January 28 (Friday)

Homework 2 in. Homework 3 out.
Continued 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).

January 31 (Monday)

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), and a hierarchy of "consequences" which is reflected in the Fitch rules Taut Con, FO Con, Ana Con.
Tomorrow (Tue Feb 1) is last day for 100% refund.

February 2 (Wednesday)

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

February 4 (Friday)

Homework 3 in. Homework 4 out. Graded Homework 2 back.
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".

February 7 (Monday)

Continue Chapter 6, working through some examples of how to construct proofs using the rules given, in particular prove a general pattern which was used twice in Exercise 4.27.
Tomorrow (Tue Feb 8) is last day for 50% refund

February 9 (Wednesday)

Graded Homework 3 back.
Present formal proofs for 3 of the 4 arguments which constitute DeMorgan's laws. Reminder: never reuse sentences from a subproof which has ended (Fitch actually prevents that).

February 11 (Friday)

Homework 4 in. Homework 5 out.
Start on Chapter 7, introducing two new connectives: "->" (which might be pronounced "implies") and "<->" (to be pronounced "if and only if", abbreviated "iff"). Discuss the relationship between formal and informal proofs.

February 14 (Monday)

Covered Sections 8.1 and 8.2: Elimination and Introduction rules for -> and <->, with example applications.

February 16 (Wednesday)

Graded Homework 4 back.
Discuss how to prove a chain of biconditionals. Cover Section 8.3 about soundness and completeness (omitting the proofs of the theorems). The notion of truth-functional completeness (Section 7.4). This completes Part I of the textbook.
Last day to drop a course without a W being recorded.
Instructor has no office hours Thursday (Feb 17).

February 18 (Friday)

No class (Abraham Lincoln's birthday, belated)

February 21 (Monday)

Homework 5 in. No class (George Washington's birthday, early)

February 22 (Tuesday)

Optional review session, 5-6pm, N122.
(Before that, instructor has usual office hours from 4-5pm.)

February 23 (Wednesday)

Test I.

February 25 (Friday)

Homework 6 out.
Distribute Lecture notes on Program Verification, and cover Sections 1-4: writing specifications; the notion of Hoare triples; the three-stage approach to software engineering; writing a program, computing the factorial function, in our simple language.

February 28 (Monday)

Motivated by our 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 covered Question V there).

March 2 (Wednesday)

Graded Homework 5 back.
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).
Look at Exercises 8.48 and 8.50, illustrating how TautCon may save us a lot of work.

March 4 (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.

March 7 (Monday)

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

March 9 (Wednesday)

Continue Chapter 9, getting more familiar with quantifiers. In addition to expressing the four Aristotelian forms, we address how to translate claims such as "at least three". Do Exercise 9.18.

March 11 (Friday)

Homework 7 in. Homework 8 out. Graded Homework 6 back.
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). This finishes Chapter 9; we also address how to translate numeric claims like "exactly one" or "at most two".

March 14 (Monday)

Present various quantifier equivalences, including DeMorgan (Sections 10.3 and 10.4).
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.
Instructor has no office hours Tuesday (Mar 15).

March 16 (Wednesday)

Graded Homework 7 back.
Elaborate on the notion of first-order consequence, denoting an argument which remains valid if the predicates in question (except for the identity "=") are consistently replaced by other (even nonsense) predicates. 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 18 (Friday)

Homework 8 in. Homework 9 out.
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. 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.
Sunday (March 20) is last day to drop a course.

March 21-25

Spring break.

March 28 (Monday)

Almost finish Chapter 11 (except that Section 11.7 is not covered), giving more examples of translations from English into FOL. We encounter a "donkey sentence" which has to be paraphrased before it becomes obvious how to translate it.

March 30 (Wednesday)

Graded Homework 8 back.
We embark on the proof rules for the quantifiers: 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) which is reflected in the Elimination rule for the Existential quantifier (Section 13.2).

April 1 (Friday)

Homework 9 in. Homework 10 out.
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). Mention that our proof system is sound and complete (Section 13.4). We give several examples of how to use the quantifier rules, in particular derive 2 of the 4 DeMorgan inferences.

April 4 (Monday)

Torben out of town; Chris will be in class to answer questions, also giving Graded Homework 9 back.

April 6 (Wednesday)

Test II.

April 8 (Friday)

No class (University Open House).

April 11 (Monday)

More examples of proofs with quantifiers (cf. Section 13.3), including the tricky interaction between existential instantiation and universal generalization (Section 12.4).
We derive the two remaining "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!

April 13 (Wednesday)

Use selected exercises to wrap up Chapters 12 & 13.
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!
Exercise 11.45 considers two seemingly non-equivalent English sentences and shows them to be equivalent; the proof employs the controversial (cf. last class) inference of Ex~P(x) from ~AxP(x).
Instructor has no office hours Thursday.

April 15 (Friday)

Homework 10 in. Homework 11 out.
After briefly covering Exercises 13.48 and 13.29, we start on the exciting topic of induction (notes handed out), 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!

April 18 (Monday)

Continue induction on natural numbers, doing Exercise 16.15 and giving an example (sum of angles in polygons) where the base case is '3' (rather than '0' or '1'). We argue that the induction principle is valid, based on the fact that any non-empty set of natural numbers has a least element.
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 20 (Wednesday)

Introduce the general principle of induction (Section 16.1), giving some examples of inductive definitions, for instance ambig-wffs (p.444). We 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 L(p) <= C(p) + 1.
Thursday, April 21: Torben's office hours will be from 3:00 to 3:45pm.

April 22 (Friday)

Homework 11 in. Homework 12 out.
We cover most of Section 3 in Lecture notes on Induction: first we inductively define an immutable version of lists; using that definition we write a recursive definition of the 'append' function '++', and prove by induction that 'nil' is a neutral element for '++' (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).

April 25 (Monday)

Continue Section 3 in Lecture notes on Induction, reasoning about lists, with main focus on proving by induction that the append function is associative.

April 27 (Wednesday)

Graded Test II back. Graded Homework 10 back.
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 29 (Friday)

TEVAL (if you were not there, you can go to the front office and fill out the two questionnaires).
Homework 12 in. Homework 13 out.
Cover some exercises from Homework 11, and wrap up induction: we 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).

May 2 (Monday)

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.

May 4 (Wednesday)

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

May 6 (Friday)

Homework 13 in. Graded Homework 12 back.
As an appetizer for future encounters with logic, we introduced CTL (computation tree logic).
Sketch the verification of programs manipulating arrays, the topic of Section 10 in Lecture notes on Program Verification.

May 9 (Monday)

Optional review session in N122, 5:15-6:00pm.
Graded Homework 13 back, otherwise open agenda.

May 11 (Wednesday)

Test III (Final exam), 11:50am-1:40pm.