Mathematical Logic and Theory of Computation
Purpose of Course showclose
Mathematics is about structure, about reasoning, and about modeling. This course braids these three threads together. Mathematical logic began as the study of the reasoning used in mathematics, but it turns out to be useful in describing the mathematical concept of structure and in modeling automated reasoning—that is, modeling computation.
The logical approach to structure gives an alternate perspective on such other mathematical subjects as combinatorics and abstract algebra. This, for the most part, is described by the area of model theory, which is the focus of Unit 1.
In Unit 2, we will look at modeling computation. The central fact of these models, from a logical standpoint, is that once we can handle a computation as a definable mathematical object, we can prove that certain computations are impossible. The most famous such proof is Gödel’s Incompleteness Theorem, showing that it is impossible to compute truth in a system sufficiently strong to describe natural number arithmetic.
Finally, in Unit 3, we turn to proof theory. Just as modeling computations results in new insights, modeling the process of mathematical proof results in a surprising connection: a proof is analogous to a computation.
These three often interact. Proofs and computations have natural parallels with the language we use to describe structures. Structures from model theory give natural settings for computation, as in Gödel’s Incompleteness Theorem. After completing this course, you will understand all three.
Course Information showclose
Course Designer: Prof. Wesley Calvert
Primary Resources: This course is composed of a range of different free, online materials. However, the course makes primary use of the following materials:
 Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory
 Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation
 Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness
 Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus
In order to pass this course, you will need to earn a 70% or higher on the Final Exam. Your score on the exam will be tabulated as soon as you complete it. If you do not pass the exam, you may take it again.
Time Commitment: It should take you about 132 hours of work to complete this course. Each unit includes a “time advisory” that lists the amount of time you might expect to spend on each subunit. Since much of the time is spent working through exercises, you may use much more or much less, depending on your personal work style.
Learning Outcomes showclose
 Prove categoricity of a firstorder theory in simple examples.
 Distinguish elementary and nonelementary properties.
 Describe mathematical models of computation and their respective limitations.
 Use the coding of computations by natural numbers to construct examples and proofs of impossibility.
 Explain the CurryHoward analogy between proofs and computations.
Course Requirements showclose
√ Have access to a computer.
√ Have continuous broadband Internet access.
√ Have the ability/permission to install plugins or software (e.g., Adobe Reader or Flash).
√ Have the ability to download and save files and documents to a computer.
√ Have the ability to open Microsoft files and documents (.doc, .ppt, .xls, etc.).
√ Be competent in the English language.
√ Have read the Saylor Student Handbook.
√ Be comfortable with mathematical proofs like those you might see in MA231: Abstract Algebra I or MA241: Real Analysis I.
Note: Familiarity with the key examples of MA231, while not strictly necessary, will be helpful in Unit 1.
Unit Outline show close

Unit 1: Model Theory
Model theory is a generalization of combinatorics and abstract algebra in which mathematical structures are described by axioms, and their structure is examined through homomorphisms and definable sets. Roughly, we start with some “language,” giving the functions, relations, and constants that are relevant. In this language, we can “define” certain properties, and can also check the truth of statements about whether these properties are satisfied.
Unit 1 Time Advisory show close
We will first define the general concepts of “structure” and “morphism,” which give rise to the language as the list of things that must be “preserved” by the morphism: in a graph, for instance, a morphism is a function that preserves adjacency. The power of this approach is clarified by three major results: the backandforth technique to construct isomorphisms, the LöwenheimSkolem Theorem to construct nonisomorphic structures sharing many properties with an original, and the Compactness Theorem, which allows us to determine some “extra” properties preserved by isomorphism but not definable in the language.
Central questions to keep in mind throughout this unit: What properties can be defined? What properties cannot? When is it possible to specify a particular mathematical object up to isomorphism, and what does this specification look like?
Unit 1 Learning Outcomes show close
 1.1 Structures and Morphisms

1.1.1 Structures and Isomorphism
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 1.1”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 1.1” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read section 1.1 in its entirety. As you read, remember the key rule to reading mathematical definitions: make up examples as you go. Can you make up firstorder structures in different languages? With the same domain? With the same language but important differences? Use these to build examples of the later definitions. Also, try to build “nearmiss” nonexamples: things that satisfy all but one part of a definition, or that otherwise nearly satisfy the definition, but not quite. Once you have done this, solve Exercise 1.1.14. When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 1.1.14” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 1.1”

