**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**

This unit should take approximately 47 hours to complete.

☐ Subunit 3.1: 13 hours

☐ Sub-subunit 3.1.1: 2 hours

☐ Sub-subunit 3.1.2: 2 hours

☐ Sub-subunit 3.1.3: 2 hours

☐ Sub-subunit 3.1.4: 2 hours

☐ Sub-subunit 3.1.5: 3 hours

☐ Sub-subunit 3.1.6: 2 hours

☐ Subunit 3.2: 7 hours

☐ Sub-subunit 3.2.1: 3 hours

☐ Sub-subunit 3.2.2: 4 hours

☐ Subunit 3.3: 8 hours

☐ Sub-subunit 3.3.1: 1 hours

☐ Sub-subunit 3.3.2: 2 hours

☐ Sub-subunit 3.3.3: 2 hours

☐ Sub-subunit 3.3.4: 3 hours

☐ Subunit 3.4: 19 hours

☐ Sub-subunit 3.4.1: 3 hours

☐ Sub-subunit 3.4.2: 3 hours

☐ Sub-subunit 3.4.3: 3 hours

☐ Sub-subunit 3.4.4: 2 hours

☐ Sub-subunit 3.4.5: 2 hours

☐ Sub-subunit 3.4.6: 3 hours

☐ Sub-subunit 3.4.7: 2 hours

☐ Sub-subunit 3.4.8: 1 hour

**Unit3 Learning Outcomes**

Upon successful completion of this unit, the student will be able to:
- Distinguish typed and untyped lambda calculi.
- Execute α- and β-reduction on lambda terms.
- Model natural numbers and functions on them in lambda calculus.
- Use the Curry-Howard isomorphism to describe extensions to
intuitionistic logic.
- Distinguish classical and intuitionistic logic.

**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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.1.1.pdf)
(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**
- **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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.1.3.pdf)
(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.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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.1.4.pdf)
(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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.1.5.pdf)
(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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.1.6.pdf)
(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**
- **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
Church-Rosser 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.
```

**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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.2.2.pdf)
(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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.3.3.pdf)
(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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.3.4.pdf)
(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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.4.1.pdf)
(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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.4.3.pdf)
(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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.4.5.pdf)
(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**
- **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.
```

**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”](http://www.saylor.org/site/wp-content/uploads/2013/02/MA201-Solutions-3.4.7.pdf)
(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.
```