Reading for Tuesday

[Joe Razavi]

Hi everyone,

Reading for Tuesday is chapter 5 of the reading material (
http://www.cs.cmu.edu/~rwh/courses/logic/www/handouts/curry-howard.pdf
).

The basic idea here is to explore the correspondence by looking at the
relationship between two new (but very familiar-looking!) systems;
combinatory logic (which, despite its name, looks like a calculating
system to me) and Hilbert-style proof systems. Then they attempt to
discover philosophically (and computationally) interesting logics
(with properties of "relevance" and "linearity") by applying the Curry-
Howard correspondence to restricted classes of lambda terms.

Questions I think are interesting are:

1) What is the relationship between combinatory logic and the lambda
calculus?
2) What is the relationship between Hilbert-style and natural
deduction proof systems?
3) What is the relationship between the previous two relationships!?
4) What is the intuition behind Definition 5.4.1?

As always, don't worry if you think about other things, or nothing,
while reading, or if you just read little bits, or none at all; come
anyway and someone will surely have found out what's really going on
in this (quite heavy) chaopter.

See you soon,

Joe