1.1.2 Examples
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 1.2”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 1.2” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read section 1.2 in its entirety. If you are not familiar with fields and groups, you have two options at this point: First, you can ignore the terms, and think of a field as being like the rational numbers with addition and multiplication, and of a group as being like the integers under addition or the invertible 2x2 matrices under matrix multiplication (the latter is the better example, if you know it). The second option is to look in, briefly, on MA231: Abstract Algebra I, where you can find definitions. (These are not critical to this course but may make you feel a bit more comfortable.) In any case, think on these questions: What are the important properties of each kind of structure that we might want to be able to express or to require a homomorphism to preserve? Make a list of important properties for each kind of structure, and keep the list for the next subunit.
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 1.2”
 1.2 FirstOrder Formulas

1.2.1 The Syntax
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 2 Introduction and Section 2.1”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 2 Introduction and Section 2.1” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read from the beginning of Chapter 2 through the end of section 2.1. Be careful in reading proofs. Even with a proof that we know is correct, the right way to read a proof is by believing, for as long as possible, that it is wrong. Much of this section is the nearobvious bookkeeping system; that is, the clerical methods by which we can keep track of necessary details. Very little will be surprising. However, a careful – even skeptical – reading of the proofs gives a good idea of the level of formal detail that is often necessary in logic, even if it is unnecessary in algebra or analysis. After you have read the formula, prove the statement given as Exercise 2.1.10. When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 2.1.10” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 2 Introduction and Section 2.1”

1.2.2 The Semantics
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 2.2”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 2.2” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read section 2.2 in its entirety, solving Exercise 2.2.4 when you come to it. Then go back to the list of properties you made in subunit 1.1.2. Write a formula, where possible, to express each of these properties. Remember, in doing so, to use the definitions strictly: the variables may range only over elements of the domain (and not, for instance, over other formulas); only finitely many applications of the rules in the inductive definition can be made (so that, for instance, one can have only a finite conjunction). In some cases, it will be impossible. Two very important points arise here, which will form a good part of the rest of Unit 1: (a) Many important properties can be expressed by formulas in the natural signature, and (b) Some important properties cannot. When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 2.2.4” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 2.2”

1.2.3 Definable Sets
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 2.3”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 2.3” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read section 2.3 in its entirety, and solve Exercise 2.3.6. When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 2.3.6” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 2.3”
 1.3 Elementarity

1.3.1 Theories and Elementarity
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 3 Introduction and Section 3.1”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 3 Introduction and Section 3.1” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read from the beginning of Chapter 3 through the end of section 3.1, solving the two intext exercises as you come to them. Continue to read the proofs carefully (i.e., skeptically). The proof in section 3.1.11 is worthy of special mention: it is the classic example of the socalled “backandforth” argument, which is ubiquitous in model theory. Why is it called “backandforth”? Can you say what the general method is? When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 3.1.2 and 3.1.4” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 3 Introduction and Section 3.1”

1.3.2 Elementary Maps and Partial Isomorphisms
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 3.2”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 3.2” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read section 3.2 in its entirety, solving the intext exercises as you come to them. The importance of this section is hard to overstate; almost everything else in model theory depends on elementary maps, and on the ability to match parts of structures. Notice that, in general, an elementary bijection need not be an isomorphism. Under what conditions must it be? When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 3.2.1, 3.2.3, 3.2.4, and 3.2.5” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.  Assignment: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Exercise 1”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Exercise 1” (PDF)
Instructions: Click on the link to “Exercise 1” and solve the problem. When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 1” (PDF).
This assignment should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 3.2”

1.3.3 The Downward LöwenheimSkolem Theorem
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 3.3”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 3.3” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read section 3.3 in its entirety, solving the intext exercise as you come to it. Notice how counterintuitive the LöwenheimSkolem Theorem is: All properties of the real numbers that can be expressed with firstorder formulas can simultaneously be satisfied in a countable structure. In algebra, this is not so surprising, but this is extremely restrictive for expressing analysis. Any talk of limits is, in particular, problematic. Many interesting parts of calculus can be reconstructed on algebraic grounds, but the usual approach to calculus and analysis is completely missed by the firstorder theory. When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 3.3.4” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 3.3”
 1.4 Compactness

