316 courses ePortfolio Forums Blog FAQ

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

Welcome to MA201. Below, please find general information on this course and its requirements.

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:
Requirements for Completion: In order to complete this course, you will need to work through each unit and all of its assigned materials.

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

Upon successful completion of this course, the student will be able to:
  • Prove categoricity of a first-order theory in simple examples.
  • Distinguish elementary and non-elementary 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 Curry-Howard analogy between proofs and computations.

Course Requirements  showclose

In order to take this course you must:

√    Have access to a computer.

√    Have continuous broadband Internet access.

√    Have the ability/permission to install plug-ins 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


Expand All Resources Collapse All Resources
  • 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.

    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 back-and-forth technique to construct isomorphisms, the Löwenheim-Skolem Theorem to construct non-isomorphic 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 Time Advisory   show close
    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 first-order 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 “near-miss” non-examples: 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.

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

  • 1.2 First-Order 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 near-obvious 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.

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

  • 1.2.3 Definable Sets  
  • 1.3 Elementarity  
  • 1.3.1 Theories and Elementarity  
  • 1.3.2 Elementary Maps and Partial Isomorphisms  
  • 1.3.3 The Downward Löwenheim-Skolem 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 in-text exercise as you come to it.  Notice how counterintuitive the Löwenheim-Skolem Theorem is: All properties of the real numbers that can be expressed with first-order 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 first-order 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.

  • 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 near-misses 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.

  • 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 in-text 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.

  • 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 in-text 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.

  • Unit 2: Modeling Computation  

    The advance of first-order 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.
     
    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
    finite-state 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 first-order structure cannot be described by a computable set of first-order 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 Time Advisory   show close
    Unit 2 Learning Outcomes   show close
  • 2.1 Finite Automata and Regular Languages  
  • 2.1.1 Deterministic Finite Automata  
  • 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.

  • 2.1.3 Non-Deterministic 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.  Non-deterministic 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.

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

  • 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 hard-wired, 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.

  • 2.1.6 Regular Expressions and Regular Languages  
  • 2.1.7 The Pumping Lemma and Non-Regular Languages  
  • 2.2 Turing Machines and Related Models  
  • 2.2.1 Turing Machines  
  • 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 general-purpose 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 near-miss non-examples.

      This reading should take approximately 2 hours.

      Terms of Use: Please respect the copyright and terms of use displayed on the webpage above.

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

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

  • 2.2.5 Church’s Thesis  
    • Reading: Stanford Encyclopedia of Philosophy: B. Jack Copeland’s “The Church-Turing Thesis”

      Link: Stanford Encyclopedia of Philosophy: B. Jack Copeland’s “The Church-Turing 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 Church-Turing Thesis (sometimes called Church’s Thesis).  The point here is that if we believe the Church-Turing Thesis, then we believe that the concept of “computation” is mathematically well-defined – 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 Church-Turing 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.

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

  • 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 so-called “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.

  • 2.3 Computability Theory  
  • 2.3.1 Computably Enumerable Sets  
  • 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 non-computability of K0 to prove non-computability 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.

  • 2.3.3 The Fixed-Point 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 fixed-point 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.

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

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

  • 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 model-theoretic 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.

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

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

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

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

  • 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 simply-typed 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.

    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 Curry-Howard isomorphism for classical logic look like?

    Unit 3 Time Advisory   show close
    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.

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

  • 3.1.3 Booleans  
  • 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.

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

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

  • 3.2 The Church-Rosser Theorem  
  • 3.2.1 Statement and Consequences of the Church-Rosser Theorem  
  • 3.2.2 Proof of the Church-Rosser 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.

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

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

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

  • 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 in-text 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.

  • 3.4 Simply-Typed Lambda Calculus, Propositional Logic, and the Curry-Howard Isomorphism  
  • 3.4.1 Simple Types and Simply-Typed 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.

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

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

  • 3.4.4 The Curry-Howard 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.

  • 3.4.5 Reductions in the Simply-Typed 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 Curry-Howard 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.

  • 3.4.6 Application of Curry-Howard  
  • 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 Curry-Howard 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.

  • 3.4.8 Classical Logic and the Curry-Howard 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 Curry-Howard isomorphism says that simply-typed 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.

  • Final Exam  
    • Final Exam: The Saylor Foundation’s “MA201 Final Exam”

      Link: The Saylor Foundation’s “MA201 Final Exam”
       
      Instructions: You must be logged into your Saylor Foundation School account in order to access this exam.  If you do not yet have an account, you will be able to create one, free of charge, after clicking the link. 

      The Saylor Foundation does not yet have materials for this portion of the course. If you are interested in contributing your content to fill this gap or aware of a resource that could be used here, please submit it here.

      Submit Materials


« Previous Unit Next Unit » Back to Top