1.4.1 Consistency
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 4 Introduction and Section 4.1”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 4 Introduction and Section 4.1” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read from the beginning of Chapter 4 through the end of section 4.1. Don’t be put off by the “How not to read this chapter” paragraph. Zambella’s advice on skipping the Henkin proof is reasonable enough for the pure model theorist, but for the present course, where we intend eventually to understand computation, this proof is important: it is a proof by induction, but one in which we must order the stages carefully in order to finish in a finite time. Such constructions are at the heart of computability. As usual, try to think of examples and nearmisses for the definitions.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Chapter 4 Introduction and Section 4.1”

1.4.2 Compactness
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 4.2”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 4.2” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read all of section 4.2, solving the intext exercises as you come to them. Compactness is, in an important sense, the combinatorial heart of model theory, and the interaction between partial isomorphisms and compactness accounts for much of the discipline. If you have heard mention of compactness in mathematics before, perhaps in analysis or topology, the notion is exactly the same (and, in fact, the Compactness Theorem in model theory can be taken as the statement that a certain topological space is compact). The proofs are technical but important. When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 4.2.8 and 4.2.9” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 4.2”

1.4.3 Monster Models
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 4.3”
Link: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 4.3” (PDF or PS)
Instructions: Click on the link to the PDF or PS version of any version of the text. Read all of section 4.3, solving the intext exercise as you come to it. You could think of the complex numbers as being the example that motivates monster models. In the complex numbers, we have solutions to every polynomial equation we could ever think of, and so algebra can be done comfortably there – even if it is a bit bigger than the world we find “natural.” A monster model is exactly that: an awkwardly big world in which we can comfortably find solutions to formulas. When you are finished, you can check your answers against the Saylor Foundation’s “Solutions for Exercises in Unit 1 – Exercise 4.3.10” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Università di Torino: Domenico Zambella’s A Crèchet Course in Model Theory: “Section 4.3”

Unit 2: Modeling Computation
The advance of firstorder logic as a way to formalize mathematical truth inspired several efforts in the 1930s to give a technical definition for what an effective process – an algorithm, or a method for computing – ought to look like. Several of these definitions turned out to be equivalent. In the next two decades, these definitions became the dominant mathematical model and the dominant metaphor behind the invention of the digital computer.
Unit 2 Time Advisory show close
Our first attempt to model computation uses a somewhat weaker definition, one that takes seriously the limitations on memory and storage space that a computer has, and that lends itself to making comprehensive pictures of the model. This model of computation is called the finitestate automaton, which proves to be very useful but very restrictive.
We then move on to the equivalent definitions given by several people in the 1930s, which abstract the time and memory restrictions in real computers – and give the most convincing negative results. After all, if you couldn’t solve the problem even with unbounded time and memory, you couldn’t solve it in a more realistic model, either. We will explore in some detail how to encode these computations as natural numbers, and how to use these encodings to prove impossibility results, including Gödel Incompleteness (the theorem that a certain kind of firstorder structure cannot be described by a computable set of firstorder axioms), and to construct examples of counterintuitive behavior in computation.
Central questions to keep in mind throughout this unit: What is a computer? What features are included or abstracted in each model? Is there a psychological or philosophical difference between the mathematically equivalent models? What is the importance of the counterexamples (e.g., the Gödel sentence and the incomplete set)?
Unit 2 Learning Outcomes show close
 2.1 Finite Automata and Regular Languages

2.1.1 Deterministic Finite Automata
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Chapter 2, Sections 2.1 and 2.2”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Chapter 2, Sections 2.1 and 2.2” (PDF)
Instructions: Read from the beginning of Chapter 2 to the end of section 2.2. Observe the usual issues about definitions. Make more examples, and some nearmisses. Verify that each example satisfies the definition. Remember that it was said (by no less an authority than statistician George Box), “Essentially, all models are wrong, but some are useful.” What aspects of a computer does the definition of a finite automaton capture well? What aspects does it capture poorly?
This reading should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.  Assignment: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Exercise 2.1”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Exercise 2.1” (PDF)
Instructions: Go to the Exercises starting on page 78 and solve any three items from Exercise 2.1.
This assignment should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Chapter 2, Sections 2.1 and 2.2”

2.1.2 Regular Operations
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.3”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.3” (PDF)
Instructions: Read all of section 2.3. You could think of the relationship between regular operations and finite automata as an image of the relationship between syntax and semantics in model theory. The hope, in the end, is that the two will coincide – that is, that the set of regular languages (those accepted by finite automata) will be generated somehow by regular operations. This works out, in the end, but it takes some time to get to this proof. Again, make sure you’re reading actively through all these definitions and bookkeeping proofs.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.3”

2.1.3 NonDeterministic Finite Automata
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.4”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.4” (PDF)
Instructions: Read all of section 2.4. Nondeterministic automata may – even should – feel a little contrived. They originated as a guess about what kind of “magic” we could add to an automaton in order to allow it to do more. The “magic” involved here is that there are two (or more) possibilities for the “right” next step, and the automaton is given the ability to “magically” know which one is right. In the end, it doesn’t matter for automata, but with other models of computation, this turns out to be a big issue – perhaps the biggest open problem in theoretical computing today.
This reading should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.  Assignment: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Exercise 2.2”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Exercise 2.2” (PDF)
Instructions: Go to page 79 and solve Exercise 2.2.
This assignment should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.4”

2.1.4 Equivalence of DFAs and NFAs
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.5”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.5” (PDF)
Instructions: Read all of section 2.5. If you have properly understood the definitions of NFAs and DFAs, you should intuitively believe that the main theorem of this section is impossible. The result should be surprising. Suppose you had a magical ability to always guess right. It should help you, shouldn’t it? And yet this result says that (at least in this context) it really doesn’t. You should perhaps read the proof of equivalence with a specific NFA in mind, perhaps one that you think would be hard for a DFA to emulate. In any case, read skeptically.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.5”

2.1.5 Closure Under the Regular Operations
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.6”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.6” (PDF)
Instructions: Read section 2.6. The goal here is to develop an “algebra” to represent what automata are doing. The roots of this sort of analysis go back to Noam Chomsky’s attempt to explain how such a complex thing as language could be biologically hardwired, and could be independent of the many wildly different natural languages in use. Try, in each proof, to draw the state diagram of the “proof” (i.e., the DFA witnessing closure under that operation) before either looking at the figure or reading the proof. Then look at the figure provided, if there is one, and then read the proof.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.6”

2.1.6 Regular Expressions and Regular Languages
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Sections 2.7 and 2.8”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Sections 2.7 and 2.8” (PDF)
Instructions: Read sections 2.7 and 2.8. This is a continuation of the work in the previous reading to develop an algebra to describe what automata do. The regular expressions are quintessential forms of “grammatically correct sentences” in the language. In English, for instance, we have a common form SVO, where S is a subject, V is a transitive verb, and O is an object. Whether you would want to say it or not, any such construction (with a few extra details) is a legitimate English sentence. Of course, the “languages” we care about in computation are a bit more abstract, but it’s helpful to think of them as languages anyway.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.  Assignment: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Exercise 2.8”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Exercise 2.8” (PDF)
Instructions: Go to page 81 and solve Exercise 2.8.
This assignment should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Sections 2.7 and 2.8”

2.1.7 The Pumping Lemma and NonRegular Languages
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.9”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.9” (PDF)
Instructions: Read all of section 2.9. While the pumping lemma is a theorem usually stated in the form, “For all regular languages A,” the real importance is in the contrapositive: “If A does not have a certain property, then A is not regular.” It’s really a way of proving that DFAs cannot do certain things; it’s a result about the limits of computers, insofar as finite automata are good models for them.
This reading should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.  Assignment: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Exercise 2.22”
Link: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Exercise 2.22” (PDF)
Instructions: Go to page 84 and solve Exercise 2.22.
This assignment should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carleton University: Anil Maheshwari and Michiel Smid’s Introduction to the Theory of Computation: “Section 2.9”
 2.2 Turing Machines and Related Models

2.2.1 Turing Machines
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Chapter 2 Introduction and Sections 2.1 and 2.2”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Chapter 2 Introduction and Sections 2.1 and 2.2” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read from the beginning of Chapter 2 through the end of section 2.2. This is a much stronger model than finite automata (i.e., one of these can do things that a DFA can’t). Again, think of the big modeling questions: Where does the Turing machine definition go right as a model of computation (e.g., where is it better than a DFA)? Where does it go wrong?
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.  Assignment: University of Manchester: Andrea Schalk’s Turing Machines: “Section 3”
Link: University of Manchester: Andrea Schalk’s Turing Machines: “Section 3” (PDF or PS)
Instructions: In the “Course notes” section, click on the link for the format you want of “Section 3: Turing machines.” Go to page 54 and solve both parts of Exercise 23.
This assignment should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Chapter 2 Introduction and Sections 2.1 and 2.2”

2.2.2 Primitive Recursion
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Sections 2.3 and 2.4”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Sections 2.3 and 2.4” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read sections 2.3 and 2.4. The great miracle of the generalpurpose computer in the 1930s was the diversity of approaches that produced the same thing. Primitive recursion was the approach of Gödel, whose motivation was more philosophical than technical. As usual, make up examples as you read. Check the examples given. Make nearmiss nonexamples.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Sections 2.3 and 2.4”

2.2.3 Recursive Functions
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.5”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.5” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 2.5. While the definitions are of great importance and should be given the usual treatment, the proof that begins the section will become the real star of the show. It is known as a “diagonal argument” (can you see why?) and is the central technique in all computability theory, although it appears in many guises.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.5”

2.2.4 Recursive is Equivalent to Turing Computable
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.6”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.6” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 2.6. Read the proof critically. It is important that, in the long run, you believe that partial recursive functions and partial Turing computable functions are the same. Pick some examples where the theorem seems hard to believe. Follow through the proof with these examples, to see how it catches them.
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.6”

2.2.5 Church’s Thesis
 Reading: Stanford Encyclopedia of Philosophy: B. Jack Copeland’s “The ChurchTuring Thesis”
Link: Stanford Encyclopedia of Philosophy: B. Jack Copeland’s “The ChurchTuring Thesis” (HTML)
Instructions: Read the article. The real importance for your learning of the proof in the previous section is that it helps you believe the extremely important ChurchTuring Thesis (sometimes called Church’s Thesis). The point here is that if we believe the ChurchTuring Thesis, then we believe that the concept of “computation” is mathematically welldefined – and that, for instance, we can prove impossibility results for computation without fear that some new idea of what computation means will come and supersede our result.
People often attempt things that are known to be impossible, thinking that there is an analogy of mathematical impossibilities (things nobody will ever be able to do) with technical impossibilities (things we can’t imagine how anybody would ever do). People who try to trisect angles, for instance, might say that “people used to think airplanes were impossible, too.” The ChurchTuring Thesis shows that any impossibility results that we prove about computation are like the impossibility of angle trisection (a genuine proof of permanent impossibility), not like the “impossibility” of flight (a matter of technological distance).
This reading should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Stanford Encyclopedia of Philosophy: B. Jack Copeland’s “The ChurchTuring Thesis”

2.2.6 Theorems on Computability
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.7”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.7” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 2.7. These theorems all have important uses, but the real importance at the moment is that you get used to the kinds of things you can do with a formally defined model of computation. Work through each proof. See if you can anticipate the next step in each proof. Then reflect on the importance of Kleene’s Normal Form Theorem: What does it mean for computer hardware?
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.7”

2.2.7 The Lambda Calculus
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.8”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.8” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 2.8. This added model of computability (equivalent to Turing computability and partial recursion) is of particular importance for computing: it points the way (in Unit 3 of this course) to a link between formal proofs and computation. If you want to be impressed by Unit 3 – or even to understand its importance – you would do well to make sure you’re convinced of the proofs in this section. Also, lambda calculus is the model of computation that has been turned most explicitly into a programming language. Most of the socalled “functional” languages (e.g., FORTRAN) are derived from lambda calculus.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 2.8”
 2.3 Computability Theory

2.3.1 Computably Enumerable Sets
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Chapter 3 Introduction and Sections 3.1 and 3.2”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Chapter 3 Introduction and Sections 3.1 and 3.2” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read from the beginning of Chapter 3 through the end of section 3.2. The noncomputability of K_{0} is our second big encounter with the diagonal argument. It is the archetypal proof of which all other noncomputability proofs are either imitations or applications. It also, in itself, places a kind of limit on automated software verification: If you can’t check whether a program halts, then you can’t check much.
This reading should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.  Assignment: University of Ottawa: Pieter Hofstra’s Recursion Theory: “Exercise 3.23”
Link: University of Ottawa: Pieter Hofstra’s Recursion Theory: “Exercise 3.23” (PS)
Instructions: Under the heading of “Lecture Notes,” click on the link to download the file. Solve Exercise 3.23 on page 77.
This assignment should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Chapter 3 Introduction and Sections 3.1 and 3.2”

2.3.2 Reducibility and Rice’s Theorem
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 3.3”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 3.3” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 3.3. This is the way one applies the noncomputability of K_{0} to prove noncomputability of other things. The results of this section justify the definition of reducibility.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 3.3”

2.3.3 The FixedPoint Theorem
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Sections 3.4 and 3.5”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Sections 3.4 and 3.5” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read sections 3.4 and 3.5. To a mathematician, a fixedpoint theorem is a very natural thing – if you’re dealing with continuous functions in some sort of geometric context. Here, the point is very technical – and it would not be worth studying if it were not useful for so many other results, some of which we’ll see in later sections.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.  Assignment: University of Ottawa: Pieter Hofstra’s Recursion Theory: “Exercise 3.11”
Link: University of Ottawa: Pieter Hofstra’s Recursion Theory: “Exercise 3.11” (PS)
Instructions: Under the heading of “Lecture Notes,” click on the link to download the file. Solve Exercise 3.11 on page 76.
This assignment should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Sections 3.4 and 3.5”
 2.4 Incompleteness

2.4.1 Historical Background
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.1”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.1” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 4.1. Many people consider the Incompleteness Theorems to be the beginning of modern logic, and certainly the beginning of its involvement with computation. The formulation of the theorems, though, is more than a little recondite outside its historical context. If we aren’t careful, the Incompleteness Theorems can sound like either shallow philosophy or uninteresting technical details in a part of math that not many people care about any more. It is neither, and the point of this section is to help you navigate this.
This reading should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.1”

2.4.2 Background in Logic
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.2”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.2” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 4.2. Many points will be familiar from our study of model theory, but it is good to read them to fill in details to which we didn’t attend then.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.2”

2.4.3 Representability in Q
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.3”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.3” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 4.3. The point here is to make a modeltheoretic definition of computability, equivalent to the others we have just seen. The ultimate goal is to use this as a way to carry out a diagonal argument. Many of the points here are technical and difficult, but they are fundamental for understanding the theorems, which are, collectively, one of the great intellectual accomplishments of human history.
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.3”

2.4.4 The First Incompleteness Theorem
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.4”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.4” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 4.4. Much has been made of this theorem in the popular literature. What do you make of it? What is its practical meaning?
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.4”

2.4.5 The Second Incompleteness Theorem
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.7”
Link: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.7” (PDF)
Instructions: Near the bottom of the page, find the bullet point, “Computability and Incompleteness,” and click on the PDF link for “Lecture notes.” Read section 4.7. What does the Second Incompleteness Theorem say that we already knew from the First? What does it tell us that is new?
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Carnegie Mellon University: Jeremy Avigad’s Computability and Incompleteness: “Section 4.7”
 2.5 Turing Reduction and Post’s Problem

2.5.1 Post’s Problem and Reducibilities
 Reading: National University of Singapore: Frank Stephan’s Recursion Theory: “Chapter 4”
Link: National University of Singapore: Frank Stephan’s Recursion Theory: “Chapter 4” (PDF or PS).
Instructions: In the section labeled “Lecture Notes,” click on the link to the file format of your choice. Read Chapter 4, and solve Exercises 4.4, 4.7, and 4.13. One can still start a very interesting (and sometimes heated) conversation among experts by asking for a “natural” solution to Post’s problem. Many people believe that the constructions of solutions that we will see (and many others more recent) have an ad hoc feel to them – as if Post might say (though he didn’t), “Yes, but that’s not really what I was looking for.”
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: National University of Singapore: Frank Stephan’s Recursion Theory: “Chapter 4”

2.5.2 A Solution to Post’s Problem for Enumerable Sets
 Reading: National University of Singapore: Frank Stephan’s Recursion Theory: “Chapter 7”
Link: National University of Singapore: Frank Stephan’s Recursion Theory: “Chapter 7” (PDF or PS)
Instructions: In the section labeled “Lecture Notes,” click on the link to the file format of your choice. Read Chapter 7, and solve Exercises 7.2, 7.3, and 7.5. Think on the issue of naturality, too. Does the set constructed in this section seem intuitively reasonable to you? Or is it one of those theorems that you know must be true because you’ve seen the proof, but that in your heart you still don’t feel quite right about? There are experts – experts at the highest level – on either side of the question.
This reading should take approximately 4 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: National University of Singapore: Frank Stephan’s Recursion Theory: “Chapter 7”

Unit 3: Proof Theory
Proofs, in the context of mathematical logic, have a combinatorial structure of their own. One can think of proofs as algebraic objects generated by a set of derivation rules. These derivation rules turn out to bear a striking resemblance – strong enough to often be called an “isomorphism” – to the rules for defining a function in the simplytyped lambda calculus. Because this analogy is so useful in the design of programming languages and in verification of software, we will take a deeper look at the lambda calculus with a view toward this “isomorphism,” which describes the sense in which logic is a model for these parts of software engineering.
Unit 3 Time Advisory show close
An important point is that the logic corresponding to computation by this isomorphism is something less than classical logic. It is a fragment of logic called “intuitionistic logic,” formerly used by people with philosophical misgivings about foundational questions in mathematics. It does not include proof by contradiction, for instance.
Questions to keep in mind: Is it intuitively believable that all computation could be expressed as proof rules? What are the key differences between classical and intuitionistic logic? What might a CurryHoward isomorphism for classical logic look like?
Unit 3 Learning Outcomes show close
 3.1 The Untyped Lambda Calculus

3.1.1 Syntax
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 2.1”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 2.1” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 2.1, and solve Exercise 3. We saw the lambda calculus before as a way of encoding computation. In this unit, it will be developed, with some new features, into a programming language that mirrors what we do when we prove theorems in a formal system. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.1.1 Solutions” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 2.1”

3.1.2 ? and ?Reduction
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 2.2 to 2.5”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 2.2 to 2.5” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read sections 2.2 to 2.5. The bookkeeping is the central feature of these sections – and the introduction of the notation for proof rules in the tables. This notation takes some getting used to, but will eventually be important. The idea is that if the conditions above the line are known, one can conclude the condition below the line.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 2.2 to 2.5”

3.1.3 Booleans
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 3 Introduction and Section 3.1”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 3 Introduction and Section 3.1” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read from the beginning of Chapter 3 through the end of section 3.1, solving Exercise 5. To be able to do logic, we should at least be able to handle notions of true and false. This section shows that the lambda calculus is strong enough to handle such things. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.1.3 Solutions” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 3 Introduction and Section 3.1”

3.1.4 Natural Numbers
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.2”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.2” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 3.2, solving Exercises 6 and 7. Another standard benchmark of being able to say interesting things is that one should be able to talk about the truth of obviously true statements of arithmetic. Here we see that the lambda calculus admits that, too. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.1.4 Solutions” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.2”

3.1.5 Fixed Points and Recursive Functions
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.3”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.3” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 3.3, solving Exercises 8, 9, 10, and 11. Fixed points (or “fixpoints”) are a subtle feature in programming language semantics. You may need to reread this section, but in any case, if you skip any exercises, don’t skip these. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.1.5 Solutions” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.3”

3.1.6 Other Data Types
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.4”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.4” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 3.4, and solve one of the three problems in Exercise 12. We have seen, in the earlier proof of the Gödel Incompleteness Theorems, that if you can encode strings of natural numbers, you can express anything. This section shows that the reasoning system of the lambda calculus is as broad as could reasonably be expected. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.1.6 Solutions” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 3.4”
 3.2 The ChurchRosser Theorem

3.2.1 Statement and Consequences of the ChurchRosser Theorem
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 4 Introduction and Sections 4.1 and 4.2”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 4 Introduction and Sections 4.1 and 4.2” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read from the beginning of Chapter 4 through the end of section 4.2. The ChurchRosser Theorem is useful for proving consistency, and for other things, but the right way to think of this section for the purposes of this course is that it gives you a real (and hard) proof on which to try out your understanding of the definitions.
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 4 Introduction and Sections 4.1 and 4.2”

3.2.2 Proof of the ChurchRosser Theorem
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 4.3 and 4.4”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 4.3 and 4.4” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read sections 4.3 and 4.4. In section 4.5, solve Exercises 13 and 18. Remember, the goal is that you check your understanding of the definitions. Look up anything from the previous work that you don’t understand. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.2.2 Solutions” (PDF).
This reading should take approximately 4 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 4.3 and 4.4”
 3.3 Combinatory Algebras

3.3.1 Applicative Structures
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 5 Introduction and Section 5.1”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 5 Introduction and Section 5.1” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read from the beginning of Chapter 5 through the end of section 5.1. We have not yet seen anything that is transparently a proof system. Have patience, though. What we are doing is a proof system in disguise. For the moment, the overt goal is to produce a structure (more or less in the sense of model theory) satisfying the formulas written in the previous two subunits.
This reading should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 5 Introduction and Section 5.1”

3.3.2 Combinatory Completeness
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 5.2”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 5.2” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 5.2. The point of combinatory completeness is that an applicative structure having this property really could be a model of the lambda calculus.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 5.2”

3.3.3 Combinatory Algebras
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 5.3”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 5.3” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 5.3, solving Exercise 20. Just as regular expressions gave an algebraic understanding of automata, combinatory algebras give an algebraic understanding of the lambda calculus. Of course, we expect the algebra here to be much more complicated. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.3.3 Solutions” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 5.3”

3.3.4 Lambda Algebras
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 5.4 and 5.5”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 5.4 and 5.5” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read sections 5.4 and 5.5, solving the intext exercises. This section completes the algebraic approach to lambda calculus, and corresponds to the proof that regular expressions correspond to regular languages. After you have attempted the exercises, you may check your answers against the Saylor Foundation’s “Subunit 3.3.4 Solutions” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 5.4 and 5.5”
 3.4 SimplyTyped Lambda Calculus, Propositional Logic, and the CurryHoward Isomorphism

3.4.1 Simple Types and SimplyTyped Terms
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 6 Introduction and Section 6.1”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 6 Introduction and Section 6.1” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read from the beginning of Chapter 6 through the end of section 6.1, solving Exercises 26, 27, and 28. Types exist in programming to catch mistakes. If a program expects a number and gets a function or an ordered pair instead, we’d like for it to recognize that something is wrong. That feature is what is being reflected in the typing system for the lambda calculus. After you have attempted the exercises, you may check your answers against the Saylor Foundation’s “Subunit 3.4.1 Solutions” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Chapter 6 Introduction and Section 6.1”

3.4.2 Connections to Propositional Logic
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.2”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.2” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 6.2. Finally, all of the lambda calculus reductions become proofs! Finally, the functions become formulas! This section either says or hints at the point of everything you’ve learned in Unit 3 thus far.
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.2”

3.4.3 Propositional Intuitionistic Logic
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.3 and 6.4”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.3 and 6.4” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read sections 6.3 and 6.4, and solve two instances of Exercise 29 (i.e., deriving two of the formulas should give you an idea of the thing). Any resemblance you see between these proof rules and the rules of the lambda calculus is exactly the point. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.4.3 Solutions” (PDF).
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.3 and 6.4”

3.4.4 The CurryHoward Isomorphism
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.5”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.5” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 6.5. In Church’s Thesis, we conclude that we have the right definition of our concept because so many definitions coincide. Here, we conclude that we have an important concept because two different concepts – proofs and computations – coincide.
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.5”

3.4.5 Reductions in the SimplyTyped Lambda Calculus
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.6 through 6.8”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.6 through 6.8” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read sections 6.6, 6.7, and 6.8, and solve Exercise 31. The way we can tell that an analogy like the CurryHoward isomorphism is a good analogy is that the concepts that have meaning, for instance, in lambda calculus, have a meaning, too, in proofs. These sections spell out some of these. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.4.5 Solutions” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.6 through 6.8”

3.4.6 Application of CurryHoward
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.9 and 6.10”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.9 and 6.10” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read sections 6.9 and 6.10. Here we take the analogy in the opposite direction. What do artifacts from the proof world mean in computations?
This reading should take approximately 3 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Sections 6.9 and 6.10”

3.4.7 Classical vs. Intuitionistic Logic
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.11”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.11” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 6.11, solving Exercise 32. Assuming that we have gotten past the philosophical debates of the early twentieth century, the CurryHoward isomorphism is really intuitionistic logic’s reason to exist. The people who, in their serious practical thinking, deny classical logic are rare. After you have attempted the exercise, you may check your answers against the Saylor Foundation’s “Subunit 3.4.7 Solutions” (PDF).
This reading should take approximately 2 hours.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.11”

3.4.8 Classical Logic and the CurryHoward Isomorphism
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.12”
Link: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.12” (PDF or PS)
Instructions: Near the bottom of the page, find the section entitled, “Lecture Notes on the Lambda Calculus,” and click on the link to any convenient format of the document. Read section 6.12. If everybody thinks in classical logic, and the CurryHoward isomorphism says that simplytyped lambda calculus corresponds to programming in intuitionistic logic, this section gives a start on thinking about what programming in classical logic might look like.
This reading should take approximately 1 hour.
Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.
 Reading: Dalhousie University: Peter Selinger’s Lecture Notes on the Lambda Calculus: “Section 6.12”